Repository: pysmt/pysmt
Pull request #215 (2015-11-12 19:45:37)

SMT-LIB: Improved parsing compliance wrt SMT-LIB 2 and 2.5
- Default parser now deals with SMT-LIB 2.5
- SmtLib20Parser can be used for strict SMT-LIB 2.0 compliance
- Improved handling of not implemented commands in parser
- Test and documentation

Some commands are still not supported by the parser.

marcogario: These two commands should fit in our parser (I just had problems figuring out how):

* ```(echo <string>)```
* ```(check-sat-assuming (...))```

However, the following is probably not supported by pySMT:

* ```(define-fun-rec ....)```
* ```(define-funs-rec ....)```
* ```(define-sort ...)```
* ```(declare-sort ...)```

Patch:
diff --git a/pysmt/smtlib/commands.py b/pysmt/smtlib/commands.py
index 022bf61..2fd138e 100644
--- a/pysmt/smtlib/commands.py
+++ b/pysmt/smtlib/commands.py
@@ -17,33 +17,69 @@
 #
 """Defines constants for the commands of the SMT-LIB"""
 
-SET_INFO='set-info'
-RESET_ASSERTIONS='reset-assertions'
-GET_VALUE='get-value'
-SET_OPTION='set-option'
 ASSERT='assert'
 CHECK_SAT='check-sat'
-EXIT='exit'
-SET_LOGIC='set-logic'
-DECLARE_FUN='declare-fun'
+CHECK_SAT_ASSUMING='check-sat-assuming'
 DECLARE_CONST='declare-const'
+DECLARE_FUN='declare-fun'
+DECLARE_SORT='declare-sort'
 DEFINE_FUN='define-fun'
-PUSH='push'
+DEFINE_FUN_REC='define-fun-rec'
+DEFINE_FUNS_REC='define-funs-rec'
+DEFINE_SORT='define-sort'
+ECHO='echo'
+EXIT='exit'
+GET_ASSERTIONS='get-assertions'
+GET_ASSIGNMENT='get-assignment'
+GET_INFO='get-info'
+GET_MODEL='get-model'
+GET_OPTION='get-option'
+GET_PROOF='get-proof'
+GET_UNSAT_ASSUMPTIONS='get-unsat-assumptions'
+GET_UNSAT_CORE='get-unsat-core'
+GET_VALUE='get-value'
 POP='pop'
+PUSH='push'
+RESET='reset'
+RESET_ASSERTIONS='reset-assertions'
+SET_INFO='set-info'
+SET_LOGIC='set-logic'
+SET_OPTION='set-option'
 
+#
 
-ALL_COMMANDS = [
-    SET_INFO,
-    RESET_ASSERTIONS,
-    GET_VALUE,
-    SET_OPTION,
-    ASSERT,
-    CHECK_SAT,
-    EXIT,
+SMT_LIB_2_0 = [
     SET_LOGIC,
+    SET_OPTION,
+    SET_INFO,
+    DECLARE_SORT,
+    DEFINE_SORT,
     DECLARE_FUN,
-    DECLARE_CONST,
     DEFINE_FUN,
     PUSH,
     POP,
+    ASSERT,
+    CHECK_SAT,
+    GET_ASSERTIONS,
+    GET_VALUE,
+    GET_MODEL,
+    GET_PROOF,
+    GET_UNSAT_CORE,
+    GET_INFO,
+    GET_OPTION,
+    EXIT,
 ]
+
+SMT_LIB_2_5 = SMT_LIB_2_0 + [
+    CHECK_SAT_ASSUMING,
+    DECLARE_CONST,
+    DEFINE_FUN_REC,
+    DEFINE_FUNS_REC,
+    ECHO,
+    GET_ASSIGNMENT,
+    GET_UNSAT_ASSUMPTIONS,
+    RESET,
+    RESET_ASSERTIONS,
+]
+
+ALL_COMMANDS = SMT_LIB_2_5
diff --git a/pysmt/smtlib/parser.py b/pysmt/smtlib/parser.py
index 117ab2b..ec27970 100644
--- a/pysmt/smtlib/parser.py
+++ b/pysmt/smtlib/parser.py
@@ -136,7 +136,7 @@ def tokenizer(handle, interactive=False):
     a SMT-Lib2-compliant solver
     """
     spaces = set([" ", "\n", "\t"])
-    separators = set(["(", ")", "|"])
+    separators = set(["(", ")", "|", "\""])
     specials = spaces | separators | set([";", ""])
 
     if not interactive:
@@ -168,9 +168,30 @@ def tokenizer(handle, interactive=False):
                     if not c:
                         raise SyntaxError("Expected '|'")
                     yield ("".join(s))
+                    c = next(reader)
+
+                elif c == "\"":
+                    # String literals
+                    s = []
+                    c = next(reader)
+                    while c:
+                        if c == "\"":
+                            c = next(reader)
+                            if c == "\"":
+                                s.append(c)
+                                c = next(reader)
+                            else:
+                                break
+                        else:
+                            s.append(c)
+                            c = next(reader)
+                    if not c:
+                        raise SyntaxError("Expected '|'")
+                    yield '"%s"' % ("".join(s)) # string literals maintain their quoting
+
                 else:
                     yield c
-                c = next(reader)
+                    c = next(reader)
 
             elif c == ";":
                 while c and c != "\n":
@@ -272,18 +293,35 @@ class SmtLibParser(object):
                             'bvsge':self._operator_adapter(mgr.BVSGE),}
 
         # Command tokens
-        self.commands = {smtcmd.SET_INFO : self._cmd_set_info,
-                         smtcmd.SET_OPTION : self._cmd_set_option,
-                         smtcmd.ASSERT : self._cmd_assert,
+        self.commands = {smtcmd.ASSERT : self._cmd_assert,
                          smtcmd.CHECK_SAT : self._cmd_check_sat,
-                         smtcmd.PUSH : self._cmd_push,
-                         smtcmd.POP : self._cmd_pop,
-                         smtcmd.EXIT : self._cmd_exit,
-                         smtcmd.SET_LOGIC : self._cmd_set_logic,
+                         smtcmd.CHECK_SAT_ASSUMING : self._cmd_check_sat_assuming,
                          smtcmd.DECLARE_CONST : self._cmd_declare_const,
-                         smtcmd.GET_VALUE : self._cmd_get_value,
                          smtcmd.DECLARE_FUN : self._cmd_declare_fun,
-                         smtcmd.DEFINE_FUN : self._cmd_define_fun,}
+                         smtcmd.DECLARE_SORT: self._cmd_declare_sort,
+                         smtcmd.DEFINE_FUN : self._cmd_define_fun,
+                         smtcmd.DEFINE_FUNS_REC : self._cmd_define_funs_rec,
+                         smtcmd.DEFINE_FUN_REC : self._cmd_define_fun_rec,
+                         smtcmd.DEFINE_SORT: self._cmd_define_sort,
+                         smtcmd.ECHO : self._cmd_echo,
+                         smtcmd.EXIT : self._cmd_exit,
+                         smtcmd.GET_ASSERTIONS: self._cmd_get_assertions,
+                         smtcmd.GET_ASSIGNMENT : self._cmd_get_assignment,
+                         smtcmd.GET_INFO: self._cmd_get_info,
+                         smtcmd.GET_MODEL: self._cmd_get_model,
+                         smtcmd.GET_OPTION: self._cmd_get_option,
+                         smtcmd.GET_PROOF: self._cmd_get_proof,
+                         smtcmd.GET_UNSAT_ASSUMPTIONS : self._cmd_get_unsat_assumptions,
+                         smtcmd.GET_UNSAT_CORE: self._cmd_get_unsat_core,
+                         smtcmd.GET_VALUE : self._cmd_get_value,
+                         smtcmd.POP : self._cmd_pop,
+                         smtcmd.PUSH : self._cmd_push,
+                         smtcmd.RESET : self._cmd_reset,
+                         smtcmd.RESET_ASSERTIONS : self._cmd_reset_assertions,
+                         smtcmd.SET_LOGIC : self._cmd_set_logic,
+                         smtcmd.SET_OPTION : self._cmd_set_option,
+                         smtcmd.SET_INFO : self._cmd_set_info,
+                     }
 
     def _reset(self):
         """Resets the parser to the initial state"""
@@ -763,12 +801,10 @@ class SmtLibParser(object):
             raise SyntaxError("Unexpected token '%s' in %s command. " \
                               "Expected ')'" % (p, command))
 
-
     def _function_call_helper(self, v, *args):
         """ Helper function for dealing with function calls """
         return self.env.formula_manager.Function(v, args)
 
-
     def get_assignment_list(self, script):
         """
         Parse an assignment list produced by get-model and get-value
@@ -791,10 +827,8 @@ class SmtLibParser(object):
         self.cache.unbind_all(symbols)
         return res
 
-
     def get_command(self, tokens):
         """Builds an SmtLibCommand instance out of a parsed term."""
-
         while True:
             self.consume_opening(tokens, "<main>")
             current = next(tokens)
@@ -804,46 +838,54 @@ class SmtLibParser(object):
             else:
                 raise UnknownSmtLibCommandError(current)
 
+    def _cmd_not_implemented(self, current, tokens):
+        raise NotImplementedError("'%s' has not been implemented yet" % current)
+
     def _cmd_set_info(self, current, tokens):
+        """(set-info <attribute>)"""
         elements = self.parse_atoms(tokens, current, 2)
         return SmtLibCommand(current, elements)
 
     def _cmd_set_option(self, current, tokens):
+        """(set-option <option>)"""
         elements = self.parse_atoms(tokens, current, 2)
         return SmtLibCommand(current, elements)
 
     def _cmd_assert(self, current, tokens):
+        """(assert <term>)"""
         expr = self.get_expression(tokens)
         self.consume_closing(tokens, current)
         return SmtLibCommand(current, [expr])
 
     def _cmd_check_sat(self, current, tokens):
+        """(check-sat)"""
         self.parse_atoms(tokens, current, 0)
         return SmtLibCommand(current, [])
 
     def _cmd_push(self, current, tokens):
+        """(push <numeral>)"""
         elements = self.parse_atoms(tokens, current, 0, 1)
-
         levels = 1
         if len(elements) > 0:
             levels = int(elements[0])
         return SmtLibCommand(current, [levels])
 
     def _cmd_pop(self, current, tokens):
+        """(pop <numeral>)"""
         elements = self.parse_atoms(tokens, current, 0, 1)
-
         levels = 1
         if len(elements) > 0:
             levels = int(elements[0])
         return SmtLibCommand(current, [levels])
 
     def _cmd_exit(self, current, tokens):
+        """(exit)"""
         self.parse_atoms(tokens, current, 0)
         return SmtLibCommand(current, [])
 
     def _cmd_set_logic(self, current, tokens):
+        """(set-logic <symbol>)"""
         elements = self.parse_atoms(tokens, current, 1)
-
         name = elements[0]
         try:
             self.logic = get_logic_by_name(name)
@@ -854,6 +896,7 @@ class SmtLibParser(object):
             return SmtLibCommand(current, [None])
 
     def _cmd_declare_const(self, current, tokens):
+        """(declare-const <symbol> <sort>)"""
         elements = self.parse_atoms(tokens, current, 2)
         (var, typename) = elements
         v = self._get_var(var, typename)
@@ -861,11 +904,13 @@ class SmtLibParser(object):
         return SmtLibCommand(current, [v])
 
     def _cmd_get_value(self, current, tokens):
+        """(get-value (<term>+)"""
         params = self.parse_expr_list(tokens, current)
         self.consume_closing(tokens, current)
         return SmtLibCommand(current, params)
 
     def _cmd_declare_fun(self, current, tokens):
+        """(declare-fun <symbol> (<sort>*) <sort>)"""
         var = self.parse_atom(tokens, current)
         params = self.parse_params(tokens, current)
         typename = self.parse_type(tokens, current)
@@ -880,6 +925,7 @@ class SmtLibParser(object):
         return SmtLibCommand(current, [v])
 
     def _cmd_define_fun(self, current, tokens):
+        """(define-fun <fun_def>)"""
         formal = []
         var = self.parse_atom(tokens, current)
         namedparams = self.parse_named_params(tokens, current)
@@ -899,6 +945,101 @@ class SmtLibParser(object):
         self.cache.define(var, formal, ebody)
         return SmtLibCommand(current, [var, formal, rtype, ebody])
 
+    def _cmd_declare_sort(self, current, tokens):
+        """(declare-sort <symbol> <numeral>)"""
+        return self._cmd_not_implemented(current, tokens)
+
+    def _cmd_define_sort(self, current, tokens):
+        """(define-sort <fun_def>)"""
+        return self._cmd_not_implemented(current, tokens)
+
+    def _cmd_get_assertions(self, current, tokens):
+        """(get_assertions)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_get_info(self, current, tokens):
+        """(get-info <info_flag>)"""
+        keyword = self.parse_atoms(tokens, current, 1)
+        return SmtLibCommand(current, keyword)
+
+    def _cmd_get_model(self, current, tokens):
+        """(get-model)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_get_option(self, current, tokens):
+        """(get-option <keyword>)"""
+        keyword = self.parse_atoms(tokens, current, 1)
+        return SmtLibCommand(current, keyword)
+
+    def _cmd_get_proof(self, current, tokens):
+        """(get-proof)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_get_unsat_core(self, current, tokens):
+        """(get-unsat-core)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_check_sat_assuming(self, current, tokens):
+        """(check-sat-assuming (<prop_literal>*) ) """
+        params = self.parse_expr_list(tokens, current)
+        self.consume_closing(tokens, current)
+        return SmtLibCommand(current, params)
+
+    def _cmd_define_fun_rec(self, current, tokens):
+        """(define-fun-rec <fun_def>)"""
+        return self._cmd_not_implemented(current, tokens)
+
+    def _cmd_define_funs_rec(self, current, tokens):
+        """(define-funs-rec (<fun_dec>^{n+1}) (<term>^{n+1>))"""
+        return self._cmd_not_implemented(current, tokens)
+
+    def _cmd_echo(self, current, tokens):
+        """(echo <string>)"""
+        elements = self.parse_atoms(tokens, current, 1)
+        return SmtLibCommand(current, elements)
+
+    def _cmd_get_assignment(self, current, tokens):
+        """(get-assignment)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_get_unsat_assumptions(self, current, tokens):
+        """(get-unsat-assumptions)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_reset(self, current, tokens):
+        """(reset)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+    def _cmd_reset_assertions(self, current, tokens):
+        """(reset-assertions)"""
+        self.parse_atoms(tokens, current, 0)
+        return SmtLibCommand(current, [])
+
+
+class SmtLib20Parser(SmtLibParser):
+    """Parser for SMT-LIB 2.0."""
+
+    def __init__(self, environment=None, interactive=False):
+        SmtLibParser.__init__(self, environment, interactive)
+
+        # Remove commands that were introduced in SMT-LIB 2.5
+        del self.commands["check-sat-assuming"]
+        del self.commands["declare-const"]
+        del self.commands["define-fun-rec"]
+        del self.commands["define-funs-rec"]
+        del self.commands["echo"]
+        del self.commands["get-assignment"]
+        del self.commands["get-unsat-assumptions"]
+        del self.commands["reset"]
+        del self.commands["reset-assertions"]
+
 
 if __name__ == "__main__":
     import sys
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index 0e46984..c4aed98 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -110,13 +110,19 @@ class SmtLibCommand(namedtuple('SmtLibCommand', ['name', 'args'])):
         elif self.name in [smtcmd.PUSH, smtcmd.POP]:
             outstream.write("(%s %d)" % (self.name, self.args[0]))
 
+        elif self.name in smtcmd.ALL_COMMANDS:
+            raise NotImplementedError("'%s' is a valid SMT-LIB command "\
+                                      "but it is currently not supported. "\
+                                      "Please open a bug-report." % self.name)
+        else:
+            raise UnknownSmtLibCommandError(self.name)
+
     def serialize_to_string(self):
         buf = cStringIO()
         self.serialize(buf)
         return buf.getvalue()
 
 
-
 class SmtLibScript(object):
 
     def __init__(self):
@@ -275,5 +281,16 @@ def evaluate_command(cmd, solver):
         (var, formals, typename, body) = cmd.args
         return solver.define_fun(var, formals, typename, body)
 
+    elif cmd.name == smtcmd.ECHO:
+        print(cmd.args[0])
+        return None
+
+    elif cmd.name == smtcmd.CHECK_SAT_ASSUMING:
+        return solver.check_sat(cmd.args)
+
+    elif cmd.name in smtcmd.ALL_COMMANDS:
+        raise NotImplementedError("'%s' is a valid SMT-LIB command "\
+                                  "but it is currently not supported. "\
+                                  "Please open a bug-report." % cmd.name)
     else:
         raise UnknownSmtLibCommandError(cmd.name)


Test patch:
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index 7d2cd36..023e8b6 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -23,7 +23,7 @@ from pysmt.typing import REAL
 from pysmt.test import TestCase, main
 from pysmt.smtlib.script import SmtLibScript, SmtLibCommand
 from pysmt.smtlib.script import smtlibscript_from_formula, evaluate_command
-from pysmt.smtlib.parser import get_formula_strict, get_formula
+from pysmt.smtlib.parser import get_formula_strict, get_formula, SmtLibParser
 from pysmt.solvers.smtlib import SmtLibIgnoreMixin
 
 class TestSmtLibScript(TestCase):
@@ -126,6 +126,60 @@ class TestSmtLibScript(TestCase):
                          solver=mock)
 
 
+    def test_all_parsing(self):
+        # Create a small file that tests all commands of smt-lib 2
+        parser = SmtLibParser()
+
+        nie = 0
+        for cmd in DEMO_SMTSCRIPT:
+            try:
+                next(parser.get_command_generator(cStringIO(cmd)))
+            except NotImplementedError:
+                nie += 1
+        # There are currently 6 not-implemented commands
+        self.assertEquals(nie, 6)
+
+DEMO_SMTSCRIPT = [ "(declare-fun a () Bool)",
+                   "(declare-fun b () Bool)",
+                   "(declare-fun c () Bool)",
+                   "(assert true)",
+                   "(assert (not a))",
+                   "(check-sat)",
+                   "(check-sat-assuming (a b c))",
+                   "(check-sat-assuming ((not a) b (not c)))",
+                   "(declare-const d Bool)",
+                   "(declare-fun xyz (A B) C)", # Shouldn't this raise an error?
+                   "(declare-fun abc () Int)",
+                   "(declare-sort A 0)",
+                   "(define-fun f ((a Bool)) B a)",
+                   "(define-fun g ((a Bool)) B (f a))",
+                   "(define-fun-rec f ((a A)) B a)",
+                   "(define-fun-rec g ((a A)) B (g a))",
+                   """(define-funs-rec ((h ((a A)) B) (i ((a A)) B) )
+                                       ( (i a) (h a))
+                   )
+                   """,
+                   "(define-sort A () B)",
+                   "(define-sort A (B C) (Array B C))",
+                   "(echo \"hello world\")",
+                   "(exit)",
+                   "(get-assertions)",
+                   "(get-assignment)",
+                   "(get-info :name)",
+                   "(get-model)",
+                   "(get-option :keyword)",
+                   "(get-proof)",
+                   "(get-unsat-assumptions)",
+                   "(get-unsat-core)",
+                   "(get-value (x y z))",
+                   "(pop 42)",
+                   "(push 42)",
+                   "(reset)",
+                   "(reset-assertions)",
+                   "(set-info :number 42)",
+                   "(set-logic QF_LIA)",
+                   "(set-option :produce-models true)",
+               ]
 
 if __name__ == "__main__":
     main()