Add support for check-sat-assuming command

vinisilvag · Oct 23, 2023 · eab2dae · eab2dae
1 parent 6dcecc1
commit eab2dae
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/carcara/src/parser/lexer.rs b/carcara/src/parser/lexer.rs
@@ -102,6 +102,9 @@ pub enum Reserved {
     /// The `assert` reserved word.
     Assert,
 
+    /// The `check-sat-assuming` reserved word.
+    CheckSatAssuming,
+
     /// The `set-logic` reserved word.
     SetLogic,
 }
@@ -125,6 +128,7 @@ impl_str_conversion_traits!(Reserved {
     DeclareSort: "declare-sort",
     DefineFun: "define-fun",
     Assert: "assert",
+    CheckSatAssuming: "check-sat-assuming",
     SetLogic: "set-logic",
 });
 

diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs
@@ -551,6 +551,12 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     self.expect_token(Token::CloseParen)?;
                     self.premises().insert(term);
                 }
+                Token::ReservedWord(Reserved::CheckSatAssuming) => {
+                    self.expect_token(Token::OpenParen)?;
+                    let terms = self.parse_sequence(Self::parse_term, true)?;
+                    self.expect_token(Token::CloseParen)?;
+                    self.premises().extend(terms);
+                }
                 Token::ReservedWord(Reserved::SetLogic) => {
                     let logic = self.expect_symbol()?;
                     self.expect_token(Token::CloseParen)?;