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

Fix lemma_as_cti option

Browse source 
Use negation of a lemma as a proof obligation. This speeds up discovering
bad lemmas that do not contain some reachable states.
This commit is contained in:
Arie Gurfinkel 2018-06-27 14:34:29 -04:00
parent bc6604441b
commit 49e9480928
2 changed files with 56 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -55,6 +55,8 @@ Notes:
#include "muz/spacer/spacer_sat_answer.h"
#define WEAKNESS_MAX 65535
namespace spacer {
/// pob -- proof obligation
@ -473,9 +475,11 @@ void derivation::premise::set_summary (expr * summary, bool must,
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_weakness(UINT_MAX) {
m_zks(m), m_bindings(m),
m_pob(nullptr), m_ctp(nullptr),
m_lvl(lvl), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(WEAKNESS_MAX),
m_external(false), m_blocked(false) {
SASSERT(m_body);
normalize(m_body, m_body);
}
@ -483,9 +487,11 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
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_weakness(p->weakness()) {
m_zks(m), m_bindings(m),
m_pob(p), m_ctp(nullptr),
m_lvl(p->level()), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(p->weakness()),
m_external(false), m_blocked(false) {
SASSERT(m_pob);
m_pob->get_skolems(m_zks);
add_binding(m_pob->get_binding());
@ -495,9 +501,11 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
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_weakness(p->weakness())
m_zks(m), m_bindings(m),
m_pob(p), m_ctp(nullptr),
m_lvl(p->level()), m_init_lvl(m_lvl),
m_bumped(0), m_weakness(p->weakness()),
m_external(false), m_blocked(false)
{
if (m_pob) {
m_pob->get_skolems(m_zks);
@ -834,7 +842,7 @@ const datalog::rule *pred_transformer::find_rule(model &model) {
for (auto &kv : m_pt_rules) {
app *tag = kv.m_value->tag();
if (model.eval(tag->get_decl(), val) && m.is_true(val)) {
if (model.is_true_decl(tag->get_decl())) {
return &kv.m_value->rule();
}
}
@ -1401,7 +1409,12 @@ bool pred_transformer::is_ctp_blocked(lemma *lem) {
// -- find rule of the ctp
const datalog::rule *r;
r = find_rule(*ctp);
if (r == nullptr) {return false;}
if (r == nullptr) {
// no rules means lemma is blocked forever because
// it does not satisfy some derived facts
lem->set_blocked(true);
return true;
}
// -- find predicates along the rule
find_predecessors(*r, m_predicates);
@ -1424,6 +1437,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
unsigned& solver_level,
expr_ref_vector* core)
{
if (lem->is_blocked()) return false;
m_stats.m_num_is_invariant++;
if (is_ctp_blocked(lem)) {
m_stats.m_num_ctp_blocked++;
@ -1465,7 +1480,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
SASSERT (level <= solver_level);
}
else if (r == l_true) {
// optionally remove unused symbols from the model
// TBD: optionally remove unused symbols from the model
if (mdl_ref_ptr) {lem->set_ctp(*mdl_ref_ptr);}
}
else {lem->reset_ctp();}
@ -3427,11 +3442,21 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
// Optionally update the node to be the negation of the lemma
if (v && m_use_lemma_as_pob) {
NOT_IMPLEMENTED_YET();
// n.new_post (mk_and(lemma->get_cube()));
// n.set_farkas_generalizer (false);
// // XXX hack while refactoring is in progress
// n.clean();
expr_ref c(m);
c = mk_and(lemma->get_cube());
// check that the post condition is different
if (c != n.post()) {
pob *f = n.pt().find_pob(n.parent(), c);
// skip if a similar pob is already in the queue
if (f != &n && (!f || !f->is_in_queue())) {
f = n.pt().mk_pob(n.parent(), n.level(),
n.depth(), c, n.get_binding());
SASSERT(!f->is_in_queue());
f->inc_level();
//f->set_farkas_generalizer(false);
out.push_back(f);
}
}
}
// schedule the node to be placed back in the queue

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

@ -122,13 +122,14 @@ class lemma {
expr_ref_vector m_cube;
app_ref_vector m_zks;
app_ref_vector m_bindings;
pob_ref m_pob;
model_ref m_ctp; // counter-example to pushing
unsigned m_lvl; // current level of the lemma
unsigned m_init_lvl; // level at which lemma was created
pob_ref m_pob;
model_ref m_ctp; // counter-example to pushing
bool m_external;
unsigned m_bumped;
unsigned m_weakness;
unsigned m_bumped:16;
unsigned m_weakness:16;
unsigned m_external:1;
unsigned m_blocked:1;
void mk_expr_core();
void mk_cube_core();
@ -159,8 +160,11 @@ public:
void add_skolem(app *zk, app* b);
inline void set_external(bool ext){m_external = ext;}
inline bool external() { return m_external;}
void set_external(bool ext){m_external = ext;}
bool external() { return m_external;}
bool is_blocked() {return m_blocked;}
void set_blocked(bool v) {m_blocked=v;}
bool is_inductive() const {return is_infty_level(m_lvl);}
unsigned level () const {return m_lvl;}
@ -496,6 +500,9 @@ public:
expr *post, app_ref_vector const &b){
return m_pobs.mk_pob(parent, level, depth, post, b);
}
pob* find_pob(pob *parent, expr *post) {
return m_pobs.find_pob(parent, post);
}
pob* mk_pob(pob *parent, unsigned level, unsigned depth,
expr *post) {