From 17b8754d78c79ecec2a8bbe05143520c62c69b72 Mon Sep 17 00:00:00 2001 From: Bruno Andreotti Date: Wed, 16 Oct 2024 18:05:41 -0300 Subject: [PATCH] Properly handle all SMT-LIB commands --- carcara/src/parser/error.rs | 18 ++++++++- carcara/src/parser/mod.rs | 79 +++++++++++++++++++++++++++++++++---- 2 files changed, 88 insertions(+), 9 deletions(-) diff --git a/carcara/src/parser/error.rs b/carcara/src/parser/error.rs index 7ba293d8..a1587e6a 100644 --- a/carcara/src/parser/error.rs +++ b/carcara/src/parser/error.rs @@ -2,7 +2,7 @@ use crate::{ ast::{Constant, PrimitivePool, Rc, Sort, Term, TermPool}, - parser::Token, + parser::{Command, Token}, utils::Range, }; use rug::Integer; @@ -144,6 +144,22 @@ pub enum ParserError { /// The parser encountered an unknown qualified operator. #[error("not a valid qualified operator: '{0}'")] InvalidQualifiedOp(String), + + /// The parser encountered a command that is not supported by Carcara. + #[error("unsupported command: '{0}'")] + UnsupportedCommand(Command), + + /// There is more than one instance of a command that can only appear once. + #[error("the '{0}' command cannot appear more than once")] + CommandAppearsMoreThanOnce(Command), + + /// The parser encountered a proof-only command when parsing the problem. + #[error("found proof-only command '{0}' when parsing problem")] + ProofCommandInProblem(Command), + + /// The parser encountered a problem-only command when parsing the proof. + #[error("found problem-only command '{0}' when parsing proof")] + ProblemCommandInProof(Command), } /// Returns an error if the length of `sequence` is not in the `expected` range. diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs index a3f74e8a..65616b1c 100644 --- a/carcara/src/parser/mod.rs +++ b/carcara/src/parser/mod.rs @@ -670,8 +670,13 @@ impl<'a, R: BufRead> Parser<'a, R> { pub fn parse_problem(&mut self) -> CarcaraResult { self.problem = Some(Problem::new()); + // Some commands can only appear once in an SMT problem + let [mut seen_check_sat, mut seen_exit, mut seen_get_proof, mut seen_set_logic] = + [false; 4]; + while self.current_token != Token::Eof { self.expect_token(Token::OpenParen)?; + let pos = self.current_position; let command = self.expect_command()?; match command { Command::DeclareFun => { @@ -733,13 +738,17 @@ impl<'a, R: BufRead> Parser<'a, R> { self.expect_token(Token::CloseParen)?; self.premises().insert(term); } - Command::CheckSatAssuming => { + Command::CheckSatAssuming if !seen_check_sat => { + seen_check_sat = true; + self.expect_token(Token::OpenParen)?; let terms = self.parse_sequence(Self::parse_term, true)?; self.expect_token(Token::CloseParen)?; self.premises().extend(terms); } - Command::SetLogic => { + Command::SetLogic if !seen_set_logic => { + seen_set_logic = true; + let logic = self.expect_symbol()?; self.expect_token(Token::CloseParen)?; self.prelude().logic = Some(logic.clone()); @@ -752,12 +761,65 @@ impl<'a, R: BufRead> Parser<'a, R> { (logic.contains("LRA") || logic.contains("NRA") || logic.contains("RDL")) && !logic.contains('I'); } - // TODO: properly handle all commands - _ => { - // If the command is not one of the commands we care about, we just ignore it. - // We do that by reading tokens until the command parenthesis is closed + Command::CheckSat if !seen_check_sat => { + seen_check_sat = true; + self.expect_token(Token::CloseParen)?; + } + Command::Exit if !seen_exit => { + seen_exit = true; + self.expect_token(Token::CloseParen)?; + } + Command::GetProof if !seen_get_proof => { + seen_get_proof = true; + self.expect_token(Token::CloseParen)?; + } + + // We only have support for problems that include at most one of these commands. If + // they appear again, we must return an error + Command::CheckSat + | Command::CheckSatAssuming + | Command::Exit + | Command::GetProof + | Command::SetLogic => { + return Err(Error::Parser( + ParserError::CommandAppearsMoreThanOnce(command), + pos, + )); + } + + // We can safely ignore these commands, since they do not change the problem state + Command::Echo + | Command::GetAssertions + | Command::GetAssignment + | Command::GetInfo + | Command::GetModel + | Command::GetOption + | Command::GetUnsatAssumptions + | Command::GetUnsatCore + | Command::GetValue + | Command::SetInfo + | Command::SetOption => { self.ignore_until_close_parens()?; } + + // These commands are not supported by Carcara, and we must reject any problem that + // contains them + Command::DeclareDatatype + | Command::DeclareDatatypes + | Command::Pop + | Command::Push + | Command::Reset + | Command::ResetAssertions => { + return Err(Error::Parser(ParserError::UnsupportedCommand(command), pos)); + } + + // These commands are only allowed when parsing the proof, not the problem + Command::Assume | Command::Step | Command::Anchor => { + return Err(Error::Parser( + ParserError::ProofCommandInProblem(command), + pos, + )); + } } } Ok(self.problem.take().unwrap()) @@ -831,10 +893,11 @@ impl<'a, R: BufRead> Parser<'a, R> { next_subproof_context_id += 1; continue; } - // TODO: properly handle all commands + + // All other commands can only appear in the problem, not the proof _ => { return Err(Error::Parser( - ParserError::UnexpectedToken(Token::Command(command)), + ParserError::ProblemCommandInProof(command), position, )); }