mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Silently bailing out on quantifiers in lackr.

Browse source
This commit is contained in:
Mikolas Janota 2016-03-29 19:19:07 +01:00
parent 1a65153872
commit 363f57a2f4
2 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/ackermannization/lackr.cpp
View file

@ -53,7 +53,7 @@ lackr::~lackr() {
lbool lackr::operator() () { lbool lackr::operator() () {
SASSERT(m_sat); SASSERT(m_sat);
init(); if (!init()) return l_undef;
const lbool rv = m_eager ? eager() : lazy(); const lbool rv = m_eager ? eager() : lazy();
if (rv == l_true) m_sat->get_model(m_model); if (rv == l_true) m_sat->get_model(m_model);
CTRACE("lackr", rv == l_true, CTRACE("lackr", rv == l_true,
@ -63,7 +63,7 @@ lbool lackr::operator() () {
bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) { bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
if (lemmas_upper_bound <= 0) return false; if (lemmas_upper_bound <= 0) return false;
init(); if (!init()) return false;
if (lemmas_upper_bound != std::numeric_limits<double>::infinity()) { if (lemmas_upper_bound != std::numeric_limits<double>::infinity()) {
const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms); const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms);
if (lemmas_bound > lemmas_upper_bound) return false; if (lemmas_bound > lemmas_upper_bound) return false;
@ -74,14 +74,15 @@ bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
return true; return true;
} }
void lackr::init() { bool lackr::init() {
SASSERT(!m_is_init); SASSERT(!m_is_init);
m_is_init = true;
params_ref simp_p(m_p); params_ref simp_p(m_p);
m_simp.updt_params(simp_p); m_simp.updt_params(simp_p);
m_info = alloc(ackr_info, m_m); m_info = alloc(ackr_info, m_m);
collect_terms(); if (!collect_terms()) return false;
abstract(); abstract();
m_is_init = true;
return true;
} }
// //
@ -96,10 +97,8 @@ bool lackr::ackr(app * const t1, app * const t2) {
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr * const arg1 = t1->get_arg(i); expr * const arg1 = t1->get_arg(i);
expr * const arg2 = t2->get_arg(i); expr * const arg2 = t2->get_arg(i);
if (arg1 == arg2) continue; // quickly skip syntactically equal if (m_m.are_equal(arg1, arg2)) continue; // quickly skip syntactically equal
if (m_ackr_helper.bvutil().is_numeral(arg1) && m_ackr_helper.bvutil().is_numeral(arg2)) { if (m_m.are_distinct(arg1, arg2)){ // quickly abort if there are two distinct (e.g. numerals)
// quickly abort if there are two distinct numerals
SASSERT(arg1 != arg2);
TRACE("lackr", tout << "never eq\n";); TRACE("lackr", tout << "never eq\n";);
return false; return false;
} }
@ -203,6 +202,7 @@ void lackr::push_abstraction() {
} }
lbool lackr::eager() { lbool lackr::eager() {
SASSERT(m_is_init);
push_abstraction(); push_abstraction();
TRACE("lackr", tout << "run sat 0\n"; ); TRACE("lackr", tout << "run sat 0\n"; );
const lbool rv0 = m_sat->check_sat(0, 0); const lbool rv0 = m_sat->check_sat(0, 0);
@ -217,6 +217,7 @@ lbool lackr::eager() {
} }
lbool lackr::lazy() { lbool lackr::lazy() {
SASSERT(m_is_init);
lackr_model_constructor mc(m_m, m_info); lackr_model_constructor mc(m_m, m_info);
push_abstraction(); push_abstraction();
unsigned ackr_head = 0; unsigned ackr_head = 0;
@ -247,7 +248,7 @@ lbool lackr::lazy() {
// //
// Collect all uninterpreted terms, skipping 0-arity. // Collect all uninterpreted terms, skipping 0-arity.
// //
void lackr::collect_terms() { bool lackr::collect_terms() {
ptr_vector<expr> stack; ptr_vector<expr> stack;
expr * curr; expr * curr;
expr_mark visited; expr_mark visited;
@ -279,12 +280,11 @@ void lackr::collect_terms() {
} }
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
UNREACHABLE(); return false; // quantifiers not supported
break;
default: default:
UNREACHABLE(); UNREACHABLE();
return; return false;
} }
} }
visited.reset(); return true;
} }

4
src/ackermannization/lackr.h
View file

@ -95,7 +95,7 @@ class lackr {
lackr_stats& m_st; lackr_stats& m_st;
bool m_is_init; bool m_is_init;
void init(); bool init();
lbool eager(); lbool eager();
lbool lazy(); lbool lazy();
@ -118,6 +118,6 @@ class lackr {
// //
// Collect all uninterpreted terms, skipping 0-arity. // Collect all uninterpreted terms, skipping 0-arity.
// //
void collect_terms(); bool collect_terms();
}; };
#endif /* LACKR_H_ */ #endif /* LACKR_H_ */