mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

expose qsat tactic to default tactics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-19 18:40:59 -07:00
parent fe201013e0
commit f0bdcbb3db
2 changed files with 25 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/smtlogics/nra_tactic.cpp
View file

@ -22,7 +22,9 @@ Notes:
#include"smt_tactic.h" #include"smt_tactic.h"
#include"nnf_tactic.h" #include"nnf_tactic.h"
#include"qe_tactic.h" #include"qe_tactic.h"
#include"nlqsat.h"
#include"qfnra_nlsat_tactic.h" #include"qfnra_nlsat_tactic.h"
#include"qe_lite.h"
#include"probe_arith.h" #include"probe_arith.h"
tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
@ -36,12 +38,19 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
return and_then(mk_simplify_tactic(m, p), return and_then(mk_simplify_tactic(m, p),
mk_nnf_tactic(m, p), mk_nnf_tactic(m, p),
mk_propagate_values_tactic(m, p), mk_propagate_values_tactic(m, p),
mk_qe_lite_tactic(m),
mk_qe_tactic(m, p), mk_qe_tactic(m, p),
cond(mk_is_qfnra_probe(), cond(mk_is_qfnra_probe(),
or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000), or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000),
try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
mk_qfnra_nlsat_tactic(m, p2)), mk_qfnra_nlsat_tactic(m, p2)),
mk_smt_tactic(p))); #if 0
or_else(mk_nlqsat_tactic(m, p),
mk_smt_tactic(p))
#else
mk_smt_tactic(p)
#endif
));
} }

18
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -23,6 +23,9 @@ Revision History:
#include"elim_uncnstr_tactic.h" #include"elim_uncnstr_tactic.h"
#include"qe_tactic.h" #include"qe_tactic.h"
#include"qe_sat_tactic.h" #include"qe_sat_tactic.h"
#include"qe_lite.h"
#include"qsat.h"
#include"nlqsat.h"
#include"ctx_simplify_tactic.h" #include"ctx_simplify_tactic.h"
#include"smt_tactic.h" #include"smt_tactic.h"
@ -37,10 +40,12 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
ctx_simp_p.set_uint("max_steps", 5000000); ctx_simp_p.set_uint("max_steps", 5000000);
tactic * solve_eqs; tactic * solve_eqs;
if (disable_gaussian) if (disable_gaussian) {
solve_eqs = mk_skip_tactic(); solve_eqs = mk_skip_tactic();
else }
else {
solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m)); solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m));
}
// remark: investigate if gaussian elimination is useful when patterns are not provided. // remark: investigate if gaussian elimination is useful when patterns are not provided.
return and_then(mk_simplify_tactic(m), return and_then(mk_simplify_tactic(m),
@ -49,6 +54,7 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
using_params(mk_simplify_tactic(m), pull_ite_p), using_params(mk_simplify_tactic(m), pull_ite_p),
solve_eqs, solve_eqs,
mk_elim_uncnstr_tactic(m), mk_elim_uncnstr_tactic(m),
mk_qe_lite_tactic(m),
mk_simplify_tactic(m)); mk_simplify_tactic(m));
} }
@ -98,13 +104,18 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
} }
tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
#if 0
tactic * st = and_then(mk_quant_preprocessor(m), tactic * st = and_then(mk_quant_preprocessor(m),
or_else(try_for(mk_smt_tactic(), 100), or_else(try_for(mk_smt_tactic(), 100),
try_for(qe::mk_sat_tactic(m), 1000), try_for(qe::mk_sat_tactic(m), 1000),
try_for(mk_smt_tactic(), 1000), try_for(mk_smt_tactic(), 1000),
and_then(mk_qe_tactic(m), mk_smt_tactic()) and_then(mk_qe_tactic(m), mk_smt_tactic())
)); ));
#else
tactic * st = and_then(mk_quant_preprocessor(m),
or_else(mk_qsat_tactic(m, p),
and_then(mk_qe_tactic(m), mk_smt_tactic())));
#endif
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
@ -116,3 +127,4 @@ tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) { tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
return mk_lra_tactic(m, p); return mk_lra_tactic(m, p);
} }