Skip to content
Permalink
Browse files

Merge pull request #585 from pysmt/issue_584

Fixed Issue #584
  • Loading branch information...
mikand committed May 23, 2019
2 parents 142d661 + 0a3a2e4 commit 8936426bc887e18a4495ccb2e26292e4791beaba
Showing with 9 additions and 3 deletions.
  1. +2 −2 pysmt/smtlib/printers.py
  2. +7 −1 pysmt/test/test_regressions.py
@@ -91,7 +91,7 @@ def walk_symbol(self, formula):
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 @@ def walk_symbol(self, formula, **kwargs):
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:
@@ -23,7 +23,7 @@
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 @@ def test_pysmt_syntax_error(self):
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()

0 comments on commit 8936426

Please sign in to comment.
You can’t perform that action at this time.