本文整理汇总了Python中pysmt.oracles.get_logic函数的典型用法代码示例。如果您正苦于以下问题:Python get_logic函数的具体用法?Python get_logic怎么用?Python get_logic使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了get_logic函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: eliminate_quantifiers
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
开发者ID:mpreiner,项目名称:pysmt,代码行数:31,代码来源:z3.py
示例2: smtlibscript_from_formula
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
开发者ID:0Chuzz,项目名称:pysmt,代码行数:32,代码来源:script.py
示例3: sequence_interpolant
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)
开发者ID:sureshgl,项目名称:pysmt,代码行数:7,代码来源:factory.py
示例4: is_unsat
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)
开发者ID:sureshgl,项目名称:pysmt,代码行数:7,代码来源:factory.py
示例5: _check_logic
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))
开发者ID:mpreiner,项目名称:pysmt,代码行数:7,代码来源:z3.py
示例6: get_implicant
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:25,代码来源:factory.py
示例7: binary_interpolant
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)
开发者ID:bogiebro,项目名称:pysmt,代码行数:8,代码来源:factory.py
示例8: all_smt
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)))
开发者ID:agriggio,项目名称:pysmt,代码行数:9,代码来源:allsmt.py
示例9: eliminate_quantifiers
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
开发者ID:diasalvatore,项目名称:pysmt,代码行数:10,代码来源:bdd.py
示例10: get_model
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
开发者ID:sureshgl,项目名称:pysmt,代码行数:10,代码来源:factory.py
示例11: get_model
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
开发者ID:bogiebro,项目名称:pysmt,代码行数:11,代码来源:factory.py
示例12: test_theory_oracle
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)
开发者ID:mpreiner,项目名称:pysmt,代码行数:21,代码来源:test_string.py
示例13: is_unsat
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:13,代码来源:factory.py
示例14: simplify
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
开发者ID:agriggio,项目名称:pysmt,代码行数:13,代码来源:simplifier.py
示例15: get_unsat_core
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()
开发者ID:sureshgl,项目名称:pysmt,代码行数:14,代码来源:factory.py
示例16: 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
示例17: exist_elim
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)
开发者ID:diasalvatore,项目名称:pysmt,代码行数:17,代码来源:msat.py
示例18: smtlibscript_from_formula
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
开发者ID:diasalvatore,项目名称:pysmt,代码行数:23,代码来源:script.py
示例19: test_get_logic
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))
开发者ID:diasalvatore,项目名称:pysmt,代码行数:5,代码来源:test_oracles.py
示例20: distance
# 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))
开发者ID:mpreiner,项目名称:pysmt,代码行数:30,代码来源:qe.py
注:本文中的pysmt.oracles.get_logic函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论