本文整理汇总了Python中pysmt.test.examples.get_example_formulae函数的典型用法代码示例。如果您正苦于以下问题:Python get_example_formulae函数的具体用法?Python get_example_formulae怎么用?Python get_example_formulae使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了get_example_formulae函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_types_oracle_examples
def test_types_oracle_examples(self):
oracle = get_env().typeso
for (f, _, _, _) in get_example_formulae():
types_all = oracle.get_types(f)
types_custom = oracle.get_types(f, custom_only=True)
# Custom types are a subset of all types
s1 = set(types_all)
s2 = set(types_custom)
self.assertTrue(s1.issuperset(s2))
# Compare logics with types
theory = self.env.theoryo.get_theory(f)
if len(f.get_free_variables()) == 0:
continue
if theory.arrays:
self.assertTrue(any(x.is_array_type() for x in types_all),
(f, types_all))
if theory.bit_vectors:
self.assertTrue(any(x.is_bv_type() for x in types_all),
(f, types_all))
if theory.integer_arithmetic:
self.assertTrue(any(x.is_int_type() for x in types_all),
(f, types_all))
if theory.real_arithmetic:
self.assertTrue(any(x.is_real_type() for x in types_all),
(f, types_all))
开发者ID:mpreiner,项目名称:pysmt,代码行数:26,代码来源:test_oracles.py
示例2: 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
示例3: test_examples_conversion
def test_examples_conversion(self):
convert = self.bdd_converter.convert
for example in get_example_formulae():
if example.logic != BOOL:
continue
expr = convert(example.expr)
self.assertIsNotNone(expr)
开发者ID:agriggio,项目名称:pysmt,代码行数:7,代码来源:test_bdd.py
示例4: test_dumped_logic
def test_dumped_logic(self):
# Dumped logic matches the logic in the example
fs = get_example_formulae()
for (f_out, _, _, logic) in fs:
buf_out = cStringIO()
script_out = smtlibscript_from_formula(f_out)
script_out.serialize(outstream=buf_out)
buf_in = cStringIO(buf_out.getvalue())
parser = SmtLibParser()
script_in = parser.get_script(buf_in)
for cmd in script_in:
if cmd.name == "set-logic":
logic_in = cmd.args[0]
if logic == logics.QF_BOOL:
self.assertEqual(logic_in, logics.QF_UF)
elif logic == logics.BOOL:
self.assertEqual(logic_in, logics.LRA)
else:
self.assertEqual(logic_in, logic, script_in)
break
else: # Loops exited normally
print("-"*40)
print(script_in)
开发者ID:0Chuzz,项目名称:pysmt,代码行数:25,代码来源:test_parser_examples.py
示例5: _helper_check_examples
def _helper_check_examples(self, solver_name):
for (f, _, satisfiability, logic) in get_example_formulae():
if not logic.quantifier_free: continue
if satisfiability == False:
with UnsatCoreSolver(name=solver_name,
unsat_cores_mode="named") as solver:
if logic not in solver.LOGICS: continue
clauses = [f]
if f.is_and():
clauses = f.args()
for i,c in enumerate(clauses):
solver.add_assertion(c, "a%d" % i)
try:
r = solver.solve()
self.assertFalse(r)
except SolverReturnedUnknownResultError:
if QF_BV <= logic:
continue # Unsat-core support for QF_UFBV might be
# incomplete
else:
raise
core = solver.get_named_unsat_core()
self.assertTrue(len(core) <= len(clauses))
for k in core.values():
self.assertIn(k, clauses)
self.assertTrue(is_unsat(And(core.values()), logic=logic))
开发者ID:agriggio,项目名称:pysmt,代码行数:31,代码来源:test_unsat_cores.py
示例6: do_model
def do_model(self, solver_name):
for (f, _, satisfiability, logic) in get_example_formulae():
if satisfiability and not logic.theory.uninterpreted and logic.quantifier_free:
try:
with Solver(name=solver_name, logic=logic) as s:
s.add_assertion(f)
check = s.solve()
self.assertTrue(check)
# Ask single values to the solver
subs = {}
for d in f.get_free_variables():
m = s.get_value(d)
subs[d] = m
simp = f.substitute(subs).simplify()
self.assertEqual(simp, TRUE(), "%s -- %s :> %s" % (f, subs, simp))
# Ask the eager model
subs = {}
model = s.get_model()
for d in f.get_free_variables():
m = model.get_value(d)
subs[d] = m
simp = f.substitute(subs).simplify()
self.assertEqual(simp, TRUE())
except NoSolverAvailableError:
pass
开发者ID:0Chuzz,项目名称:pysmt,代码行数:30,代码来源:test_solving.py
示例7: test_bdd_simplify
def test_bdd_simplify(self):
s = BddSimplifier()
for (f, _, _, logic) in get_example_formulae():
if logic == QF_BOOL:
fprime = s.simplify(f)
self.assertValid(Iff(fprime, f))
s = BddSimplifier()
try:
s.validate_simplifications = True
except ValueError:
self.assertTrue(len(self.env.factory.all_solvers())==1)
for (f, _, _, logic) in get_example_formulae():
if logic == QF_BOOL:
fprime = s.simplify(f)
self.assertValid(Iff(fprime, f))
开发者ID:agriggio,项目名称:pysmt,代码行数:16,代码来源:test_simplify.py
示例8: 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
示例9: 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
示例10: 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
示例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_propagate_toplevel_examples
def test_propagate_toplevel_examples(self):
for (f, _, _, logic) in get_example_formulae():
if self.env.factory.has_solvers(logic=logic):
rwf = propagate_toplevel(f)
try:
ok = is_valid(Iff(f, rwf), logic=logic)
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
开发者ID:pysmt,项目名称:pysmt,代码行数:9,代码来源:test_rewritings.py
示例13: test_prenex_examples
def test_prenex_examples(self):
for (f, _, _, logic) in get_example_formulae():
if self.env.factory.has_solvers(logic=logic):
prenex = prenex_normal_form(f)
try:
ok = is_valid(Iff(f, prenex), logic=logic)
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
开发者ID:agriggio,项目名称:pysmt,代码行数:9,代码来源:test_rewritings.py
示例14: test_examples_get_implicant
def test_examples_get_implicant(self):
for (f, _, satisfiability, logic) in get_example_formulae():
if logic.quantifier_free:
for sname in get_env().factory.all_solvers(logic=logic):
f_i = get_implicant(f, logic=logic, solver_name=sname)
if satisfiability:
self.assertValid(Implies(f_i, f), logic=logic, msg=(f_i, f))
else:
self.assertIsNone(f_i)
开发者ID:pysmt,项目名称:pysmt,代码行数:9,代码来源:test_solving.py
示例15: test_nnf_examples
def test_nnf_examples(self):
for (f, _, _, logic) in get_example_formulae():
if get_env().factory.has_solvers(logic=logic):
rf = nnf(f)
try:
ok = is_valid(Iff(f, rf), logic=logic)
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
开发者ID:idkwim,项目名称:pysmt,代码行数:9,代码来源:test_rewritings.py
示例16: test_conj_partitioning
def test_conj_partitioning(self):
for (f, _, _, logic) in get_example_formulae():
if get_env().factory.has_solvers(logic=logic):
conjuncts = list(conjunctive_partition(f))
try:
ok = is_valid(Iff(f, And(conjuncts)), logic=logic)
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
开发者ID:idkwim,项目名称:pysmt,代码行数:9,代码来源:test_rewritings.py
示例17: test_aig_examples
def test_aig_examples(self):
for (f, _, _, logic) in get_example_formulae():
if get_env().factory.has_solvers(logic=logic):
f_aig = aig(f)
try:
ok = is_valid(Iff(f, f_aig), logic=logic)
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok, "Was: %s\n Got:%s" % (f, f_aig))
开发者ID:bogiebro,项目名称:pysmt,代码行数:9,代码来源:test_rewritings.py
示例18: 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
示例19: test_basic
def test_basic(self):
with Portfolio(["z3", "msat", "cvc4"],
environment=self.env,
logic="QF_LRA") as p:
for example in get_example_formulae():
if not example.logic <= QF_LRA: continue
res = p.is_sat(example.expr)
self.assertEqual(res, example.is_sat, example.expr)
if res:
self.assertTrue(p.get_model().get_value(example.expr).is_true())
开发者ID:mpreiner,项目名称:pysmt,代码行数:10,代码来源:test_portfolio.py
示例20: do_back
def do_back(self, solver_name):
for formula, _, _, logic in get_example_formulae():
if logic.quantifier_free:
try:
s = Solver(name=solver_name, logic=logic)
term = s.converter.convert(formula)
res = s.converter.back(term)
self.assertValid(Iff(formula, res), logic=logic)
except NoSolverAvailableError:
pass
开发者ID:bogiebro,项目名称:pysmt,代码行数:10,代码来源:test_back.py
注:本文中的pysmt.test.examples.get_example_formulae函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论