本文整理汇总了Python中pysmt.shortcuts.is_sat函数的典型用法代码示例。如果您正苦于以下问题:Python is_sat函数的具体用法?Python is_sat怎么用?Python is_sat使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了is_sat函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_shortcuts
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"])
开发者ID:mpreiner,项目名称:pysmt,代码行数:8,代码来源:test_portfolio.py
示例2: test_div_pow
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))
开发者ID:0Chuzz,项目名称:pysmt,代码行数:9,代码来源:test_nlira.py
示例3: _verify_ackermannization
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:12,代码来源:test_rewritings.py
示例4: test_integer
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))
开发者ID:0Chuzz,项目名称:pysmt,代码行数:13,代码来源:test_nlira.py
示例5: test_conversion_error
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)
开发者ID:0Chuzz,项目名称:pysmt,代码行数:14,代码来源:test_solving.py
示例6: test_logic_as_string
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))
开发者ID:0Chuzz,项目名称:pysmt,代码行数:15,代码来源:test_solving.py
示例7: test_examples_z3
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)
开发者ID:0Chuzz,项目名称:pysmt,代码行数:7,代码来源:test_solving.py
示例8: test_examples_by_logic
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())
开发者ID:diasalvatore,项目名称:pysmt,代码行数:8,代码来源:test_solving.py
示例9: test_examples_yices
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)
开发者ID:diasalvatore,项目名称:pysmt,代码行数:8,代码来源:test_solving.py
示例10: test_exactly_one_is_sat
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")
开发者ID:bingcao,项目名称:pysmt,代码行数:8,代码来源:test_formula.py
示例11: _std_examples
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)
开发者ID:agriggio,项目名称:pysmt,代码行数:9,代码来源:test_qe.py
示例12: test_examples_btor
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
开发者ID:0Chuzz,项目名称:pysmt,代码行数:10,代码来源:test_solving.py
示例13: test_examples_msat
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:10,代码来源:test_solving.py
示例14: do_examples
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)
开发者ID:bogiebro,项目名称:pysmt,代码行数:11,代码来源:test_cnf.py
示例15: test_examples_z3
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
开发者ID:pysmt,项目名称:pysmt,代码行数:12,代码来源:test_solving.py
示例16: test_examples_btor
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)
开发者ID:pysmt,项目名称:pysmt,代码行数:12,代码来源:test_solving.py
示例17: test_examples_cvc4
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)
开发者ID:diasalvatore,项目名称:pysmt,代码行数:13,代码来源:test_solving.py
示例18: test_examples_by_logic
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")
开发者ID:0Chuzz,项目名称:pysmt,代码行数:14,代码来源:test_solving.py
示例19: test_examples
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)
开发者ID:bingcao,项目名称:pysmt,代码行数:14,代码来源:test_generic_wrapper.py
示例20: check_property
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
开发者ID:diasalvatore,项目名称:pysmt,代码行数:15,代码来源:model_checking.py
注:本文中的pysmt.shortcuts.is_sat函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论