From 1ea606092c580895686a217c8fd3daae4c5c1902 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 15:44:53 -0700 Subject: [PATCH] checkpoint Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 2 +- .../rewriter}/bit_blaster/bit_blaster.cpp | 0 .../rewriter}/bit_blaster/bit_blaster.h | 0 .../bit_blaster/bit_blaster_rewriter.cpp | 4 +- .../bit_blaster/bit_blaster_rewriter.h | 0 .../rewriter}/bit_blaster/bit_blaster_tpl.h | 0 .../bit_blaster/bit_blaster_tpl_def.h | 7 +- .../bit_blaster/eager_bit_blaster.cpp | 0 .../rewriter}/bit_blaster/eager_bit_blaster.h | 0 src/dead/install_tactics.cpp | 48 --- src/muz_qe/qe_sat_tactic.h | 4 +- src/muz_qe/qe_tactic.h | 4 +- src/muz_qe/vsubst_tactic.h | 3 + src/tactic/aig/aig_tactic.h | 2 +- src/tactic/arith/degree_shift_tactic.h | 4 + src/tactic/arith/diff_neq_tactic.h | 4 +- src/tactic/arith/factor_tactic.h | 4 +- src/tactic/arith/fix_dl_var_tactic.h | 4 + src/tactic/arith/fm_tactic.h | 3 + src/tactic/arith/lia2pb_tactic.h | 3 + src/tactic/arith/nla2bv_tactic.h | 3 + src/tactic/arith/pb2bv_tactic.h | 3 + src/tactic/arith/propagate_ineqs_tactic.h | 3 + src/tactic/arith/purify_arith_tactic.h | 4 + src/tactic/arith/recover_01_tactic.h | 3 + .../bit_blaster_model_converter.cpp | 0 .../bit_blaster_model_converter.h | 0 src/tactic/bv/bit_blaster_tactic.cpp | 8 +- .../bv1_blaster_tactic.cpp | 0 .../{bit_blaster => bv}/bv1_blaster_tactic.h | 4 +- src/tactic/bv/bv_size_reduction_tactic.h | 3 + src/tactic/bv/max_bv_sharing_tactic.h | 3 + src/tactic/core/cofactor_term_ite_tactic.h | 3 + src/tactic/core/ctx_simplify_tactic.h | 4 + src/tactic/core/der_tactic.h | 4 + src/tactic/core/reduce_args_tactic.h | 3 + src/tactic/core/tseitin_cnf_tactic.h | 5 + src/tactic/fpa/fpa2bv_tactic.h | 5 +- src/tactic/fpa/qffpa_tactic.h | 3 + src/tactic/nlsat/qfnra_nlsat_tactic.h | 4 + src/tactic/sls/sls_tactic.h | 4 +- src/tactic/smt/smt_tactic.cpp | 302 +++++++++--------- src/tactic/smtlogics/qfbv_tactic.h | 3 + src/tactic/smtlogics/qflia_tactic.h | 3 + src/tactic/smtlogics/qflra_tactic.h | 3 + src/tactic/smtlogics/qfnia_tactic.h | 3 + src/tactic/smtlogics/qfnra_tactic.h | 3 + src/tactic/subpaving/subpaving_tactic.h | 3 + src/tactic/tactic.h | 1 + src/tactic/ufbv/ufbv_tactic.h | 4 + 50 files changed, 279 insertions(+), 211 deletions(-) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster.cpp (100%) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster.h (100%) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster_rewriter.cpp (99%) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster_rewriter.h (100%) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster_tpl.h (100%) rename src/{tactic => ast/rewriter}/bit_blaster/bit_blaster_tpl_def.h (99%) rename src/{tactic => ast/rewriter}/bit_blaster/eager_bit_blaster.cpp (100%) rename src/{tactic => ast/rewriter}/bit_blaster/eager_bit_blaster.h (100%) rename src/tactic/{bit_blaster => bv}/bit_blaster_model_converter.cpp (100%) rename src/tactic/{bit_blaster => bv}/bit_blaster_model_converter.h (100%) rename src/tactic/{bit_blaster => bv}/bv1_blaster_tactic.cpp (100%) rename src/tactic/{bit_blaster => bv}/bv1_blaster_tactic.h (80%) diff --git a/scripts/mk_make.py b/scripts/mk_make.py index a2c640661..6583caa00 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -37,7 +37,7 @@ add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker') -add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster') +add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') diff --git a/src/tactic/bit_blaster/bit_blaster.cpp b/src/ast/rewriter/bit_blaster/bit_blaster.cpp similarity index 100% rename from src/tactic/bit_blaster/bit_blaster.cpp rename to src/ast/rewriter/bit_blaster/bit_blaster.cpp diff --git a/src/tactic/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h similarity index 100% rename from src/tactic/bit_blaster/bit_blaster.h rename to src/ast/rewriter/bit_blaster/bit_blaster.h diff --git a/src/tactic/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp similarity index 99% rename from src/tactic/bit_blaster/bit_blaster_rewriter.cpp rename to src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index c00ea6794..c64ea56d0 100644 --- a/src/tactic/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -139,7 +139,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("bit blaster"); if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; } @@ -307,7 +307,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); } void throw_unsupported() { - throw tactic_exception("operator is not supported, you must simplify the goal before applying bit-blasting"); + throw rewriter_exception("operator is not supported, you must simplify the goal before applying bit-blasting"); } void blast_bv_term(expr * t, expr_ref & result, proof_ref & result_pr) { diff --git a/src/tactic/bit_blaster/bit_blaster_rewriter.h b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h similarity index 100% rename from src/tactic/bit_blaster/bit_blaster_rewriter.h rename to src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h diff --git a/src/tactic/bit_blaster/bit_blaster_tpl.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h similarity index 100% rename from src/tactic/bit_blaster/bit_blaster_tpl.h rename to src/ast/rewriter/bit_blaster/bit_blaster_tpl.h diff --git a/src/tactic/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h similarity index 99% rename from src/tactic/bit_blaster/bit_blaster_tpl_def.h rename to src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 4c8ef7662..72c0a447e 100644 --- a/src/tactic/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -20,14 +20,15 @@ Revision History: #include"rational.h" #include"ast_pp.h" #include"cooperate.h" -#include"tactic_exception.h" +#include"common_msgs.h" +#include"rewriter_types.h" template void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + throw rewriter_exception(Z3_MAX_MEMORY_MSG); if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw rewriter_exception(Z3_CANCELED_MSG); cooperate("bit-blaster"); } diff --git a/src/tactic/bit_blaster/eager_bit_blaster.cpp b/src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp similarity index 100% rename from src/tactic/bit_blaster/eager_bit_blaster.cpp rename to src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp diff --git a/src/tactic/bit_blaster/eager_bit_blaster.h b/src/ast/rewriter/bit_blaster/eager_bit_blaster.h similarity index 100% rename from src/tactic/bit_blaster/eager_bit_blaster.h rename to src/ast/rewriter/bit_blaster/eager_bit_blaster.h diff --git a/src/dead/install_tactics.cpp b/src/dead/install_tactics.cpp index 7655a263f..cde80ebee 100644 --- a/src/dead/install_tactics.cpp +++ b/src/dead/install_tactics.cpp @@ -139,58 +139,10 @@ MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p)); void install_tactics(tactic_manager & ctx) { - - - - 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("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("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("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("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); - ADD_TACTIC_CMD("tseitin-cnf-core", "convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic.", tseitin_cnf_core_fct); - ADD_TACTIC_CMD("degree-shift", "try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied).", degree_shift_fct); - ADD_TACTIC_CMD("purify-arith", "eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.", purify_arith_fct); - ADD_TACTIC_CMD("nlsat", "(try to) solve goal using a nonlinear arithmetic solver.", nlsat_fct); - ADD_TACTIC_CMD("factor", "polynomial factorization.", factor_fct); - ADD_TACTIC_CMD("fm", "eliminate variables using fourier-motzkin elimination.", fm_fct); - ADD_TACTIC_CMD("fail-if-undecided", "fail if goal is undecided.", fail_if_undecided_fct); - ADD_TACTIC_CMD("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numberal, and all constants are bounded.", diff_neq_fct); - ADD_TACTIC_CMD("lia2pb", "convert bounded integer variables into a sequence of 0-1 variables.", lia2pb_fct); - ADD_TACTIC_CMD("fpa2bv", "convert floating point numbers to bit-vectors.", fpa2bv_fct); - 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("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); - ADD_TACTIC_CMD("reduce-bv-size", "try to reduce bit-vector sizes using inequalities.", bv_size_reduction_fct); - ADD_TACTIC_CMD("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", propagate_ineqs_fct); - ADD_TACTIC_CMD("cofactor-term-ite", "eliminate term if-the-else using cofactors.", cofactor_term_ite_fct); - ADD_TACTIC_CMD("nla2bv", "convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models.", nla2bv_fct); - ADD_TACTIC_CMD("vsubst", "checks satsifiability of quantifier-free non-linear constraints using virtual substitution.", vsubst_fct); - ADD_TACTIC_CMD("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", qfbv_sls_fct); - ADD_TACTIC_CMD("qflia", "builtin strategy for solving QF_LIA problems.", qflia_fct); - ADD_TACTIC_CMD("qflra", "builtin strategy for solving QF_LRA problems.", qflra_fct); - ADD_TACTIC_CMD("qfnia", "builtin strategy for solving QF_NIA problems.", qfnia_fct); - ADD_TACTIC_CMD("qfnra", "builtin strategy for solving QF_NRA problems.", qfnra_fct); - ADD_TACTIC_CMD("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", qfnra_nlsat_fct); - ADD_TACTIC_CMD("qfbv", "builtin strategy for solving QF_BV problems.", qfbv_fct); - ADD_TACTIC_CMD("ufbv", "builtin strategy for solving UFBV problems (with quantifiers).", ufbv_fct); - ADD_TACTIC_CMD("bv", "builtin strategy for solving BV problems (with quantifiers).", ufbv_fct); -#ifndef _EXTERNAL_RELEASE - ADD_TACTIC_CMD("subpaving", "tactic for testing subpaving module.", subpaving_fct); -#endif - 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()); diff --git a/src/muz_qe/qe_sat_tactic.h b/src/muz_qe/qe_sat_tactic.h index fce609aa0..c539216be 100644 --- a/src/muz_qe/qe_sat_tactic.h +++ b/src/muz_qe/qe_sat_tactic.h @@ -29,6 +29,8 @@ namespace qe { tactic * mk_sat_tactic(ast_manager& m, params_ref const& p); }; - +/* + ADD_TACTIC("qe-sat", "check satisfiability of quantified formulas using quantifier elimination.", "qe::mk_sat_tactic(m, p)") +*/ #endif diff --git a/src/muz_qe/qe_tactic.h b/src/muz_qe/qe_tactic.h index 93440a608..c49f47795 100644 --- a/src/muz_qe/qe_tactic.h +++ b/src/muz_qe/qe_tactic.h @@ -24,5 +24,7 @@ class ast_manager; class tactic; tactic * mk_qe_tactic(ast_manager & m, params_ref const & p = params_ref()); - +/* + ADD_TACTIC("qe", "apply quantifier elimination.", "mk_qe_tactic(m, p)") +*/ #endif diff --git a/src/muz_qe/vsubst_tactic.h b/src/muz_qe/vsubst_tactic.h index 3fccbafc4..b64232d60 100644 --- a/src/muz_qe/vsubst_tactic.h +++ b/src/muz_qe/vsubst_tactic.h @@ -25,6 +25,9 @@ class ast_manager; class tactic; tactic * mk_vsubst_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("vsubst", "checks satsifiability of quantifier-free non-linear constraints using virtual substitution.", "mk_vsubst_tactic(m, p)") +*/ #endif diff --git a/src/tactic/aig/aig_tactic.h b/src/tactic/aig/aig_tactic.h index fad07d2b6..a54da6226 100644 --- a/src/tactic/aig/aig_tactic.h +++ b/src/tactic/aig/aig_tactic.h @@ -24,6 +24,6 @@ class tactic; tactic * mk_aig_tactic(params_ref const & p = params_ref()); /* - ADD_TACTIC("aig", "simplify Boolean structure using AIGs.", "mk_aig_tactic") + ADD_TACTIC("aig", "simplify Boolean structure using AIGs.", "mk_aig_tactic()") */ #endif diff --git a/src/tactic/arith/degree_shift_tactic.h b/src/tactic/arith/degree_shift_tactic.h index d2406a5a4..ab8185869 100644 --- a/src/tactic/arith/degree_shift_tactic.h +++ b/src/tactic/arith/degree_shift_tactic.h @@ -28,4 +28,8 @@ class tactic; tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("degree-shift", "try to reduce degree of polynomials (remark: :mul2power simplification is automatically applied).", "mk_degree_shift_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/arith/diff_neq_tactic.h b/src/tactic/arith/diff_neq_tactic.h index a63940fde..8e19d3ceb 100644 --- a/src/tactic/arith/diff_neq_tactic.h +++ b/src/tactic/arith/diff_neq_tactic.h @@ -28,5 +28,7 @@ class ast_manager; class tactic; tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p = params_ref()); - +/* + ADD_TACTIC("diff-neq", "specialized solver for integer arithmetic problems that contain only atoms of the form (<= k x) (<= x k) and (not (= (- x y) k)), where x and y are constants and k is a numberal, and all constants are bounded.", "mk_diff_neq_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/factor_tactic.h b/src/tactic/arith/factor_tactic.h index d19b57bed..a668ce26d 100644 --- a/src/tactic/arith/factor_tactic.h +++ b/src/tactic/arith/factor_tactic.h @@ -24,5 +24,7 @@ class ast_manager; class tactic; tactic * mk_factor_tactic(ast_manager & m, params_ref const & p = params_ref()); - +/* + ADD_TACTIC("factor", "polynomial factorization.", "mk_factor_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/fix_dl_var_tactic.h b/src/tactic/arith/fix_dl_var_tactic.h index c0d6fc4e4..9b0bddf3f 100644 --- a/src/tactic/arith/fix_dl_var_tactic.h +++ b/src/tactic/arith/fix_dl_var_tactic.h @@ -30,4 +30,8 @@ class tactic; tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("fix-dl-var", "if goal is in the difference logic fragment, then fix the variable with the most number of occurrences at 0.", "mk_fix_dl_var_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/arith/fm_tactic.h b/src/tactic/arith/fm_tactic.h index f13a1e6ba..f9b237d24 100644 --- a/src/tactic/arith/fm_tactic.h +++ b/src/tactic/arith/fm_tactic.h @@ -29,5 +29,8 @@ class ast_manager; class tactic; tactic * mk_fm_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("fm", "eliminate variables using fourier-motzkin elimination.", "mk_fm_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/lia2pb_tactic.h b/src/tactic/arith/lia2pb_tactic.h index a9c2d1c52..195e07a66 100644 --- a/src/tactic/arith/lia2pb_tactic.h +++ b/src/tactic/arith/lia2pb_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_lia2pb_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("lia2pb", "convert bounded integer variables into a sequence of 0-1 variables.", "mk_lia2pb_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/nla2bv_tactic.h b/src/tactic/arith/nla2bv_tactic.h index 0b0febb1f..6fa42fbe4 100644 --- a/src/tactic/arith/nla2bv_tactic.h +++ b/src/tactic/arith/nla2bv_tactic.h @@ -25,6 +25,9 @@ class ast_manager; class tactic; tactic * mk_nla2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("nla2bv", "convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models.", "mk_nla2bv_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/pb2bv_tactic.h b/src/tactic/arith/pb2bv_tactic.h index 9b91d6810..1398477d6 100644 --- a/src/tactic/arith/pb2bv_tactic.h +++ b/src/tactic/arith/pb2bv_tactic.h @@ -24,6 +24,9 @@ class ast_manager; class tactic; tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("pb2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_pb2bv_tactic(m, p)") +*/ probe * mk_is_pb_probe(); diff --git a/src/tactic/arith/propagate_ineqs_tactic.h b/src/tactic/arith/propagate_ineqs_tactic.h index e86a6dc2e..048043f2d 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.h +++ b/src/tactic/arith/propagate_ineqs_tactic.h @@ -38,5 +38,8 @@ class ast_manager; class tactic; tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "mk_propagate_ineqs_tactic(m, p)") +*/ #endif diff --git a/src/tactic/arith/purify_arith_tactic.h b/src/tactic/arith/purify_arith_tactic.h index 32951431b..1e42549a3 100644 --- a/src/tactic/arith/purify_arith_tactic.h +++ b/src/tactic/arith/purify_arith_tactic.h @@ -54,5 +54,9 @@ class tactic; tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("purify-arith", "eliminate unnecessary operators: -, /, div, mod, rem, is-int, to-int, ^, root-objects.", "mk_purify_arith_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/arith/recover_01_tactic.h b/src/tactic/arith/recover_01_tactic.h index 7962fb342..a48addc2d 100644 --- a/src/tactic/arith/recover_01_tactic.h +++ b/src/tactic/arith/recover_01_tactic.h @@ -38,5 +38,8 @@ class ast_manager; class tactic; tactic * mk_recover_01_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("recover-01", "recover 0-1 variables hidden as Boolean variables.", "mk_recover_01_tactic(m, p)") +*/ #endif diff --git a/src/tactic/bit_blaster/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp similarity index 100% rename from src/tactic/bit_blaster/bit_blaster_model_converter.cpp rename to src/tactic/bv/bit_blaster_model_converter.cpp diff --git a/src/tactic/bit_blaster/bit_blaster_model_converter.h b/src/tactic/bv/bit_blaster_model_converter.h similarity index 100% rename from src/tactic/bit_blaster/bit_blaster_model_converter.h rename to src/tactic/bv/bit_blaster_model_converter.h diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 4e2f45a01..63d534cbb 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include"bit_blaster_rewriter.h" #include"ast_smt2_pp.h" #include"model_pp.h" +#include"rewriter_types.h" class bit_blaster_tactic : public tactic { @@ -130,7 +131,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(g, result, mc, pc, core); + try { + (*m_imp)(g, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/bit_blaster/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp similarity index 100% rename from src/tactic/bit_blaster/bv1_blaster_tactic.cpp rename to src/tactic/bv/bv1_blaster_tactic.cpp diff --git a/src/tactic/bit_blaster/bv1_blaster_tactic.h b/src/tactic/bv/bv1_blaster_tactic.h similarity index 80% rename from src/tactic/bit_blaster/bv1_blaster_tactic.h rename to src/tactic/bv/bv1_blaster_tactic.h index a38d53d1a..cdc42b7b8 100644 --- a/src/tactic/bit_blaster/bv1_blaster_tactic.h +++ b/src/tactic/bv/bv1_blaster_tactic.h @@ -31,5 +31,7 @@ class tactic; tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_ref()); 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)") +*/ #endif diff --git a/src/tactic/bv/bv_size_reduction_tactic.h b/src/tactic/bv/bv_size_reduction_tactic.h index 696740096..2d0e0d4f4 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.h +++ b/src/tactic/bv/bv_size_reduction_tactic.h @@ -29,5 +29,8 @@ class ast_manager; class tactic; tactic * mk_bv_size_reduction_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("reduce-bv-size", "try to reduce bit-vector sizes using inequalities.", "mk_bv_size_reduction_tactic(m, p)") +*/ #endif diff --git a/src/tactic/bv/max_bv_sharing_tactic.h b/src/tactic/bv/max_bv_sharing_tactic.h index 1c016ebf9..b1abc3787 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.h +++ b/src/tactic/bv/max_bv_sharing_tactic.h @@ -27,6 +27,9 @@ class ast_manager; class tactic; tactic * mk_max_bv_sharing_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("max-bv-sharing", "use heuristics to maximize the sharing of bit-vector expressions such as adders and multipliers.", "mk_max_bv_sharing_tactic(m, p)") +*/ #endif diff --git a/src/tactic/core/cofactor_term_ite_tactic.h b/src/tactic/core/cofactor_term_ite_tactic.h index 46eba627f..0dcfc212a 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.h +++ b/src/tactic/core/cofactor_term_ite_tactic.h @@ -25,5 +25,8 @@ class ast_manager; class tactic; tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("cofactor-term-ite", "eliminate term if-the-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)") +*/ #endif diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 5d33d1043..8ab920bef 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -53,4 +53,8 @@ inline tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = p return clean(alloc(ctx_simplify_tactic, m, p)); } +/* + ADD_TACTIC("ctx-simplify", "apply contextual simplification rules.", "mk_ctx_simplify_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/core/der_tactic.h b/src/tactic/core/der_tactic.h index 8e7d1453f..95b0a95da 100644 --- a/src/tactic/core/der_tactic.h +++ b/src/tactic/core/der_tactic.h @@ -22,4 +22,8 @@ class tactic; tactic * mk_der_tactic(ast_manager & m); +/* + ADD_TACTIC_CMD("der", "destructive equality resolution.", "mk_der_tactic(m)") +*/ + #endif /* _DER_TACTIC_H_ */ diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h index 00955eb83..34377c815 100644 --- a/src/tactic/core/reduce_args_tactic.h +++ b/src/tactic/core/reduce_args_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic(m, p)") +*/ #endif diff --git a/src/tactic/core/tseitin_cnf_tactic.h b/src/tactic/core/tseitin_cnf_tactic.h index 0a32651ea..a5c96e335 100644 --- a/src/tactic/core/tseitin_cnf_tactic.h +++ b/src/tactic/core/tseitin_cnf_tactic.h @@ -28,4 +28,9 @@ tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p = para tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("tseitin-cnf", "convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored).", "mk_tseitin_cnf_tactic(m, p)") + ADD_TACTIC("tseitin-cnf-core", "convert goal into CNF using tseitin-like encoding (note: quantifiers are ignored). This tactic does not apply required simplifications to the input goal like the tseitin-cnf tactic.", "mk_tseitin_cnf_core_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/fpa/fpa2bv_tactic.h b/src/tactic/fpa/fpa2bv_tactic.h index 91647318f..129ae5fd5 100644 --- a/src/tactic/fpa/fpa2bv_tactic.h +++ b/src/tactic/fpa/fpa2bv_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("fpa2bv", "convert floating point numbers to bit-vectors.", "mk_fpa2bv_tactic(m, p)") +*/ -#endif \ No newline at end of file +#endif diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 355b96063..660565463 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -25,5 +25,8 @@ class ast_manager; class tactic; tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qffpa", "(try to) solve goal using the tactic for QF_FPA.", "mk_qffpa_tactic(m, p)") +*/ #endif diff --git a/src/tactic/nlsat/qfnra_nlsat_tactic.h b/src/tactic/nlsat/qfnra_nlsat_tactic.h index bcaf4b5ce..e0633fed9 100644 --- a/src/tactic/nlsat/qfnra_nlsat_tactic.h +++ b/src/tactic/nlsat/qfnra_nlsat_tactic.h @@ -27,4 +27,8 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_re MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p)); +/* + ADD_TACTIC("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", "mk_qfnra_nlsat_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/sls/sls_tactic.h b/src/tactic/sls/sls_tactic.h index be350ee15..50b8f0d5b 100644 --- a/src/tactic/sls/sls_tactic.h +++ b/src/tactic/sls/sls_tactic.h @@ -24,7 +24,9 @@ class ast_manager; class tactic; tactic * mk_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); - tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", "mk_qfbv_sls_tactic(m, p)") +*/ #endif diff --git a/src/tactic/smt/smt_tactic.cpp b/src/tactic/smt/smt_tactic.cpp index 094b16d42..7afce667a 100644 --- a/src/tactic/smt/smt_tactic.cpp +++ b/src/tactic/smt/smt_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include"smt_solver.h" #include"front_end_params.h" #include"params2front_end_params.h" +#include"rewriter_types.h" class smt_tactic : public tactic { scoped_ptr m_params; @@ -146,159 +147,164 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(in->is_well_sorted()); - ast_manager & m = in->m(); - TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " - << " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n"; - tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; - tout << "params_ref: " << m_params_ref << "\n";); - TRACE("smt_tactic_detail", in->display(tout);); - TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); - scoped_init_ctx init(*this, m); - SASSERT(m_ctx != 0); - - scoped_ptr dep2bool; - scoped_ptr bool2dep; - ptr_vector assumptions; - if (in->unsat_core_enabled()) { - if (in->proofs_enabled()) - throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); - dep2bool = alloc(expr2expr_map); - bool2dep = alloc(expr2expr_map); - ptr_vector deps; - ptr_vector clause; - unsigned sz = in->size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = in->form(i); - expr_dependency * d = in->dep(i); - if (d == 0) { - m_ctx->assert_expr(f); - } - else { - // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. - clause.reset(); - clause.push_back(f); - deps.reset(); - m.linearize(d, deps); - SASSERT(!deps.empty()); // d != 0, then deps must not be empty - ptr_vector::iterator it = deps.begin(); - ptr_vector::iterator end = deps.end(); - for (; it != end; ++it) { - expr * d = *it; - if (is_uninterp_const(d) && m.is_bool(d)) { - // no need to create a fresh boolean variable for d - if (!bool2dep->contains(d)) { - assumptions.push_back(d); - bool2dep->insert(d, d); - } - clause.push_back(m.mk_not(d)); - } - else { - // must normalize assumption - expr * b = 0; - if (!dep2bool->find(d, b)) { - b = m.mk_fresh_const(0, m.mk_bool_sort()); - dep2bool->insert(d, b); - bool2dep->insert(b, d); - assumptions.push_back(b); - } - clause.push_back(m.mk_not(b)); - } - } - SASSERT(clause.size() > 1); - expr_ref cls(m); - cls = m.mk_or(clause.size(), clause.c_ptr()); - m_ctx->assert_expr(cls); - } - } - } - else if (in->proofs_enabled()) { - unsigned sz = in->size(); - for (unsigned i = 0; i < sz; i++) { - m_ctx->assert_expr(in->form(i), in->pr(i)); - } - } - else { - unsigned sz = in->size(); - for (unsigned i = 0; i < sz; i++) { - m_ctx->assert_expr(in->form(i)); - } - } - - lbool r; - if (assumptions.empty()) - r = m_ctx->setup_and_check(); - else - r = m_ctx->check(assumptions.size(), assumptions.c_ptr()); - m_ctx->collect_statistics(m_stats); - - switch (r) { - case l_true: { - if (m_fail_if_inconclusive && !in->sat_preserved()) - throw tactic_exception("over-approximated goal found to be sat"); - // the empty assertion set is trivially satifiable. - in->reset(); - result.push_back(in.get()); - // store the model in a do nothin model converter. - if (in->models_enabled()) { - model_ref md; - m_ctx->get_model(md); - mc = model2model_converter(md.get()); - } - pc = 0; - core = 0; - return; - } - case l_false: { - if (m_fail_if_inconclusive && !in->unsat_preserved()) { - TRACE("smt_tactic", tout << "failed to show to be unsat...\n";); - throw tactic_exception("under-approximated goal found to be unsat"); - } - // formula is unsat, reset the goal, and store false there. - in->reset(); - proof * pr = 0; - expr_dependency * lcore = 0; - if (in->proofs_enabled()) - pr = m_ctx->get_proof(); + try { + SASSERT(in->is_well_sorted()); + ast_manager & m = in->m(); + TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " + << " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n"; + tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; + tout << "params_ref: " << m_params_ref << "\n";); + TRACE("smt_tactic_detail", in->display(tout);); + TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); + scoped_init_ctx init(*this, m); + SASSERT(m_ctx != 0); + + scoped_ptr dep2bool; + scoped_ptr bool2dep; + ptr_vector assumptions; if (in->unsat_core_enabled()) { - unsigned sz = m_ctx->get_unsat_core_size(); + if (in->proofs_enabled()) + throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); + dep2bool = alloc(expr2expr_map); + bool2dep = alloc(expr2expr_map); + ptr_vector deps; + ptr_vector clause; + unsigned sz = in->size(); for (unsigned i = 0; i < sz; i++) { - expr * b = m_ctx->get_unsat_core_expr(i); - SASSERT(is_uninterp_const(b) && m.is_bool(b)); - expr * d = bool2dep->find(b); - lcore = m.mk_join(lcore, m.mk_leaf(d)); - } - } - in->assert_expr(m.mk_false(), pr, lcore); - result.push_back(in.get()); - mc = 0; - pc = 0; - core = 0; - return; - } - case l_undef: - if (m_fail_if_inconclusive) - throw tactic_exception("smt tactic failed to show goal to be sat/unsat"); - result.push_back(in.get()); - if (m_candidate_models) { - switch (m_ctx->last_failure()) { - case smt::NUM_CONFLICTS: - case smt::THEORY: - case smt::QUANTIFIERS: - if (in->models_enabled()) { - model_ref md; - m_ctx->get_model(md); - mc = model2model_converter(md.get()); + expr * f = in->form(i); + expr_dependency * d = in->dep(i); + if (d == 0) { + m_ctx->assert_expr(f); + } + else { + // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. + clause.reset(); + clause.push_back(f); + deps.reset(); + m.linearize(d, deps); + SASSERT(!deps.empty()); // d != 0, then deps must not be empty + ptr_vector::iterator it = deps.begin(); + ptr_vector::iterator end = deps.end(); + for (; it != end; ++it) { + expr * d = *it; + if (is_uninterp_const(d) && m.is_bool(d)) { + // no need to create a fresh boolean variable for d + if (!bool2dep->contains(d)) { + assumptions.push_back(d); + bool2dep->insert(d, d); + } + clause.push_back(m.mk_not(d)); + } + else { + // must normalize assumption + expr * b = 0; + if (!dep2bool->find(d, b)) { + b = m.mk_fresh_const(0, m.mk_bool_sort()); + dep2bool->insert(d, b); + bool2dep->insert(b, d); + assumptions.push_back(b); + } + clause.push_back(m.mk_not(b)); + } + } + SASSERT(clause.size() > 1); + expr_ref cls(m); + cls = m.mk_or(clause.size(), clause.c_ptr()); + m_ctx->assert_expr(cls); } - pc = 0; - core = 0; - return; - default: - break; } } - m_failure = m_ctx->last_failure_as_string(); - throw tactic_exception(m_failure.c_str()); + else if (in->proofs_enabled()) { + unsigned sz = in->size(); + for (unsigned i = 0; i < sz; i++) { + m_ctx->assert_expr(in->form(i), in->pr(i)); + } + } + else { + unsigned sz = in->size(); + for (unsigned i = 0; i < sz; i++) { + m_ctx->assert_expr(in->form(i)); + } + } + + lbool r; + if (assumptions.empty()) + r = m_ctx->setup_and_check(); + else + r = m_ctx->check(assumptions.size(), assumptions.c_ptr()); + m_ctx->collect_statistics(m_stats); + + switch (r) { + case l_true: { + if (m_fail_if_inconclusive && !in->sat_preserved()) + throw tactic_exception("over-approximated goal found to be sat"); + // the empty assertion set is trivially satifiable. + in->reset(); + result.push_back(in.get()); + // store the model in a do nothin model converter. + if (in->models_enabled()) { + model_ref md; + m_ctx->get_model(md); + mc = model2model_converter(md.get()); + } + pc = 0; + core = 0; + return; + } + case l_false: { + if (m_fail_if_inconclusive && !in->unsat_preserved()) { + TRACE("smt_tactic", tout << "failed to show to be unsat...\n";); + throw tactic_exception("under-approximated goal found to be unsat"); + } + // formula is unsat, reset the goal, and store false there. + in->reset(); + proof * pr = 0; + expr_dependency * lcore = 0; + if (in->proofs_enabled()) + pr = m_ctx->get_proof(); + if (in->unsat_core_enabled()) { + unsigned sz = m_ctx->get_unsat_core_size(); + for (unsigned i = 0; i < sz; i++) { + expr * b = m_ctx->get_unsat_core_expr(i); + SASSERT(is_uninterp_const(b) && m.is_bool(b)); + expr * d = bool2dep->find(b); + lcore = m.mk_join(lcore, m.mk_leaf(d)); + } + } + in->assert_expr(m.mk_false(), pr, lcore); + result.push_back(in.get()); + mc = 0; + pc = 0; + core = 0; + return; + } + case l_undef: + if (m_fail_if_inconclusive) + throw tactic_exception("smt tactic failed to show goal to be sat/unsat"); + result.push_back(in.get()); + if (m_candidate_models) { + switch (m_ctx->last_failure()) { + case smt::NUM_CONFLICTS: + case smt::THEORY: + case smt::QUANTIFIERS: + if (in->models_enabled()) { + model_ref md; + m_ctx->get_model(md); + mc = model2model_converter(md.get()); + } + pc = 0; + core = 0; + return; + default: + break; + } + } + m_failure = m_ctx->last_failure_as_string(); + throw tactic_exception(m_failure.c_str()); + } + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); } } }; diff --git a/src/tactic/smtlogics/qfbv_tactic.h b/src/tactic/smtlogics/qfbv_tactic.h index 3e3eb7224..7210f6f25 100644 --- a/src/tactic/smtlogics/qfbv_tactic.h +++ b/src/tactic/smtlogics/qfbv_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfbv", "builtin strategy for solving QF_BV problems.", "mk_qfbv_tactic(m, p)") +*/ #endif diff --git a/src/tactic/smtlogics/qflia_tactic.h b/src/tactic/smtlogics/qflia_tactic.h index e5d5a1f76..9ddaf1f88 100644 --- a/src/tactic/smtlogics/qflia_tactic.h +++ b/src/tactic/smtlogics/qflia_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qflia", "builtin strategy for solving QF_LIA problems.", "mk_qflia_tactic(m, p)") +*/ #endif diff --git a/src/tactic/smtlogics/qflra_tactic.h b/src/tactic/smtlogics/qflra_tactic.h index 9da48f064..54ff228d4 100644 --- a/src/tactic/smtlogics/qflra_tactic.h +++ b/src/tactic/smtlogics/qflra_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qflra", "builtin strategy for solving QF_LRA problems.", "mk_qflra_tactic(m, p)") +*/ #endif diff --git a/src/tactic/smtlogics/qfnia_tactic.h b/src/tactic/smtlogics/qfnia_tactic.h index a6ed01109..40bb95652 100644 --- a/src/tactic/smtlogics/qfnia_tactic.h +++ b/src/tactic/smtlogics/qfnia_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfnia", "builtin strategy for solving QF_NIA problems.", "mk_qfnia_tactic(m, p)") +*/ #endif diff --git a/src/tactic/smtlogics/qfnra_tactic.h b/src/tactic/smtlogics/qfnra_tactic.h index 85fc453d1..a0497f6f3 100644 --- a/src/tactic/smtlogics/qfnra_tactic.h +++ b/src/tactic/smtlogics/qfnra_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_qfnra_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfnra", "builtin strategy for solving QF_NRA problems.", "mk_qfnra_tactic(m, p)") +*/ #endif diff --git a/src/tactic/subpaving/subpaving_tactic.h b/src/tactic/subpaving/subpaving_tactic.h index b39acf1a4..087c72847 100644 --- a/src/tactic/subpaving/subpaving_tactic.h +++ b/src/tactic/subpaving/subpaving_tactic.h @@ -24,5 +24,8 @@ class ast_manager; class tactic; tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("subpaving", "tactic for testing subpaving module.", "mk_subpaving_tactic(m, p)") +*/ #endif diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 55eeafac9..cb2c3f515 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -131,6 +131,7 @@ tactic * mk_fail_if_undecided_tactic(); /* ADD_TACTIC("skip", "do nothing tactic.", "mk_skip_tactic()") ADD_TACTIC("fail", "always fail tactic.", "mk_fail_tactic()") + ADD_TACTIC("fail-if-undecided", "fail if goal is undecided.", "mk_fail_if_undecided_tactic()") */ tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl); diff --git a/src/tactic/ufbv/ufbv_tactic.h b/src/tactic/ufbv/ufbv_tactic.h index 00499c8a1..939185491 100644 --- a/src/tactic/ufbv/ufbv_tactic.h +++ b/src/tactic/ufbv/ufbv_tactic.h @@ -26,5 +26,9 @@ class tactic; tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p); tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p); +/* + ADD_TACTIC("bv", "builtin strategy for solving BV problems (with quantifiers).", "mk_ufbv_tactic(m, p)") + ADD_TACTIC("ufbv", "builtin strategy for solving UFBV problems (with quantifiers).", "mk_ufbv_tactic(m, p)") +*/ #endif