本文整理汇总了Python中z3.main_ctx函数的典型用法代码示例。如果您正苦于以下问题:Python main_ctx函数的具体用法?Python main_ctx怎么用?Python main_ctx使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了main_ctx函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: ResetZ3
def ResetZ3 ():
z3._main_ctx = None
z3.main_ctx()
z3.set_param('auto_config', False)
z3.set_param('smt.mbqi', True)
z3.set_param('model.compact', True)
z3.set_param('smt.pull_nested_quantifiers', True)
z3.set_param('smt.mbqi.max_iterations', 10000)
z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))
开发者ID:apanda,项目名称:modeling,代码行数:9,代码来源:num_branch_test.py
示例2: is_sat
def is_sat(solver,f):
solver.push()
ctx = z3.main_ctx()
z3.Z3_solver_assert(ctx.ref(), solver.solver, f.as_ast())
#solver.add(f)
res = solver.check() != z3.unsat
solver.pop()
return res
开发者ID:yotamfe,项目名称:ivy,代码行数:8,代码来源:ivy_alpha.py
示例3: string_regexdigit
def string_regexdigit():
ctx = z3.main_ctx()
decl = z3strlib.z3str_regexdigit_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例4: string_unroll
def string_unroll():
ctx = z3.main_ctx()
decl = z3strlib.z3str_unroll_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例5: string_replace
def string_replace():
ctx = z3.main_ctx()
decl = z3strlib.z3str_replace_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例6: StringSort
z3strlib.z3str_regexunion_decl.argtypes = []
z3strlib.z3str_regexconcat_decl.restype = z3.FuncDecl
z3strlib.z3str_regexconcat_decl.argtypes = []
z3strlib.z3str_unroll_decl.restype = z3.FuncDecl
z3strlib.z3str_unroll_decl.argtypes = []
z3strlib.z3str_regexdigit_decl.restype = z3.FuncDecl
z3strlib.z3str_regexdigit_decl.argtypes = []
z3strlib.z3str_register_vars.restype = None
z3strlib.z3str_register_vars.argtypes = [z3.Ast]
z3strlib.setAlphabet.restype = None
z3strlib.setAlphabet.argtypes = []
z3strlib.setAlphabet7bit.restype = None
z3strlib.setAlphabet7bit.argtypes = []
## Set the default Z3py context to use z3str
ctx = z3.main_ctx()
ctx.ctx = z3strlib.z3str_context()
z3strlib.setAlphabet7bit()
## Wrappers around the various z3str_*() functions in libz3str2.so
def StringSort():
ctx = z3.main_ctx()
sort = z3strlib.z3str_mk_string_sort()
return z3.SortRef(sort, ctx)
def RegexSort():
ctx = z3.main_ctx()
sort = z3strlib.z3str_mk_regex_sort()
return z3.SortRef(sort, ctx)
def string_concat():
开发者ID:sukwon0709,项目名称:byterun,代码行数:31,代码来源:z3str2.py
示例7: my_eq
def my_eq(x, y):
ctx = z3.main_ctx()
# print "my_eq: {} = {}".format(x,y)
return z3.BoolRef(z3.Z3_mk_eq(ctx.ref(), x.as_ast(), y.as_ast()), ctx)
开发者ID:odedp,项目名称:ivy,代码行数:4,代码来源:ivy_solver.py
示例8: string_substring
def string_substring():
ctx = z3.main_ctx()
decl = z3strlib.z3str_substring_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例9: string_concat
def string_concat():
ctx = z3.main_ctx()
decl = z3strlib.z3str_concat_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例10: __init__
def __init__(self, environment, logic=None):
QuantifierEliminator.__init__(self)
self.environment = environment
self.logic = logic
self.converter = Z3Converter(environment, z3.main_ctx())
开发者ID:mpreiner,项目名称:pysmt,代码行数:5,代码来源:z3.py
示例11: ResetZ3
def ResetZ3 ():
z3._main_ctx = None
z3.main_ctx()
z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))
z3.set_param('smt.mbqi.max_iterations', 10000)
z3.set_param('smt.mbqi.max_cexs', 100)
开发者ID:apanda,项目名称:modeling,代码行数:6,代码来源:path_length_test_neg.py
示例12: ResetZ3
def ResetZ3 ():
z3._main_ctx = None
z3.main_ctx()
z3.set_param('smt.random_seed', random.SystemRandom().randint(0, sys.maxint))
开发者ID:apanda,项目名称:modeling,代码行数:4,代码来源:policy_scaling.py
示例13: my_eq
def my_eq(x,y):
ctx = z3.main_ctx()
return z3.BoolRef(z3.Z3_mk_eq(ctx.ref(), x.as_ast(), y.as_ast()), ctx)
开发者ID:yotamfe,项目名称:ivy,代码行数:3,代码来源:ivy_alpha.py
示例14: my_and
def my_and(*args):
ctx = z3.main_ctx()
_args, sz = z3._to_ast_array(args)
return z3.BoolRef(z3.Z3_mk_and(ctx.ref(), sz, _args), ctx)
开发者ID:yotamfe,项目名称:ivy,代码行数:4,代码来源:ivy_alpha.py
示例15: RegexSort
def RegexSort():
ctx = z3.main_ctx()
sort = z3strlib.z3str_mk_regex_sort()
return z3.SortRef(sort, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例16: _context
def _context(self):
try:
return self._tls.context
except AttributeError:
self._tls.context = z3.Context() if threading.current_thread().name != 'MainThread' else z3.main_ctx()
return self._tls.context
开发者ID:redragonvn,项目名称:claripy,代码行数:6,代码来源:backend_z3.py
示例17: string_length
def string_length():
ctx = z3.main_ctx()
decl = z3strlib.z3str_length_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例18: ResetZ3
def ResetZ3 (seed):
z3._main_ctx = None
z3.main_ctx()
z3.set_param('smt.random_seed', seed)
开发者ID:apanda,项目名称:modeling,代码行数:4,代码来源:fattree_pfw_test_slice.py
示例19: string_indexof
def string_indexof():
ctx = z3.main_ctx()
decl = z3strlib.z3str_indexof_decl()
return z3.FuncDeclRef(decl, ctx)
开发者ID:sukwon0709,项目名称:byterun,代码行数:4,代码来源:z3str2.py
示例20: ResetZ3
def ResetZ3 ():
z3._main_ctx = None
z3.main_ctx()
开发者ID:apanda,项目名称:modeling,代码行数:3,代码来源:perf_test.py
注:本文中的z3.main_ctx函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论