diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 6583caa00..a2ee92926 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -70,8 +70,6 @@ add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_n mk_auto_src() update_version(4, 2, 0, 0) -mk_all_install_tactic_cpps() - # mk_makefile() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0a98d8ce1..bdf385031 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -395,7 +395,7 @@ def reg_component(name, c): _ComponentNames.add(name) _Name2Component[name] = c if VERBOSE: - print "Processed '%s'" % name + print "New component: '%s'" % name def add_lib(name, deps=[], path=None): c = LibComponent(name, path, deps) @@ -464,6 +464,7 @@ def mk_makefile(): def mk_auto_src(): if not ONLY_MAKEFILES: mk_pat_db() + mk_all_install_tactic_cpps() # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h @@ -552,18 +553,23 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is print "Updated %s" % assemblyinfo ADD_TACTIC_DATA=[] +ADD_PROBE_DATA=[] def ADD_TACTIC(name, descr, cmd): global ADD_TACTIC_DATA ADD_TACTIC_DATA.append((name, descr, cmd)) +def ADD_PROBE(name, descr, cmd): + global ADD_PROBE_DATA + ADD_PROBE_DATA.append((name, descr, cmd)) + # Generate an install_tactics.cpp at path. # This file implements the procedure # void install_tactics(tactic_manager & ctx) # It installs all tactics in the given component (name) list cnames # The procedure looks for ADD_TACTIC commands in the .h files of these components. def mk_install_tactic_cpp(cnames, path): - global ADD_TACTIC_DATA + global ADD_TACTIC_DATA, ADD_PROBE_DATA ADD_TACTIC_DATA = [] fullname = '%s/install_tactic.cpp' % path fout = open(fullname, 'w') @@ -571,19 +577,31 @@ def mk_install_tactic_cpp(cnames, path): fout.write('#include"tactic.h"\n') fout.write('#include"tactic_cmds.h"\n') fout.write('#include"cmd_context.h"\n') - pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') + tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') + probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') for cname in cnames: c = _Name2Component[cname] h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir)) for h_file in h_files: + added_include = False fin = open("%s/%s" % (c.src_dir, h_file), 'r') for line in fin: - if pat.match(line): - fout.write('#include"%s"\n' % h_file) + if tactic_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) try: exec line.strip('\n ') in globals() except: raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line)) + if probe_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + try: + exec line.strip('\n ') in globals() + except: + raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) # First pass will just generate the tactic factories idx = 0 for data in ADD_TACTIC_DATA: @@ -596,6 +614,8 @@ def mk_install_tactic_cpp(cnames, path): for data in ADD_TACTIC_DATA: fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) idx = idx + 1 + for data in ADD_PROBE_DATA: + fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) fout.write('}\n') if VERBOSE: print "Generated '%s'" % fullname diff --git a/src/dead/install_tactics.cpp b/src/dead/install_tactics.cpp deleted file mode 100644 index cde80ebee..000000000 --- a/src/dead/install_tactics.cpp +++ /dev/null @@ -1,178 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - install_tactics.cpp - -Abstract: - Install tactics in the SMT 2.0 frontend. - -Author: - - Leonardo (leonardo) 2012-02-19 - -Notes: - ---*/ -#include"tactic_cmds.h" -#include"cmd_context.h" -#include"simplify_tactic.h" -#include"split_clause_tactic.h" -#include"normalize_bounds_tactic.h" -#include"elim_uncnstr_tactic.h" -#include"add_bounds_tactic.h" -#include"ctx_simplify_tactic.h" -#include"ctx_solver_simplify_tactic.h" - -#include"bit_blaster_tactic.h" -#include"bv1_blaster_tactic.h" -#include"der_tactic.h" -#include"aig_tactic.h" -#include"smt_tactic.h" -#include"sat_tactic.h" -#include"occf_tactic.h" -#include"qe_tactic.h" -#include"qe_sat_tactic.h" -#include"propagate_values_tactic.h" -#include"nnf_tactic.h" -#include"solve_eqs_tactic.h" -#include"max_bv_sharing_tactic.h" -#include"elim_term_ite_tactic.h" -#include"fix_dl_var_tactic.h" -#include"tseitin_cnf_tactic.h" -#include"degree_shift_tactic.h" -#include"purify_arith_tactic.h" -#include"nla2bv_tactic.h" -#include"nlsat_tactic.h" -#include"factor_tactic.h" -#include"fm_tactic.h" -#include"diff_neq_tactic.h" -#include"lia2pb_tactic.h" -#include"fpa2bv_tactic.h" -#include"qffpa_tactic.h" -#include"pb2bv_tactic.h" -#include"recover_01_tactic.h" -#include"symmetry_reduce_tactic.h" -#include"distribute_forall_tactic.h" -#include"reduce_args_tactic.h" -#include"bv_size_reduction_tactic.h" -#include"propagate_ineqs_tactic.h" -#include"cofactor_term_ite_tactic.h" -// include"mip_tactic.h" -#include"vsubst_tactic.h" -#include"sls_tactic.h" -#include"probe_arith.h" -#include"qflia_tactic.h" -#include"qflra_tactic.h" -#include"qfnia_tactic.h" -#include"qfnra_tactic.h" -#include"qfbv_tactic.h" -#include"subpaving_tactic.h" -#include"unit_subsumption_tactic.h" -#include"qfnra_nlsat_tactic.h" -#include"ufbv_tactic.h" - -MK_SIMPLE_TACTIC_FACTORY(simplifier_fct, mk_simplify_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(split_clause_fct, mk_split_clause_tactic(p)); -MK_SIMPLE_TACTIC_FACTORY(normalize_bounds_fct, mk_normalize_bounds_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(elim_uncnstr_fct, mk_elim_uncnstr_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(add_bounds_fct, mk_add_bounds_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(bitblaster_fct, mk_bit_blaster_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(bv1blaster_fct, mk_bv1_blaster_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(aig_fct, mk_aig_tactic(p)); -MK_SIMPLE_TACTIC_FACTORY(skip_fct, mk_skip_tactic()); -MK_SIMPLE_TACTIC_FACTORY(fail_fct, mk_fail_tactic()); -MK_SIMPLE_TACTIC_FACTORY(smt_fct, mk_smt_tactic(p)); -MK_SIMPLE_TACTIC_FACTORY(sat_fct, mk_sat_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(sat_preprocess_fct, mk_sat_preprocessor_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(ctx_simplify_fct, mk_ctx_simplify_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(ctx_solver_simplify_fct, mk_ctx_solver_simplify_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(unit_subsume_fct, mk_unit_subsumption_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(der_fct, mk_der_tactic(m)); -MK_SIMPLE_TACTIC_FACTORY(occf_fct, mk_occf_tactic(m)); -MK_SIMPLE_TACTIC_FACTORY(qe_fct, mk_qe_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qe_sat_fct, qe::mk_sat_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(propagate_values_fct, mk_propagate_values_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(snf_fct, mk_snf_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(nnf_fct, mk_nnf_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(solve_eqs_fct, mk_solve_eqs_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(max_bv_sharing_fct, mk_max_bv_sharing_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(elim_term_ite_fct, mk_elim_term_ite_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(fix_dl_var_fct, mk_fix_dl_var_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(tseitin_cnf_fct, mk_tseitin_cnf_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(tseitin_cnf_core_fct, mk_tseitin_cnf_core_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(degree_shift_fct, mk_degree_shift_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(purify_arith_fct, mk_purify_arith_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(nlsat_fct, mk_nlsat_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(factor_fct, mk_factor_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(fm_fct, mk_fm_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(fail_if_undecided_fct, mk_fail_if_undecided_tactic()); -MK_SIMPLE_TACTIC_FACTORY(diff_neq_fct, mk_diff_neq_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(lia2pb_fct, mk_lia2pb_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(fpa2bv_fct, mk_fpa2bv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(pb2bv_fct, mk_pb2bv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(recover_01_fct, mk_recover_01_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(elim_and_fct, mk_elim_and_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(symmetry_reduce_fct, mk_symmetry_reduce_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(distribute_forall_fct, mk_distribute_forall_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(reduce_args_fct, mk_reduce_args_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(bv_size_reduction_fct, mk_bv_size_reduction_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(propagate_ineqs_fct, mk_propagate_ineqs_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(cofactor_term_ite_fct, mk_cofactor_term_ite_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(nla2bv_fct, mk_nla2bv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(vsubst_fct, mk_vsubst_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfbv_sls_fct, mk_qfbv_sls_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(subpaving_fct, mk_subpaving_tactic(m, p)); - -MK_SIMPLE_TACTIC_FACTORY(qflia_fct, mk_qflia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qflra_fct, mk_qflra_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfbv_fct, mk_qfbv_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p)); -MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p)); - -#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY))) -#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE)) - -void install_tactics(tactic_manager & ctx) { - - - ADD_TACTIC_CMD("ctx-solver-simplify", "apply solver-based contextual simplification rules.", ctx_solver_simplify_fct); - ADD_TACTIC_CMD("unit-subsume-simplify", "unit subsumption simplification.", unit_subsume_fct); - - - ADD_PROBE("memory", "ammount of used memory in megabytes.", mk_memory_probe()); - ADD_PROBE("depth", "depth of the input goal.", mk_depth_probe()); - ADD_PROBE("size", "number of assertions in the given goal.", mk_size_probe()); - ADD_PROBE("num-exprs", "number of expressions/terms in the given goal.", mk_num_exprs_probe()); - ADD_PROBE("num-consts", "number of non Boolean constants in the given goal.", mk_num_consts_probe()); - ADD_PROBE("num-bool-consts", "number of Boolean constants in the given goal.", mk_num_bool_consts_probe()); - ADD_PROBE("num-arith-consts", "number of arithmetic constants in the given goal.", mk_num_arith_consts_probe()); - ADD_PROBE("num-bv-consts", "number of bit-vector constants in the given goal.", mk_num_bv_consts_probe()); - ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", mk_produce_proofs_probe()); - ADD_PROBE("produce-model", "true if model generation is enabled for the given goal.", mk_produce_models_probe()); - ADD_PROBE("produce-unsat-cores", "true if unsat-core generation is enabled for the given goal.", mk_produce_unsat_cores_probe()); - ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", mk_has_pattern_probe()); - ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", mk_is_propositional_probe()); - ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", mk_is_qfbv_probe()); - ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", mk_is_qfbv_eq_probe()); - ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", mk_is_qflia_probe()); - ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", mk_is_qflra_probe()); - ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", mk_is_qflira_probe()); - ADD_PROBE("is-ilp", "true if the goal is ILP.", mk_is_ilp_probe()); - ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", mk_is_unbounded_probe()); - ADD_PROBE("is-pb", "true if the goal is a pseudo-boolean problem.", mk_is_pb_probe()); - ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", mk_arith_max_degree_probe()); - ADD_PROBE("arith-avg-deg", "avg polynomial total degree of an arithmetic atom.", mk_arith_avg_degree_probe()); - ADD_PROBE("arith-max-bw", "max coefficient bit width.", mk_arith_max_bw_probe()); - ADD_PROBE("arith-avg-bw", "avg coefficient bit width.", mk_arith_avg_bw_probe()); - - ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", mk_is_qfnia_probe()); - ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", mk_is_qfnra_probe()); - ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", mk_is_nia_probe()); - ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", mk_is_nra_probe()); -} - - diff --git a/src/dead/install_tactics.h b/src/dead/install_tactics.h deleted file mode 100644 index da0c829f1..000000000 --- a/src/dead/install_tactics.h +++ /dev/null @@ -1,24 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - install_tactics.h - -Abstract: - Install tactics in the SMT 2.0 frontend. - -Author: - - Leonardo (leonardo) 2012-02-19 - -Notes: - ---*/ -#ifndef _INSTALL_TACTICS_H_ -#define _INSTALL_TACTICS_H_ - -class tactic_manager; -void install_tactics(tactic_manager & ctx); - -#endif diff --git a/src/muz_qe/unit_subsumption_tactic.h b/src/muz_qe/unit_subsumption_tactic.h index df5968113..5a7aac99b 100644 --- a/src/muz_qe/unit_subsumption_tactic.h +++ b/src/muz_qe/unit_subsumption_tactic.h @@ -26,5 +26,8 @@ Notes: #include "tactic.h" tactic * mk_unit_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("unit-subsume-simplify", "unit subsumption simplification.", "mk_unit_subsumption_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/add_bounds_tactic.h b/src/tactic/arith/add_bounds_tactic.h index 75566efba..4bd94f373 100644 --- a/src/tactic/arith/add_bounds_tactic.h +++ b/src/tactic/arith/add_bounds_tactic.h @@ -32,7 +32,8 @@ probe * mk_is_unbounded_probe(); tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p = params_ref()); /* - ADD_TACTIC("add-bounds", "add bounds to unbounded variables (under approximation).", "mk_add_bounds_tactic(m, p)") + ADD_TACTIC("add-bounds", "add bounds to unbounded variables (under approximation).", "mk_add_bounds_tactic(m, p)") + ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", "mk_is_unbounded_probe()") */ #endif diff --git a/src/tactic/arith/pb2bv_tactic.h b/src/tactic/arith/pb2bv_tactic.h index 1398477d6..329bd8f99 100644 --- a/src/tactic/arith/pb2bv_tactic.h +++ b/src/tactic/arith/pb2bv_tactic.h @@ -30,4 +30,8 @@ tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); probe * mk_is_pb_probe(); +/* + ADD_PROBE("is-pb", "true if the goal is a pseudo-boolean problem.", "mk_is_pb_probe()") +*/ + #endif diff --git a/src/tactic/arith/probe_arith.h b/src/tactic/arith/probe_arith.h index 3824027db..829bcfab8 100644 --- a/src/tactic/arith/probe_arith.h +++ b/src/tactic/arith/probe_arith.h @@ -25,15 +25,35 @@ probe * mk_arith_max_bw_probe(); probe * mk_arith_avg_degree_probe(); probe * mk_arith_max_degree_probe(); +/* + ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", "mk_arith_max_degree_probe()") + ADD_PROBE("arith-avg-deg", "avg polynomial total degree of an arithmetic atom.", "mk_arith_avg_degree_probe()") + ADD_PROBE("arith-max-bw", "max coefficient bit width.", "mk_arith_max_bw_probe()") + ADD_PROBE("arith-avg-bw", "avg coefficient bit width.", "mk_arith_avg_bw_probe()") +*/ + probe * mk_is_qflia_probe(); probe * mk_is_qflra_probe(); probe * mk_is_qflira_probe(); probe * mk_is_ilp_probe(); probe * mk_is_mip_probe(); +/* + ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", "mk_is_qflia_probe()") + ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", "mk_is_qflra_probe()") + ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", "mk_is_qflira_probe()") + ADD_PROBE("is-ilp", "true if the goal is ILP.", "mk_is_ilp_probe()") +*/ + probe * mk_is_qfnia_probe(); probe * mk_is_qfnra_probe(); probe * mk_is_nia_probe(); probe * mk_is_nra_probe(); +/* + ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()") + ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", "mk_is_qfnra_probe()") + ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", "mk_is_nia_probe()") + ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", "mk_is_nra_probe()") +*/ #endif diff --git a/src/tactic/bv/bv1_blaster_tactic.h b/src/tactic/bv/bv1_blaster_tactic.h index cdc42b7b8..9429ac983 100644 --- a/src/tactic/bv/bv1_blaster_tactic.h +++ b/src/tactic/bv/bv1_blaster_tactic.h @@ -33,5 +33,6 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_re probe * mk_is_qfbv_eq_probe(); /* ADD_TACTIC("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "mk_bv1_blaster_tactic(m, p)") + ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", "mk_is_qfbv_eq_probe()") */ #endif diff --git a/src/tactic/probe.h b/src/tactic/probe.h index 269480b15..2f61b340f 100644 --- a/src/tactic/probe.h +++ b/src/tactic/probe.h @@ -55,20 +55,44 @@ public: typedef ref probe_ref; +probe * mk_const_probe(double val); + probe * mk_memory_probe(); probe * mk_depth_probe(); probe * mk_size_probe(); + +/* + ADD_PROBE("memory", "ammount of used memory in megabytes.", "mk_memory_probe()") + ADD_PROBE("depth", "depth of the input goal.", "mk_depth_probe()") + ADD_PROBE("size", "number of assertions in the given goal.", "mk_size_probe()") +*/ + probe * mk_num_exprs_probe(); -probe * mk_const_probe(double val); probe * mk_num_consts_probe(); probe * mk_num_bool_consts_probe(); probe * mk_num_arith_consts_probe(); probe * mk_num_bv_consts_probe(); + +/* + ADD_PROBE("num-exprs", "number of expressions/terms in the given goal.", "mk_num_exprs_probe()") + ADD_PROBE("num-consts", "number of non Boolean constants in the given goal.", "mk_num_consts_probe()") + ADD_PROBE("num-bool-consts", "number of Boolean constants in the given goal.", "mk_num_bool_consts_probe()") + ADD_PROBE("num-arith-consts", "number of arithmetic constants in the given goal.", "mk_num_arith_consts_probe()") + ADD_PROBE("num-bv-consts", "number of bit-vector constants in the given goal.", "mk_num_bv_consts_probe()") +*/ + probe * mk_produce_proofs_probe(); probe * mk_produce_models_probe(); probe * mk_produce_unsat_cores_probe(); probe * mk_has_pattern_probe(); +/* + ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", "mk_produce_proofs_probe()") + ADD_PROBE("produce-model", "true if model generation is enabled for the given goal.", "mk_produce_models_probe()") + ADD_PROBE("produce-unsat-cores", "true if unsat-core generation is enabled for the given goal.", "mk_produce_unsat_cores_probe()") + ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()") +*/ + // Some basic combinators for probes probe * mk_not(probe * p1); probe * mk_and(probe * p1, probe * p2); @@ -88,4 +112,9 @@ probe * mk_div(probe * p1, probe * p2); probe * mk_is_propositional_probe(); probe * mk_is_qfbv_probe(); +/* + ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()") + ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", "mk_is_qfbv_probe()") +*/ + #endif diff --git a/src/tactic/smt/ctx_solver_simplify_tactic.h b/src/tactic/smt/ctx_solver_simplify_tactic.h index 09467f311..378103b03 100644 --- a/src/tactic/smt/ctx_solver_simplify_tactic.h +++ b/src/tactic/smt/ctx_solver_simplify_tactic.h @@ -22,5 +22,8 @@ Notes: #include"tactical.h" tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("ctx-solver-simplify", "apply solver-based contextual simplification rules.", "mk_ctx_solver_simplify_tactic(m, p)") +*/ #endif