本文整理汇总了Python中pysmt.shortcuts.is_valid函数的典型用法代码示例。如果您正苦于以下问题:Python is_valid函数的具体用法?Python is_valid怎么用?Python is_valid使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了is_valid函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: test_propagate_toplevel
def test_propagate_toplevel(self):
x = Symbol("x", REAL)
y = Symbol("y", REAL)
f = And(LT(Real(4), Times(x, x)), Equals(Real(1), x))
fp = propagate_toplevel(f)
self.assertTrue(fp.is_false())
if self.env.factory.has_solvers(logic=QF_NRA):
try:
ok = is_valid(Iff(f, fp))
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
f = And(LT(Real(4), Times(x, x)), Equals(y, x), Equals(y, Real(1)))
fp = propagate_toplevel(f)
self.assertTrue(fp.is_false())
if self.env.factory.has_solvers(logic=QF_NRA):
try:
ok = is_valid(Iff(f, fp))
except SolverReturnedUnknownResultError:
ok = not logic.quantifier_free
self.assertTrue(ok)
f = And(Equals(Real(4), x), Equals(y, x), Equals(y, Real(0)))
fp = propagate_toplevel(f)
self.assertTrue(fp.is_false())
fp = propagate_toplevel(f, preserve_equivalence=False)
self.assertTrue(fp.is_false())
fp = propagate_toplevel(f, preserve_equivalence=False, do_simplify=False)
self.assertTrue(fp.is_false())
f = Equals(Real(4), Real(5))
fp = propagate_toplevel(f, do_simplify=False)
self.assertTrue(fp.is_false())
开发者ID:pysmt,项目名称:pysmt,代码行数:35,代码来源:test_rewritings.py
示例2: _validate
def _validate(self, old, new):
if self.validate_simplifications:
Iff = self.env.formula_manager.Iff
is_valid = self.env.factory.is_valid
sname = self._validation_sname
assert is_valid(Iff(old, new), solver_name=sname ), \
"Was: %s \n Obtained: %s\n" % (str(old), str(new))
开发者ID:agriggio,项目名称:pysmt,代码行数:7,代码来源:simplifier.py
示例3: 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
示例4: 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
示例5: 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
示例6: _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
示例7: 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
示例8: 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
示例9: 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
示例10: 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
示例11: 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
示例12: 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
示例13: 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
示例14: 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
示例15: 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
示例16: 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
示例17: 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
示例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_cvc4
def test_examples_cvc4(self):
for (f, validity, satisfiability, logic) in get_example_formulae():
if not logic.theory.linear: continue
if logic.theory.arrays_const: continue
try:
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)
except NoSolverAvailableError:
# Logic is not supported by CVC4
pass
开发者ID:pysmt,项目名称:pysmt,代码行数:15,代码来源:test_solving.py
示例20: walk_debug
def walk_debug(self, formula, **kwargs):
from pysmt.shortcuts import Equals, Iff, get_type, is_valid
from pysmt.typing import BOOL
if formula in self.memoization:
return self.memoization[formula]
args = [self.walk(s, **kwargs) for s in formula.args()]
f = self.functions[formula.node_type()]
res = f(formula, args=args, **kwargs)
ltype = get_type(formula)
rtype = get_type(res)
test = Equals(formula, res) if ltype != BOOL else Iff(formula, res)
assert (ltype == rtype) and is_valid(test, solver_name="z3"), \
("Was: %s \n Obtained: %s\n" % (str(formula), str(res)))
return res
开发者ID:agriggio,项目名称:pysmt,代码行数:17,代码来源:simplifier.py
注:本文中的pysmt.shortcuts.is_valid函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论