def test_01_dwf(self):
        # Ad-hoc method to handle printing of the new node
        def hrprinter_walk_XOR(self, formula):
            self.stream.write("(")
            yield formula.arg(0)
            self.stream.write(" *+* ")
            yield formula.arg(1)
            self.stream.write(")")

        # Shortcuts for function in env
        add_dwf = get_env().add_dynamic_walker_function
        create_node = get_env().formula_manager.create_node

        # Define the new node type and register the walkers in the env
        XOR = new_node_type()
        add_dwf(XOR, SimpleTypeChecker, SimpleTypeChecker.walk_bool_to_bool)
        add_dwf(XOR, HRPrinter, hrprinter_walk_XOR)

        # Create a test node (This implicitely calls the Type-checker)
        x = Symbol("x")
        f1 = create_node(node_type=XOR, args=(x,x))
        self.assertIsNotNone(f1)

        # String conversion should use the function defined above.
        s_f1 = str(f1)
        self.assertEqual(s_f1, "(x *+* x)")

        # We did not define an implementation for the Simplifier
        with self.assertRaises(UnsupportedOperatorError):
            f1.simplify()

    def test_infix(self):
        x, y, p = self.x, self.y, self.p

        with self.assertRaises(Exception):
            x.Implies(y)
        get_env().enable_infix_notation = True
        self.assertEqual(Implies(x,y), x.Implies(y))

        self.assertEqual(p + p, Plus(p,p))
        self.assertEqual(p > p, GT(p,p))
        get_env().enable_infix_notation = False

    def test_conversion_error(self):
        from pysmt.type_checker import SimpleTypeChecker
        add_dwf = get_env().add_dynamic_walker_function
        create_node = get_env().formula_manager.create_node

        # Create a node that is not supported by any solver
        idx = op.new_node_type()
        x = Symbol("x")
        add_dwf(idx, SimpleTypeChecker, SimpleTypeChecker.walk_bool_to_bool)
        invalid_node = create_node(idx, args=(x,x))

        for sname in get_env().factory.all_solvers(logic=QF_BOOL):
            with self.assertRaises(ConvertExpressionError):
                is_sat(invalid_node, solver_name=sname, logic=QF_BOOL)

    def test_substituter_conditions(self):
        x = Symbol("x")
        y = Symbol("y")
        and_x_x = And(x, x)
        ftype = FunctionType(BOOL, [BOOL])
        f = Symbol("f", ftype)

        # 1. All arguments must be terms
        args_good = {x:y}
        args_bad = {x:f}

        substitute(and_x_x, args_good)
        with self.assertRaisesRegex(TypeError, " substitutions"):
            substitute(and_x_x, args_bad)

        # 2. All arguments belong to the manager of the substituter.
        new_mgr = FormulaManager(get_env())
        new_x = new_mgr.Symbol("x")
        self.assertNotEqual(x, new_x)
        args_1 = {x: new_x}
        args_2 = {new_x: new_x}

        with self.assertRaisesRegex(TypeError, "Formula Manager" ):
            substitute(and_x_x, args_1)

        with self.assertRaisesRegex(TypeError, "Formula Manager."):
            substitute(and_x_x, args_2)

        with self.assertRaisesRegex(TypeError, "substitute()"):
            substitute(f, {x:x})

    def test_types_oracle(self):
        get_env().enable_infix_notation = True

        S = Type("S")
        U = Type("U", 1)
        B = Type("B", 2)
        csort = B(U(S),
                  B(BOOL, S))
        v = Symbol("v", csort)
        types_all = self.env.typeso.get_types(v)
        types_custom = self.env.typeso.get_types(v, custom_only=True)
        self.assertIsNotNone(types_all)
        # Only BOOL does not appear in types_custom
        self.assertTrue(len(types_all) == 5)
        self.assertTrue(len(types_custom) == 4)

        # Types are in partial order: simpler is earlier
        idx_S = types_custom.index(S)
        idx_US = types_custom.index(U(S))
        idx_BBS = types_custom.index(B(BOOL, S))
        idx_BUSBBS = types_custom.index(B(U(S), B(BOOL, S)))

        self.assertIsNotNone(idx_S)
        self.assertIsNotNone(idx_US)
        self.assertIsNotNone(idx_BBS)
        self.assertIsNotNone(idx_BUSBBS)

        self.assertEqual(types_custom[0], S)
        self.assertTrue(idx_S < idx_US)
        self.assertTrue(idx_US < idx_BUSBBS)
        self.assertTrue(idx_BBS < idx_BUSBBS)

    def test_shortcut_is_using_global_env(self):
        global_mgr = get_env().formula_manager
        a1 = Symbol("z", BOOL)
        a2 = global_mgr.Symbol("z", BOOL)

        self.assertEqual(a1, a2,
                          "Symbols generated by env and Symbol are not the same")

 def test_atoms_oracle(self):
     oracle = get_env().ao
     stc = get_env().stc
     for (f, _, _, _) in get_example_formulae():
         atoms = oracle.get_atoms(f)
         if ( atoms is not None):
             if len(f.get_free_variables()) > 0:
                 self.assertTrue(len(atoms) > 0)
         for a in atoms:
             ty = stc.get_type(a)
             self.assertEqual(ty, BOOL)
             self.assertFalse(a.is_and())
             self.assertFalse(a.is_or())
             self.assertFalse(a.is_not())
             self.assertFalse(a.is_iff())
             self.assertFalse(a.is_quantifier())

    def test_types_oracle_examples(self):
        oracle = get_env().typeso
        for (f, _, _, _) in get_example_formulae():
            types_all = oracle.get_types(f)
            types_custom = oracle.get_types(f, custom_only=True)
            # Custom types are a subset of all types
            s1 = set(types_all)
            s2 = set(types_custom)
            self.assertTrue(s1.issuperset(s2))

            # Compare logics with types
            theory = self.env.theoryo.get_theory(f)
            if len(f.get_free_variables()) == 0:
                continue
            if theory.arrays:
                self.assertTrue(any(x.is_array_type() for x in types_all),
                                (f, types_all))
            if theory.bit_vectors:
                self.assertTrue(any(x.is_bv_type() for x in types_all),
                                (f, types_all))
            if theory.integer_arithmetic:
                self.assertTrue(any(x.is_int_type() for x in types_all),
                                (f, types_all))
            if theory.real_arithmetic:
                self.assertTrue(any(x.is_real_type() for x in types_all),
                                (f, types_all))

    def test_msat_converter_on_msat_error(self):
        import mathsat
        import _mathsat
        from pysmt.solvers.msat import MathSAT5Solver, MSatConverter


        env = get_env()
        msat = MathSAT5Solver(env, logic=QF_UFLIRA)
        new_converter = MSatConverter(env, msat.msat_env)

        def walk_plus(formula, args):
            res = mathsat.MSAT_MAKE_ERROR_TERM()
            return res

        # Replace the function used to compute the Plus()
        # with one that returns a msat_error
        new_converter.set_function(walk_plus, op.PLUS)

        r, s = FreshSymbol(REAL), FreshSymbol(REAL)
        f1 = GT(r, s)
        f2 = Plus(r, s)

        t1 = new_converter.convert(f1)
        self.assertFalse(mathsat.MSAT_ERROR_TERM(t1))

        with self.assertRaises(InternalSolverError):
            new_converter.convert(f2)

    def test_get_value_of_function_bool(self):
        """Proper handling of models with functions with bool args."""
        hr = Symbol("hr", FunctionType(REAL, [BOOL, REAL, REAL]))
        hb = Symbol("hb", FunctionType(BOOL, [BOOL, REAL, REAL]))

        hr_0_1 = Function(hr, (TRUE(), Real(0), Real(1)))
        hb_0_1 = Function(hb, (TRUE(), Real(0), Real(1)))
        hbx = Function(hb, (Symbol("x"), Real(0), Real(1)))
        f = GT(hr_0_1, Real(0))
        g = hb_0_1

        for sname in get_env().factory.all_solvers(logic=QF_UFLIRA):
            with Solver(name=sname) as solver:
                # First hr
                solver.add_assertion(f)
                res = solver.solve()
                self.assertTrue(res)
                v = solver.get_value(hr_0_1)
                self.assertIsNotNone(solver.get_value(v))
                # Now hb
                solver.add_assertion(g)
                res = solver.solve()
                self.assertTrue(res)
                v = solver.get_value(hb_0_1)
                self.assertIsNotNone(v in [TRUE(), FALSE()])
                # Hbx
                solver.add_assertion(hbx)
                res = solver.solve()
                self.assertTrue(res)
                v = solver.get_value(hbx)
                self.assertIsNotNone(v in [TRUE(), FALSE()])
                # Get model
                model = solver.get_model()
                self.assertIsNotNone(model)

    def test_incremental(self):
        a = Symbol('a', BOOL)
        b = Symbol('b', BOOL)
        c = Symbol('c', BOOL)

        for name in get_env().factory.all_solvers(logic=QF_BOOL):
            with Solver(name) as solver:
                solver.add_assertion(Or(a, b))
                solver.add_assertion(Or(Not(b), c))
                self.assertTrue(solver.solve())
                try:
                    solver.push(1)
                except NotImplementedError:
                    # if push not implemented, pop shouldn't be either
                    self.assertRaises(NotImplementedError, solver.pop)
                    continue

                solver.add_assertion(And(Not(a), Not(c)))
                self.assertFalse(solver.solve())
                solver.pop(1)
                self.assertTrue(solver.solve())
                solver.add_assertion(FALSE())
                self.assertFalse(solver.solve())
                solver.reset_assertions()
                solver.add_assertion(a)
                self.assertTrue(solver.solve())

    def test_solving_under_assumption_theory(self):
        x = Symbol("x", REAL)
        y = Symbol("y", REAL)

        v1 = GT(x, Real(10))
        v2 = LE(y, Real(2))

        xor = Or(And(v1, Not(v2)), And(Not(v1), v2))

        for name in get_env().factory.all_solvers(logic=QF_LRA):
            with Solver(name=name) as solver:
                solver.add_assertion(xor)
                res1 = solver.solve(assumptions=[v1, Not(v2)])
                model1 = solver.get_model()
                res2 = solver.solve(assumptions=[Not(v1), v2])
                model2 = solver.get_model()
                res3 = solver.solve(assumptions=[v1, v2])
                self.assertTrue(res1)
                self.assertTrue(res2)
                self.assertFalse(res3)

                self.assertEqual(model1.get_value(v1), TRUE())
                self.assertEqual(model1.get_value(v2), FALSE())
                self.assertEqual(model2.get_value(v1), FALSE())
                self.assertEqual(model2.get_value(v2), TRUE())

    def test_determinism(self):
        def get_set(env):
            mgr = env.formula_manager
            r = set(mgr.Symbol("x%d" % i) for i in xrange(1000))
            for (f, _, _, _) in get_example_formulae(env):
                r |= set([f])
            return r

        # As first thing on the environment we build the set of formulae
        l1 = list(get_set(get_env()))

        # We try this ten times...
        for _ in xrange(10):
            # Do something to screw up memory layout...
            for y in (Symbol("y%d" % i) for i in xrange(1000)):
                self.assertIsNotNone(y)

            with Environment() as new_env:
                # As first thing on the environment we build the set of formulae
                l_test = list(get_set(new_env))

                # The ordering of the sets should be the same...
                for i,f in enumerate(l1):
                    nf = new_env.formula_manager.normalize(f)
                    self.assertEquals(nf, l_test[i])

 def test_multiple_exit(self):
     for sname in get_env().factory.all_solvers():
         # Multiple exits should be ignored
         s = Solver(name=sname)
         s.exit()
         s.exit()
         self.assertTrue(True)

    def test_atoms_oracle(self):
        oracle = get_env().ao
        stc = get_env().stc
        for (f, _, _, _) in EXAMPLE_FORMULAS:
            atoms = oracle.get_atoms(f)
            if len(f.get_free_variables()) > 0:
                self.assertTrue(len(atoms) > 0)

            for a in atoms:
                ty = stc.get_type(a)
                self.assertEqual(ty, BOOL)

                self.assertFalse(a.is_and())
                self.assertFalse(a.is_or())
                self.assertFalse(a.is_not())
                self.assertFalse(a.is_iff())
                self.assertFalse(a.is_quantifier())

 def test_initial_ordering(self):
     from pysmt.solvers.bdd import BddSolver
     with BddSolver(get_env(), pysmt.logics.BOOL,
                    {"static_ordering" : [self.x, self.y],
                     "dynamic_reordering" : True}) as s:
         s.add_assertion(self.big_tree)
         self.assertTrue(s.solve())
         self.assertNotEquals(s.ddmanager.ReorderingStatus()[1], 0)

 def test_options_random_seed(self):
     for sname in get_env().factory.all_solvers(logic=QF_BOOL):
         if sname in ["btor", "bdd"]:
             with self.assertRaises(PysmtValueError):
                 Solver(name=sname, random_seed=42)
         else:
             s = Solver(name=sname, random_seed=42)
             self.assertIsNotNone(s)

    def test_examples_by_logic(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            if len(get_env().factory.all_solvers(logic=logic)) > 0:
                v = is_valid(f, logic=logic)
                s = is_sat(f, logic=logic)

                self.assertEqual(validity, v, f.serialize())
                self.assertEqual(satisfiability, s, f.serialize())

 def test_nnf_examples(self):
     for (f, _, _, logic) in get_example_formulae():
         if get_env().factory.has_solvers(logic=logic):
             rf = nnf(f)
             try:
                 ok = is_valid(Iff(f, rf), logic=logic)
             except SolverReturnedUnknownResultError:
                 ok = not logic.quantifier_free
             self.assertTrue(ok)

 def test_conj_partitioning(self):
     for (f, _, _, logic) in get_example_formulae():
         if get_env().factory.has_solvers(logic=logic):
             conjuncts = list(conjunctive_partition(f))
             try:
                 ok = is_valid(Iff(f, And(conjuncts)), logic=logic)
             except SolverReturnedUnknownResultError:
                 ok = not logic.quantifier_free
             self.assertTrue(ok)