diff --git a/lowlevel/src/ast.rs b/lowlevel/src/ast.rs index 86b353c..a87aa2c 100644 --- a/lowlevel/src/ast.rs +++ b/lowlevel/src/ast.rs @@ -1406,6 +1406,14 @@ pub enum Command { SetOption(Option), /// `(simplify )` Simplify(Term), + /// `(eval )` + Eval(Term), + /// `(maximize )` + Maximize(Term), + /// `(minimize )` + Minimize(Term), + /// `(assert-soft *)` + AssertSoft(Term, Vec), } impl std::fmt::Display for Command { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -1459,6 +1467,12 @@ impl std::fmt::Display for Command { Self::SetLogic(m0) => write!(f, "(set-logic {})", m0), Self::SetOption(m0) => write!(f, "(set-option {})", m0), Self::Simplify(m0) => write!(f, "(simplify {})", m0), + Self::Eval(m0) => write!(f, "(eval {})", m0), + Self::Maximize(m0) => write!(f, "(maximize {})", m0), + Self::Minimize(m0) => write!(f, "(minimize {})", m0), + Self::AssertSoft(m0, m1) => { + write!(f, "(assert-soft {} {})", m0, m1.iter().format(" ")) + } } } } @@ -1485,6 +1499,14 @@ impl SmtlibParse for Command { || (p.nth(offset) == Token::LParen && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming") && p.nth(offset + 2) == Token::LParen) + || (p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "assert-soft")) + || (p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "minimize")) + || (p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "maximize")) + || (p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "eval")) || (p.nth(offset) == Token::LParen && p.nth_matches(offset + 1, Token::Symbol, "simplify")) || (p.nth(offset) == Token::LParen @@ -1633,6 +1655,44 @@ impl SmtlibParse for Command { #[allow(clippy::useless_conversion)] return Ok(Self::CheckSatAssuming(m0.into())); } + if p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "assert-soft") + { + p.expect(Token::LParen)?; + p.expect_matches(Token::Symbol, "assert-soft")?; + let m0 = ::parse(p)?; + let m1 = p.any::()?; + p.expect(Token::RParen)?; + #[allow(clippy::useless_conversion)] + return Ok(Self::AssertSoft(m0.into(), m1.into())); + } + if p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "minimize") + { + p.expect(Token::LParen)?; + p.expect_matches(Token::Symbol, "minimize")?; + let m0 = ::parse(p)?; + p.expect(Token::RParen)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Minimize(m0.into())); + } + if p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "maximize") + { + p.expect(Token::LParen)?; + p.expect_matches(Token::Symbol, "maximize")?; + let m0 = ::parse(p)?; + p.expect(Token::RParen)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Maximize(m0.into())); + } + if p.nth(offset) == Token::LParen + && p.nth_matches(offset + 1, Token::Symbol, "eval") + { + p.expect(Token::LParen)?; + p.expect_matches(Token::Symbol, "eval")?; + let m0 = ::parse(p)?; + p.expect(Token::RParen)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Eval(m0.into())); + } if p.nth(offset) == Token::LParen && p.nth_matches(offset + 1, Token::Symbol, "simplify") { @@ -1902,6 +1962,10 @@ impl Command { Self::SetLogic(_) => false, Self::SetOption(_) => false, Self::Simplify(_) => true, + Self::Eval(_) => true, + Self::Maximize(_) => false, + Self::Minimize(_) => false, + Self::AssertSoft(_, _) => false, } } pub fn parse_response( @@ -2044,7 +2108,68 @@ impl Command { ), ) } + Self::Eval(_) => { + Ok( + Some( + SpecificSuccessResponse::EvalResponse( + EvalResponse::parse(response)?, + ), + ), + ) + } + Self::Maximize(_) => Ok(None), + Self::Minimize(_) => Ok(None), + Self::AssertSoft(_, _) => Ok(None), + } + } +} +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub enum OptimizationAttribute { + /// `:weight ` + Weight(Numeral), + /// `:id ` + Id(Symbol), + /// `` + Attribute(Attribute), +} +impl std::fmt::Display for OptimizationAttribute { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + match self { + Self::Weight(m0) => write!(f, ":weight {}", m0), + Self::Id(m0) => write!(f, ":id {}", m0), + Self::Attribute(m0) => write!(f, "{}", m0), + } + } +} +impl OptimizationAttribute { + pub fn parse(src: &str) -> Result { + SmtlibParse::parse(&mut Parser::new(src)) + } +} +impl SmtlibParse for OptimizationAttribute { + fn is_start_of(offset: usize, p: &mut Parser) -> bool { + (p.nth_matches(offset, Token::Keyword, ":id")) + || (p.nth_matches(offset, Token::Keyword, ":weight")) + || (Attribute::is_start_of(offset, p)) + } + fn parse(p: &mut Parser) -> Result { + let offset = 0; + if p.nth_matches(offset, Token::Keyword, ":id") { + p.expect_matches(Token::Keyword, ":id")?; + let m0 = ::parse(p)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Id(m0.into())); + } + if p.nth_matches(offset, Token::Keyword, ":weight") { + p.expect_matches(Token::Keyword, ":weight")?; + let m0 = ::parse(p)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Weight(m0.into())); } + if Attribute::is_start_of(offset, p) { + let m0 = ::parse(p)?; + #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into())); + } + Err(p.stuck("optimization_attribute")) } } /// `*` @@ -2101,6 +2226,8 @@ pub enum Option { ReproducibleResourceLimit(Numeral), /// `:verbosity ` Verbosity(Numeral), + /// `:opt.priority ` + OptPriority(OptimizationPriority), /// `` Attribute(Attribute), } @@ -2127,6 +2254,7 @@ impl std::fmt::Display for Option { write!(f, ":reproducible-resource-limit {}", m0) } Self::Verbosity(m0) => write!(f, ":verbosity {}", m0), + Self::OptPriority(m0) => write!(f, ":opt.priority {}", m0), Self::Attribute(m0) => write!(f, "{}", m0), } } @@ -2138,7 +2266,8 @@ impl Option { } impl SmtlibParse for Option { fn is_start_of(offset: usize, p: &mut Parser) -> bool { - (p.nth_matches(offset, Token::Keyword, ":verbosity")) + (p.nth_matches(offset, Token::Keyword, ":opt.priority")) + || (p.nth_matches(offset, Token::Keyword, ":verbosity")) || (p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit")) || (p.nth_matches(offset, Token::Keyword, ":regular-output-channel")) || (p.nth_matches(offset, Token::Keyword, ":random-seed")) @@ -2156,6 +2285,11 @@ impl SmtlibParse for Option { } fn parse(p: &mut Parser) -> Result { let offset = 0; + if p.nth_matches(offset, Token::Keyword, ":opt.priority") { + p.expect_matches(Token::Keyword, ":opt.priority")?; + let m0 = ::parse(p)?; + #[allow(clippy::useless_conversion)] return Ok(Self::OptPriority(m0.into())); + } if p.nth_matches(offset, Token::Keyword, ":verbosity") { p.expect_matches(Token::Keyword, ":verbosity")?; let m0 = ::parse(p)?; @@ -2247,6 +2381,53 @@ impl SmtlibParse for Option { } #[derive(Debug, Clone, PartialEq, Eq, Hash)] #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub enum OptimizationPriority { + /// `pareto` + Pareto, + /// `lex` + Lex, + /// `box` + Box, +} +impl std::fmt::Display for OptimizationPriority { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + match self { + Self::Pareto => write!(f, "pareto"), + Self::Lex => write!(f, "lex"), + Self::Box => write!(f, "box"), + } + } +} +impl OptimizationPriority { + pub fn parse(src: &str) -> Result { + SmtlibParse::parse(&mut Parser::new(src)) + } +} +impl SmtlibParse for OptimizationPriority { + fn is_start_of(offset: usize, p: &mut Parser) -> bool { + (p.nth_matches(offset, Token::Symbol, "box")) + || (p.nth_matches(offset, Token::Symbol, "lex")) + || (p.nth_matches(offset, Token::Symbol, "pareto")) + } + fn parse(p: &mut Parser) -> Result { + let offset = 0; + if p.nth_matches(offset, Token::Symbol, "box") { + p.expect_matches(Token::Symbol, "box")?; + #[allow(clippy::useless_conversion)] return Ok(Self::Box); + } + if p.nth_matches(offset, Token::Symbol, "lex") { + p.expect_matches(Token::Symbol, "lex")?; + #[allow(clippy::useless_conversion)] return Ok(Self::Lex); + } + if p.nth_matches(offset, Token::Symbol, "pareto") { + p.expect_matches(Token::Symbol, "pareto")?; + #[allow(clippy::useless_conversion)] return Ok(Self::Pareto); + } + Err(p.stuck("optimization_priority")) + } +} +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] pub enum InfoFlag { /// `:all-statistics` AllStatistics, @@ -2951,6 +3132,29 @@ impl SmtlibParse for SimplifyResponse { Ok(Self(m0)) } } +/// `` +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +pub struct EvalResponse(pub Term); +impl std::fmt::Display for EvalResponse { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + write!(f, "{}", self.0) + } +} +impl EvalResponse { + pub fn parse(src: &str) -> Result { + SmtlibParse::parse(&mut Parser::new(src)) + } +} +impl SmtlibParse for EvalResponse { + fn is_start_of(offset: usize, p: &mut Parser) -> bool { + Term::is_start_of(offset, p) + } + fn parse(p: &mut Parser) -> Result { + let m0 = ::parse(p)?; + Ok(Self(m0)) + } +} #[derive(Debug, Clone, PartialEq, Eq, Hash)] #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] pub enum SpecificSuccessResponse { @@ -2978,6 +3182,8 @@ pub enum SpecificSuccessResponse { GetValueResponse(GetValueResponse), /// `` SimplifyResponse(SimplifyResponse), + /// `` + EvalResponse(EvalResponse), } impl std::fmt::Display for SpecificSuccessResponse { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -2994,6 +3200,7 @@ impl std::fmt::Display for SpecificSuccessResponse { Self::GetUnsatCoreResponse(m0) => write!(f, "{}", m0), Self::GetValueResponse(m0) => write!(f, "{}", m0), Self::SimplifyResponse(m0) => write!(f, "{}", m0), + Self::EvalResponse(m0) => write!(f, "{}", m0), } } } @@ -3004,7 +3211,8 @@ impl SpecificSuccessResponse { } impl SmtlibParse for SpecificSuccessResponse { fn is_start_of(offset: usize, p: &mut Parser) -> bool { - (SimplifyResponse::is_start_of(offset, p)) + (EvalResponse::is_start_of(offset, p)) + || (SimplifyResponse::is_start_of(offset, p)) || (GetValueResponse::is_start_of(offset, p)) || (GetUnsatCoreResponse::is_start_of(offset, p)) || (GetProofResponse::is_start_of(offset, p)) @@ -3019,6 +3227,11 @@ impl SmtlibParse for SpecificSuccessResponse { } fn parse(p: &mut Parser) -> Result { let offset = 0; + if EvalResponse::is_start_of(offset, p) { + let m0 = ::parse(p)?; + #[allow(clippy::useless_conversion)] + return Ok(Self::EvalResponse(m0.into())); + } if SimplifyResponse::is_start_of(offset, p) { let m0 = ::parse(p)?; #[allow(clippy::useless_conversion)] diff --git a/lowlevel/src/backend/mod.rs b/lowlevel/src/backend/mod.rs index 1121afd..4a2b0aa 100644 --- a/lowlevel/src/backend/mod.rs +++ b/lowlevel/src/backend/mod.rs @@ -7,13 +7,18 @@ //! //! ## Backends //! -//! - **[`Z3Binary`](z3_binary::Z3Binary)**: A [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface. -//! - **[`Z3BinaryTokio`](z3_binary::tokio::Z3BinaryTokio)**: An async [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface with [`tokio`](::tokio). +//! - **[`Z3Binary`](z3_binary::Z3Binary)**: A [Z3](https://github.com/Z3Prover/z3) +//! backend using the binary CLI interface. +//! - **[`Z3BinaryTokio`](z3_binary::tokio::Z3BinaryTokio)**: An async [Z3](https://github.com/Z3Prover/z3) +//! backend using the binary CLI interface with [`tokio`](::tokio). //! - **Enabled by feature:** `tokio` -//! - **`Z3Static`**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` crate](https://github.com/prove-rs/z3.rs). +//! - **`Z3Static`**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` +//! crate](https://github.com/prove-rs/z3.rs). //! - **Enabled by feature:** `z3-static` -//! - **[`Cvc5Binary`](cvc5_binary::Cvc5Binary)**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface. -//! - **[`Cvc5BinaryTokio`](cvc5_binary::tokio::Cvc5BinaryTokio)**: An async [cvc5](https://cvc5.github.io/) backend using the binary CLI interface with [`tokio`](::tokio). +//! - **[`Cvc5Binary`](cvc5_binary::Cvc5Binary)**: A [cvc5](https://cvc5.github.io/) +//! backend using the binary CLI interface. +//! - **[`Cvc5BinaryTokio`](cvc5_binary::tokio::Cvc5BinaryTokio)**: An async [cvc5](https://cvc5.github.io/) +//! backend using the binary CLI interface with [`tokio`](::tokio). //! - **Enabled by feature:** `tokio` use std::{ @@ -30,7 +35,8 @@ pub mod z3_static; use crate::parse::Token; -/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB language. +/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB +/// language. /// /// For more details read the [`backend`](crate::backend) module documentation. pub trait Backend { @@ -65,6 +71,7 @@ impl BinaryBackend { buf: String::new(), }) } + pub(crate) fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> { // println!("> {cmd}"); writeln!(self.stdin, "{cmd}")?; @@ -78,10 +85,12 @@ impl BinaryBackend { } if Lexer::new(self.buf.as_str()) .map(|tok| tok.unwrap_or(Token::Error)) - .fold(0i32, |acc, tok| match tok { - Token::LParen => acc + 1, - Token::RParen => acc - 1, - _ => acc, + .fold(0i32, |acc, tok| { + match tok { + Token::LParen => acc + 1, + Token::RParen => acc - 1, + _ => acc, + } }) != 0 { @@ -101,9 +110,11 @@ pub mod tokio { use crate::parse::Token; - /// The [`TokioBackend`] trait is used to interact with SMT solver using the SMT-LIB language. + /// The [`TokioBackend`] trait is used to interact with SMT solver using the + /// SMT-LIB language. /// - /// For more details read the [`backend`](crate::backend) module documentation. + /// For more details read the [`backend`](crate::backend) module + /// documentation. pub trait TokioBackend { fn exec( &mut self, @@ -126,6 +137,7 @@ pub mod tokio { init: impl FnOnce(&mut tokio::process::Command), ) -> Result { use std::process::Stdio; + use tokio::process::Command; let mut cmd = Command::new(program); @@ -145,6 +157,7 @@ pub mod tokio { buf: String::new(), }) } + pub(crate) async fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> { // eprintln!("> {cmd}"); self.stdin.write_all(cmd.to_string().as_bytes()).await?; @@ -159,10 +172,12 @@ pub mod tokio { } if Lexer::new(self.buf.as_str()) .map(|tok| tok.unwrap_or(Token::Error)) - .fold(0i32, |acc, tok| match tok { - Token::LParen => acc + 1, - Token::RParen => acc - 1, - _ => acc, + .fold(0i32, |acc, tok| { + match tok { + Token::LParen => acc + 1, + Token::RParen => acc - 1, + _ => acc, + } }) != 0 { diff --git a/lowlevel/src/lexicon.rs b/lowlevel/src/lexicon.rs index be85971..00a4f14 100644 --- a/lowlevel/src/lexicon.rs +++ b/lowlevel/src/lexicon.rs @@ -16,6 +16,7 @@ impl SmtlibParse for Numeral { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Numeral } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Numeral)?.into())) } @@ -32,6 +33,7 @@ impl SmtlibParse for Decimal { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Decimal } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Decimal)?.into())) } @@ -48,6 +50,7 @@ impl SmtlibParse for Symbol { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Symbol } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Symbol)?.into())) } @@ -64,6 +67,7 @@ impl SmtlibParse for Hexadecimal { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Hexadecimal } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Hexadecimal)?.into())) } @@ -85,6 +89,7 @@ impl SmtlibParse for Binary { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Binary } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Binary)?.into())) } @@ -106,6 +111,7 @@ impl SmtlibParse for Reserved { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Reserved } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Reserved)?.into())) } @@ -122,6 +128,7 @@ impl SmtlibParse for Keyword { fn is_start_of(offset: usize, tokens: &mut Parser) -> bool { tokens.nth(offset) == Token::Keyword } + fn parse(tokens: &mut Parser) -> Result { Ok(Self(tokens.expect(Token::Keyword)?.into())) } diff --git a/lowlevel/src/lib.rs b/lowlevel/src/lib.rs index 302f429..59ca236 100644 --- a/lowlevel/src/lib.rs +++ b/lowlevel/src/lib.rs @@ -88,9 +88,11 @@ where Ok(driver) } + pub fn set_logger(&mut self, logger: impl Logger) { self.logger = Some(Box::new(logger)) } + pub fn exec(&mut self, cmd: &Command) -> Result { if let Some(logger) = &self.logger { logger.exec(cmd); @@ -111,9 +113,9 @@ where #[cfg(feature = "tokio")] pub mod tokio { use crate::{ + Error, Logger, ast::{self, Command, GeneralResponse}, backend::tokio::TokioBackend, - Error, Logger, }; pub struct TokioDriver { @@ -153,9 +155,11 @@ pub mod tokio { Ok(driver) } + pub fn set_logger(&mut self, logger: impl Logger) { self.logger = Some(Box::new(logger)) } + pub async fn exec(&mut self, cmd: &Command) -> Result { if let Some(logger) = &self.logger { logger.exec(cmd); @@ -181,14 +185,15 @@ impl Term { Term::SpecConstant(_) => HashSet::new(), Term::Identifier(q) => std::iter::once(q).collect(), Term::Application(_, args) => args.iter().flat_map(|arg| arg.all_consts()).collect(), - Term::Let(_, _) => todo!(), + Term::Let(..) => todo!(), // TODO - Term::Forall(_, _) => HashSet::new(), - Term::Exists(_, _) => todo!(), - Term::Match(_, _) => todo!(), - Term::Annotation(_, _) => todo!(), + Term::Forall(..) => HashSet::new(), + Term::Exists(..) => todo!(), + Term::Match(..) => todo!(), + Term::Annotation(..) => todo!(), } } + pub fn strip_sort(self) -> Term { match self { Term::SpecConstant(_) => self, @@ -198,15 +203,17 @@ impl Term { Term::Application( QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _), args, - ) => Term::Application( - QualIdentifier::Identifier(ident), - args.into_iter().map(|arg| arg.strip_sort()).collect(), - ), - Term::Let(_, _) => todo!(), + ) => { + Term::Application( + QualIdentifier::Identifier(ident), + args.into_iter().map(|arg| arg.strip_sort()).collect(), + ) + } + Term::Let(..) => todo!(), Term::Forall(qs, rs) => Term::Forall(qs, rs), - Term::Exists(_, _) => todo!(), - Term::Match(_, _) => todo!(), - Term::Annotation(_, _) => todo!(), + Term::Exists(..) => todo!(), + Term::Match(..) => todo!(), + Term::Annotation(..) => todo!(), } } } diff --git a/lowlevel/src/parse.rs b/lowlevel/src/parse.rs index 79084af..9736cdf 100644 --- a/lowlevel/src/parse.rs +++ b/lowlevel/src/parse.rs @@ -9,7 +9,8 @@ pub(crate) enum Token { #[token(")")] RParen, - /// A ⟨numeral⟩ is the digit 0 or a non-empty sequence of digits not starting with 0 . + /// A ⟨numeral⟩ is the digit 0 or a non-empty sequence of digits not + /// starting with 0 . #[regex("0|([1-9][0-9]*)", priority = 2)] Numeral, @@ -132,14 +133,17 @@ impl SourceSpan { pub fn offset(&self) -> usize { self.offset } + #[must_use] pub fn len(&self) -> usize { self.length } + #[must_use] pub fn is_empty(&self) -> bool { self.len() == 0 } + #[must_use] pub fn join(&self, span: SourceSpan) -> SourceSpan { let offset = self.offset.min(span.offset); @@ -147,10 +151,12 @@ impl SourceSpan { let length = end - offset; SourceSpan { offset, length } } + #[must_use] pub fn end(&self) -> usize { self.offset + self.length } + #[must_use] pub fn contains(&self, byte_offset: usize) -> bool { self.offset() <= byte_offset && byte_offset < self.end() @@ -248,27 +254,34 @@ impl<'src> Parser<'src> { errors: vec![], } } + pub(crate) fn current(&self) -> Token { self.nth(0) } + pub(crate) fn nth_span(&self, n: usize) -> SourceSpan { self.nth_raw(n).1 } + pub(crate) fn current_span(&self) -> SourceSpan { self.nth_span(0) } + pub(crate) fn nth_str(&self, n: usize) -> &'src str { let span = self.nth_span(n); &self.src[span.offset()..span.end()] } + pub(crate) fn current_str(&self) -> &'src str { self.nth_str(0) } + #[allow(unused)] pub(crate) fn current_src_str(&self) -> Spanned<&'src str> { let span = self.current_span(); Spanned(self.current_str(), span) } + pub(crate) fn nth_raw(&self, n: usize) -> (Token, SourceSpan) { if self.cursor + n >= self.lexer.len() { (Token::Error, SourceSpan::from((self.src.len(), 0))) @@ -276,24 +289,30 @@ impl<'src> Parser<'src> { self.lexer[self.cursor + n] } } + pub(crate) fn nth(&self, n: usize) -> Token { self.nth_raw(n).0 } + // TODO: Maybe we should assert end of stream when parsing scripts? #[allow(unused)] pub(crate) fn eoi(&self) -> bool { self.cursor >= self.lexer.len() } + #[allow(unused)] pub(crate) fn pos(&self) -> usize { self.cursor } + pub(crate) fn bump(&mut self) { self.cursor += 1 } + pub(crate) fn nth_matches(&self, n: usize, t: Token, s: &str) -> bool { self.nth(n) == t && self.nth_str(n) == s } + pub(crate) fn expect_matches(&mut self, t: Token, s: &str) -> Result<&'src str, ParseError> { if self.nth_matches(0, t, s) { let s = self.current_str(); @@ -303,6 +322,7 @@ impl<'src> Parser<'src> { todo!() } } + pub(crate) fn expect(&mut self, t: Token) -> Result<&'src str, ParseError> { match self.current() { found if found == t => { @@ -324,6 +344,7 @@ impl<'src> Parser<'src> { } } } + pub(crate) fn any(&mut self) -> Result, ParseError> { let mut res = vec![]; while T::is_start_of(0, self) { @@ -331,6 +352,7 @@ impl<'src> Parser<'src> { } Ok(res) } + pub(crate) fn non_zero(&mut self) -> Result, ParseError> { let mut res = vec![T::parse(self)?]; while T::is_start_of(0, self) { @@ -338,6 +360,7 @@ impl<'src> Parser<'src> { } Ok(res) } + pub(crate) fn n_plus_one(&mut self) -> Result, ParseError> { // TODO self.non_zero() diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs index 58146f1..dd79856 100644 --- a/lowlevel/src/tests.rs +++ b/lowlevel/src/tests.rs @@ -13,7 +13,7 @@ fn bubble_sort() { } mod z3 { - use crate::{ast::Command, backend::z3_binary::Z3Binary, Driver}; + use crate::{Driver, ast::Command, backend::z3_binary::Z3Binary}; macro_rules! cmd { ($d:expr, $cmd:literal) => { @@ -46,7 +46,7 @@ mod z3 { #[cfg(feature = "z3-static")] mod z3_static { - use crate::{ast::Command, backend::Z3Static, Driver}; + use crate::{Driver, ast::Command, backend::Z3Static}; macro_rules! cmd { ($d:expr, $cmd:literal) => { diff --git a/smtlib/examples/queens.rs b/smtlib/examples/queens.rs index 9559033..591332a 100644 --- a/smtlib/examples/queens.rs +++ b/smtlib/examples/queens.rs @@ -3,11 +3,10 @@ use miette::IntoDiagnostic; #[cfg(feature = "z3-static")] use smtlib::backend::Z3Static; use smtlib::{ - and, - backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, + Int, Logic, SatResultWithModel, Solver, and, + backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary}, distinct, or, prelude::*, - Int, Logic, SatResultWithModel, Solver, }; fn queens(backend: B) -> miette::Result<()> { @@ -82,10 +81,12 @@ fn main() -> miette::Result<()> { #[cfg(feature = "z3-static")] "z3-static" => queens(Z3Static::new().into_diagnostic()?)?, "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?, - given => miette::bail!( - "Invalid backend: '{}'. Available backends are: 'z3', 'z3-static', 'cvc5'", - given - ), + given => { + miette::bail!( + "Invalid backend: '{}'. Available backends are: 'z3', 'z3-static', 'cvc5'", + given + ) + } } Ok(()) diff --git a/smtlib/examples/queens_bv.rs b/smtlib/examples/queens_bv.rs index 6198856..ff061d6 100644 --- a/smtlib/examples/queens_bv.rs +++ b/smtlib/examples/queens_bv.rs @@ -3,11 +3,10 @@ use itertools::Itertools; use miette::IntoDiagnostic; use smtlib::{ - and, - backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, + BitVec, SatResultWithModel, Solver, and, + backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary}, distinct, or, prelude::*, - BitVec, SatResultWithModel, Solver, }; fn queens(backend: B) -> miette::Result<()> { @@ -80,10 +79,12 @@ fn main() -> miette::Result<()> { match std::env::args().nth(1).as_deref().unwrap_or("z3") { "z3" => queens(Z3Binary::new("z3").into_diagnostic()?)?, "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?, - given => miette::bail!( - "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'", - given - ), + given => { + miette::bail!( + "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'", + given + ) + } } Ok(()) diff --git a/smtlib/examples/queens_bv2.rs b/smtlib/examples/queens_bv2.rs index 911256f..1aea41d 100644 --- a/smtlib/examples/queens_bv2.rs +++ b/smtlib/examples/queens_bv2.rs @@ -3,11 +3,10 @@ use itertools::Itertools; use miette::IntoDiagnostic; use smtlib::{ - and, - backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend}, + BitVec, Logic, SatResultWithModel, Solver, and, + backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary}, distinct, or, prelude::*, - BitVec, Logic, SatResultWithModel, Solver, }; fn queens(backend: B) -> miette::Result<()> { @@ -94,10 +93,12 @@ fn main() -> miette::Result<()> { match std::env::args().nth(1).as_deref().unwrap_or("z3") { "z3" => queens(Z3Binary::new("z3").into_diagnostic()?)?, "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?, - given => miette::bail!( - "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'", - given - ), + given => { + miette::bail!( + "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'", + given + ) + } } Ok(()) diff --git a/smtlib/src/funs.rs b/smtlib/src/funs.rs index 01e6997..5c48951 100644 --- a/smtlib/src/funs.rs +++ b/smtlib/src/funs.rs @@ -2,7 +2,7 @@ use smtlib_lowlevel::{ast, lexicon::Symbol}; use crate::{ sorts::Sort, - terms::{qual_ident, Dynamic}, + terms::{Dynamic, qual_ident}, }; #[derive(Debug)] diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs index 135dd7b..0fd3aa4 100644 --- a/smtlib/src/lib.rs +++ b/smtlib/src/lib.rs @@ -5,15 +5,14 @@ use std::collections::HashMap; +pub use backend::Backend; use itertools::Itertools; +pub use logics::Logic; use smtlib_lowlevel::ast; +pub use smtlib_lowlevel::{self as lowlevel, Logger, backend}; use terms::Const; pub use terms::Sorted; -pub use backend::Backend; -pub use logics::Logic; -pub use smtlib_lowlevel::{self as lowlevel, backend, Logger}; - #[cfg(feature = "tokio")] mod tokio_solver; #[rustfmt::skip] @@ -56,8 +55,9 @@ impl std::fmt::Display for SatResult { } } -/// The satisfiability result produced by a solver, where the [`Sat`](SatResultWithModel::Sat) variant -/// carries the satisfying model as well. +/// The satisfiability result produced by a solver, where the +/// [`Sat`](SatResultWithModel::Sat) variant carries the satisfying model as +/// well. #[derive(Debug)] pub enum SatResultWithModel { /// The solver produced `unsat` @@ -74,14 +74,18 @@ impl SatResultWithModel { pub fn expect_sat(self) -> Result { match self { SatResultWithModel::Sat(m) => Ok(m), - SatResultWithModel::Unsat => Err(Error::UnexpectedSatResult { - expected: SatResult::Sat, - actual: SatResult::Unsat, - }), - SatResultWithModel::Unknown => Err(Error::UnexpectedSatResult { - expected: SatResult::Sat, - actual: SatResult::Unknown, - }), + SatResultWithModel::Unsat => { + Err(Error::UnexpectedSatResult { + expected: SatResult::Sat, + actual: SatResult::Unsat, + }) + } + SatResultWithModel::Unknown => { + Err(Error::UnexpectedSatResult { + expected: SatResult::Sat, + actual: SatResult::Unknown, + }) + } } } } @@ -156,14 +160,17 @@ impl Model { values: model .0 .into_iter() - .map(|res| match res { - ast::ModelResponse::DefineFun(f) => (f.0 .0.trim_matches('|').into(), f.3), - ast::ModelResponse::DefineFunRec(_) => todo!(), - ast::ModelResponse::DefineFunsRec(_, _) => todo!(), + .map(|res| { + match res { + ast::ModelResponse::DefineFun(f) => (f.0.0.trim_matches('|').into(), f.3), + ast::ModelResponse::DefineFunRec(_) => todo!(), + ast::ModelResponse::DefineFunsRec(..) => todo!(), + } }) .collect(), } } + /// Extract the value of a constant. Returns `None` if the value was not /// part of the model, which occurs if the constant was not part of any /// expression asserted. diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs index 10a2510..49ec524 100644 --- a/smtlib/src/solver.rs +++ b/smtlib/src/solver.rs @@ -1,15 +1,17 @@ -use indexmap::{map::Entry, IndexMap, IndexSet}; +use indexmap::{IndexMap, IndexSet, map::Entry}; use smtlib_lowlevel::{ - ast::{self, Identifier, QualIdentifier}, + Driver, Logger, + ast::{ + self, EvalResponse, GeneralResponse, Identifier, OptimizationPriority, QualIdentifier, + SpecificSuccessResponse, Term, + }, backend, lexicon::{Numeral, Symbol}, - Driver, Logger, }; use crate::{ - funs, sorts, - terms::{qual_ident, Dynamic}, - Bool, Error, Logic, Model, SatResult, SatResultWithModel, + Bool, Error, Logic, Model, SatResult, SatResultWithModel, Sorted, funs, sorts, + terms::{Dynamic, qual_ident}, }; /// The [`Solver`] type is the primary entrypoint to interaction with the @@ -68,9 +70,11 @@ where declared_sorts: Default::default(), }) } + pub fn set_logger(&mut self, logger: impl Logger) { self.driver.set_logger(logger) } + pub fn set_timeout(&mut self, ms: usize) -> Result<(), Error> { let cmd = ast::Command::SetOption(ast::Option::Attribute(ast::Attribute::WithValue( smtlib_lowlevel::lexicon::Keyword(":timeout".to_string()), @@ -82,6 +86,18 @@ where _ => todo!(), } } + + /// sets the :opt.priority option to the given value + pub fn set_opt_priority(&mut self, priority: ast::OptimizationPriority) -> Result<(), Error> { + let cmd = ast::Command::SetOption(ast::Option::OptPriority(priority)); + + match self.driver.exec(&cmd)? { + ast::GeneralResponse::Success => Ok(()), + ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())), + _ => unimplemented!(), + } + } + /// Explicitly sets the logic for the solver. For some backends this is not /// required, as they will infer what ever logic fits the current program. /// @@ -95,10 +111,12 @@ where ast::GeneralResponse::Error(_) => todo!(), } } + /// Runs the given command on the solver, and returns the result. pub fn run_command(&mut self, cmd: &ast::Command) -> Result { Ok(self.driver.exec(cmd)?) } + /// Adds the constraint of `b` as an assertion to the solver. To check for /// satisfiability call [`Solver::check_sat`] or /// [`Solver::check_sat_with_model`]. @@ -114,6 +132,58 @@ where _ => todo!(), } } + + /// Adds the optimization goal of `g` as a goal to the solver. + pub fn maximize(&mut self, g: S) -> Result<(), Error> + where + S: Sorted, + { + let term = g.into(); + + self.declare_all_consts(&term)?; + + let cmd = ast::Command::Maximize(term); + + match self.driver.exec(&cmd)? { + ast::GeneralResponse::Success => Ok(()), + ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())), + _ => unimplemented!(), + } + } + + /// Adds soft-constraint `b` to the solver. + pub fn assert_soft(&mut self, b: Bool) -> Result<(), Error> { + let term = b.into(); + + self.declare_all_consts(&term)?; + + let cmd = ast::Command::AssertSoft(term, vec![]); + + match self.driver.exec(&cmd)? { + ast::GeneralResponse::Success => Ok(()), + ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())), + _ => unimplemented!(), + } + } + + /// Adds the optimization goal of `g` as a goal to the solver. + pub fn minimize(&mut self, g: S) -> Result<(), Error> + where + S: Sorted, + { + let term = g.into(); + + self.declare_all_consts(&term)?; + + let cmd = ast::Command::Minimize(term); + + match self.driver.exec(&cmd)? { + ast::GeneralResponse::Success => Ok(()), + ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())), + _ => unimplemented!(), + } + } + /// Checks for satisfiability of the assertions sent to the solver using /// [`Solver::assert`]. /// @@ -124,15 +194,18 @@ where match self.driver.exec(&cmd)? { ast::GeneralResponse::SpecificSuccessResponse( ast::SpecificSuccessResponse::CheckSatResponse(res), - ) => Ok(match res { - ast::CheckSatResponse::Sat => SatResult::Sat, - ast::CheckSatResponse::Unsat => SatResult::Unsat, - ast::CheckSatResponse::Unknown => SatResult::Unknown, - }), + ) => { + Ok(match res { + ast::CheckSatResponse::Sat => SatResult::Sat, + ast::CheckSatResponse::Unsat => SatResult::Unsat, + ast::CheckSatResponse::Unknown => SatResult::Unknown, + }) + } ast::GeneralResponse::Error(msg) => Err(Error::Smt(msg, format!("{cmd}"))), res => todo!("{res:?}"), } } + /// Checks for satisfiability of the assertions sent to the solver using /// [`Solver::assert`], and produces a [model](Model) in case of `sat`. /// @@ -145,6 +218,7 @@ where SatResult::Unknown => Ok(SatResultWithModel::Unknown), } } + /// Produces the model for satisfying the assertions. If you are looking to /// retrieve a model after calling [`Solver::check_sat`], consider using /// [`Solver::check_sat_with_model`] instead. @@ -159,6 +233,7 @@ where res => todo!("{res:?}"), } } + pub fn declare_fun(&mut self, fun: &funs::Fun) -> Result<(), Error> { for var in &fun.vars { self.declare_sort(&var.ast())?; @@ -180,6 +255,7 @@ where _ => todo!(), } } + /// Simplifies the given term pub fn simplify(&mut self, t: Dynamic) -> Result { self.declare_all_consts(&t.into())?; @@ -194,6 +270,22 @@ where } } + pub fn eval(&mut self, term: S) -> Result + where + S: Sorted, + S::Inner: From, + { + let cmd = ast::Command::Eval(term.into()); + + match self.driver.exec(&cmd)? { + GeneralResponse::SpecificSuccessResponse(SpecificSuccessResponse::EvalResponse( + EvalResponse(t), + )) => Ok(t.into()), + GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())), + _ => unimplemented!(), + } + } + pub fn scope( &mut self, f: impl FnOnce(&mut Solver) -> Result, @@ -254,7 +346,7 @@ where self.driver .exec(&ast::Command::DeclareConst(sym.clone(), s.clone()))?; } - Identifier::Indexed(_, _) => todo!(), + Identifier::Indexed(..) => todo!(), } } } @@ -272,7 +364,7 @@ where ast::Sort::Sort(ident) => { let sym = match ident { Identifier::Simple(sym) => sym, - Identifier::Indexed(_, _) => { + Identifier::Indexed(..) => { // TODO: is it correct that only sorts from theores can // be indexed, and thus does not need to be declared? return Ok(()); @@ -286,7 +378,7 @@ where ast::Sort::Parametric(ident, params) => { let sym = match ident { Identifier::Simple(sym) => sym, - Identifier::Indexed(_, _) => { + Identifier::Indexed(..) => { // TODO: is it correct that only sorts from theores can // be indexed, and thus does not need to be declared? return Ok(()); diff --git a/smtlib/src/sorts.rs b/smtlib/src/sorts.rs index 1d16b46..462b927 100644 --- a/smtlib/src/sorts.rs +++ b/smtlib/src/sorts.rs @@ -55,7 +55,7 @@ impl Index { pub(crate) fn is_built_in_sort(name: &str) -> bool { match name { - "Int" | "Bool" => true, + "Int" | "Bool" | "Real" => true, _ => false, } } @@ -63,16 +63,13 @@ pub(crate) fn is_built_in_sort(name: &str) -> bool { impl Sort { pub fn new(name: impl Into) -> Self { let mut name = name.into(); - if !is_built_in_sort(&name) { - // HACK: how should we handle this? or should we event handle it? - name += "_xxx"; - } Self { name, index: Vec::new(), parameters: Vec::new(), } } + pub fn new_parametric(name: impl Into, parameters: Vec) -> Self { Self { name: name.into(), @@ -80,6 +77,7 @@ impl Sort { parameters, } } + pub fn new_indexed(name: impl Into, index: Vec) -> Self { Self { name: name.into(), diff --git a/smtlib/src/terms.rs b/smtlib/src/terms.rs index b67b20a..bec3707 100644 --- a/smtlib/src/terms.rs +++ b/smtlib/src/terms.rs @@ -11,7 +11,7 @@ use smtlib_lowlevel::{ lexicon::{Keyword, Symbol}, }; -use crate::{sorts::Sort, Bool}; +use crate::{Bool, sorts::Sort}; pub(crate) fn fun(name: &str, args: Vec) -> Term { Term::Application(qual_ident(name.to_string(), None), args) @@ -74,7 +74,8 @@ pub trait StaticSorted: Into + From { /// low-level primitive that is used to define expressions for the SMT solvers /// to evaluate. pub trait Sorted: Into { - /// The inner type of the term. This is used for [`Const`](Const) where the inner type is `T`. + /// The inner type of the term. This is used for [`Const`](Const) where + /// the inner type is `T`. type Inner: Sorted; /// The sort of the term fn sort(&self) -> Sort; @@ -135,13 +136,10 @@ pub trait Sorted: Into { ( label, - Term::Annotation( - Box::new(self.into()), - vec![Attribute::WithValue( - Keyword("named".to_string()), - AttributeValue::Symbol(Symbol(name)), - )], - ) + Term::Annotation(Box::new(self.into()), vec![Attribute::WithValue( + Keyword("named".to_string()), + AttributeValue::Symbol(Symbol(name)), + )]) .into(), ) } @@ -153,9 +151,11 @@ impl> From> for Term { } impl Sorted for Const { type Inner = T; + fn sort(&self) -> Sort { T::sort(self) } + fn is_sort(sort: &Sort) -> bool { T::is_sort(sort) } @@ -188,6 +188,7 @@ impl Label { Label(n, PhantomData) } + pub(crate) fn name(&self) -> String { format!("named-label-{}", self.0) } @@ -240,9 +241,11 @@ impl Dynamic { } impl Sorted for Dynamic { type Inner = Self; + fn sort(&self) -> Sort { self.1.clone() } + fn is_sort(_sort: &Sort) -> bool { true } @@ -293,7 +296,8 @@ macro_rules! impl_op { }; } -/// This trait is implemented for types and sequences which can be used as quantified variables in [`forall`] and [`exists`]. +/// This trait is implemented for types and sequences which can be used as +/// quantified variables in [`forall`] and [`exists`]. pub trait QuantifierVars { /// The concrete sequence of variable declaration which should be quantified /// over. @@ -340,7 +344,7 @@ impl_quantifiers!(A 0, B 1, C 2, D 3, E 4); impl QuantifierVars for Vec> { fn into_vars(self) -> Vec { self.into_iter() - .map(|v| SortedVar(Symbol(v.0.into()), v.1 .1.ast())) + .map(|v| SortedVar(Symbol(v.0.into()), v.1.1.ast())) .collect() } } diff --git a/smtlib/src/tests.rs b/smtlib/src/tests.rs index 94168a7..44dff2f 100644 --- a/smtlib/src/tests.rs +++ b/smtlib/src/tests.rs @@ -1,8 +1,7 @@ use terms::StaticSorted; -use crate::terms::{forall, Sorted}; - use super::*; +use crate::terms::{Sorted, forall}; #[test] fn int_math() { diff --git a/smtlib/src/theories/core.rs b/smtlib/src/theories/core.rs index 14bfdc5..9409600 100644 --- a/smtlib/src/theories/core.rs +++ b/smtlib/src/theories/core.rs @@ -5,7 +5,7 @@ use smtlib_lowlevel::ast::{self, Term}; use crate::{ impl_op, sorts::Sort, - terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted}, + terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident}, }; /// A [`Bool`] is a term containing a @@ -77,9 +77,11 @@ impl From<(Term, Sort)> for Bool { } impl StaticSorted for Bool { type Inner = Self; + fn static_sort() -> Sort { Sort::new("Bool") } + fn new_const(name: impl Into) -> Const { let name = String::leak(name.into()); Const(name, Bool(BoolImpl::Const(name))) @@ -89,9 +91,11 @@ impl Bool { pub fn sort() -> Sort { Self::static_sort() } + fn binop(self, op: &str, other: Bool) -> Self { fun(op, vec![self.into(), other.into()]).into() } + /// Construct the term expressing `(==> self other)`. /// /// The value of the returned boolean is true if: @@ -100,6 +104,7 @@ impl Bool { pub fn implies(self, other: Bool) -> Bool { self.binop("=>", other) } + /// Construct the term expressing `(ite self then otherwise)`. /// /// This is similar to the [ternary condition @@ -134,8 +139,8 @@ pub fn and(terms: [Bool; N]) -> Bool { fun("and", terms.map(Into::into).to_vec()).into() } /// Construct the term expressing `(or ...terms)` representing the disjunction -/// of all of the terms. That is to say, the result is true iff any of the terms in -/// `terms` is true. +/// of all of the terms. That is to say, the result is true iff any of the terms +/// in `terms` is true. pub fn or(terms: [Bool; N]) -> Bool { fun("or", terms.map(Into::into).to_vec()).into() } @@ -152,8 +157,8 @@ where { fun("=", terms.map(Into::into).to_vec()).into() } -/// Construct the term expressing `(distinct terms)` representing that all of the -/// terms in `terms` are distinct (or not-equal). +/// Construct the term expressing `(distinct terms)` representing that all of +/// the terms in `terms` are distinct (or not-equal). pub fn distinct(terms: [T; N]) -> Bool where T: Into, diff --git a/smtlib/src/theories/fixed_size_bit_vectors.rs b/smtlib/src/theories/fixed_size_bit_vectors.rs index 1c8e6d5..5c829e6 100644 --- a/smtlib/src/theories/fixed_size_bit_vectors.rs +++ b/smtlib/src/theories/fixed_size_bit_vectors.rs @@ -4,9 +4,9 @@ use itertools::Itertools; use smtlib_lowlevel::ast::{self, Term}; use crate::{ - sorts::{Index, Sort}, - terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted}, Bool, + sorts::{Index, Sort}, + terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident}, }; /// A bit-vec is a fixed size sequence of boolean values. You can [read more @@ -57,13 +57,15 @@ impl TryFrom> for i64 { fn try_from(value: BitVec) -> Result { match value.0 { - Term::SpecConstant(c) => match c { - ast::SpecConstant::Numeral(_) => todo!(), - ast::SpecConstant::Decimal(_) => todo!(), - ast::SpecConstant::Hexadecimal(h) => h.parse(), - ast::SpecConstant::Binary(b) => b.parse(), - ast::SpecConstant::String(_) => todo!(), - }, + Term::SpecConstant(c) => { + match c { + ast::SpecConstant::Numeral(_) => todo!(), + ast::SpecConstant::Decimal(_) => todo!(), + ast::SpecConstant::Hexadecimal(h) => h.parse(), + ast::SpecConstant::Binary(b) => b.parse(), + ast::SpecConstant::String(_) => todo!(), + } + } _ => todo!(), } } @@ -78,6 +80,7 @@ impl TryFrom> for [bool; M] { impl StaticSorted for BitVec { type Inner = Self; + fn static_sort() -> Sort { Sort::new_indexed("BitVec", vec![Index::Numeral(M)]) } @@ -100,6 +103,7 @@ impl BitVec { fn binop>(self, op: &str, other: BitVec) -> T { fun(op, vec![self.into(), other.into()]).into() } + fn unop>(self, op: &str) -> T { fun(op, vec![self.into()]).into() } @@ -128,14 +132,15 @@ impl BitVec { ) .into() } + #[cfg(feature = "const-bit-vec")] /// Concatenates `self` and `other` bit-vecs to a single contiguous bit-vec /// with length `N + M` pub fn concat(self, other: impl Into>) -> BitVec<{ N + M }> { - Term::Application( - qual_ident("concat".to_string(), None), - vec![self.into(), other.into().into()], - ) + Term::Application(qual_ident("concat".to_string(), None), vec![ + self.into(), + other.into().into(), + ]) .into() } @@ -144,6 +149,7 @@ impl BitVec { pub fn bvnot(self) -> Self { self.unop("bvnot") } + /// Calls `(bvneg self)` i.e. two's complement negation pub fn bvneg(self) -> Self { self.unop("bvneg") @@ -154,42 +160,52 @@ impl BitVec { pub fn bvnand(self, other: impl Into) -> Self { self.binop("bvnand", other.into()) } + /// Calls `(bvnor self other)` i.e. bitwise nor pub fn bvnor(self, other: impl Into) -> Self { self.binop("bvnor", other.into()) } + /// Calls `(bvxnor self other)` i.e. bitwise xnor pub fn bvxnor(self, other: impl Into) -> Self { self.binop("bvxnor", other.into()) } + /// Calls `(bvult self other)` pub fn bvult(self, other: impl Into) -> Bool { self.binop("bvult", other.into()) } + /// Calls `(bvule self other)` i.e. unsigned less or equal pub fn bvule(self, other: impl Into) -> Bool { self.binop("bvule", other.into()) } + /// Calls `(bvugt self other)` i.e. unsigned greater than pub fn bvugt(self, other: impl Into) -> Bool { self.binop("bvugt", other.into()) } + /// Calls `(bvuge self other)` i.e. unsigned greater or equal pub fn bvuge(self, other: impl Into) -> Bool { self.binop("bvuge", other.into()) } + /// Calls `(bvslt self other)` i.e. signed less than pub fn bvslt(self, other: impl Into) -> Bool { self.binop("bvslt", other.into()) } + /// Calls `(bvsle self other)` i.e. signed less or equal pub fn bvsle(self, other: impl Into) -> Bool { self.binop("bvsle", other.into()) } + /// Calls `(bvsgt self other)` i.e. signed greater than pub fn bvsgt(self, other: impl Into) -> Bool { self.binop("bvsgt", other.into()) } + /// Calls `(bvsge self other)` i.e. signed greater or equal pub fn bvsge(self, other: impl Into) -> Bool { self.binop("bvsge", other.into()) @@ -198,12 +214,14 @@ impl BitVec { impl std::ops::Not for BitVec { type Output = Self; + fn not(self) -> Self::Output { self.bvnot() } } impl std::ops::Neg for BitVec { type Output = Self; + fn neg(self) -> Self::Output { self.bvneg() } @@ -274,9 +292,8 @@ impl_op!(BitVec, [bool; M], Shl, shl, bvshl, ShlAssign, shl_assign, <<); mod tests { use smtlib_lowlevel::backend::Z3Binary; - use crate::{terms::Sorted, Solver}; - use super::BitVec; + use crate::{Solver, terms::Sorted}; #[test] fn bit_vec_extract_concat() -> Result<(), Box> { diff --git a/smtlib/src/theories/ints.rs b/smtlib/src/theories/ints.rs index 3ff55ce..846b2d2 100644 --- a/smtlib/src/theories/ints.rs +++ b/smtlib/src/theories/ints.rs @@ -3,10 +3,9 @@ use smtlib_lowlevel::{ast::Term, lexicon::Numeral}; use crate::{ - impl_op, + Bool, impl_op, sorts::Sort, - terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted}, - Bool, + terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident}, }; /// A [`Int`] is a term containing a @@ -48,6 +47,7 @@ impl From<(Term, Sort)> for Int { } impl StaticSorted for Int { type Inner = Self; + fn static_sort() -> Sort { Sort::new("Int") } @@ -64,25 +64,31 @@ impl Int { pub fn sort() -> Sort { Self::static_sort() } + fn binop>(self, op: &str, other: Int) -> T { fun(op, vec![self.into(), other.into()]).into() } + /// Construct the term expressing `(> self other)` pub fn gt(self, other: impl Into) -> Bool { self.binop(">", other.into()) } + /// Construct the term expressing `(>= self other)` pub fn ge(self, other: impl Into) -> Bool { self.binop(">=", other.into()) } + /// Construct the term expressing `(< self other)` pub fn lt(self, other: impl Into) -> Bool { self.binop("<", other.into()) } + /// Construct the term expressing `(<= self other)` pub fn le(self, other: impl Into) -> Bool { self.binop("<=", other.into()) } + // TODO: This seems to not be supported by z3? /// Construct the term expressing `(abs self)` pub fn abs(self) -> Int { @@ -92,6 +98,7 @@ impl Int { impl std::ops::Neg for Int { type Output = Self; + fn neg(self) -> Self::Output { fun("-", vec![self.into()]).into() } diff --git a/smtlib/src/theories/reals.rs b/smtlib/src/theories/reals.rs index 6bd77db..9885acc 100644 --- a/smtlib/src/theories/reals.rs +++ b/smtlib/src/theories/reals.rs @@ -3,10 +3,9 @@ use smtlib_lowlevel::ast::Term; use crate::{ - impl_op, + Bool, impl_op, sorts::Sort, - terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted}, - Bool, + terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident}, }; /// A [`Real`] is a term containing a @@ -43,6 +42,7 @@ impl From for Real { } impl StaticSorted for Real { type Inner = Self; + fn static_sort() -> Sort { Sort::new("Real") } @@ -66,33 +66,48 @@ impl Real { pub fn sort() -> Sort { Self::static_sort() } + fn binop>(self, op: &str, other: Real) -> T { fun(op, vec![self.into(), other.into()]).into() } + /// Construct the term expressing `(> self other)` pub fn gt(self, other: impl Into) -> Bool { self.binop(">", other.into()) } + /// Construct the term expressing `(>= self other)` pub fn ge(self, other: impl Into) -> Bool { self.binop(">=", other.into()) } + /// Construct the term expressing `(< self other)` pub fn lt(self, other: impl Into) -> Bool { self.binop("<", other.into()) } + /// Construct the term expressing `(<= self other)` pub fn le(self, other: impl Into) -> Bool { self.binop("<=", other.into()) } + /// Construct the term expressing `(abs self)` pub fn abs(self) -> Real { fun("abs", vec![self.into()]).into() } + + /// Construct the term expressing floor division of two terms + pub fn floor_div(self, rhs: R) -> Self + where + R: Into, + { + self.binop("div", rhs.into()) + } } impl std::ops::Neg for Real { type Output = Self; + fn neg(self) -> Self::Output { fun("-", vec![self.into()]).into() } @@ -101,4 +116,4 @@ impl std::ops::Neg for Real { impl_op!(Real, f64, Add, add, "+", AddAssign, add_assign, +); impl_op!(Real, f64, Sub, sub, "-", SubAssign, sub_assign, -); impl_op!(Real, f64, Mul, mul, "*", MulAssign, mul_assign, *); -impl_op!(Real, f64, Div, div, "div", DivAssign, div_assign, /); +impl_op!(Real, f64, Div, div, "/", DivAssign, div_assign, /); diff --git a/smtlib/src/tokio_solver.rs b/smtlib/src/tokio_solver.rs index c828277..2ca2e10 100644 --- a/smtlib/src/tokio_solver.rs +++ b/smtlib/src/tokio_solver.rs @@ -1,4 +1,4 @@ -use std::collections::{hash_map::Entry, HashMap}; +use std::collections::{HashMap, hash_map::Entry}; use smtlib_lowlevel::{ ast::{self, Identifier, QualIdentifier}, @@ -57,6 +57,7 @@ where decls: Default::default(), }) } + /// Explicitly sets the logic for the solver. For some backends this is not /// required, as they will infer what ever logic fits the current program. /// @@ -70,10 +71,12 @@ where ast::GeneralResponse::Error(_) => todo!(), } } + /// Runs the given command on the solver, and returns the result. pub async fn run_command(&mut self, cmd: &ast::Command) -> Result { Ok(self.driver.exec(cmd).await?) } + /// Adds the constraint of `b` as an assertion to the solver. To check for /// satisfiability call [`TokioSolver::check_sat`] or /// [`TokioSolver::check_sat_with_model`]. @@ -82,20 +85,22 @@ where for q in term.all_consts() { match q { QualIdentifier::Identifier(_) => {} - QualIdentifier::Sorted(i, s) => match self.decls.entry(i.clone()) { - Entry::Occupied(stored) => assert_eq!(s, stored.get()), - Entry::Vacant(v) => { - v.insert(s.clone()); - match i { - Identifier::Simple(sym) => { - self.driver - .exec(&ast::Command::DeclareConst(sym.clone(), s.clone())) - .await?; + QualIdentifier::Sorted(i, s) => { + match self.decls.entry(i.clone()) { + Entry::Occupied(stored) => assert_eq!(s, stored.get()), + Entry::Vacant(v) => { + v.insert(s.clone()); + match i { + Identifier::Simple(sym) => { + self.driver + .exec(&ast::Command::DeclareConst(sym.clone(), s.clone())) + .await?; + } + Identifier::Indexed(..) => todo!(), } - Identifier::Indexed(_, _) => todo!(), } } - }, + } } } let cmd = ast::Command::Assert(term); @@ -105,6 +110,7 @@ where _ => todo!(), } } + /// Checks for satisfiability of the assertions sent to the solver using /// [`TokioSolver::assert`]. /// @@ -115,15 +121,18 @@ where match self.driver.exec(&cmd).await? { ast::GeneralResponse::SpecificSuccessResponse( ast::SpecificSuccessResponse::CheckSatResponse(res), - ) => Ok(match res { - ast::CheckSatResponse::Sat => SatResult::Sat, - ast::CheckSatResponse::Unsat => SatResult::Unsat, - ast::CheckSatResponse::Unknown => SatResult::Unknown, - }), + ) => { + Ok(match res { + ast::CheckSatResponse::Sat => SatResult::Sat, + ast::CheckSatResponse::Unsat => SatResult::Unsat, + ast::CheckSatResponse::Unknown => SatResult::Unknown, + }) + } ast::GeneralResponse::Error(msg) => Err(Error::Smt(msg, format!("{cmd}"))), res => todo!("{res:?}"), } } + /// Checks for satisfiability of the assertions sent to the solver using /// [`TokioSolver::assert`], and produces a [model](Model) in case of `sat`. /// @@ -136,9 +145,10 @@ where SatResult::Unknown => Ok(SatResultWithModel::Unknown), } } + /// Produces the model for satisfying the assertions. If you are looking to - /// retrieve a model after calling [`TokioSolver::check_sat`], consider using - /// [`TokioSolver::check_sat_with_model`] instead. + /// retrieve a model after calling [`TokioSolver::check_sat`], consider + /// using [`TokioSolver::check_sat_with_model`] instead. /// /// > **NOTE:** This must only be called after having called /// > [`TokioSolver::check_sat`] and it returning [`SatResult::Sat`]. diff --git a/xtask/src/ast.rs b/xtask/src/ast.rs index c0f14ac..c61f3cb 100644 --- a/xtask/src/ast.rs +++ b/xtask/src/ast.rs @@ -48,35 +48,40 @@ impl RawSyntax { priority, separator, response, - } => Syntax::Rule(Rule { - syntax: parse_raw_grammar(syntax), - priority: priority.unwrap_or_default(), - separator: separator.clone(), - response: response.as_ref().map(|s| parse_raw_token(s, 0)), - }), - RawSyntax::Class { response, cases } => Syntax::Class { - response: response.clone(), - cases: cases - .iter() - .map(|(n, s)| match s { - RawSyntax::Just { - syntax, - priority, - separator, - response, - } => ( - n.clone(), - Rule { - syntax: parse_raw_grammar(syntax), - priority: priority.unwrap_or_default(), - separator: separator.clone(), - response: response.as_ref().map(|r| parse_raw_token(r, 0)), - }, - ), - RawSyntax::Class { .. } => todo!(), - }) - .collect(), - }, + } => { + Syntax::Rule(Rule { + syntax: parse_raw_grammar(syntax), + priority: priority.unwrap_or_default(), + separator: separator.clone(), + response: response.as_ref().map(|s| parse_raw_token(s, 0)), + }) + } + RawSyntax::Class { response, cases } => { + Syntax::Class { + response: response.clone(), + cases: cases + .iter() + .map(|(n, s)| { + match s { + RawSyntax::Just { + syntax, + priority, + separator, + response, + } => { + (n.clone(), Rule { + syntax: parse_raw_grammar(syntax), + priority: priority.unwrap_or_default(), + separator: separator.clone(), + response: response.as_ref().map(|r| parse_raw_token(r, 0)), + }) + } + RawSyntax::Class { .. } => todo!(), + } + }) + .collect(), + } + } } } } @@ -128,7 +133,7 @@ impl Token { LParen | RParen | Underscore | Annotation | Keyword(_) | Builtin(_) | Reserved(_) => { true } - Field(_, _) => false, + Field(..) => false, } } } @@ -190,7 +195,7 @@ fn parse_raw_grammar(s: &str) -> Grammar { .split(' ') .map(|t| { let t = parse_raw_token(t, acc); - if let Token::Field(_, _) = t { + if let Token::Field(..) = t { acc += 1 } t @@ -198,9 +203,11 @@ fn parse_raw_grammar(s: &str) -> Grammar { .collect_vec(); let fields = p .iter() - .filter_map(|t| match t { - Token::Field(_, f) => Some(f.clone()), - _ => None, + .filter_map(|t| { + match t { + Token::Field(_, f) => Some(f.clone()), + _ => None, + } }) .collect(); Grammar { tokens: p, fields } @@ -285,72 +292,86 @@ impl Syntax { fn rust_ty_decl_top(&self, name: &str) -> String { let derive = r#"#[derive(Debug, Clone, PartialEq, Eq, Hash)] #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]"#; match self { - Syntax::Rule(r) => format!( - "/// `{}`\n{derive}\npub struct {}({});", - r.syntax, - name.to_pascal_case(), - r.syntax - .tuple_fields(&[name.to_string()].into_iter().collect()) - .map(|f| format!("pub {f}")) - .format(",") - ), - Syntax::Class { cases, .. } => format!( - "{derive}pub enum {} {{ {} }}", - name.to_pascal_case(), - cases - .iter() - .map(|(n, c)| c.rust_ty_decl_child(n, [name.to_string()].into_iter().collect())) - .format(", ") - ), + Syntax::Rule(r) => { + format!( + "/// `{}`\n{derive}\npub struct {}({});", + r.syntax, + name.to_pascal_case(), + r.syntax + .tuple_fields(&[name.to_string()].into_iter().collect()) + .map(|f| format!("pub {f}")) + .format(",") + ) + } + Syntax::Class { cases, .. } => { + format!( + "{derive}pub enum {} {{ {} }}", + name.to_pascal_case(), + cases + .iter() + .map(|(n, c)| { + c.rust_ty_decl_child(n, [name.to_string()].into_iter().collect()) + }) + .format(", ") + ) + } } } + fn rust_display(&self, name: &str) -> String { match self { - Syntax::Rule(r) => format!( - r#" + Syntax::Rule(r) => { + format!( + r#" impl std::fmt::Display for {} {{ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {{ {} }} }} "#, - name.to_pascal_case(), - r.rust_display_impl("self.") - ), - Syntax::Class { cases, .. } => format!( - r#" + name.to_pascal_case(), + r.rust_display_impl("self.") + ) + } + Syntax::Class { cases, .. } => { + format!( + r#" impl std::fmt::Display for {} {{ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {{ match self {{ {} }} }} }} "#, - name.to_pascal_case(), - cases - .iter() - .map(|(n, c)| if c.syntax.fields.is_empty() { - format!( - "Self::{} => {},", - n.to_pascal_case(), - c.rust_display_impl("todo.") - ) - } else { - format!( - "Self::{}({}) => {},", - n.to_pascal_case(), - c.syntax - .fields - .iter() - .enumerate() - .map(|(idx, _)| format!("m{idx}")) - .format(","), - c.rust_display_impl("m") - ) - }) - .format("\n") - ), + name.to_pascal_case(), + cases + .iter() + .map(|(n, c)| { + if c.syntax.fields.is_empty() { + format!( + "Self::{} => {},", + n.to_pascal_case(), + c.rust_display_impl("todo.") + ) + } else { + format!( + "Self::{}({}) => {},", + n.to_pascal_case(), + c.syntax + .fields + .iter() + .enumerate() + .map(|(idx, _)| format!("m{idx}")) + .format(","), + c.rust_display_impl("m") + ) + } + }) + .format("\n") + ) + } } } + fn rust_parse(&self, name: &str) -> String { match self { Syntax::Rule(r) => { @@ -440,6 +461,7 @@ impl Syntax { } } } + fn rust_response(&self, name: &str) -> String { match self { Syntax::Rule(_) | Syntax::Class { response: None, .. } => "".to_string(), @@ -482,12 +504,14 @@ impl Syntax { | Token::Builtin(_) | Token::Reserved(_) | Token::Keyword(_) => todo!(), - Token::Field(_, f) => match f { - Field::One(t) - | Field::Any(t) - | Field::NonZero(t) - | Field::NPlusOne(t) => t.to_string(), - }, + Token::Field(_, f) => { + match f { + Field::One(t) + | Field::Any(t) + | Field::NonZero(t) + | Field::NPlusOne(t) => t.to_string(), + } + } }; format!( "Ok(Some({}::{}({}::parse(response)?)))", @@ -550,7 +574,7 @@ impl Rule { Builtin(s) => s, Reserved(s) => s, Keyword(k) => k, - Field(_, _) => "{}", + Field(..) => "{}", }; acc }), @@ -558,20 +582,23 @@ impl Rule { .fields .iter() .enumerate() - .map(|(idx, f)| match f { - Field::One(_) => { - format!(", {scope}{idx}") - } - Field::Any(_) | Field::NonZero(_) | Field::NPlusOne(_) => { - format!( - r#", {scope}{idx}.iter().format({:?})"#, - self.separator.as_deref().unwrap_or(" ") - ) + .map(|(idx, f)| { + match f { + Field::One(_) => { + format!(", {scope}{idx}") + } + Field::Any(_) | Field::NonZero(_) | Field::NPlusOne(_) => { + format!( + r#", {scope}{idx}.iter().format({:?})"#, + self.separator.as_deref().unwrap_or(" ") + ) + } } }) .format("") ) } + fn rust_ty_decl_child(&self, name: &str, inside_of: HashSet) -> String { if self.syntax.fields.is_empty() { format!("/// `{}`\n{}", self.syntax, name.to_pascal_case()) @@ -584,6 +611,7 @@ impl Rule { ) } } + fn rust_start_of_check(&self) -> String { let is_all_variable = !self.syntax.tokens.iter().any(|t| t.is_concrete()); @@ -610,9 +638,11 @@ impl Rule { .to_string() } } + fn rust_start_of_impl(&self) -> String { self.rust_start_of_check() } + fn rust_parse_impl(&self) -> String { let stmts = self.syntax.tokens.iter().map(rust_parse_token); stmts.format("\n").to_string() @@ -649,19 +679,23 @@ fn rust_parse_token(t: &Token) -> String { Token::Builtin(b) => format!("p.expect_matches(Token::Symbol, {b:?})?;"), Token::Reserved(b) => format!("p.expect_matches(Token::Reserved, {b:?})?;"), Token::Keyword(kw) => format!("p.expect_matches(Token::Keyword, {kw:?})?;"), - Token::Field(idx, f) => match f { - Field::One(t) => format!( - "let m{idx} = <{} as SmtlibParse>::parse(p)?;", - t.to_pascal_case() - ), - Field::Any(t) => format!("let m{idx} = p.any::<{}>()?;", t.to_pascal_case()), - Field::NonZero(t) => { - format!("let m{idx} = p.non_zero::<{}>()?;", t.to_pascal_case()) - } - Field::NPlusOne(t) => { - format!("let m{idx} = p.n_plus_one::<{}>()?;", t.to_pascal_case()) + Token::Field(idx, f) => { + match f { + Field::One(t) => { + format!( + "let m{idx} = <{} as SmtlibParse>::parse(p)?;", + t.to_pascal_case() + ) + } + Field::Any(t) => format!("let m{idx} = p.any::<{}>()?;", t.to_pascal_case()), + Field::NonZero(t) => { + format!("let m{idx} = p.non_zero::<{}>()?;", t.to_pascal_case()) + } + Field::NPlusOne(t) => { + format!("let m{idx} = p.n_plus_one::<{}>()?;", t.to_pascal_case()) + } } - }, + } } } @@ -676,12 +710,14 @@ fn rust_check_token(idx: usize, t: &Token) -> String { Token::Keyword(kw) => { format!("p.nth_matches(offset + {idx}, Token::Keyword, {kw:?})") } - Token::Field(_, f) => match f { - Field::One(t) | Field::NonZero(t) | Field::NPlusOne(t) => { - format!("{}::is_start_of(offset + {idx}, p)", t.to_pascal_case()) + Token::Field(_, f) => { + match f { + Field::One(t) | Field::NonZero(t) | Field::NPlusOne(t) => { + format!("{}::is_start_of(offset + {idx}, p)", t.to_pascal_case()) + } + Field::Any(_) => "todo!(\"{offset:?}, {p:?}\")".to_string(), } - Field::Any(_) => "todo!(\"{offset:?}, {p:?}\")".to_string(), - }, + } } } @@ -690,16 +726,18 @@ impl Grammar { &'a self, inside_of: &'a HashSet, ) -> impl Iterator + 'a { - self.fields.iter().map(|f| match &f { - Field::One(t) => { - if inside_of.contains(t) { - format!("Box<{}>", t.to_pascal_case()) - } else { - t.to_pascal_case() + self.fields.iter().map(|f| { + match &f { + Field::One(t) => { + if inside_of.contains(t) { + format!("Box<{}>", t.to_pascal_case()) + } else { + t.to_pascal_case() + } + } + Field::Any(t) | Field::NonZero(t) | Field::NPlusOne(t) => { + format!("Vec<{}>", t.to_pascal_case()) } - } - Field::Any(t) | Field::NonZero(t) | Field::NPlusOne(t) => { - format!("Vec<{}>", t.to_pascal_case()) } }) } diff --git a/xtask/src/logics.rs b/xtask/src/logics.rs index be85e6a..3f2bb28 100644 --- a/xtask/src/logics.rs +++ b/xtask/src/logics.rs @@ -1,5 +1,4 @@ use color_eyre::Result; - use itertools::Itertools; use quote::{format_ident, quote}; use xshell::Shell; diff --git a/xtask/src/spec.toml b/xtask/src/spec.toml index 5774fde..09a9bde 100644 --- a/xtask/src/spec.toml +++ b/xtask/src/spec.toml @@ -263,6 +263,30 @@ syntax = "( set-option