def eliminate_quantifiers(self, formula):
        logic = get_logic(formula, self.environment)
        if not logic <= LRA and not logic <= LIA:
            raise PysmtValueError("Z3 quantifier elimination only "\
                                  "supports LRA or LIA without combination."\
                                  "(detected logic is: %s)" % str(logic))

        simplifier = z3.Tactic('simplify')
        eliminator = z3.Tactic('qe')

        f = self.converter.convert(formula)
        s = simplifier(f, elim_and=True,
                       pull_cheap_ite=True,
                       ite_extra_rules=True).as_expr()
        res = eliminator(f).as_expr()

        pysmt_res = None
        try:
            pysmt_res = self.converter.back(res)
        except ConvertExpressionError:
            if logic <= LRA:
                raise
            raise ConvertExpressionError(message=("Unable to represent" \
                "expression %s in pySMT: the quantifier elimination for " \
                "LIA is incomplete as it requires the modulus. You can " \
                "find the Z3 expression representing the quantifier " \
                "elimination as the attribute 'expression' of this " \
                "exception object" % str(res)),
                                          expression=res)

        return pysmt_res

def smtlibscript_from_formula(formula):
    script = SmtLibScript()

    # Get the simplest SmtLib logic that contains the formula
    f_logic = get_logic(formula)

    smt_logic = None
    try:
        smt_logic = get_closer_smtlib_logic(f_logic)
    except NoLogicAvailableError:
        warnings.warn("The logic %s is not reducible to any SMTLib2 " \
                      "standard logic. Proceeding with non-standard " \
                      "logic '%s'" % (f_logic, f_logic))
        smt_logic = f_logic

    script.add(name=smtcmd.SET_LOGIC,
               args=[smt_logic])

    deps = formula.get_free_variables()
    # Declare all variables
    for symbol in deps:
        assert symbol.is_symbol()
        script.add(name=smtcmd.DECLARE_FUN, args=[symbol])

    # Assert formula
    script.add_command(SmtLibCommand(name=smtcmd.ASSERT,
                                     args=[formula]))
    # check-sat
    script.add_command(SmtLibCommand(name=smtcmd.CHECK_SAT,
                                     args=[]))

    return script

    def sequence_interpolant(self, formulas, solver_name=None, logic=None):
        if logic is None or logic == AUTO_LOGIC:
            _And = self.environment.formula_manager.And
            logic = get_logic(_And(formulas))

        with self.Interpolator(name=solver_name, logic=logic) as itp:
            return itp.sequence_interpolant(formulas)

 def is_unsat(self, formula, solver_name=None, logic=None):
     if logic is None or logic == AUTO_LOGIC:
         logic = get_logic(formula, self.environment)
     with self.Solver(name=solver_name, logic=logic,
                      generate_models=False,
                      incremental=False) as solver:
         return solver.is_unsat(formula)

 def _check_logic(self, formulas):
     for f in formulas:
         logic = get_logic(f, self.environment)
         ok = any(logic <= l for l in self.LOGICS)
         if not ok:
             raise PysmtValueError("Logic not supported by Z3 interpolation."
                                   "(detected logic is: %s)" % str(logic))

    def get_implicant(self, formula, solver_name=None,
                      logic=None):
        mgr = self.environment.formula_manager
        if logic is None or logic == AUTO_LOGIC:
            logic = get_logic(formula, self.environment)

        with self.Solver(name=solver_name, logic=logic) \
             as solver:
            solver.add_assertion(formula)
            check = solver.solve()
            if not check:
                return None
            else:
                model = solver.get_model()
                atoms = formula.get_atoms()
                res = []
                for a in atoms:
                    fv = a.get_free_variables()
                    if any(v in model for v in fv):
                        if solver.get_value(a).is_true():
                            res.append(a)
                        else:
                            assert solver.get_value(a).is_false()
                            res.append(mgr.Not(a))
                return mgr.And(res)

    def binary_interpolant(self, formula_a, formula_b,
                           solver_name=None, logic=None):
        if logic == AUTO_LOGIC:
            logic = get_logic(
                self.environment.formula_manager.And(formula_a, formula_b))

        with self.Interpolator(name=solver_name, logic=logic) as itp:
            return itp.binary_interpolant(formula_a, formula_b)

def all_smt(formula, keys):
    target_logic = get_logic(formula)
    print("Target Logic: %s" % target_logic)
    with Solver(logic=target_logic) as solver:
        solver.add_assertion(formula)
        while solver.solve():
            partial_model = [EqualsOrIff(k, solver.get_value(k)) for k in keys]
            print(partial_model)
            solver.add_assertion(Not(And(partial_model)))

    def eliminate_quantifiers(self, formula):
        logic = get_logic(formula, self.environment)
        if not logic <= pysmt.logics.BOOL:
            raise NotImplementedError("BDD-based quantifier elimination only "\
                                      "supports pure-boolean formulae."\
                                      "(detected logic is: %s)" % str(logic))

        bdd = self.converter.convert(formula)
        pysmt_res = self.converter.back(bdd)
        return pysmt_res

 def get_model(self, formula, solver_name=None, logic=None):
     if logic is None or logic == AUTO_LOGIC:
         logic = get_logic(formula, self.environment)
     with self.Solver(name=solver_name, logic=logic,
                      generate_models=True,
                      incremental=False) as solver:
         solver.add_assertion(formula)
         if solver.solve():
             return solver.get_model()
         return None

 def get_model(self, formula, solver_name=None, logic=None):
     if logic == AUTO_LOGIC:
         logic = get_logic(formula, self.environment)
     with self.Solver(name=solver_name, logic=logic) \
          as solver:
         solver.add_assertion(formula)
         check = solver.solve()
         retval = None
         if check:
             retval = solver.get_model()
         return retval

    def test_theory_oracle(self):
        from pysmt.oracles import get_logic
        s1 = Symbol("s1", STRING)
        s2 = Symbol("s2", STRING)

        f = Equals(StrConcat(s1, s1), s2)
        theory = get_logic(f).theory
        self.assertTrue(theory.strings, theory)

        f = Not(And(GE(StrLength(StrConcat(s1, s2)),
                       StrLength(s1)),
                    GE(StrLength(StrConcat(s1, s2)),
                       StrLength(s2))))
        theory = get_logic(f).theory
        self.assertTrue(theory.strings, theory)

        f = And(GT(StrLength(s1), Int(2)),
                GT(StrLength(s2), StrLength(s1)),
                And(StrSuffixOf(s2, s1), StrContains(s2, s1)))
        theory = get_logic(f).theory
        self.assertTrue(theory.strings, theory)

 def is_unsat(self, formula, solver_name=None, logic=None, portfolio=None):
     if logic is None or logic == AUTO_LOGIC:
         logic = get_logic(formula, self.environment)
     if portfolio is not None:
         solver = Portfolio(solvers_set=portfolio,
                            environment=self.environment,
                            logic=logic,
                            generate_models=False, incremental=False)
     else:
         solver = self.Solver(name=solver_name, logic=logic,
                              generate_models=False, incremental=False)
     with solver:
         return solver.is_unsat(formula)

 def simplify(self, formula):
     from pysmt.oracles import get_logic
     from pysmt.logics import BOOL, QF_BOOL
     if self.bool_abstraction:
         logic = get_logic(formula)
         if logic > QF_BOOL and logic != BOOL:
             res = self.abstract_and_simplify(formula)
         else:
             res = self.back(self.convert(formula))
     else:
         res = self.back(self.convert(formula))
     self._validate(formula, res)
     return res

    def get_unsat_core(self, clauses, solver_name=None, logic=None):
        if logic is None or logic == AUTO_LOGIC:
            logic = get_logic(self.environment.formula_manager.And(clauses),
                              self.environment)

        with self.UnsatCoreSolver(name=solver_name, logic=logic) \
             as solver:
            for c in clauses:
                solver.add_assertion(c)
            check = solver.solve()
            if check:
                return None

            return solver.get_unsat_core()

def smtlibscript_from_formula(formula, logic=None):
    script = SmtLibScript()

    if logic is None:
        # Get the simplest SmtLib logic that contains the formula
        f_logic = get_logic(formula)

        smt_logic = None
        try:
            smt_logic = get_closer_smtlib_logic(f_logic)
        except NoLogicAvailableError:
            warnings.warn("The logic %s is not reducible to any SMTLib2 " \
                          "standard logic. Proceeding with non-standard " \
                          "logic '%s'" % (f_logic, f_logic),
                          stacklevel=3)
            smt_logic = f_logic
    elif not (isinstance(logic, Logic) or isinstance(logic, str)):
        raise UndefinedLogicError(str(logic))
    else:
        if logic not in SMTLIB2_LOGICS:
            warnings.warn("The logic %s is not reducible to any SMTLib2 " \
                          "standard logic. Proceeding with non-standard " \
                          "logic '%s'" % (logic, logic),
                          stacklevel=3)
        smt_logic = logic

    script.add(name=smtcmd.SET_LOGIC,
               args=[smt_logic])

    # Declare all types
    types = get_env().typeso.get_types(formula, custom_only=True)
    for type_ in types:
        script.add(name=smtcmd.DECLARE_SORT, args=[type_.decl])

    deps = formula.get_free_variables()
    # Declare all variables
    for symbol in deps:
        assert symbol.is_symbol()
        script.add(name=smtcmd.DECLARE_FUN, args=[symbol])

    # Assert formula
    script.add_command(SmtLibCommand(name=smtcmd.ASSERT,
                                     args=[formula]))
    # check-sat
    script.add_command(SmtLibCommand(name=smtcmd.CHECK_SAT,
                                     args=[]))
    return script

        def exist_elim(self, variables, formula):
            logic = get_logic(formula, self.env)
            if not logic <= LRA:
                raise NotImplementedError("MathSAT quantifier elimination only"\
                                          " supports LRA (detected logic " \
                                          "is: %s)" % str(logic))

            fterm = self.converter.convert(formula)
            tvars = [self.converter.convert(x) for x in variables]

            algo = mathsat.MSAT_EXIST_ELIM_ALLSMT_FM
            if self.algorithm == 'lw':
                algo = mathsat.MSAT_EXIST_ELIM_VTS

            res = mathsat.msat_exist_elim(self.msat_env(), fterm, tvars, algo)

            return self.converter.back(res)

def smtlibscript_from_formula(formula):
    script = SmtLibScript()

    # Get the simplest SmtLib logic that contains the formula
    f_logic = get_logic(formula)
    smt_logic = get_closer_smtlib_logic(f_logic)
    script.add(name=smtcmd.SET_LOGIC,
               args=[smt_logic])

    deps = formula.get_free_variables()
    # Declare all variables
    for symbol in deps:
        assert symbol.is_symbol()
        script.add(name=smtcmd.DECLARE_FUN, args=[symbol])

    # Assert formula
    script.add_command(SmtLibCommand(name=smtcmd.ASSERT,
                                     args=[formula]))
    # check-sat
    script.add_command(SmtLibCommand(name=smtcmd.CHECK_SAT,
                                     args=[]))

    return script

 def test_get_logic(self):
     for example in EXAMPLE_FORMULAS:
         target_logic = example.logic
         res = get_logic(example.expr)
         self.assertEqual(res, target_logic, "%s - %s != %s" % (example.expr, target_logic, res))

# represents the grid distance (aka Manhattan distance) of (x,y) from
# the origin.
z = Symbol("z", REAL)
distance= z.Equals(x + y)

# We want to characterize the set of points in the rectangle, in terms
# of their grid distance from the origin. In other words, we want to
# constraint z to be able to assume values that are possible within
# the rectangle. We want a formula in z that is satisfiable iff there
# is a value for z s.t.  exists a value for x,y within the rectangle.
# An example of the type of information that we expect to see is the
# maximum and minimum value of z.
f3 = Exists([x,y], rect & distance)
qe_f3 = qelim(f3)
print(qe_f3.serialize())

# Depending on the solver in use you might get a different
# result. Try: qelim(f3, solver_name="msat_fm")
#
# MathSAT Fourier Motzkin (FM) returns a compact result: (0.0
# <= z) & (z <= 15.0) , meaning that the further point in grid
# distance is at most 15.0 units away from the origin.
#
# By definition, the expression obtained after performing quantifier
# elimination is in the quantifier free fragment of the logic.  It is
# therefore possible to remove the quantifiers using qelim, and use a
# solver that does not support quantifiers natively to solve the new
# formula.
from pysmt.oracles import get_logic
print(get_logic(f3), get_logic(qe_f3))