WIP: Support parsing theories

smt2parser/src/concrete.rs

@@ -7,7 +7,7 @@ use crate::{
     lexer,
     visitors::{
         CommandVisitor, ConstantVisitor, KeywordVisitor, QualIdentifierVisitor, SExprVisitor,
-        Smt2Visitor, SortVisitor, SymbolKind, SymbolVisitor, TermVisitor,
+        Smt2Visitor, SortVisitor, SymbolKind, SymbolVisitor, TermVisitor, TheoryVisitor,
     },
     Binary, Decimal, Hexadecimal, Numeral, Position,
 };
@@ -196,6 +196,10 @@ pub enum Command<
     },
 }
 
+pub struct Theory<Symbol = self::Symbol> {
+    name: Symbol,
+}
+
 /// An implementation of [`Smt2Visitor`] that returns concrete syntax values.
 #[derive(Default, Debug, Eq, PartialEq, Clone, Hash, Serialize, Deserialize)]
 pub struct SyntaxBuilder;
@@ -1045,6 +1049,15 @@ impl Command {
     }
 }
 
+impl TheoryVisitor<Symbol> for SyntaxBuilder {
+    type E = Error;
+    type T = Theory;
+
+    fn visit_theory(&mut self, name: Symbol) -> Result<Self::T, Self::E> {
+        Ok(Theory { name })
+    }
+}
+
 impl Smt2Visitor for SyntaxBuilder {
     type Error = Error;
     type Constant = Constant;
@@ -1055,6 +1068,7 @@ impl Smt2Visitor for SyntaxBuilder {
     type Symbol = Symbol;
     type Term = Term;
     type Command = Command;
+    type Theory = Theory;
 
     fn syntax_error(&mut self, position: crate::Position, s: String) -> Self::Error {
         Error::SyntaxError(position, s)

smt2parser/src/lexer.rs

@@ -79,6 +79,7 @@ const KEYWORDS: &[(&str, Token)] = {
         ("set-info", SetInfo),
         ("set-logic", SetLogic),
         ("set-option", SetOption),
+        ("theory", Theory),
     ]
 };
 

smt2parser/src/lib.rs

@@ -53,6 +53,7 @@ pub type Binary = Vec<bool>;
 pub use concrete::Error;
 /// A position in the input.
 pub use lexer::Position;
+use parser::ParseResult;
 
 /// Parse the input data and return a stream of interpreted SMT2 commands
 pub struct CommandStream<R, T>
@@ -121,7 +122,8 @@ where
             }
             if unmatched_paren == 0 {
                 return match parser.end_of_input() {
-                    Ok((command, _)) => Some(Ok(command)),
+                    Ok((ParseResult::Command(command), _)) => Some(Ok(command)),
+                    Ok((ParseResult::Theory(res), _)) => unimplemented!(),
                     Err(err) => Some(Err(err)),
                 };
             }

smt2parser/src/parser.rs

@@ -10,7 +10,7 @@ pub use internal::{Parser, Token};
 
 pomelo! {
     %module internal;
-    %include { use crate::visitors; }
+    %include { use crate::visitors; use crate::parser::ParseResult; }
 
     %stack_size 0;
 
@@ -34,6 +34,10 @@ pomelo! {
 
     %type command T::Command;
 
+    %type theory T::Theory;
+
+    %type mode ParseResult<T::Command, T::Theory>;
+
     %type term T::Term;
     %type terms Vec<T::Term>;
 
@@ -89,7 +93,7 @@ pomelo! {
     %type sort_dec (T::Symbol, crate::Numeral);
     %type sort_decs Vec<(T::Symbol, crate::Numeral)>;
 
-    %start_symbol command;
+    %start_symbol mode;
 
     bound_symbol ::= Symbol(s) { extra.0.visit_bound_symbol(s)? }
     fresh_symbol ::= Symbol(s) { extra.0.visit_fresh_symbol(s, crate::visitors::SymbolKind::Unknown)? }
@@ -355,6 +359,18 @@ pomelo! {
     command ::= LeftParen SetLogic bound_symbol(x) RightParen { extra.0.visit_set_logic(x)? }
     //   ( set-option ⟨attribute⟩ )
     command ::= LeftParen SetOption keyword(k) attribute_value(v) RightParen { extra.0.visit_set_option(k, v)? }
+
+
+    //   ( theory ⟨symbol⟩ ⟨theory_attributes⟩+ )
+    theory ::= LeftParen Theory fresh_symbol(s) RightParen { extra.0.visit_theory(s)? }
+
+    mode ::= command(c) { ParseResult::Command(c) }
+    mode ::= theory(td) { ParseResult::Theory(td) }
+}
+
+pub enum ParseResult<C, T> {
+    Command(C),
+    Theory(T),
 }
 
 #[cfg(test)]
@@ -369,7 +385,10 @@ pub(crate) mod tests {
         for token in tokens.into_iter() {
             p.parse(token)?;
         }
-        Ok(p.end_of_input()?.0)
+        match p.end_of_input()?.0 {
+            ParseResult::Command(c) => Ok(c),
+            ParseResult::Theory(t) => panic!("Expected command"),
+        }
     }
 
     #[test]

smt2parser/src/rewriter.rs

@@ -9,7 +9,7 @@ use crate::{
     visitors::{
         AttributeValue, CommandVisitor, ConstantVisitor, DatatypeDec, FunctionDec, Identifier,
         KeywordVisitor, QualIdentifierVisitor, SExprVisitor, Smt2Visitor, SortVisitor, SymbolKind,
-        SymbolVisitor, TermVisitor,
+        SymbolVisitor, TermVisitor, TheoryVisitor,
     },
     Binary, Decimal, Hexadecimal, Numeral, Position,
 };
@@ -720,6 +720,19 @@ where
     }
 }
 
+impl<R, V> TheoryVisitor<V::Symbol> for R
+where
+    R: Rewriter<V = V>,
+    V: Smt2Visitor,
+{
+    type T = V::Theory;
+    type E = R::Error;
+
+    fn visit_theory(&mut self, name: V::Symbol) -> Result<Self::T, Self::E> {
+        self.visit_theory(name)
+    }
+}
+
 impl<R, V> CommandVisitor<V::Term, V::Symbol, V::Sort, V::Keyword, V::Constant, V::SExpr> for R
 where
     R: Rewriter<V = V>,
@@ -910,6 +923,7 @@ where
     type Symbol = V::Symbol;
     type Term = V::Term;
     type Command = V::Command;
+    type Theory = V::Theory;
 
     fn syntax_error(&mut self, pos: Position, s: String) -> Self::Error {
         self.visitor().syntax_error(pos, s).into()

smt2parser/src/stats.rs

@@ -7,7 +7,7 @@ use crate::{
     concrete::Error,
     visitors::{
         CommandVisitor, ConstantVisitor, KeywordVisitor, QualIdentifierVisitor, SExprVisitor,
-        Smt2Visitor, SortVisitor, SymbolKind, SymbolVisitor, TermVisitor,
+        Smt2Visitor, SortVisitor, SymbolKind, SymbolVisitor, TermVisitor, TheoryVisitor,
     },
     Binary, Decimal, Hexadecimal, Numeral, Position,
 };
@@ -553,6 +553,15 @@ impl CommandVisitor<Term, Symbol, Sort, Keyword, Constant, SExpr> for Smt2Counte
     }
 }
 
+impl TheoryVisitor<Symbol> for Smt2Counters {
+    type E = Error;
+    type T = ();
+
+    fn visit_theory(&mut self, _name: Symbol) -> Result<(), Self::E> {
+        Ok(())
+    }
+}
+
 impl Smt2Visitor for Smt2Counters {
     type Error = Error;
     type Constant = ();
@@ -563,6 +572,7 @@ impl Smt2Visitor for Smt2Counters {
     type Symbol = ();
     type Term = Term;
     type Command = ();
+    type Theory = ();
 
     fn syntax_error(&mut self, position: Position, s: String) -> Self::Error {
         Error::SyntaxError(position, s)

smt2parser/src/visitors.rs

@@ -482,6 +482,10 @@ pub trait Smt2Visitor:
         <Self as Smt2Visitor>::SExpr,
         T = <Self as Smt2Visitor>::Command,
         E = <Self as Smt2Visitor>::Error,
+    > + TheoryVisitor<
+        <Self as Smt2Visitor>::Symbol,
+        T = <Self as Smt2Visitor>::Theory,
+        E = <Self as Smt2Visitor>::Error,
     >
 {
     type Error;
@@ -493,11 +497,20 @@ pub trait Smt2Visitor:
     type Symbol;
     type Term;
     type Command;
+    type Theory;
 
     fn syntax_error(&mut self, position: crate::Position, s: String) -> Self::Error;
     fn parsing_error(&mut self, position: crate::Position, s: String) -> Self::Error;
 }
 
+/// A visitor for the entire SMT2 syntax.
+pub trait TheoryVisitor<Symbol> {
+    type E;
+    type T;
+
+    fn visit_theory(&mut self, name: Symbol) -> Result<Self::T, Self::E>;
+}
+
 impl<Symbol> std::fmt::Display for Index<Symbol>
 where
     Symbol: std::fmt::Display,