Merge pull request #376 from pysmt/smtlibparser_testing

Use Fuzzer for testing of SMTLIB Parser

pysmt/formula.py

@@ -486,7 +486,7 @@ def AllDifferent(self, *args):
         res = []
         for i, a in enumerate(exprs):
             for b in exprs[i+1:]:
-                res.append(self.Not(self.Equals(a, b)))
+                res.append(self.Not(self.EqualsOrIff(a, b)))
         return self.And(res)
 
     def Xor(self, left, right):

pysmt/smtlib/parser.py

@@ -26,7 +26,7 @@
 from pysmt.environment import get_env
 from pysmt.typing import BOOL, REAL, INT, FunctionType, BVType, ArrayType
 from pysmt.logics import get_logic_by_name, UndefinedLogicError
-from pysmt.exceptions import UnknownSmtLibCommandError, PysmtSyntaxError
+from pysmt.exceptions import UnknownSmtLibCommandError, PysmtSyntaxError, PysmtTypeError
 from pysmt.smtlib.script import SmtLibCommand, SmtLibScript
 from pysmt.smtlib.annotations import Annotations
 from pysmt.utils import interactive_char_iterator
@@ -285,32 +285,70 @@ def __init__(self, environment=None, interactive=False):
         self.logic = None
         self._reset()
 
+        mgr = self.env.formula_manager
+
+        # Fixing the issue with integer/real numbers on arithmetic
+        # operators.
+        #
+        # We try to apply the operator as it is, in case of failure,
+        # we try to interpret as reals the constant operands that are
+        # integers
+        def fix_real(op, *args):
+            try:
+                return op(*args)
+            except PysmtTypeError:
+                get_type = self.env.stc.get_type
+                get_free_variables = self.env.fvo.get_free_variables
+                new_args = []
+                for x in args:
+                    if get_type(x).is_int_type() and\
+                       len(get_free_variables(x)) == 0:
+                        new_args.append(mgr.ToReal(x))
+                    else:
+                        new_args.append(x)
+                if args == new_args:
+                    raise
+                return op(*new_args)
+
+        self.LT = functools.partial(fix_real, mgr.LT)
+        self.GT = functools.partial(fix_real, mgr.GT)
+        self.LE = functools.partial(fix_real, mgr.LE)
+        self.GE = functools.partial(fix_real, mgr.GE)
+        self.Equals = functools.partial(fix_real, mgr.Equals)
+        self.EqualsOrIff = functools.partial(fix_real, mgr.EqualsOrIff)
+        self.Plus = functools.partial(fix_real, mgr.Plus)
+        self.Minus = functools.partial(fix_real, mgr.Minus)
+        self.Times = functools.partial(fix_real, mgr.Times)
+        self.Div = functools.partial(fix_real, mgr.Div)
+        self.Ite = functools.partial(fix_real, mgr.Ite)
+        self.AllDifferent = functools.partial(fix_real, mgr.AllDifferent)
+
         # Tokens representing interpreted functions appearing in expressions
         # Each token is handled by a dedicated function that takes the
         # recursion stack, the token stream and the parsed token
         # Common tokens are handled in the _reset function
-        mgr = self.env.formula_manager
         self.interpreted = {"let" : self._enter_let,
                             "!" : self._enter_annotation,
                             "exists" : self._enter_quantifier,
                             "forall" : self._enter_quantifier,
-                            '+':self._operator_adapter(mgr.Plus),
+                            '+':self._operator_adapter(self.Plus),
                             '-':self._operator_adapter(self._minus_or_uminus),
-                            '*':self._operator_adapter(mgr.Times),
+                            '*':self._operator_adapter(self.Times),
                             '/':self._operator_adapter(self._division),
                             'pow':self._operator_adapter(mgr.Pow),
-                            '>':self._operator_adapter(mgr.GT),
-                            '<':self._operator_adapter(mgr.LT),
-                            '>=':self._operator_adapter(mgr.GE),
-                            '<=':self._operator_adapter(mgr.LE),
+                            '>':self._operator_adapter(self.GT),
+                            '<':self._operator_adapter(self.LT),
+                            '>=':self._operator_adapter(self.GE),
+                            '<=':self._operator_adapter(self.LE),
                             '=':self._operator_adapter(self._equals_or_iff),
                             'not':self._operator_adapter(mgr.Not),
                             'and':self._operator_adapter(mgr.And),
                             'or':self._operator_adapter(mgr.Or),
                             'xor':self._operator_adapter(mgr.Xor),
                             '=>':self._operator_adapter(mgr.Implies),
                             '<->':self._operator_adapter(mgr.Iff),
-                            'ite':self._operator_adapter(mgr.Ite),
+                            'ite':self._operator_adapter(self.Ite),
+                            'distinct':self._operator_adapter(self.AllDifferent),
                             'to_real':self._operator_adapter(mgr.ToReal),
                             'concat':self._operator_adapter(mgr.BVConcat),
                             'bvnot':self._operator_adapter(mgr.BVNot),
@@ -404,7 +442,7 @@ def _minus_or_uminus(self, *args):
             return mgr.Times(mult, args[0])
         else:
             assert len(args) == 2
-            return mgr.Minus(args[0], args[1])
+            return self.Minus(args[0], args[1])
 
     def _enter_smtlib_as(self, stack, tokens, key):
         """Utility function that handles 'as' that is a special function in SMTLIB"""
@@ -497,11 +535,7 @@ def _smtlib_underscore(self, stack, tokens, key):
         else:
             raise PysmtSyntaxError("Unexpected '_' expression '%s'" % op)
 
-        # Consume the closed parenthesis of the (_ ...) term and add the
-        # resulting function to the correct level in the stack
-        self.consume_closing(tokens, "expression")
-        stack.pop()
-        stack[-1].append(fun)
+        stack[-1].append(lambda : fun)
 
     def _equals_or_iff(self, left, right):
         """Utility function that treats = between booleans as <->"""
@@ -510,15 +544,15 @@ def _equals_or_iff(self, left, right):
         if lty == BOOL:
             return mgr.Iff(left, right)
         else:
-            return mgr.Equals(left, right)
+            return self.Equals(left, right)
 
     def _division(self, left, right):
         """Utility function that builds a division"""
         mgr = self.env.formula_manager
         if left.is_constant() and right.is_constant():
             return mgr.Real(Fraction(left.constant_value()) / \
                             Fraction(right.constant_value()))
-        return mgr.Div(left, right)
+        return self.Div(left, right)
 
     def _get_basic_type(self, type_name, params=None):
         """

pysmt/test/smtlib/fuzzed/NOTICE

@@ -0,0 +1,5 @@
+These files were generated using FuzzSMT by JKU, with the patch by the
+patch by Christoph Wintersteiger.
+
+See: Robert Brummayer and Armin Biere.
+     Fuzzing and Delta-Debugging SMT Solvers

pysmt/test/smtlib/test_fuzzed.py

@@ -0,0 +1,72 @@
+#
+# This file is part of pySMT.
+#
+#   Copyright 2014 Andrea Micheli and Marco Gario
+#
+#   Licensed under the Apache License, Version 2.0 (the "License");
+#   you may not use this file except in compliance with the License.
+#   You may obtain a copy of the License at
+#
+#       http://www.apache.org/licenses/LICENSE-2.0
+#
+#   Unless required by applicable law or agreed to in writing, software
+#   distributed under the License is distributed on an "AS IS" BASIS,
+#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#   See the License for the specific language governing permissions and
+#   limitations under the License.
+#
+import os
+
+from pysmt.shortcuts import reset_env
+from pysmt.test import TestCase
+from pysmt.smtlib.parser import SmtLibParser
+
+
+class TestSmtLibParserFuzzer(TestCase):
+
+    def test_fuzzed(self):
+        failed = []
+        for fname in FUZZED_FILES:
+            try:
+                self.parse(os.path.join(SMTLIB_DIR, fname))
+            except NotImplementedError as ex:
+                print("Ignoring not implemented SMT command error: %s"\
+                      % str(ex))
+            except Exception as ex:
+                failed.append((fname, ex))
+        if len(failed) != 0:
+            for fname, ex in failed:
+                print(fname, ex)
+                print("-"*50)
+        self.assertTrue(len(failed) == 0,
+                        "%d/%d" %(len(failed), len(FUZZED_FILES)))
+
+    def parse(self, fname):
+        reset_env()
+        parser = SmtLibParser()
+        script = parser.get_script_fname(fname)
+        self.assertIsNotNone(script)
+        # Can we know that the last command is a check-sat?
+
+SMTLIB_DIR = "pysmt/test/smtlib/fuzzed"
+FUZZED_FILES = ["AUFLIA.smt2.bz2",
+                "QF_AUFBV.smt2.bz2",
+                "QF_LRA.smt2.bz2",
+                "QF_UFLIA.smt2.bz2",
+                "AUFLIRA.smt2.bz2",
+                "QF_AUFLIA.smt2.bz2",
+                "QF_NIA.smt2.bz2",
+                "QF_UFLRA.smt2.bz2",
+                "AUFNIRA.smt2.bz2",
+                "QF_AX.smt2.bz2",
+                "QF_NRA.smt2.bz2",
+                "QF_UFNRA.smt2.bz2",
+                "QF_BV.smt2.bz2",
+                "QF_RDL.smt2.bz2",
+                "QF_UFRDL.smt2.bz2",
+                "QF_IDL.smt2.bz2",
+                "QF_UFBV.smt2.bz2",
+                "QF_UF.smt2.bz2",
+                "QF_LIA.smt2.bz2",
+                "QF_UFIDL.smt2.bz2",
+                ]