mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

Parameter fix for the qflia default tactic

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-08 15:37:17 +01:00
parent 24a5ff825a
commit f920644892
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -101,9 +101,11 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
static tactic * mk_pb_tactic(ast_manager & m) { static tactic * mk_pb_tactic(ast_manager & m) {
params_ref pb2bv_p; params_ref pb2bv_p;
pb2bv_p.set_bool("ite_extra", true);
pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8); pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return and_then(fail_if_not(mk_is_pb_probe()), return and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()), fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()), fail_if(mk_produce_unsat_cores_probe()),
@ -113,15 +115,17 @@ static tactic * mk_pb_tactic(ast_manager & m) {
mk_fail_if_undecided_tactic()), mk_fail_if_undecided_tactic()),
and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p), and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()), fail_if_not(mk_is_qfbv_probe()),
mk_bv2sat_tactic(m)))); using_params(mk_bv2sat_tactic(m), bv2sat_p))));
} }
static tactic * mk_lia2sat_tactic(ast_manager & m) { static tactic * mk_lia2sat_tactic(ast_manager & m) {
params_ref pb2bv_p; params_ref pb2bv_p;
pb2bv_p.set_bool("ite_extra", true);
pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8); pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return and_then(fail_if(mk_is_unbounded_probe()), return and_then(fail_if(mk_is_unbounded_probe()),
fail_if(mk_produce_proofs_probe()), fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()), fail_if(mk_produce_unsat_cores_probe()),
@ -130,7 +134,7 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
mk_lia2pb_tactic(m), mk_lia2pb_tactic(m),
using_params(mk_pb2bv_tactic(m), pb2bv_p), using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()), fail_if_not(mk_is_qfbv_probe()),
mk_bv2sat_tactic(m)); using_params(mk_bv2sat_tactic(m), bv2sat_p));
} }
// Try to find a model for an unbounded ILP problem. // Try to find a model for an unbounded ILP problem.