本文整理汇总了Python中z3._get_ctx函数的典型用法代码示例。如果您正苦于以下问题:Python _get_ctx函数的具体用法?Python _get_ctx怎么用?Python _get_ctx使用的例子?那么恭喜您, 这里精选的函数代码示例或许可以为您提供帮助。
在下文中一共展示了_get_ctx函数的20个代码示例,这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞,您的评价将有助于我们的系统推荐出更棒的Python代码示例。
示例1: subpaving_tactic
def subpaving_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'subpaving'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例2: split_clause_tactic
def split_clause_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'split-clause'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例3: propagate_values_tactic
def propagate_values_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'propagate-values'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例4: sat_preprocess_tactic
def sat_preprocess_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'sat-preprocess'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例5: der_tactic
def der_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'der'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例6: fail_tactic
def fail_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fail'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例7: smt_tactic
def smt_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'smt'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例8: num_bv_consts_probe
def num_bv_consts_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-bv-consts'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例9: produce_proofs_probe
def produce_proofs_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-proofs'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例10: size_probe
def size_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'size'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例11: num_exprs_probe
def num_exprs_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-exprs'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例12: depth_probe
def depth_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'depth'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例13: add_bounds_tactic
def add_bounds_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'add-bounds'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例14: memory_probe
def memory_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'memory'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例15: arith_avg_bw_probe
def arith_avg_bw_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-avg-bw'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例16: produce_model_probe
def produce_model_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-model'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例17: is_nra_probe
def is_nra_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-nra'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例18: produce_unsat_cores_probe
def produce_unsat_cores_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-unsat-cores'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例19: simplify_tactic
def simplify_tactic(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'simplify'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
示例20: has_patterns_probe
def has_patterns_probe(ctx=None):
ctx = z3._get_ctx(ctx)
return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'has-patterns'), ctx)
开发者ID:LFY,项目名称:ssmt,代码行数:3,代码来源:z3tactics.py
注:本文中的z3._get_ctx函数示例由纯净天空整理自Github/MSDocs等源码及文档管理平台,相关代码片段筛选自各路编程大神贡献的开源项目,源码版权归原作者所有,传播和使用请参考对应项目的License;未经允许,请勿转载。 |
请发表评论