mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

Cleanup lemma definition

Browse source 
exposes a potential bug. See comments in code.
This commit is contained in:
Arie Gurfinkel 2017-12-18 12:06:10 -05:00
parent f51c07adf6
commit 981e521b18
2 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/muz/spacer/spacer_context.cpp
View file

@ -1177,7 +1177,7 @@ void pred_transformer::inherit_properties(pred_transformer& other)
lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
m_ref_count(0), m(manager), m_ref_count(0), m(manager),
m_body(body, m), m_cube(m), m_body(body, m), m_cube(m),
m_bindings(m), m_zks(m), m_lvl(lvl), m_zks(m), m_bindings(m), m_lvl(lvl),
m_pob(nullptr), m_new_pob(false) { m_pob(nullptr), m_new_pob(false) {
SASSERT(m_body); SASSERT(m_body);
normalize(m_body, m_body); normalize(m_body, m_body);
@ -1186,17 +1186,17 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
lemma::lemma(pob_ref const &p) : lemma::lemma(pob_ref const &p) :
m_ref_count(0), m(p->get_ast_manager()), m_ref_count(0), m(p->get_ast_manager()),
m_body(m), m_cube(m), m_body(m), m_cube(m),
m_bindings(m), m_zks(m), m_lvl(p->level()), m_zks(m), m_bindings(m), m_lvl(p->level()),
m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob); m_pob->get_skolems(m_zks);} m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob); m_pob->get_skolems(m_zks);}
lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
m_ref_count(0), m_ref_count(0),
m(p->get_ast_manager()), m(p->get_ast_manager()),
m_body(m), m_cube(m), m_body(m), m_cube(m),
m_bindings(m), m_zks(m), m_lvl(p->level()), m_zks(m), m_bindings(m), m_lvl(p->level()),
m_pob(p), m_new_pob(m_pob) m_pob(p), m_new_pob(m_pob)
{ {
m_pob->get_skolems(m_zks); if (m_pob) {m_pob->get_skolems(m_zks);}
update_cube(p, cube); update_cube(p, cube);
set_level(lvl); set_level(lvl);
} }
@ -1229,6 +1229,9 @@ void lemma::mk_expr_core() {
names.c_ptr(), names.c_ptr(),
m_body, 15, symbol(m_body->get_id())); m_body, 15, symbol(m_body->get_id()));
if (m_new_pob) { if (m_new_pob) {
// XXX This assertion will fail when a lemma is
// XXX generalized with additional quantified variables
SASSERT(m_pob->get_binding().size() == m_zks.size());
add_binding(m_pob->get_binding()); add_binding(m_pob->get_binding());
} }
} }

6
src/muz/spacer/spacer_context.h
View file

@ -110,8 +110,8 @@ class lemma {
ast_manager &m; ast_manager &m;
expr_ref m_body; expr_ref m_body;
expr_ref_vector m_cube; expr_ref_vector m_cube;
app_ref_vector m_bindings;
app_ref_vector m_zks; app_ref_vector m_zks;
app_ref_vector m_bindings;
unsigned m_lvl; unsigned m_lvl;
pob_ref m_pob; pob_ref m_pob;
bool m_new_pob; bool m_new_pob;
@ -134,7 +134,9 @@ public:
pob_ref &get_pob() {return m_pob;} pob_ref &get_pob() {return m_pob;}
inline unsigned weakness(); inline unsigned weakness();
void set_skolems(app_ref_vector &zks) { m_zks.append(zks); } void add_skolems(app_ref_vector &zks) {m_zks.append(zks);}
void add_skolem(app *zk) {m_zks.push_back(zk);}
unsigned level () const {return m_lvl;} unsigned level () const {return m_lvl;}
void set_level (unsigned lvl) {m_lvl = lvl;} void set_level (unsigned lvl) {m_lvl = lvl;}
app_ref_vector& get_bindings() {return m_bindings;} app_ref_vector& get_bindings() {return m_bindings;}