@@ 1,258 0,0 @@
-Backport of an upstream patch which fixes a test failure with our
-packaged version of the Z3 SMT solver.
-
-Taken from: https://github.com/pysmt/pysmt/commit/f522e8cd8f3e75ff85f5eae29b427e18a6701859
-
-diff --git a/pysmt/formula.py b/pysmt/formula.py
-index ea4b46c..6cb9cbf 100644
---- a/pysmt/formula.py
-+++ b/pysmt/formula.py
-@@ -252,11 +252,7 @@ class FormulaManager(object):
-
- if base.is_constant():
- val = base.constant_value() ** exponent.constant_value()
-- if base.is_constant(types.REAL):
-- return self.Real(val)
-- else:
-- assert base.is_constant(types.INT)
-- return self.Int(val)
-+ return self.Real(val)
- return self.create_node(node_type=op.POW, args=(base, exponent))
-
- def Div(self, left, right):
-diff --git a/pysmt/logics.py b/pysmt/logics.py
-index ef88dd6..9dc45b1 100644
---- a/pysmt/logics.py
-+++ b/pysmt/logics.py
-@@ -495,6 +495,12 @@ QF_NRA = Logic(name="QF_NRA",
- real_arithmetic=True,
- linear=False)
-
-+QF_NIRA = Logic(name="QF_NIRA",
-+ description="""Quantifier-free integer and real arithmetic.""",
-+ quantifier_free=True,
-+ integer_arithmetic=True,
-+ real_arithmetic=True,
-+ linear=False)
-
- QF_RDL = Logic(name="QF_RDL",
- description=\
-@@ -619,41 +625,41 @@ QF_AUFBVLIRA = Logic(name="QF_AUFBVLIRA",
- AUTO = Logic(name="Auto",
- description="Special logic used to indicate that the logic to be used depends on the formula.")
-
--SMTLIB2_LOGICS = frozenset([ AUFLIA,
-- AUFLIRA,
-- AUFNIRA,
-- ALIA,
-- LRA,
-- LIA,
-- NIA,
-- NRA,
-- UFLRA,
-- UFNIA,
-- UFLIRA,
-- QF_ABV,
-- QF_AUFBV,
-- QF_AUFLIA,
-- QF_ALIA,
-- QF_AX,
-- QF_BV,
-- QF_IDL,
-- QF_LIA,
-- QF_LRA,
-- QF_NIA,
-- QF_NRA,
-- QF_RDL,
-- QF_UF,
-- QF_UFBV ,
-- QF_UFIDL,
-- QF_UFLIA,
-- QF_UFLRA,
-- QF_UFNRA,
-- QF_UFNIA,
-- QF_UFLIRA,
-- QF_SLIA
-- ])
--
--LOGICS = SMTLIB2_LOGICS | frozenset([ QF_BOOL, BOOL, QF_AUFBVLIRA])
-+SMTLIB2_LOGICS = frozenset([AUFLIA,
-+ AUFLIRA,
-+ AUFNIRA,
-+ ALIA,
-+ LRA,
-+ LIA,
-+ NIA,
-+ NRA,
-+ UFLRA,
-+ UFNIA,
-+ UFLIRA,
-+ QF_ABV,
-+ QF_AUFBV,
-+ QF_AUFLIA,
-+ QF_ALIA,
-+ QF_AX,
-+ QF_BV,
-+ QF_IDL,
-+ QF_LIA,
-+ QF_LRA,
-+ QF_NIA,
-+ QF_NRA,
-+ QF_RDL,
-+ QF_UF,
-+ QF_UFBV,
-+ QF_UFIDL,
-+ QF_UFLIA,
-+ QF_UFLRA,
-+ QF_UFNRA,
-+ QF_UFNIA,
-+ QF_UFLIRA,
-+ QF_SLIA
-+ ])
-+
-+LOGICS = SMTLIB2_LOGICS | frozenset([QF_BOOL, BOOL, QF_AUFBVLIRA, QF_NIRA])
-
- QF_LOGICS = frozenset(_l for _l in LOGICS if _l.quantifier_free)
-
-@@ -668,8 +674,8 @@ PYSMT_LOGICS = frozenset([QF_BOOL, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFI
- QF_BV, QF_UFBV,
- QF_ABV, QF_AUFBV, QF_AUFLIA, QF_ALIA, QF_AX,
- QF_AUFBVLIRA,
-- QF_NRA, QF_NIA, UFBV, BV,
-- ])
-+ QF_NRA, QF_NIA, QF_NIRA, UFBV, BV,
-+ ])
-
- # PySMT Logics includes additional features:
- # - constant arrays: QF_AUFBV becomes QF_AUFBV*
-@@ -697,7 +703,6 @@ for l in PYSMT_LOGICS:
- ext_logics.add(nl)
-
-
--
- LOGICS = LOGICS | frozenset(ext_logics)
- PYSMT_LOGICS = PYSMT_LOGICS | frozenset(ext_logics)
-
-diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
-index 3fb42b9..210b771 100644
---- a/pysmt/solvers/z3.py
-+++ b/pysmt/solvers/z3.py
-@@ -595,6 +595,8 @@ class Z3Converter(Converter, DagWalker):
- None, None,
- 0, None,
- expr.ast)
-+ print("Z3: SMTLIB")
-+ print(s)
- stream_in = StringIO(s)
- r = parser.get_script(stream_in).get_last_formula(self.mgr)
- key = (askey(expr), None)
-diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py
-index 73455ee..b653185 100644
---- a/pysmt/test/examples.py
-+++ b/pysmt/test/examples.py
-@@ -898,12 +898,12 @@ def get_full_example_formulae(environment=None):
- logic=pysmt.logics.QF_NRA
- ),
-
-- Example(hr="((p ^ 2) = 0)",
-- expr=Equals(Pow(p, Int(2)), Int(0)),
-+ Example(hr="((p ^ 2) = 0.0)",
-+ expr=Equals(Pow(p, Int(2)), Real(0)),
- is_valid=False,
- is_sat=True,
-- logic=pysmt.logics.QF_NIA
-- ),
-+ logic=pysmt.logics.QF_NIRA
-+ ),
-
- Example(hr="((r ^ 2.0) = 0.0)",
- expr=Equals(Pow(r, Real(2)), Real(0)),
-diff --git a/pysmt/test/test_back.py b/pysmt/test/test_back.py
-index bceb45b..7a0ad63 100644
---- a/pysmt/test/test_back.py
-+++ b/pysmt/test/test_back.py
-@@ -55,10 +55,10 @@ class TestBasic(TestCase):
- res = msat.converter.back(term)
- self.assertFalse(f == res)
-
-- def do_back(self, solver_name, z3_string_buffer=False):
-+ def do_back(self, solver_name, via_smtlib=False):
- for formula, _, _, logic in get_example_formulae():
- if logic.quantifier_free:
-- if logic.theory.custom_type and z3_string_buffer:
-+ if logic.theory.custom_type and via_smtlib:
- # Printing of declare-sort from Z3 is not conformant
- # with the SMT-LIB. We might consider extending our
- # parser.
-@@ -67,7 +67,7 @@ class TestBasic(TestCase):
- s = Solver(name=solver_name, logic=logic)
- term = s.converter.convert(formula)
- if solver_name == "z3":
-- if z3_string_buffer:
-+ if via_smtlib:
- res = s.converter.back_via_smtlib(term)
- else:
- res = s.converter.back(term)
-@@ -84,8 +84,8 @@ class TestBasic(TestCase):
-
- @skipIfSolverNotAvailable("z3")
- def test_z3_back_formulae(self):
-- self.do_back("z3", z3_string_buffer=False)
-- self.do_back("z3", z3_string_buffer=True)
-+ self.do_back("z3", via_smtlib=True)
-+ self.do_back("z3", via_smtlib=False)
-
-
- if __name__ == '__main__':
-diff --git a/pysmt/type_checker.py b/pysmt/type_checker.py
-index b700fcf..7ce05aa 100644
---- a/pysmt/type_checker.py
-+++ b/pysmt/type_checker.py
-@@ -33,6 +33,8 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def __init__(self, env=None):
- walkers.DagWalker.__init__(self, env=env)
-+ # Return None if the type cannot be computed rather than
-+ # raising an exception.
- self.be_nice = False
-
- def _get_key(self, formula, **kwargs):
-@@ -42,7 +44,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- """ Returns the pysmt.types type of the formula """
- res = self.walk(formula)
- if not self.be_nice and res is None:
-- raise PysmtTypeError("The formula '%s' is not well-formed" \
-+ raise PysmtTypeError("The formula '%s' is not well-formed"
- % str(formula))
- return res
-
-@@ -114,7 +116,7 @@ class SimpleTypeChecker(walkers.DagWalker):
-
- def walk_bv_comp(self, formula, args, **kwargs):
- # We check that all children are BV and the same size
-- a,b = args
-+ a, b = args
- if a != b or (not a.is_bv_type()):
- return None
- return BVType(1)
-@@ -187,7 +189,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- if args[0].is_bool_type():
- raise PysmtTypeError("The formula '%s' is not well-formed."
- "Equality operator is not supported for Boolean"
-- " terms. Use Iff instead." \
-+ " terms. Use Iff instead."
- % str(formula))
- elif args[0].is_bv_type():
- return self.walk_bv_to_bool(formula, args)
-@@ -324,10 +326,7 @@ class SimpleTypeChecker(walkers.DagWalker):
- def walk_pow(self, formula, args, **kwargs):
- if args[0] != args[1]:
- return None
-- # Exponent must be positive for INT
-- if args[0].is_int_type() and formula.arg(1).constant_value() < 0 :
-- return None
-- return args[0]
-+ return REAL
-
- # EOC SimpleTypeChecker
-
@@ 1,86 0,0 @@
-Backport of an upstream patch fixing a test suite failure.
-
-Taken from: https://github.com/pysmt/pysmt/commit/a246669a487aff69f5da34570ef867841d18508a
-
-diff --git a/pysmt/test/smtlib/test_parser_examples.py b/pysmt/test/smtlib/test_parser_examples.py
-index cca4194..c0852be 100644
---- a/pysmt/test/smtlib/test_parser_examples.py
-+++ b/pysmt/test/smtlib/test_parser_examples.py
-@@ -29,6 +29,7 @@ from pysmt.shortcuts import Iff
- from pysmt.shortcuts import read_smtlib, write_smtlib, get_env
- from pysmt.exceptions import PysmtSyntaxError
-
-+
- class TestSMTParseExamples(TestCase):
-
- def test_parse_examples(self):
-@@ -41,7 +42,6 @@ class TestSMTParseExamples(TestCase):
- buf = StringIO()
- script_out = smtlibscript_from_formula(f_out)
- script_out.serialize(outstream=buf)
-- #print(buf)
-
- buf.seek(0)
- parser = SmtLibParser()
-@@ -49,7 +49,6 @@ class TestSMTParseExamples(TestCase):
- f_in = script_in.get_last_formula()
- self.assertEqual(f_in.simplify(), f_out.simplify())
-
--
- @skipIfNoSolverForLogic(logics.QF_BV)
- def test_parse_examples_bv(self):
- """For BV we represent a superset of the operators defined in SMT-LIB.
-@@ -108,7 +107,18 @@ class TestSMTParseExamples(TestCase):
- self.assertValid(Iff(f_in, f_out), f_in.serialize())
-
- def test_dumped_logic(self):
-- # Dumped logic matches the logic in the example
-+ # Dumped logic matches the logic in the example.
-+ #
-+ # There are a few cases where we use a logic
-+ # that does not exist in SMT-LIB, and the SMT-LIB
-+ # serialization logic will find a logic that
-+ # is more expressive. We need to adjust the test
-+ # for those cases (see rewrite dict below).
-+ rewrite = {
-+ logics.QF_BOOL: logics.QF_UF,
-+ logics.BOOL: logics.LRA,
-+ logics.QF_NIRA: logics.AUFNIRA,
-+ }
- fs = get_example_formulae()
-
- for (f_out, _, _, logic) in fs:
-@@ -121,14 +131,9 @@ class TestSMTParseExamples(TestCase):
- for cmd in script_in:
- if cmd.name == "set-logic":
- logic_in = cmd.args[0]
-- if logic == logics.QF_BOOL:
-- self.assertEqual(logic_in, logics.QF_UF)
-- elif logic == logics.BOOL:
-- self.assertEqual(logic_in, logics.LRA)
-- else:
-- self.assertEqual(logic_in, logic, script_in)
-+ self.assertEqual(logic_in, rewrite.get(logic, logic))
- break
-- else: # Loops exited normally
-+ else: # Loops exited normally
- print("-"*40)
- print(script_in)
-
-@@ -136,7 +141,7 @@ class TestSMTParseExamples(TestCase):
- fs = get_example_formulae()
-
- fdi, tmp_fname = mkstemp()
-- os.close(fdi) # Close initial file descriptor
-+ os.close(fdi) # Close initial file descriptor
- for (f_out, _, _, _) in fs:
- write_smtlib(f_out, tmp_fname)
- # with open(tmp_fname) as fin:
-@@ -197,7 +202,6 @@ class TestSMTParseExamples(TestCase):
- f_in = script.get_last_formula()
- self.assertSat(f_in)
-
--
- def test_int_promotion_define_fun(self):
- script = """
- (define-fun x () Int 8)