def test_shortcuts(self):
        for (expr, _, sat_res, logic) in get_example_formulae():
            if not logic <= QF_UFLIRA: continue
            res = is_sat(expr, portfolio=["z3", "cvc4", "msat"])
            self.assertEqual(res, sat_res, expr)

        with self.assertRaises(ValueError):
            is_sat(TRUE(), portfolio=["supersolver"])

    def test_div_pow(self):
        x = FreshSymbol(REAL)
        f = Equals(Times(Real(4), Pow(x, Real(-1))), Real(2))
        self.assertTrue(is_sat(f))

        f = Equals(Div(Real(4), x), Real(2))
        self.assertTrue(is_sat(f, solver_name="z3"))
        f = Equals(Times(x, x), Real(16))
        self.assertTrue(is_sat(f))

 def _verify_ackermannization(self, formula):
     ackermannization = Ackermannizer()
     ack = ackermannization.do_ackermannization(formula)
     #verify that there are no functions in ack
     atoms = ack.get_atoms()
     for atom in atoms:
         for arg in atom.args():
             self.assertFalse(arg.is_function_application())
     #verify that ack and formula are equisat
     formula_sat = is_sat(formula)
     ack_sat = is_sat(ack)
     self.assertTrue(formula_sat == ack_sat)

    def test_integer(self):
        x = FreshSymbol(INT)
        f = Equals(Times(x, x), Int(2))
        with Solver(name="z3") as s:
            self.assertFalse(s.is_sat(f))

        # f = Equals(Times(Int(4), Pow(x, Int(-1))), Int(2))
        # self.assertTrue(is_sat(f, solver_name="z3"))

        f = Equals(Div(Int(4), x), Int(2))
        self.assertTrue(is_sat(f, solver_name="z3"))
        f = Equals(Times(x, x), Int(16))
        self.assertTrue(is_sat(f))

    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_logic_as_string(self):
        self.assertEqual(convert_logic_from_string("QF_LRA"), QF_LRA)
        if PY2:
            self.assertEqual(convert_logic_from_string(unicode("QF_LRA")),
                             QF_LRA)
        with self.assertRaises(UndefinedLogicError):
            convert_logic_from_string("PAPAYA")
        self.assertIsNone(convert_logic_from_string(None))

        x = Symbol("x")
        self.assertTrue(is_sat(x, logic="QF_LRA"))
        with self.assertRaises(UndefinedLogicError):
            is_sat(x, logic="PAPAYA")
        self.assertTrue(is_sat(x, logic=None))
        self.assertTrue(is_sat(x))

    def test_examples_z3(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            v = is_valid(f, solver_name='z3', logic=logic)
            s = is_sat(f, solver_name='z3', logic=logic)

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

    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_examples_yices(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            if not logic.quantifier_free: continue
            v = is_valid(f, solver_name='yices', logic=logic)
            s = is_sat(f, solver_name='yices', logic=logic)

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

 def test_exactly_one_is_sat(self):
     symbols = [ self.mgr.Symbol("s%d"%i, BOOL) for i in range(5) ]
     c = self.mgr.ExactlyOne(symbols)
     all_zero = self.mgr.And([self.mgr.Iff(s, self.mgr.Bool(False))
                               for s in symbols])
     test_zero = self.mgr.And(c, all_zero)
     self.assertFalse(is_sat(test_zero, logic=QF_BOOL),
                      "ExactlyOne should not allow all symbols to be False")

    def _std_examples(self, qe, target_logic):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            if logic != target_logic: continue
            qf = qe.eliminate_quantifiers(f)
            s = is_sat(qf)
            v = is_valid(qf)

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

 def test_examples_btor(self):
     for (f, validity, satisfiability, logic) in get_example_formulae():
         if not logic.quantifier_free: continue
         try:
             v = is_valid(f, solver_name='btor', logic=logic)
             s = is_sat(f, solver_name='btor', logic=logic)
             self.assertEqual(validity, v, f)
             self.assertEqual(satisfiability, s, f)
         except NoSolverAvailableError:
             pass #Skip tests for unsupported logic

    def test_examples_msat(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            if not logic.quantifier_free: continue
            if not logic.theory.linear: continue
            if logic.theory.strings: continue

            v = is_valid(f, solver_name='msat', logic=logic)
            s = is_sat(f, solver_name='msat', logic=logic)
            self.assertEqual(validity, v, f)
            self.assertEqual(satisfiability, s, f)

    def do_examples(self, logic):
        conv = CNFizer()
        for example in EXAMPLE_FORMULAS:
            if example.logic != logic:
                continue
            cnf = conv.convert_as_formula(example.expr)

            self.assertValid(Implies(cnf, example.expr), logic=logic)

            res = is_sat(cnf, logic=logic)
            self.assertEqual(res, example.is_sat)

    def test_examples_z3(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            try:
                v = is_valid(f, solver_name='z3', logic=logic)
                s = is_sat(f, solver_name='z3', logic=logic)

                self.assertEqual(validity, v, f)
                self.assertEqual(satisfiability, s, f)
            except NoSolverAvailableError:
                # Trying to solve a logic that mathsat does not support
                theory = logic.theory
                assert theory.strings

    def test_examples_btor(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            if not logic.quantifier_free: continue
            if logic.theory.strings: continue
            if logic.theory.integer_arithmetic: continue
            if logic.theory.real_arithmetic: continue
            if logic.theory.custom_type: continue

            v = is_valid(f, solver_name='btor', logic=logic)
            s = is_sat(f, solver_name='btor', logic=logic)
            self.assertEqual(validity, v, f)
            self.assertEqual(satisfiability, s, f)

    def test_examples_cvc4(self):
        for (f, validity, satisfiability, logic) in get_example_formulae():
            try:
                if not logic.quantifier_free: continue
                v = is_valid(f, solver_name='cvc4', logic=logic)
                s = is_sat(f, solver_name='cvc4', logic=logic)

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

            except SolverReturnedUnknownResultError:
                # CVC4 does not handle quantifiers in a complete way
                self.assertFalse(logic.quantifier_free)

 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:
             try:
                 v = is_valid(f, logic=logic)
                 s = is_sat(f, logic=logic)
                 self.assertEqual(validity, v, f.serialize())
                 self.assertEqual(satisfiability, s, f.serialize())
             except SolverReturnedUnknownResultError:
                 s = Solver(logic=logic)
                 print(s, logic, f)
                 self.assertFalse(logic.quantifier_free,
                                  "Unkown result are accepted only on "\
                                  "Quantified formulae")

    def test_examples(self):
        for n in self.all_solvers:
            with Solver(name=n) as solver:
                for (f, validity, satisfiability, logic) in \
                    get_example_formulae():
                    try:
                        get_closer_logic(solver.LOGICS, logic)
                    except NoLogicAvailableError:
                        continue
                    v = is_valid(f, solver_name=n, logic=logic)
                    s = is_sat(f, solver_name=n, logic=logic)

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

def check_property(system, prop):
    """Interleaves BMC and K-Ind to verify the property."""
    print("Checking property %s..." % prop)
    for b in xrange(100):
        f = get_bmc(system, prop, b)
        print("   [BMC]    Checking bound %d..." % (b+1))
        if is_sat(f):
            print("--> Bug found at step %d" % (b+1))
            return

        f = get_k_induction(system, prop, b)
        print("   [K-IND]  Checking bound %d..." % (b+1))
        if is_unsat(f):
            print("--> The system is safe!")
            return