def test_stack_env(self):
        env1 = get_env()
        push_env()
        push_env(env1)

        self.assertEqual(env1, pop_env(), "Pushed environment was ignored.")
        env2  = get_env()
        self.assertIsNotNone(env2)
        self.assertNotEqual(env1, pop_env(), "New environment was not created.")

 def test_simplify_q(self):
     simp = get_env().simplifier
     Iff = get_env().formula_manager.Iff
     for (f, _, _, logic) in get_example_formulae():
         if logic.quantifier_free: continue
         simp.validate_simplifications = True
         sf = f.simplify()
         simp.validate_simplifications = False
         self.assertValid(Iff(f, sf), solver_name='z3',
                          msg="Simplification did not provide equivalent "+
                         "result:\n f= %s\n sf = %s" % (f, sf))

    def test_with_env(self):
        env1 = get_env()
        a1 = Symbol("A", REAL)
        with Environment():
            env2 = get_env()
            self.assertIsNotNone(env2, "Context should create an environment")
            self.assertNotEqual(env1, env2, "Context should create a new environment")
            a2 = Symbol("A", REAL)
            self.assertNotEqual(a1, a2, "Symbols in different context should differ")

        a3 = Symbol("A", REAL)
        self.assertEqual(a1, a3, "Exiting a context should restore the previous environment")

    def setUp(self):
        super(TestSimpleTypeChecker, self).setUp()

        self.tc = get_env().stc
        self.x = Symbol("x", BOOL)
        self.y = Symbol("y", BOOL)
        self.p = Symbol("p", INT)
        self.q = Symbol("q", INT)
        self.r = Symbol("r", REAL)
        self.s = Symbol("s", REAL)

        self.qfo = get_env().qfo

    def test_solver_factory_preferences(self):
        env = get_env()

        factory = env.factory
        self.assertEqual(factory.solver_preference_list,
                          pysmt.factory.DEFAULT_SOLVER_PREFERENCE_LIST)

        for solver_name in factory.all_solvers(logic=logics.QF_UFLIRA):
            factory.set_solver_preference_list([solver_name])
            self.assertEqual(factory.solver_preference_list, [solver_name])
            solver = factory.get_solver(logic=logics.QF_UFLIRA)
            self.assertTrue(isinstance(solver, factory.all_solvers()[solver_name]))

        factory.set_solver_preference_list(['nosolver'])
        with self.assertRaises(NoSolverAvailableError):
            factory.get_solver()

        for qelim_name in factory.all_quantifier_eliminators():
            factory.set_qelim_preference_list([qelim_name])
            self.assertEqual(factory.qelim_preference_list, [qelim_name])
            qelim = factory.get_quantifier_eliminator(logic=logics.BOOL)
            self.assertTrue(isinstance(qelim, factory.all_quantifier_eliminators()[qelim_name]))

        factory.set_qelim_preference_list(['nosolver'])
        with self.assertRaises(NoSolverAvailableError):
            factory.get_quantifier_eliminator()

    def get_last_formula(self, mgr=None):
        """Returns the last formula of the execution of the Script.

        This coincides with the conjunction of the assertions that are
        left on the assertion stack at the end of the SMTLibScript.
        """
        stack = []
        backtrack = []
        _And = mgr.And if mgr else get_env().formula_manager.And

        for cmd in self.commands:
            if cmd.name == smtcmd.ASSERT:
                stack.append(cmd.args[0])
            if cmd.name == smtcmd.RESET_ASSERTIONS:
                stack = []
                backtrack = []
            elif cmd.name == smtcmd.PUSH:
                for _ in xrange(cmd.args[0]):
                    backtrack.append(len(stack))
            elif cmd.name == smtcmd.POP:
                for _ in xrange(cmd.args[0]):
                    l = backtrack.pop()
                    stack = stack[:l]

        return _And(stack)

    def test_cannot_replace_global_walkers(self):
        env = get_env()

        # Check that environment contains standard walkers
        self.assertIsNotNone(env.formula_manager)
        self.assertIsNotNone(env.substituter)
        self.assertIsNotNone(env.simplifier)
        self.assertIsNotNone(env.serializer)
        self.assertIsNotNone(env.stc)

        # Cannot modify these elements
        with self.assertRaises(AttributeError):
            env.formula_manager = None

        with self.assertRaises(AttributeError):
            env.substituter = None

        with self.assertRaises(AttributeError):
            env.simplifier = None

        with self.assertRaises(AttributeError):
            env.serializer = None

        with self.assertRaises(AttributeError):
            env.stc = None

 def __call__(self, test_fun):
     msg = "Quantifier Eliminator for %s not available" % self.logic
     cond = len(get_env().factory.all_quantifier_eliminators(logic=self.logic)) == 0
     @unittest.skipIf(cond, msg)
     @wraps(test_fun)
     def wrapper(*args, **kwargs):
         return test_fun(*args, **kwargs)
     return wrapper

 def __init__(self, assignment, environment=None):
     if environment is None:
         environment = get_env()
     Model.__init__(self, environment)
     self.environment = environment
     self.assignment = assignment
     # Create a copy of the assignments to memoize completions
     self.completed_assignment = dict(self.assignment)

def check_installed(required_solvers, install_dir, bindings_dir, mirror_link):
    """Checks which solvers are visible to pySMT."""

    # Check which solvers are accessible from the Factory
    pypath_solvers = get_env().factory.all_solvers()

    global_solvers_status = []
    print("Installed Solvers:")
    for i in INSTALLERS:
        installer_ = i.InstallerClass(install_dir=install_dir,
                                      bindings_dir=bindings_dir,
                                      solver_version=i.version,
                                      mirror_link=mirror_link,
                                      **i.extra_params)
        solver = installer_.SOLVER
        version = installer_.get_installed_version()
        is_installed = (version is not None)
        global_solvers_status.append((solver, is_installed, version))
        del installer_

    for solver in required_solvers:
        if solver not in pypath_solvers:
            raise PysmtException("Was expecting to find %s installed" % solver)

    #
    # Output information
    #
    for (solver, is_installed, version) in global_solvers_status:
        msg = "  %s%s " % (solver.ljust(10), is_installed)
        msg += ("(%s)" % version).ljust(20)
        if solver not in pypath_solvers:
            msg += "Not in Python's path!"
        print(msg)
    print("")


    print("Solvers: %s" % ", ".join(name for name in pypath_solvers))
    qes = get_env().factory.all_quantifier_eliminators()
    print("Quantifier Eliminators: %s" % ", ".join(name for name in qes))

    ucs = get_env().factory.all_unsat_core_solvers()
    print("UNSAT-Cores: %s" % ", ".join(name for name in ucs))

    interps = get_env().factory.all_interpolators()
    print("Interpolators: %s" % ", ".join(name for name in interps))

def skipIfNoSolverAvailable(test_fun):
    """Skip the test if no solver is available."""

    msg = "No solver available"
    cond = len(get_env().factory.all_solvers()) == 0
    @unittest.skipIf(cond, msg)
    @wraps(test_fun)
    def wrapper(self, *args, **kwargs):
        return test_fun(self, *args, **kwargs)
    return wrapper

    def __init__(self, env=None):
        if env is None:
            env = get_env()
        self.env = env
        self.mgr = env.formula_manager
        self.get_type = env.stc.get_type

        self.rules = []
        self.scanner = None
        self.eoi = EndOfInput()

    def __init__(self, stream, template=".def_%d"):
        DagWalker.__init__(self, invalidate_memoization=True)
        self.stream = stream
        self.write = self.stream.write
        self.openings = 0
        self.name_seed = 0
        self.template = template
        self.names = None
        self.mgr = get_env().formula_manager

        self.set_function(partial(self._walk_nary, "and"), op.AND)
        self.set_function(partial(self._walk_nary, "or"), op.OR)
        self.set_function(partial(self._walk_nary, "not"), op.NOT)
        self.set_function(partial(self._walk_nary, "=>"), op.IMPLIES)
        self.set_function(partial(self._walk_nary, "="), op.IFF)
        self.set_function(partial(self._walk_nary, "+"), op.PLUS)
        self.set_function(partial(self._walk_nary, "-"), op.MINUS)
        self.set_function(partial(self._walk_nary, "*"), op.TIMES)
        self.set_function(partial(self._walk_nary, "pow"), op.POW)
        self.set_function(partial(self._walk_nary, "="), op.EQUALS)
        self.set_function(partial(self._walk_nary, "<="), op.LE)
        self.set_function(partial(self._walk_nary, "<"), op.LT)
        self.set_function(partial(self._walk_nary, "ite"), op.ITE)
        self.set_function(partial(self._walk_nary, "to_real"), op.TOREAL)
        self.set_function(partial(self._walk_nary, "/"), op.DIV)

        self.set_function(partial(self._walk_nary, "bvand"), op.BV_AND)
        self.set_function(partial(self._walk_nary, "bvor"), op.BV_OR)
        self.set_function(partial(self._walk_nary, "bvnot"), op.BV_NOT)
        self.set_function(partial(self._walk_nary, "bvxor"), op.BV_XOR)
        self.set_function(partial(self._walk_nary, "bvadd"), op.BV_ADD)
        self.set_function(partial(self._walk_nary, "bvsub"), op.BV_SUB)
        self.set_function(partial(self._walk_nary, "bvneg"), op.BV_NEG)
        self.set_function(partial(self._walk_nary, "bvmul"), op.BV_MUL)
        self.set_function(partial(self._walk_nary, "bvudiv"), op.BV_UDIV)
        self.set_function(partial(self._walk_nary, "bvurem"), op.BV_UREM)
        self.set_function(partial(self._walk_nary, "bvshl"), op.BV_LSHL)
        self.set_function(partial(self._walk_nary, "bvlshr"), op.BV_LSHR)
        self.set_function(partial(self._walk_nary, "bvult"), op.BV_ULT)
        self.set_function(partial(self._walk_nary, "bvule"), op.BV_ULE)
        self.set_function(partial(self._walk_nary, "bvslt"), op.BV_SLT)
        self.set_function(partial(self._walk_nary, "bvsle"), op.BV_SLE)
        self.set_function(partial(self._walk_nary, "concat"), op.BV_CONCAT)
        self.set_function(partial(self._walk_nary, "bvcomp"), op.BV_COMP)
        self.set_function(partial(self._walk_nary, "bvashr"), op.BV_ASHR)
        self.set_function(partial(self._walk_nary, "bvsdiv"), op.BV_SDIV)
        self.set_function(partial(self._walk_nary, "bvsrem"), op.BV_SREM)
        self.set_function(self.walk_bv_extract, op.BV_EXTRACT)
        self.set_function(self.walk_bv_rotate, op.BV_ROR)
        self.set_function(self.walk_bv_rotate, op.BV_ROL)
        self.set_function(self.walk_bv_extend, op.BV_SEXT)
        self.set_function(self.walk_bv_extend, op.BV_ZEXT)

        self.set_function(partial(self._walk_nary, "select"), op.ARRAY_SELECT)
        self.set_function(partial(self._walk_nary, "store"), op.ARRAY_STORE)

    def get_strict_formula(self, mgr=None):
        if self.contains_command(smtcmd.PUSH) or \
           self.contains_command(smtcmd.POP):
            raise PysmtValueError("Was not expecting push-pop commands")
        if self.count_command_occurrences(smtcmd.CHECK_SAT) != 1:
            raise PysmtValueError("Was expecting exactly one check-sat command")
        _And = mgr.And if mgr else get_env().formula_manager.And

        assertions = [cmd.args[0]
                      for cmd in self.filter_by_command_name([smtcmd.ASSERT])]
        return _And(assertions)

 def test_simplify_qf(self):
     simp = get_env().simplifier
     for (f, _, _, logic) in get_example_formulae():
         if logic.is_quantified(): continue
         sname = "z3" if not logic.theory.strings else "cvc4"
         simp.validate_simplifications = sname
         sf = f.simplify()
         simp.validate_simplifications = None
         self.assertValid(Iff(f, sf), solver_name=sname,
                          msg="Simplification did not provide equivalent "+
                             "result:\n f= %s\n sf = %s" % (f, sf))

def _run_solver(idx, solver, options, formula, signaling_queue, ctrl_pipe):
    """Function used by the child Process to handle Portfolio requests.

    solver  : name of the solver
    options : options for the solver
    formula : formula to assert
    signaling_queue: queue in which to write to indicate completion of solve
    ctrl_pipe: Pipe to communicate with parent process *after* solve
    """
    from pysmt.environment import get_env

    Solver = get_env().factory.Solver
    with Solver(name=solver, **options) as s:
        s.add_assertion(formula)
        try:
            local_res = s.solve()
        except Exception as ex:
            signaling_queue.put((solver, ex))
            return

        signaling_queue.put((idx, local_res))
        _exit = False
        while not _exit:
            try:
                cmd = ctrl_pipe.recv()
            except EOFError:
                break
            if type(cmd) == tuple:
                cmd, args = cmd
            if cmd == "exit":
                _exit = True
            elif cmd == "get_model":
                # MG: Can we pickle the EagerModel directly?
                # Note: contextualization happens on the receiver side
                model = list(s.get_model())
                ctrl_pipe.send(model)
            elif cmd == "get_value":
                args = get_env().formula_manager.normalize(args)
                ctrl_pipe.send(s.get_value(args))
            else:
                raise ValueError("Unknown command '%s'" % cmd)

    def __init__(self, environment=None):
        self.pysmt_env = get_env() if environment is None else environment

        # Placeholders for fields filled by self._reset
        self._current_env = None
        self.cache = None
        self.logic = None
        self._reset()

        # Special tokens appearing in expressions
        self.parentheses = set(["(", ")"])
        self.specials = set(["let", "!", "exists", "forall"])

    def test_boolean(self):
        varA = Symbol("At", INT)
        varB = Symbol("Bt", INT)

        f = And(LT(varA, Plus(varB, Int(1))),
                GT(varA, Minus(varB, Int(1))))
        g = Equals(varA, varB)
        h = Iff(f, g)

        tc = get_env().stc
        res = tc.walk(h)
        self.assertEqual(res, BOOL)

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 __init__(self, stream):
        TreeWalker.__init__(self)
        self.stream = stream
        self.write = self.stream.write
        self.mgr = get_env().formula_manager


        self.set_function(partial(self._walk_nary, "and"), op.AND)
        self.set_function(partial(self._walk_nary, "or"), op.OR)
        self.set_function(partial(self._walk_nary, "not"), op.NOT)
        self.set_function(partial(self._walk_nary, "=>"), op.IMPLIES)
        self.set_function(partial(self._walk_nary, "="), op.IFF)
        self.set_function(partial(self._walk_nary, "+"), op.PLUS)
        self.set_function(partial(self._walk_nary, "-"), op.MINUS)
        self.set_function(partial(self._walk_nary, "*"), op.TIMES)
        self.set_function(partial(self._walk_nary, "="), op.EQUALS)
        self.set_function(partial(self._walk_nary, "<="), op.LE)
        self.set_function(partial(self._walk_nary, "<"), op.LT)
        self.set_function(partial(self._walk_nary, "ite"), op.ITE)
        self.set_function(partial(self._walk_nary, "to_real"), op.TOREAL)

        self.set_function(partial(self._walk_nary, "bvand"), op.BV_AND)
        self.set_function(partial(self._walk_nary, "bvor"), op.BV_OR)
        self.set_function(partial(self._walk_nary, "bvnot"), op.BV_NOT)
        self.set_function(partial(self._walk_nary, "bvxor"), op.BV_XOR)
        self.set_function(partial(self._walk_nary, "bvadd"), op.BV_ADD)
        self.set_function(partial(self._walk_nary, "bvsub"), op.BV_SUB)
        self.set_function(partial(self._walk_nary, "bvneg"), op.BV_NEG)
        self.set_function(partial(self._walk_nary, "bvmul"), op.BV_MUL)
        self.set_function(partial(self._walk_nary, "bvudiv"), op.BV_UDIV)
        self.set_function(partial(self._walk_nary, "bvurem"), op.BV_UREM)
        self.set_function(partial(self._walk_nary, "bvshl"), op.BV_LSHL)
        self.set_function(partial(self._walk_nary, "bvlshr"), op.BV_LSHR)
        self.set_function(partial(self._walk_nary, "bvult"), op.BV_ULT)
        self.set_function(partial(self._walk_nary, "bvule"), op.BV_ULE)
        self.set_function(partial(self._walk_nary, "bvslt"), op.BV_SLT)
        self.set_function(partial(self._walk_nary, "bvsle"), op.BV_SLE)
        self.set_function(partial(self._walk_nary, "concat"), op.BV_CONCAT)
        self.set_function(partial(self._walk_nary, "bvcomp"), op.BV_COMP)
        self.set_function(partial(self._walk_nary, "bvashr"), op.BV_ASHR)
        self.set_function(partial(self._walk_nary, "bvsdiv"), op.BV_SDIV)
        self.set_function(partial(self._walk_nary, "bvsrem"), op.BV_SREM)
        self.set_function(self.walk_bv_extract, op.BV_EXTRACT)
        self.set_function(self.walk_bv_rotate, op.BV_ROR)
        self.set_function(self.walk_bv_rotate, op.BV_ROL)
        self.set_function(self.walk_bv_extend, op.BV_ZEXT)
        self.set_function(self.walk_bv_extend, op.BV_SEXT)