3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-25 15:06:40 -07:00
parent 760b12c4cb
commit 8a4f6d5719
18 changed files with 78 additions and 24 deletions

View file

@ -571,7 +571,7 @@ 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(.*)')
pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
for cname in cnames:
c = _Name2Component[cname]
h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
@ -580,7 +580,10 @@ def mk_install_tactic_cpp(cnames, path):
for line in fin:
if pat.match(line):
fout.write('#include"%s"\n' % h_file)
exec line.strip('\n ') in globals()
try:
exec line.strip('\n ') in globals()
except:
raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
# First pass will just generate the tactic factories
idx = 0
for data in ADD_TACTIC_DATA:

View file

@ -137,33 +137,23 @@ MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))
void install_tactics(tactic_manager & ctx) {
ADD_TACTIC_CMD("simplify", "apply simplification rules.", simplifier_fct);
ADD_TACTIC_CMD("split-clause", "split a clause in many subgoals.", split_clause_fct);
ADD_TACTIC_CMD("normalize-bounds", "replace a variable x with lower bound k <= x with x' = x - k.", normalize_bounds_fct);
ADD_TACTIC_CMD("elim-uncnstr", "eliminate application containing unconstrained variables.", elim_uncnstr_fct);
ADD_TACTIC_CMD("elim-and", "convert (and a b) into (not (or (not a) (not b))).", elim_and_fct);
ADD_TACTIC_CMD("add-bounds", "add bounds to unbounded variables (under approximation).", add_bounds_fct);
ADD_TACTIC_CMD("aig", "simplify Boolean structure using AIGs.", aig_fct);
ADD_TACTIC_CMD("skip", "do nothing tactic.", skip_fct);
ADD_TACTIC_CMD("fail", "always fail tactic.", fail_fct);
ADD_TACTIC_CMD("smt", "apply a SAT based SMT solver.", smt_fct);
ADD_TACTIC_CMD("bit-blast", "reduce bit-vector expressions into SAT.", bitblaster_fct);
ADD_TACTIC_CMD("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", bv1blaster_fct);
ADD_TACTIC_CMD("sat", "(try to) solve goal using a SAT solver.", sat_fct);
ADD_TACTIC_CMD("sat-preprocess", "Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).", sat_preprocess_fct);
ADD_TACTIC_CMD("ctx-simplify", "apply contextual simplification rules.", ctx_simplify_fct);
ADD_TACTIC_CMD("ctx-solver-simplify", "apply solver-based contextual simplification rules.", ctx_solver_simplify_fct);
ADD_TACTIC_CMD("der", "destructive equality resolution.", der_fct);
ADD_TACTIC_CMD("unit-subsume-simplify", "unit subsumption simplification.", unit_subsume_fct);
ADD_TACTIC_CMD("occf", "put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered).", occf_fct);
ADD_TACTIC_CMD("qe", "apply quantifier elimination.", qe_fct);
ADD_TACTIC_CMD("qe-sat", "check satisfiability of quantified formulas using quantifier elimination.", qe_sat_fct);
ADD_TACTIC_CMD("propagate-values", "propagate constants.", propagate_values_fct);
ADD_TACTIC_CMD("snf", "put goal in skolem normal form.", snf_fct);
ADD_TACTIC_CMD("nnf", "put goal in negation normal form.", nnf_fct);
ADD_TACTIC_CMD("solve-eqs", "eliminate variables by solving equations.", solve_eqs_fct);
ADD_TACTIC_CMD("max-bv-sharing", "use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.", max_bv_sharing_fct);
ADD_TACTIC_CMD("elim-term-ite", "eliminate term if-then-else by adding fresh auxiliary declarations.", elim_term_ite_fct);
ADD_TACTIC_CMD("fix-dl-var", "if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0.",
fix_dl_var_fct);
ADD_TACTIC_CMD("tseitin-cnf", "convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).", tseitin_cnf_fct);
@ -180,7 +170,6 @@ void install_tactics(tactic_manager & ctx) {
ADD_TACTIC_CMD("qffpa", "(try to) solve goal using the tactic for QF_FPA.", qffpa_fct);
ADD_TACTIC_CMD("pb2bv", "convert pseudo-boolean constraints to bit-vectors.", pb2bv_fct);
ADD_TACTIC_CMD("recover-01", "recover 0-1 variables hidden as Boolean variables.", recover_01_fct);
ADD_TACTIC_CMD("symmetry-reduce", "apply symmetry reduction.", symmetry_reduce_fct);
ADD_TACTIC_CMD("distribute-forall", "distribute forall over conjunctions.", distribute_forall_fct);
ADD_TACTIC_CMD("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.",
reduce_args_fct);

View file

@ -23,5 +23,7 @@ Notes:
class tactic;
tactic * mk_aig_tactic(params_ref const & p = params_ref());
/*
ADD_TACTIC("aig", "simplify Boolean structure using AIGs.", "mk_aig_tactic")
*/
#endif

View file

@ -31,4 +31,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)")
*/
#endif

View file

@ -27,4 +27,8 @@ class tactic;
tactic * mk_normalize_bounds_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("normalize-bounds", "replace a variable x with lower bound k <= x with x' = x - k.", "mk_normalize_bounds_tactic(m, p)")
*/
#endif

View file

@ -24,5 +24,7 @@ class ast_manager;
class tactic;
tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("bit-blast", "reduce bit-vector expressions into SAT.", "mk_bit_blaster_tactic(m, p)")
*/
#endif

View file

@ -23,4 +23,8 @@ class tactic;
tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("distribute-forall", "distribute forall over conjunctions.", "mk_distribute_forall_tactic(m, p)")
*/
#endif

View file

@ -26,4 +26,8 @@ class tactic;
tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("elim-term-ite", "eliminate term if-then-else by adding fresh auxiliary declarations.", "mk_elim_term_ite_tactic(m, p)")
*/
#endif

View file

@ -26,5 +26,8 @@ class ast_manager;
tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("elim-uncnstr", "eliminate application containing unconstrained variables.", "mk_elim_uncnstr_tactic(m, p)")
*/
#endif

View file

@ -26,5 +26,10 @@ class tactic;
tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("snf", "put goal in skolem normal form.", "mk_snf_tactic(m, p)")
ADD_TACTIC("nnf", "put goal in negation normal form.", "mk_nnf_tactic(m, p)")
*/
#endif

View file

@ -30,5 +30,9 @@ class tactic;
tactic * mk_occf_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("occf", "put goal in one constraint per clause normal form (notes: fails if proof generation is enabled; only clauses are considered).", "mk_occf_tactic(m, p)")
*/
#endif

View file

@ -26,4 +26,8 @@ class tactic;
tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC_CMD("propagate-values", "propagate constants.", "mk_propagate_values_tactic(m, p)")
*/
#endif

View file

@ -51,4 +51,9 @@ public:
tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("simplify", "apply simplification rules.", "mk_simplify_tactic(m, p)")
ADD_TACTIC("elim-and", "convert (and a b) into (not (or (not a) (not b))).", "mk_elim_and_tactic(m, p)")
*/
#endif

View file

@ -26,5 +26,9 @@ class expr_replacer;
tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref(), expr_replacer * r = 0);
/*
ADD_TACTIC("solve-eqs", "eliminate variables by solving equations.", "mk_solve_eqs_tactic(m, p)")
*/
#endif

View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_split_clause_tactic(params_ref const & p = params_ref());
/*
ADD_TACTIC("split-clause", "split a clause in many subgoals.", "mk_split_clause_tactic(p)")
*/
#endif

View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("symmetry-reduce", "apply symmetry reduction.", "mk_symmetry_reduce_tactic(m, p)")
*/
#endif

View file

@ -27,4 +27,8 @@ tactic * mk_smt_tactic(params_ref const & p = params_ref());
// syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
*/
#endif

View file

@ -128,6 +128,11 @@ tactic * mk_skip_tactic();
tactic * mk_fail_tactic();
tactic * mk_fail_if_undecided_tactic();
/*
ADD_TACTIC("skip", "do nothing tactic.", "mk_skip_tactic()")
ADD_TACTIC("fail", "always fail tactic.", "mk_fail_tactic()")
*/
tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
tactic * mk_trace_tactic(char const * tag);