From 8a4f6d571968d9db22bd2d2abf10f636e0ff76bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 15:06:40 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 7 ++++-- src/dead/install_tactics.cpp | 29 +++++++--------------- src/tactic/aig/aig_tactic.h | 4 ++- src/tactic/arith/add_bounds_tactic.h | 4 +++ src/tactic/arith/normalize_bounds_tactic.h | 4 +++ src/tactic/bv/bit_blaster_tactic.h | 4 ++- src/tactic/core/distribute_forall_tactic.h | 4 +++ src/tactic/core/elim_term_ite_tactic.h | 4 +++ src/tactic/core/elim_uncnstr_tactic.h | 3 +++ src/tactic/core/nnf_tactic.h | 5 ++++ src/tactic/core/occf_tactic.h | 4 +++ src/tactic/core/propagate_values_tactic.h | 4 +++ src/tactic/core/simplify_tactic.h | 5 ++++ src/tactic/core/solve_eqs_tactic.h | 4 +++ src/tactic/core/split_clause_tactic.h | 4 +++ src/tactic/core/symmetry_reduce_tactic.h | 4 +++ src/tactic/smt/smt_tactic.h | 4 +++ src/tactic/tactic.h | 5 ++++ 18 files changed, 78 insertions(+), 24 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 93d4504c9..0a98d8ce1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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: diff --git a/src/dead/install_tactics.cpp b/src/dead/install_tactics.cpp index 6d5ebb13c..7655a263f 100644 --- a/src/dead/install_tactics.cpp +++ b/src/dead/install_tactics.cpp @@ -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); diff --git a/src/tactic/aig/aig_tactic.h b/src/tactic/aig/aig_tactic.h index f635a8865..fad07d2b6 100644 --- a/src/tactic/aig/aig_tactic.h +++ b/src/tactic/aig/aig_tactic.h @@ -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 diff --git a/src/tactic/arith/add_bounds_tactic.h b/src/tactic/arith/add_bounds_tactic.h index 97b63e1ad..75566efba 100644 --- a/src/tactic/arith/add_bounds_tactic.h +++ b/src/tactic/arith/add_bounds_tactic.h @@ -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 diff --git a/src/tactic/arith/normalize_bounds_tactic.h b/src/tactic/arith/normalize_bounds_tactic.h index 8805a221e..a4bcc2a91 100644 --- a/src/tactic/arith/normalize_bounds_tactic.h +++ b/src/tactic/arith/normalize_bounds_tactic.h @@ -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 diff --git a/src/tactic/bv/bit_blaster_tactic.h b/src/tactic/bv/bit_blaster_tactic.h index 1454be703..4ffab2fcb 100644 --- a/src/tactic/bv/bit_blaster_tactic.h +++ b/src/tactic/bv/bit_blaster_tactic.h @@ -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 diff --git a/src/tactic/core/distribute_forall_tactic.h b/src/tactic/core/distribute_forall_tactic.h index ac722e61c..0c3b4c91d 100644 --- a/src/tactic/core/distribute_forall_tactic.h +++ b/src/tactic/core/distribute_forall_tactic.h @@ -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 diff --git a/src/tactic/core/elim_term_ite_tactic.h b/src/tactic/core/elim_term_ite_tactic.h index 9bc0a9294..81ca86a11 100644 --- a/src/tactic/core/elim_term_ite_tactic.h +++ b/src/tactic/core/elim_term_ite_tactic.h @@ -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 diff --git a/src/tactic/core/elim_uncnstr_tactic.h b/src/tactic/core/elim_uncnstr_tactic.h index d83c49262..8c5605c3c 100644 --- a/src/tactic/core/elim_uncnstr_tactic.h +++ b/src/tactic/core/elim_uncnstr_tactic.h @@ -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 diff --git a/src/tactic/core/nnf_tactic.h b/src/tactic/core/nnf_tactic.h index 573031af3..b007bf6f9 100644 --- a/src/tactic/core/nnf_tactic.h +++ b/src/tactic/core/nnf_tactic.h @@ -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 diff --git a/src/tactic/core/occf_tactic.h b/src/tactic/core/occf_tactic.h index 06acf1d4e..7bd3c5b23 100644 --- a/src/tactic/core/occf_tactic.h +++ b/src/tactic/core/occf_tactic.h @@ -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 diff --git a/src/tactic/core/propagate_values_tactic.h b/src/tactic/core/propagate_values_tactic.h index 6a5e5a1ef..f5ef200b7 100644 --- a/src/tactic/core/propagate_values_tactic.h +++ b/src/tactic/core/propagate_values_tactic.h @@ -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 diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index c186dc365..fc9cb393c 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -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 diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index 9554d238a..4c0f5cc3b 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -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 diff --git a/src/tactic/core/split_clause_tactic.h b/src/tactic/core/split_clause_tactic.h index 695e0d700..7c716938b 100644 --- a/src/tactic/core/split_clause_tactic.h +++ b/src/tactic/core/split_clause_tactic.h @@ -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 diff --git a/src/tactic/core/symmetry_reduce_tactic.h b/src/tactic/core/symmetry_reduce_tactic.h index 4d0a93a57..f663e8525 100644 --- a/src/tactic/core/symmetry_reduce_tactic.h +++ b/src/tactic/core/symmetry_reduce_tactic.h @@ -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 diff --git a/src/tactic/smt/smt_tactic.h b/src/tactic/smt/smt_tactic.h index d570e2bfe..521a454f7 100644 --- a/src/tactic/smt/smt_tactic.h +++ b/src/tactic/smt/smt_tactic.h @@ -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 diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index fb443cd41..55eeafac9 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -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);