From a9a46ec1453e974c2faa67a9f3680704fd62f03b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 16:57:11 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/update_api.py | 20 -- src/bindings/python/z3.py | 1 - src/bindings/python/z3tactics.py | 360 ------------------------------- 3 files changed, 381 deletions(-) delete mode 100644 src/bindings/python/z3tactics.py diff --git a/scripts/update_api.py b/scripts/update_api.py index 8c0eb98da..aefb08d2e 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -196,25 +196,6 @@ def mk_z3tactics_py(): z3tactics.write(' ctx = z3._get_ctx(ctx)\n') z3tactics.write(' return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), \'%s\'), ctx)\n\n' % probe) -# Create .def files for DLL generation -def mk_dll_defs(): - pat1 = re.compile(".*Z3_API.*") - z3def = open('dll%sz3.def' % os.sep, 'w') - z3def.write('LIBRARY "Z3"\nEXPORTS\n') - num = 1 - for api_file in API_FILES: - api = open(api_file, 'r') - for line in api: - m = pat1.match(line) - if m: - words = re.split('\W+', line) - i = 0 - for w in words: - if w == 'Z3_API': - f = words[i+1] - z3def.write('\t%s @%s\n' % (f, num)) - i = i + 1 - num = num + 1 # # Generate logging support and bindings @@ -861,7 +842,6 @@ def def_APIs(): mk_z3consts_donet() mk_z3consts_py() mk_z3tactics_py() -mk_dll_defs() def_Types() def_APIs() mk_bindings() diff --git a/src/bindings/python/z3.py b/src/bindings/python/z3.py index 011d63851..7e3d4b1ae 100644 --- a/src/bindings/python/z3.py +++ b/src/bindings/python/z3.py @@ -41,7 +41,6 @@ failed: 'sort mismatch' from z3core import * from z3types import * from z3consts import * -from z3tactics import * from z3printer import * import io diff --git a/src/bindings/python/z3tactics.py b/src/bindings/python/z3tactics.py deleted file mode 100644 index a7f057fb7..000000000 --- a/src/bindings/python/z3tactics.py +++ /dev/null @@ -1,360 +0,0 @@ -# Automatically generated file, generator: update_api.py -import z3core -import z3 - -def simplify_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'simplify'), ctx) - -def split_clause_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'split-clause'), ctx) - -def normalize_bounds_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'normalize-bounds'), ctx) - -def elim_uncnstr_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-uncnstr'), ctx) - -def elim_and_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-and'), ctx) - -def add_bounds_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'add-bounds'), ctx) - -def aig_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'aig'), ctx) - -def skip_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'skip'), ctx) - -def fail_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fail'), ctx) - -def smt_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'smt'), ctx) - -def bit_blast_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'bit-blast'), ctx) - -def bv1_blast_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'bv1-blast'), ctx) - -def sat_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'sat'), ctx) - -def sat_preprocess_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'sat-preprocess'), ctx) - -def ctx_simplify_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'ctx-simplify'), ctx) - -def ctx_solver_simplify_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'ctx-solver-simplify'), ctx) - -def der_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'der'), ctx) - -def unit_subsume_simplify_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'unit-subsume-simplify'), ctx) - -def occf_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'occf'), ctx) - -def qe_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qe'), ctx) - -def qe_sat_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qe-sat'), ctx) - -def propagate_values_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'propagate-values'), ctx) - -def snf_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'snf'), ctx) - -def nnf_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nnf'), ctx) - -def solve_eqs_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'solve-eqs'), ctx) - -def max_bv_sharing_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'max-bv-sharing'), ctx) - -def elim_term_ite_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'elim-term-ite'), ctx) - -def fix_dl_var_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fix-dl-var'), ctx) - -def tseitin_cnf_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'tseitin-cnf'), ctx) - -def tseitin_cnf_core_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'tseitin-cnf-core'), ctx) - -def degree_shift_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'degree-shift'), ctx) - -def purify_arith_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'purify-arith'), ctx) - -def nlsat_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nlsat'), ctx) - -def factor_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'factor'), ctx) - -def fm_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fm'), ctx) - -def fail_if_undecided_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fail-if-undecided'), ctx) - -def diff_neq_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'diff-neq'), ctx) - -def lia2pb_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'lia2pb'), ctx) - -def fpa2bv_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'fpa2bv'), ctx) - -def qffpa_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qffpa'), ctx) - -def pb2bv_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'pb2bv'), ctx) - -def recover_01_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'recover-01'), ctx) - -def symmetry_reduce_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'symmetry-reduce'), ctx) - -def distribute_forall_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'distribute-forall'), ctx) - -def reduce_args_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'reduce-args'), ctx) - -def reduce_bv_size_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'reduce-bv-size'), ctx) - -def propagate_ineqs_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'propagate-ineqs'), ctx) - -def cofactor_term_ite_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'cofactor-term-ite'), ctx) - -def mip_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'mip'), ctx) - -def nla2bv_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'nla2bv'), ctx) - -def vsubst_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'vsubst'), ctx) - -def qfbv_sls_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfbv-sls'), ctx) - -def qflia_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qflia'), ctx) - -def qflra_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qflra'), ctx) - -def qfnia_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfnia'), ctx) - -def qfnra_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfnra'), ctx) - -def qfnra_nlsat_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfnra-nlsat'), ctx) - -def qfbv_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'qfbv'), ctx) - -def subpaving_tactic(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Tactic(z3core.Z3_mk_tactic(ctx.ref(), 'subpaving'), ctx) - -def memory_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'memory'), ctx) - -def depth_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'depth'), ctx) - -def size_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'size'), ctx) - -def num_exprs_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-exprs'), ctx) - -def num_consts_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-consts'), ctx) - -def num_bool_consts_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-bool-consts'), ctx) - -def num_arith_consts_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'num-arith-consts'), ctx) - -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) - -def produce_proofs_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-proofs'), ctx) - -def produce_model_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'produce-model'), ctx) - -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) - -def has_patterns_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'has-patterns'), ctx) - -def is_propositional_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-propositional'), ctx) - -def is_qfbv_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfbv'), ctx) - -def is_qfbv_eq_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfbv-eq'), ctx) - -def is_qflia_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflia'), ctx) - -def is_qflra_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflra'), ctx) - -def is_qflira_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qflira'), ctx) - -def is_ilp_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-ilp'), ctx) - -def is_mip_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-mip'), ctx) - -def is_unbounded_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-unbounded'), ctx) - -def is_pb_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-pb'), ctx) - -def arith_max_deg_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-max-deg'), ctx) - -def arith_avg_deg_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-avg-deg'), ctx) - -def arith_max_bw_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'arith-max-bw'), ctx) - -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) - -def is_qfnia_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfnia'), ctx) - -def is_qfnra_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-qfnra'), ctx) - -def is_nia_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-nia'), ctx) - -def is_nra_probe(ctx=None): - ctx = z3._get_ctx(ctx) - return z3.Probe(z3core.Z3_mk_probe(ctx.ref(), 'is-nra'), ctx) -