mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Weakness of the lemma independent of the pob

Browse source 
Lemma inherits its weakness score from the pob. However,
pob's weakness might be reset or changed for some other reason.

To avoid affecting the lemma, the weakness is copied on
construction.
This commit is contained in:
Arie Gurfinkel 2018-06-26 11:33:54 -04:00
parent eabe91cdef
commit d9100437ce
2 changed files with 8 additions and 5 deletions

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

@ -463,7 +463,8 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
m_ref_count(0), m(manager),
m_body(body, m), m_cube(m),
m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl),
m_pob(nullptr), m_ctp(nullptr), m_external(false), m_bumped(0) {
m_pob(nullptr), m_ctp(nullptr), m_external(false),
m_bumped(0), m_weakness(UINT_MAX) {
SASSERT(m_body);
normalize(m_body, m_body);
}
@ -472,7 +473,8 @@ lemma::lemma(pob_ref const &p) :
m_ref_count(0), m(p->get_ast_manager()),
m_body(m), m_cube(m),
m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) {
m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0),
m_weakness(p->weakness()) {
SASSERT(m_pob);
m_pob->get_skolems(m_zks);
add_binding(m_pob->get_binding());
@ -483,7 +485,8 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
m(p->get_ast_manager()),
m_body(m), m_cube(m),
m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0)
m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0),
m_weakness(p->weakness())
{
if (m_pob) {
m_pob->get_skolems(m_zks);

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

@ -128,6 +128,7 @@ class lemma {
model_ref m_ctp; // counter-example to pushing
bool m_external;
unsigned m_bumped;
unsigned m_weakness;
void mk_expr_core();
void mk_cube_core();
@ -154,7 +155,7 @@ public:
bool has_pob() {return m_pob;}
pob_ref &get_pob() {return m_pob;}
inline unsigned weakness();
unsigned weakness() {return m_weakness;}
void add_skolem(app *zk, app* b);
@ -690,7 +691,6 @@ struct pob_ref_gt :
{return gt (n1.get (), n2.get ());}
};
inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;}
/**
*/
class derivation {