本文整理汇总了Python中pysmt.environment.get_env函数的典型用法代码示例。如果您正苦于以下问题:Python get_env函数的具体用法?Python get_env怎么用?Python get_env使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了get_env函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_stack_env
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.")
开发者ID:agriggio,项目名称:pysmt,代码行数:9,代码来源:test_env.py
示例2: test_simplify_q
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))
开发者ID:0Chuzz,项目名称:pysmt,代码行数:11,代码来源:test_simplify.py
示例3: test_with_env
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")
开发者ID:agriggio,项目名称:pysmt,代码行数:12,代码来源:test_env.py
示例4: setUp
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
开发者ID:diasalvatore,项目名称:pysmt,代码行数:12,代码来源:test_typechecker.py
示例5: test_solver_factory_preferences
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()
开发者ID:agriggio,项目名称:pysmt,代码行数:26,代码来源:test_env.py
示例6: get_last_formula
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:25,代码来源:script.py
示例7: test_cannot_replace_global_walkers
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
开发者ID:agriggio,项目名称:pysmt,代码行数:25,代码来源:test_env.py
示例8: __call__
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
开发者ID:pysmt,项目名称:pysmt,代码行数:8,代码来源:__init__.py
示例9: __init__
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)
开发者ID:bogiebro,项目名称:pysmt,代码行数:8,代码来源:eager.py
示例10: check_installed
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))
开发者ID:pysmt,项目名称:pysmt,代码行数:45,代码来源:install.py
示例11: skipIfNoSolverAvailable
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
开发者ID:diasalvatore,项目名称:pysmt,代码行数:10,代码来源:__init__.py
示例12: __init__
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()
开发者ID:agriggio,项目名称:pysmt,代码行数:10,代码来源:parsing.py
示例13: __init__
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)
开发者ID:agriggio,项目名称:pysmt,代码行数:55,代码来源:printers.py
示例14: get_strict_formula
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:11,代码来源:script.py
示例15: test_simplify_qf
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))
开发者ID:pysmt,项目名称:pysmt,代码行数:11,代码来源:test_simplify.py
示例16: _run_solver
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)
开发者ID:agriggio,项目名称:pysmt,代码行数:41,代码来源:portfolio.py
示例17: __init__
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"])
开发者ID:bogiebro,项目名称:pysmt,代码行数:12,代码来源:parser.py
示例18: test_boolean
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)
开发者ID:diasalvatore,项目名称:pysmt,代码行数:12,代码来源:test_typechecker.py
示例19: smtlibscript_from_formula
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
开发者ID:pysmt,项目名称:pysmt,代码行数:47,代码来源:script.py
示例20: __init__
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)
开发者ID:bogiebro,项目名称:pysmt,代码行数:47,代码来源:printers.py
注:本文中的pysmt.environment.get_env函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论