mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

Exported the quasi-pb probe as per user request.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-08 15:35:29 +01:00
parent 0997d0d2b5
commit 3e1042c680
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -56,7 +56,7 @@ struct quasi_pb_probe : public probe {
} }
}; };
probe * mk_quasi_pb_probe() { probe * mk_is_quasi_pb_probe() {
return mk_and(mk_not(mk_is_unbounded_probe()), return mk_and(mk_not(mk_is_unbounded_probe()),
alloc(quasi_pb_probe)); alloc(quasi_pb_probe));
} }
@ -208,7 +208,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(preamble_st, tactic * st = using_params(and_then(preamble_st,
or_else(mk_ilp_model_finder_tactic(m), or_else(mk_ilp_model_finder_tactic(m),
mk_pb_tactic(m), mk_pb_tactic(m),
and_then(fail_if_not(mk_quasi_pb_probe()), and_then(fail_if_not(mk_is_quasi_pb_probe()),
using_params(mk_lia2sat_tactic(m), quasi_pb_p), using_params(mk_lia2sat_tactic(m), quasi_pb_p),
mk_fail_if_undecided_tactic()), mk_fail_if_undecided_tactic()),
mk_bounded_tactic(m), mk_bounded_tactic(m),

7
src/tactic/smtlogics/qflia_tactic.h
View file

@ -28,4 +28,11 @@ 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)") ADD_TACTIC("qflia", "builtin strategy for solving QF_LIA problems.", "mk_qflia_tactic(m, p)")
*/ */
probe * mk_is_quasi_pb_probe();
/*
ADD_PROBE("is-quasi-pb", "true if the goal is quasi-pb.", "mk_is_quasi_pb_probe()")
*/
#endif #endif