def test_threshold_printing(self):
        x = Symbol("x")
        f = And(x,x)
        for _ in xrange(10):
            f = And(f,f)

        short_f_str = str(f)
        long_f_str = f.serialize()
        self.assertTrue(len(short_f_str) < len(long_f_str))

    def test_substitute_memoization(self):
        a = Symbol("A", BOOL)
        b = Symbol("B", BOOL)

        f = And(a, b)
        g = f.substitute({a:Bool(True)})
        h = f.substitute({a:Bool(False)})

        self.assertNotEqual(h, g)

    def test_get_implicant_unsat(self):
        varA = Symbol("A", BOOL)
        varB = Symbol("B", BOOL)

        f = And(varA, Not(varB))
        g = f.substitute({varB:varA})

        for solver in get_env().factory.all_solvers(logic=QF_BOOL):
            res = get_implicant(g, solver_name=solver)
            self.assertIsNone(res, "Formula was expected to be UNSAT")

    def test_is_sat(self):
        varA = Symbol("A", BOOL)
        varB = Symbol("B", BOOL)

        f = And(varA, Not(varB))
        g = f.substitute({varB:varA})

        self.assertUnsat(g, logic=QF_BOOL,
                         msg="Formula was expected to be UNSAT")

        for solver in get_env().factory.all_solvers():
            self.assertUnsat(g, solver_name=solver,
                             msg="Formula was expected to be UNSAT")

    def test_create_and_solve(self):
        solver = Solver(logic=QF_BOOL)

        varA = Symbol("A", BOOL)
        varB = Symbol("B", BOOL)

        f = And(varA, Not(varB))

        g = f.substitute({varB:varA})
        solver.add_assertion(g)
        res = solver.solve()
        self.assertFalse(res, "Formula was expected to be UNSAT")

        h = And(g, Bool(False))
        simp_h = h.simplify()
        self.assertEqual(simp_h, Bool(False))

    def test_ackermannization_dictionaries(self):
        self.env.enable_infix_notation = True
        a,b = (Symbol(x, INT) for x in "ab")
        f,g = (Symbol(x, FunctionType(INT, [INT, INT])) for x in "fg")
        h = Symbol("h", FunctionType(INT, [INT]))

        formula1 = Not(Equals(f(a, g(a, h(a))),
                              f(b, g(b, h(b)))))
        formula2 = Equals(a, b)
        formula = And(formula1, formula2)
        ackermannization = Ackermannizer()
        _ = ackermannization.do_ackermannization(formula)
        terms_to_consts = ackermannization.get_term_to_const_dict()
        consts_to_terms = ackermannization.get_const_to_term_dict()
        # The maps have the same length
        self.assertEqual(len(terms_to_consts), len(consts_to_terms))
        # The maps are the inverse of each other
        for t in terms_to_consts:
            self.assertEqual(t, consts_to_terms[terms_to_consts[t]])
        # Check that the the functions are there
        for atom in formula.get_atoms():
            if atom.is_function_application():
                self.assertIsNotNone(terms_to_consts[atom])

    def test_basic(self):
        varA = Symbol("A")
        f = And(varA, Not(varA))

        self.assertEqual(f.size(), 4)
        self.assertEqual(f.size(SizeOracle.MEASURE_TREE_NODES), 4)
        self.assertEqual(f.size(SizeOracle.MEASURE_DAG_NODES), 3)
        self.assertEqual(varA.size(SizeOracle.MEASURE_LEAVES), 1)
        self.assertEqual(f.size(SizeOracle.MEASURE_DEPTH), 3)
        self.assertEqual(f.size(SizeOracle.MEASURE_SYMBOLS), 1)

# Checking satisfiability of a formula.
#
# This example shows:
#  1. How to build a formula
#  2. How to perform substitution
#  3. Printing
#  4. Satisfiability checking
from pysmt.shortcuts import Symbol, And, Not, is_sat

varA = Symbol("A") # Default type is Boolean
varB = Symbol("B")
f = And([varA, Not(varB)])
g = f.substitute({varB:varA})

res = is_sat(f)
assert res # SAT
print("f := %s is SAT? %s" % (f, res))

res = is_sat(g)
print("g := %s is SAT? %s" % (g, res))
assert not res # UNSAT

 def test_trivial_false_and(self):
     x,y,z = (Symbol(name) for name in "xyz")
     f = And(x, y, z, Not(x))
     self.assertEqual(f.simplify(), FALSE())

 def test_and_flattening(self):
     x,y,z = (Symbol(name) for name in "xyz")
     f1 = And(x, y, z)
     f2 = And(x, And(y, z))
     self.assertEqual(f2.simplify(), f1)