本文整理汇总了Python中pysmt.smtlib.parser.SmtLibParser类的典型用法代码示例。如果您正苦于以下问题:Python SmtLibParser类的具体用法?Python SmtLibParser怎么用?Python SmtLibParser使用的例子?那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。
在下文中一共展示了SmtLibParser类的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: TestParserExtensibility
class TestParserExtensibility(TestCase):
def setUp(self):
self.ts_parser = TSSmtLibParser()
self.smt_parser = SmtLibParser()
def test_wrong(self):
txt = """
(declare-fun A () Bool)
(declare-fun B () Bool)
(assert (and A B))
(check-sat)
(exit)
"""
with self.assertRaises(UnknownSmtLibCommandError):
self.ts_parser.get_ts(cStringIO(txt))
script = self.smt_parser.get_script(cStringIO(txt))
self.assertIsNotNone(script)
def test_basic(self):
txt = """
(declare-fun A () Bool)
(declare-fun B () Bool)
(init (and A B))
(trans (=> A (next A)))
(exit)
"""
with self.assertRaises(UnknownSmtLibCommandError):
self.smt_parser.get_script(cStringIO(txt))
ts = self.ts_parser.get_ts(cStringIO(txt))
self.assertIsNotNone(ts)
开发者ID:bingcao,项目名称:pysmt,代码行数:31,代码来源:test_parser_extensibility.py
示例2: parse
def parse(self, file_id):
fname = SMTLIB_FILE_PATTERN % file_id
reset_env()
parser = SmtLibParser()
script = parser.get_script_fname(fname)
self.assertIsNotNone(script)
return script
开发者ID:mpreiner,项目名称:pysmt,代码行数:7,代码来源:test_griggio.py
示例3: test_parse_bvconst_width
def test_parse_bvconst_width(self):
smtlib_input = "(assert (> #x10 #x10))"
parser = SmtLibParser()
buffer_ = cStringIO(smtlib_input)
expr = parser.get_script(buffer_).get_last_formula()
const = expr.args()[0]
self.assertEqual(const.bv_width(), 8, const.bv_width())
开发者ID:mpreiner,项目名称:pysmt,代码行数:7,代码来源:test_regressions.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: __init__
def __init__(self, env=None, interactive=False):
SmtLibParser.__init__(self, env, interactive)
# Add new commands
#
# The mapping function takes care of consuming the command
# name from the input stream, e.g., '(init' . Therefore,
# _cmd_init will receive the rest of the stream, in our
# example, '(and A B)) ...'
self.commands["init"] = self._cmd_init
self.commands["trans"] = self._cmd_trans
# Remove unused commands
#
# If some commands are not compatible with the extension, they
# can be removed from the parser. If found, they will cause
# the raising of the exception UnknownSmtLibCommandError
del self.commands["check-sat"]
del self.commands["get-value"]
# ...
# Add 'next' function
#
# New operators can be added similarly as done for commands.
# e.g., 'next'. The helper function _operator_adapter,
# simplifies the writing of such extensions. In this example,
# we will rewrite the content of the next without the need of
# introducing a new pySMT operator. If you are interested in a
# simple way of handling new operators in pySMT see
# pysmt.test.test_dwf.
self.interpreted["next"] = self._operator_adapter(self._next_var)
开发者ID:agriggio,项目名称:pysmt,代码行数:31,代码来源:smtlib.py
示例6: test_define_funs_arg_and_fun
def test_define_funs_arg_and_fun(self):
smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(declare-fun n () Real)'])
stream = cStringIO(smtlib_script)
parser = SmtLibParser()
_ = parser.get_script(stream)
# No exceptions are thrown
self.assertTrue(True)
开发者ID:pysmt,项目名称:pysmt,代码行数:7,代码来源:test_smtlibscript.py
示例7: test_smtlib_define_fun_serialization
def test_smtlib_define_fun_serialization(self):
smtlib_input = "(define-fun init ((x Bool)) Bool (and x (and x (and x (and x (and x (and x x)))))))"
parser = SmtLibParser()
buffer_ = cStringIO(smtlib_input)
s = parser.get_script(buffer_)
for c in s:
res = c.serialize_to_string(daggify=False)
self.assertEqual(res.replace('__x0', 'x'), smtlib_input)
开发者ID:mpreiner,项目名称:pysmt,代码行数:8,代码来源:test_regressions.py
示例8: test_define_funs_same_args
def test_define_funs_same_args(self):
# n is defined once as an Int and once as a Real
smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(define-fun f ((n Real)) Real n)'])
stream = cStringIO(smtlib_script)
parser = SmtLibParser()
_ = parser.get_script(stream)
# No exceptions are thrown
self.assertTrue(True)
开发者ID:pysmt,项目名称:pysmt,代码行数:8,代码来源:test_smtlibscript.py
示例9: test_parse_declare_const
def test_parse_declare_const(self):
smtlib_input = """
(declare-const s Int)
(check-sat)"""
parser = SmtLibParser()
buffer_ = cStringIO(smtlib_input)
script = parser.get_script(buffer_)
self.assertIsNotNone(script)
开发者ID:mpreiner,项目名称:pysmt,代码行数:8,代码来源:test_regressions.py
示例10: smtlib_solver
def smtlib_solver(self, stream):
smt_parser = SmtLibParser()
name = self.args.solver
if name == "auto":
solver = Solver()
else:
solver = Solver(name=name)
for cmd in smt_parser.get_command_generator(stream):
r = evaluate_command(cmd, solver)
self.print_result(cmd, r)
开发者ID:0Chuzz,项目名称:pysmt,代码行数:11,代码来源:shell.py
示例11: test_complex_annotations_values
def test_complex_annotations_values(self):
source ="""\
(declare-fun |"v__AT0"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next (+ 1 meaningless)))
"""
buf = StringIO(source)
parser = SmtLibParser()
script = parser.get_script(buf)
ann = script.annotations
v0 = self.env.formula_manager.get_symbol('"v__AT0"')
v1_str = next(iter(ann[v0]["next"]))
self.assertEquals(v1_str, "(+ 1 meaningless)")
开发者ID:agriggio,项目名称:pysmt,代码行数:12,代码来源:test_annotations.py
示例12: test_parse_exception
def test_parse_exception(self):
from pysmt.exceptions import PysmtSyntaxError
smtlib_input = "(declare-const x x x Int)" +\
"(check-sat)"
parser = SmtLibParser()
buffer_ = cStringIO(smtlib_input)
try:
parser.get_script(buffer_)
self.assertFalse(True)
except PysmtSyntaxError as ex:
self.assertEqual(ex.pos_info[0], 0)
self.assertEqual(ex.pos_info[1], 19)
开发者ID:mpreiner,项目名称:pysmt,代码行数:12,代码来源:test_regressions.py
示例13: test_annotations_colon_values
def test_annotations_colon_values(self):
source ="""\
(declare-fun |"v__AT0"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next :this_is_considered_a_value))
"""
buf = StringIO(source)
parser = SmtLibParser()
script = parser.get_script(buf)
ann = script.annotations
v0 = self.env.formula_manager.get_symbol('"v__AT0"')
v1_str = next(iter(ann[v0]["next"]))
self.assertEquals(v1_str, ":this_is_considered_a_value")
开发者ID:agriggio,项目名称:pysmt,代码行数:12,代码来源:test_annotations.py
示例14: test_all_parsing
def test_all_parsing(self):
# Create a small file that tests all commands of smt-lib 2
parser = SmtLibParser()
nie = 0
for cmd in DEMO_SMTSCRIPT:
try:
next(parser.get_command_generator(cStringIO(cmd)))
except NotImplementedError:
nie += 1
# There are currently 3 not-implemented commands
self.assertEquals(nie, 3)
开发者ID:mpreiner,项目名称:pysmt,代码行数:12,代码来源:test_smtlibscript.py
示例15: test_string_constant_quote_escaping_parsing
def test_string_constant_quote_escaping_parsing(self):
script = """
(declare-const x String)
(assert (= x "a""b"))
(assert (= x "\"\""))
(assert (= x "\"\"\"\""))
"""
p = SmtLibParser()
buffer = cStringIO(script)
s = p.get_script(buffer)
self.assertEqual('a"b', s.commands[1].args[0].arg(1).constant_value())
self.assertEqual('"', s.commands[2].args[0].arg(1).constant_value())
self.assertEqual('""', s.commands[3].args[0].arg(1).constant_value())
开发者ID:mpreiner,项目名称:pysmt,代码行数:14,代码来源:test_regressions.py
示例16: __init__
def __init__(self, env=None, interactive=False):
SmtLibParser.__init__(self, env, interactive)
# Add new commands
self.commands["init"] = self._cmd_init
self.commands["trans"] = self._cmd_trans
# Remove unused commands
del self.commands["check-sat"]
del self.commands["get-value"]
# ...
# Add 'next' function
self.interpreted["next"] = self._operator_adapter(self._next_var)
开发者ID:bingcao,项目名称:pysmt,代码行数:14,代码来源:test_parser_extensibility.py
示例17: test_interpreting_annotations
def test_interpreting_annotations(self):
source ="""\
(declare-fun |"v__AT0"| () Bool)
(declare-fun |"v__AT1"| () Bool)
(define-fun .def_1 () Bool (! |"v__AT0"| :next |"v__AT1"|))
"""
buf = StringIO(source)
parser = SmtLibParser()
script = parser.get_script(buf)
ann = script.annotations
v0 = self.env.formula_manager.get_symbol('"v__AT0"')
v1_str = next(iter(ann[v0]["next"]))
self.env.formula_manager.get_symbol(v1_str)
self.assertEquals(v1_str, '"v__AT1"')
开发者ID:agriggio,项目名称:pysmt,代码行数:14,代码来源:test_annotations.py
示例18: test_parse_examples_daggified_bv
def test_parse_examples_daggified_bv(self):
fs = get_example_formulae()
for (f_out, _, _, logic) in fs:
if logic != logics.QF_BV:
# See test_parse_examples_daggified
continue
buf_out = cStringIO()
script_out = smtlibscript_from_formula(f_out)
script_out.serialize(outstream=buf_out, daggify=True)
buf_in = cStringIO(buf_out.getvalue())
parser = SmtLibParser()
script_in = parser.get_script(buf_in)
f_in = script_in.get_last_formula()
self.assertValid(Iff(f_in, f_out), f_in.serialize())
开发者ID:mpreiner,项目名称:pysmt,代码行数:15,代码来源:test_parser_examples.py
示例19: __init__
def __init__(self, args, environment, logic, LOGICS=None, **options):
Solver.__init__(self,
environment,
logic=logic,
**options)
self.to = self.environment.typeso
if LOGICS is not None: self.LOGICS = LOGICS
self.args = args
self.declared_vars = set()
self.declared_sorts = set()
self.solver = Popen(args, stdout=PIPE, stderr=PIPE, stdin=PIPE,
bufsize=-1)
# Give time to the process to start-up
time.sleep(0.01)
self.parser = SmtLibParser(interactive=True)
if PY2:
self.solver_stdin = self.solver.stdin
self.solver_stdout = self.solver.stdout
else:
self.solver_stdin = TextIOWrapper(self.solver.stdin)
self.solver_stdout = TextIOWrapper(self.solver.stdout)
# Initialize solver
self.options(self)
self.set_logic(logic)
开发者ID:pysmt,项目名称:pysmt,代码行数:25,代码来源:solver.py
示例20: test_parse_examples
def test_parse_examples(self):
fs = get_example_formulae()
for (f_out, _, _, logic) in fs:
if logic == logics.QF_BV:
# See test_parse_examples_bv
continue
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)
f_in = script_in.get_last_formula()
self.assertEqual(f_in.simplify(), f_out.simplify())
开发者ID:0Chuzz,项目名称:pysmt,代码行数:16,代码来源:test_parser_examples.py
注:本文中的pysmt.smtlib.parser.SmtLibParser类示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论