nebius/SWE-rebench-V2-PRs huggingface dataset:
Repository: pysmt/pysmt
Pull request #576 (2019-05-04 17:15:23)

PysmtSyntaxError: Fix missing message in init


Patch:
diff --git a/pysmt/exceptions.py b/pysmt/exceptions.py
index b302ae3..3c7eb1b 100644
--- a/pysmt/exceptions.py
+++ b/pysmt/exceptions.py
@@ -137,6 +137,7 @@ class PysmtSyntaxError(PysmtException, SyntaxError):
     def __init__(self, message, pos_info=None):
         super(PysmtSyntaxError, self).__init__(message)
         self.pos_info = pos_info
+        self.message = message
 
     def __str__(self):
         if self.pos_info:


Test patch:
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 9dcaf75..54e35ae 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -509,6 +509,12 @@ class TestRegressions(TestCase):
         self.assertEqual('"', s.commands[2].args[0].arg(1).constant_value())
         self.assertEqual('""', s.commands[3].args[0].arg(1).constant_value())
 
+    def test_pysmt_syntax_error(self):
+        from pysmt.exceptions import PysmtSyntaxError
+        try:
+            raise PysmtSyntaxError("'define-fun' expected", (5,5))
+        except PysmtSyntaxError as ex:
+            self.assertEqual(str(ex), "Line 5, Col 5: 'define-fun' expected")
 
 
 if __name__ == "__main__":
Repository: pysmt/pysmt
Pull request #585 (2019-05-23 08:02:19)

Fixed Issue #584
Fixed printing as suggested by @ekiwi in #584


Patch:
diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
index b3fb6f5..57ba74c 100644
--- a/pysmt/smtlib/printers.py
+++ b/pysmt/smtlib/printers.py
@@ -91,7 +91,7 @@ class SmtPrinter(TreeWalker):
         self.write(quote(formula.symbol_name()))
 
     def walk_function(self, formula):
-        return self.walk_nary(formula, formula.function_name())
+        return self.walk_nary(formula, quote(formula.function_name().symbol_name()))
 
     def walk_int_constant(self, formula):
         if formula.constant_value() < 0:
@@ -445,7 +445,7 @@ class SmtDagPrinter(DagWalker):
         return quote(formula.symbol_name())
 
     def walk_function(self, formula, args, **kwargs):
-        return self.walk_nary(formula, args, formula.function_name())
+        return self.walk_nary(formula, args, quote(formula.function_name().symbol_name()))
 
     def walk_int_constant(self, formula, **kwargs):
         if formula.constant_value() < 0:


Test patch:
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index b95b24d..beb2b0e 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -23,7 +23,7 @@ import pysmt.smtlib.commands as smtcmd
 from pysmt.shortcuts import (Real, Plus, Symbol, Equals, And, Bool, Or, Not,
                              Div, LT, LE, Int, ToReal, Iff, Exists, Times, FALSE,
                              BVLShr, BVLShl, BVAShr, BV, BVAdd, BVULT, BVMul,
-                             Select, Array, Ite, String)
+                             Select, Array, Ite, String, Function, to_smtlib)
 from pysmt.shortcuts import Solver, get_env, qelim, get_model, TRUE, ExactlyOne
 from pysmt.typing import REAL, BOOL, INT, BVType, FunctionType, ArrayType
 from pysmt.test import (TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic,
@@ -509,6 +509,12 @@ class TestRegressions(TestCase):
         except PysmtSyntaxError as ex:
             self.assertEqual(str(ex), "Line 5, Col 5: 'define-fun' expected")
 
+    def test_function_smtlib_print(self):
+        f_t = FunctionType(BOOL, [BOOL])
+        f0 = Symbol('f 0', f_t)
+        f0_of_false = Function(f0, [Bool(False)])
+        s = to_smtlib(f0_of_false, False)
+        self.assertEqual(s, '(|f 0| false)')
 
 if __name__ == "__main__":
     main()
Repository: pysmt/pysmt
Pull request #710 (2022-03-25 16:13:26)

Fixed issue #613


Patch:
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index e66e34c..f0179cc 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -101,13 +101,13 @@ class SmtLibCommand(namedtuple('SmtLibCommand', ['name', 'args'])):
         elif self.name == smtcmd.DEFINE_FUN:
             name = self.args[0]
             params_list = self.args[1]
-            params = " ".join(["(%s %s)" % (v, v.symbol_type()) for v in params_list])
+            params = " ".join(["(%s %s)" % (v, v.symbol_type().as_smtlib(funstyle=False)) for v in params_list])
             rtype = self.args[2]
             expr = self.args[3]
             outstream.write("(%s %s (%s) %s " % (self.name,
                                                 name,
                                                 params,
-                                                rtype))
+                                                rtype.as_smtlib(funstyle=False)))
             printer.printer(expr)
             outstream.write(")")
 
@@ -117,12 +117,12 @@ class SmtLibCommand(namedtuple('SmtLibCommand', ['name', 'args'])):
         elif self.name == smtcmd.DEFINE_SORT:
             name = self.args[0]
             params_list = self.args[1]
-            params = " ".join(params_list)
+            params = " ".join(x.as_smtlib(funstyle=False) for x in params_list)
             rtype = self.args[2]
             outstream.write("(%s %s (%s) %s)" % (self.name,
                                                  name,
                                                  params,
-                                                 rtype))
+                                                 rtype.as_smtlib(funstyle=False)))
         elif self.name == smtcmd.DECLARE_SORT:
             type_decl = self.args[0]
             outstream.write("(%s %s %d)" % (self.name,


Test patch:
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index eb3276d..2ae7c9d 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -167,6 +167,14 @@ class TestSmtLibScript(TestCase):
         # No exceptions are thrown
         self.assertTrue(True)
 
+    def test_define_fun_serialize_complex_type(self):
+        smtlib_script = '(define-fun f ((var (_ BitVec 32))) (_ BitVec 32) var)'
+        stream = StringIO(smtlib_script)
+        parser = SmtLibParser()
+        script = parser.get_script(stream)
+        # No exceptions are thrown
+        self.assertEqual(smtlib_script.replace('var', '__var0'), script.commands[0].serialize_to_string())
+
 
     def test_evaluate_command(self):
         class SmtLibIgnore(SmtLibIgnoreMixin):
Repository: pysmt/pysmt
Pull request #768 (2023-12-14 15:44:41)

Fixed issue #767
The test reported in issue #767 highlighted an issue in the substituter which was unable to correctly handle the case of a function application.

The base case for the `walk_function` is implemented in the `Substituter` class, but this function does not handle substitutions, only interpretations, hence I forced the code to pass through the `MGSubstituter` or the `MSSubstituter` before calling the `Substituter.walk_function`.

I believe this should be the correct path.


Patch:
diff --git a/pysmt/substituter.py b/pysmt/substituter.py
index e45ca3a..adf5821 100644
--- a/pysmt/substituter.py
+++ b/pysmt/substituter.py
@@ -259,7 +259,7 @@ class MGSubstituter(Substituter):
     def __init__(self, env):
         Substituter.__init__(self, env=env)
 
-    @handles(set(op.ALL_TYPES) - op.QUANTIFIERS - {op.FUNCTION})
+    @handles(set(op.ALL_TYPES) - op.QUANTIFIERS)
     def walk_identity_or_replace(self, formula, args, **kwargs):
         """
         If the formula appears in the substitution, return the substitution.
@@ -314,7 +314,7 @@ class MSSubstituter(Substituter):
         """
         return substitutions.get(formula, formula)
 
-    @handles(set(op.ALL_TYPES) - op.QUANTIFIERS - {op.FUNCTION})
+    @handles(set(op.ALL_TYPES) - op.QUANTIFIERS)
     def walk_replace(self, formula, args, **kwargs):
         new_f =  Substituter.super(self, formula, args=args, **kwargs)
         return self._substitute(new_f, kwargs['substitutions'])


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 25cb4db..a95b12d 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -1085,6 +1085,20 @@ class TestFormulaManager(TestCase):
         self.assertRaises(PysmtValueError,
             lambda: self.mgr.BVMul([]))
 
+    def test_function_substitute(self):
+        FunTy = FunctionType(BOOL, [INT])
+        f = self.mgr.Symbol(f"myf", FunTy)
+        g = self.mgr.Symbol(f"myg", FunTy)
+        v = self.mgr.Symbol("v", INT)
+        w = self.mgr.Symbol("w", INT)
+
+        f_v = self.mgr.Function(f, [v])
+        f_w = self.mgr.Function(f, [w])
+        g_v = self.mgr.Function(g, [v])
+
+        phi = Iff(f_v, f_w)
+        self.assertEqual(phi.substitute({f_w: g_v}), Iff(f_v, g_v))
+
 class TestShortcuts(TestCase):
 
     def test_shortcut_is_using_global_env(self):
Repository: pysmt/pysmt
Pull request #779 (2024-07-17 07:03:34)

Fixed issue #778
When printing a real constant in SMTLib, we used a notation `(/ n d)` where `n` is the integer numerator  and `d` the integer denominator. 

This causes issues on more restrictive parsers, so we now print `(/ n.0 d.0)` to force a rational interpretation.


Patch:
diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
index c87c776..f05dff1 100644
--- a/pysmt/smtlib/printers.py
+++ b/pysmt/smtlib/printers.py
@@ -143,7 +143,7 @@ class SmtPrinter(TreeWalker):
         (n,d) = abs(formula.constant_value().numerator), \
                     formula.constant_value().denominator
         if d != 1:
-            res = template % ( "(/ " + str(n) + " " + str(d) + ")" )
+            res = template % ( "(/ " + str(n) + ".0 " + str(d) + ".0)" )
         else:
             res = template % (str(n) + ".0")
 
@@ -521,7 +521,7 @@ class SmtDagPrinter(DagWalker):
         (n,d) = abs(formula.constant_value().numerator), \
                     formula.constant_value().denominator
         if d != 1:
-            return template % ( "(/ " + str(n) + " " + str(d) + ")" )
+            return template % ( "(/ " + str(n) + ".0 " + str(d) + ".0)" )
         else:
             return template % (str(n) + ".0")
 


Test patch:
diff --git a/pysmt/test/test_printing.py b/pysmt/test/test_printing.py
index c0ad4f2..01d6f1b 100644
--- a/pysmt/test/test_printing.py
+++ b/pysmt/test/test_printing.py
@@ -98,9 +98,9 @@ class TestPrinting(TestCase):
         self.assertEqual(b1.to_smtlib(daggify=True), "true")
         self.assertEqual(b2.to_smtlib(daggify=True), "false")
 
-        self.assertEqual(r1.to_smtlib(daggify=True), "(/ 11 2)")
+        self.assertEqual(r1.to_smtlib(daggify=True), "(/ 11.0 2.0)")
         self.assertEqual(r2.to_smtlib(daggify=True), "5.0")
-        self.assertEqual(r3.to_smtlib(daggify=True), "(- (/ 11 2))")
+        self.assertEqual(r3.to_smtlib(daggify=True), "(- (/ 11.0 2.0))")
 
         self.assertEqual(i1.to_smtlib(daggify=True), "4")
         self.assertEqual(i2.to_smtlib(daggify=True), "(- 4)")
@@ -108,9 +108,9 @@ class TestPrinting(TestCase):
         self.assertEqual(b1.to_smtlib(daggify=False), "true")
         self.assertEqual(b2.to_smtlib(daggify=False), "false")
 
-        self.assertEqual(r1.to_smtlib(daggify=False), "(/ 11 2)")
+        self.assertEqual(r1.to_smtlib(daggify=False), "(/ 11.0 2.0)")
         self.assertEqual(r2.to_smtlib(daggify=False), "5.0")
-        self.assertEqual(r3.to_smtlib(daggify=False), "(- (/ 11 2))")
+        self.assertEqual(r3.to_smtlib(daggify=False), "(- (/ 11.0 2.0))")
 
         self.assertEqual(i1.to_smtlib(daggify=False), "4")
         self.assertEqual(i2.to_smtlib(daggify=False), "(- 4)")