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

Refine default_tactic: if the constraint is an SAT instance and proof is not enabled, then use the qffd tactic

Browse source
This commit is contained in:
rainoftime 2018-06-22 16:46:47 +08:00
parent 8969a7035c
commit fc8b1d9a7d
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/portfolio/default_tactic.cpp
View file

@ -31,9 +31,11 @@ Notes:
#include "tactic/fpa/qffplra_tactic.h" #include "tactic/fpa/qffplra_tactic.h"
#include "tactic/smtlogics/qfaufbv_tactic.h" #include "tactic/smtlogics/qfaufbv_tactic.h"
#include "tactic/smtlogics/qfauflia_tactic.h" #include "tactic/smtlogics/qfauflia_tactic.h"
#include "tactic/portfolio/fd_solver.h"
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(mk_simplify_tactic(m), tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_propositional_probe(), if_no_proofs(mk_fd_tactic(m, p)),
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m),
cond(mk_is_qflia_probe(), mk_qflia_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
@ -46,7 +48,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p), cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p),
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
mk_smt_tactic())))))))))))), mk_smt_tactic()))))))))))))),
p); p);
return st; return st;
} }