Skip to content
Permalink
Browse files

Fixed Issue #584

Fixed printing as suggested by @ekiwi
  • Loading branch information...
mikand committed May 23, 2019
1 parent 142d661 commit 0a3a2e43ab112b24d28d2b5c790aa789880cfab7
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 0a3a2e4

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