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

Use refutation to compute ground sat answer

Browse source
This commit is contained in:
Arie Gurfinkel 2019-07-25 15:16:19 -04:00
parent 8a0d79251e
commit 92db639caf
4 changed files with 44 additions and 139 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2938,7 +2938,7 @@ expr_ref context::mk_unsat_answer() const
}
proof_ref context::get_ground_refutation() {
proof_ref context::get_ground_refutation() const {
if (m_last_result != l_true) {
IF_VERBOSE(0, verbose_stream()
<< "Sat answer unavailable when result is false\n";);
@ -2948,142 +2948,45 @@ proof_ref context::get_ground_refutation() {
ground_sat_answer_op op(*this);
return op(*m_query);
}
expr_ref context::get_ground_sat_answer() {
expr_ref context::get_ground_sat_answer() const {
if (m_last_result != l_true) {
IF_VERBOSE(0, verbose_stream()
<< "Sat answer unavailable when result is false\n";);
return expr_ref(m);
}
// treat the following as queues: read from left to right and insert at the right
reach_fact_ref_vector reach_facts;
ptr_vector<func_decl> preds;
ptr_vector<pred_transformer> pts;
expr_ref_vector cex (m); // pre-order list of ground instances of predicates
expr_ref_vector cex_facts (m); // equalities for the ground cex using signature constants
// convert a ground refutation into a linear counterexample
// only works for linear CHC systems
expr_ref_vector cex(m);
proof_ref pf = get_ground_refutation();
// temporary
reach_fact *reach_fact;
pred_transformer* pt;
expr_ref cex_fact (m);
datalog::rule const* r;
// get and discard query rule
reach_fact = m_query->get_last_rf ();
r = &reach_fact->get_rule ();
// initialize queues
reach_facts.append (reach_fact->get_justifications ());
if (reach_facts.size() != 1) {
// XXX Escape if an assertion is about to fail
IF_VERBOSE(1,
verbose_stream () <<
"Warning: counterexample is trivial or non-existent\n";);
return expr_ref(m.mk_true(), m);
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned>> positions;
vector<expr_ref_vector> substs;
unsigned count = 0;
while (m.is_hyper_resolve(pf, premises, conclusion, positions, substs)) {
// skip the first fact since it is query!X introduced by the encoding
// and not a user-visible predicate
if (count++ > 0)
cex.push_back(m.get_fact(pf));
if (premises.size() > 1) {
SASSERT(premises.size() == 2 && "Non linear CHC detected");
pf = premises.get(1);
} else {
pf.reset();
break;
}
m_query->find_predecessors (*r, preds);
SASSERT (preds.size () == 1);
pts.push_back (&(get_pred_transformer (preds[0])));
cex_facts.push_back (m.mk_true ());
// XXX a hack to avoid assertion when query predicate is not nullary
if (preds[0]->get_arity () == 0)
{ cex.push_back(m.mk_const(preds[0])); }
// smt context to obtain local cexes
ref<solver> cex_ctx =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
bool first = true;
// preorder traversal of the query derivation tree
for (unsigned curr = 0; curr < pts.size (); curr++) {
// pick next pt, fact, and cex_fact
pt = pts.get (curr);
reach_fact = reach_facts[curr];
cex_fact = cex_facts.get (curr);
ptr_vector<pred_transformer> child_pts;
// get justifying rule and child facts for the derivation of reach_fact at pt
r = &reach_fact->get_rule ();
const reach_fact_ref_vector &child_reach_facts =
reach_fact->get_justifications ();
// get child pts
preds.reset();
pt->find_predecessors(*r, preds);
for (unsigned j = 0; j < preds.size (); j++) {
child_pts.push_back (&(get_pred_transformer (preds[j])));
}
// update the queues
reach_facts.append (child_reach_facts);
pts.append (child_pts);
// update cex and cex_facts by making a local sat check:
// check consistency of reach facts of children, rule body, and cex_fact
cex_ctx->push ();
cex_ctx->assert_expr (cex_fact);
unsigned u_tail_sz = r->get_uninterpreted_tail_size ();
SASSERT (child_reach_facts.size () == u_tail_sz);
for (unsigned i = 0; i < u_tail_sz; i++) {
expr_ref ofml (m);
m_pm.formula_n2o(child_reach_facts[i]->get(), ofml, i);
cex_ctx->assert_expr (ofml);
}
cex_ctx->assert_expr(pt->transition());
cex_ctx->assert_expr(pt->rule2tag(r));
TRACE("cex", cex_ctx->display(tout););
lbool res = cex_ctx->check_sat(0, nullptr);
CTRACE("cex", res == l_false,
tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n";
for (unsigned i = 0; i < u_tail_sz; i++)
tout << "Pre" << i << " "
<< mk_pp(child_reach_facts[i]->get(), m) << "\n";
tout << "Rule: ";
get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n";
);
VERIFY (res == l_true);
model_ref local_mdl;
cex_ctx->get_model (local_mdl);
cex_ctx->pop (1);
local_mdl->set_model_completion(true);
if (first) {
unsigned sig_size = pt->sig_size();
expr_ref_vector ground_fact_conjs(m);
expr_ref_vector ground_arg_vals(m);
for (unsigned j = 0; j < sig_size; j++) {
expr_ref sig_arg(m), sig_val(m);
sig_arg = m.mk_const (m_pm.o2n(pt->sig(j), 0));
sig_val = (*local_mdl)(sig_arg);
ground_arg_vals.push_back(sig_val);
}
cex.push_back(m.mk_app(pt->head(), sig_size, ground_arg_vals.c_ptr()));
first = false;
}
for (unsigned i = 0; i < child_pts.size(); i++) {
pred_transformer& ch_pt = *(child_pts.get(i));
unsigned sig_size = ch_pt.sig_size();
expr_ref_vector ground_fact_conjs(m);
expr_ref_vector ground_arg_vals(m);
for (unsigned j = 0; j < sig_size; j++) {
expr_ref sig_arg(m), sig_val(m);
sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i));
sig_val = (*local_mdl)(sig_arg);
ground_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val));
ground_arg_vals.push_back(sig_val);
}
if (!ground_fact_conjs.empty()) {
expr_ref ground_fact(m);
ground_fact = mk_and(ground_fact_conjs);
m_pm.formula_o2n(ground_fact, ground_fact, i);
cex_facts.push_back (ground_fact);
} else {
cex_facts.push_back (m.mk_true ());
}
cex.push_back(m.mk_app(ch_pt.head(),
sig_size, ground_arg_vals.c_ptr()));
premises.reset();
conclusion.reset();
positions.reset();
substs.reset();
}
SASSERT(!pf || !m.is_hyper_resolve(pf));
if (pf) {
cex.push_back(m.get_fact(pf));
}
TRACE ("spacer", tout << "ground cex\n" << cex << "\n";);
@ -3091,7 +2994,7 @@ expr_ref context::get_ground_sat_answer() {
return mk_and(cex);
}
void context::display_certificate(std::ostream &out) {
void context::display_certificate(std::ostream &out) const {
switch(m_last_result) {
case l_false:
out << mk_pp(mk_unsat_answer(), m);

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

@ -1006,7 +1006,7 @@ class context {
/**
\brief Retrieve satisfying assignment with explanation.
*/
expr_ref mk_sat_answer() {return get_ground_sat_answer();}
expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
expr_ref mk_unsat_answer() const;
unsigned get_cex_depth ();
@ -1065,6 +1065,7 @@ public:
ast_manager& get_ast_manager() const {return m;}
manager& get_manager() {return m_pm;}
const manager & get_manager() const {return m_pm;}
decl2rel const& get_pred_transformers() const {return m_rels;}
pred_transformer& get_pred_transformer(func_decl* p) const {return *m_rels.find(p);}
@ -1082,8 +1083,8 @@ public:
* get bottom-up (from query) sequence of ground predicate instances
* (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
*/
expr_ref get_ground_sat_answer ();
proof_ref get_ground_refutation();
expr_ref get_ground_sat_answer () const;
proof_ref get_ground_refutation() const;
void get_rules_along_trace (datalog::rule_ref_vector& rules);
void collect_statistics(statistics& st) const;
@ -1091,7 +1092,7 @@ public:
void reset();
std::ostream& display(std::ostream& out) const;
void display_certificate(std::ostream& out);
void display_certificate(std::ostream& out) const;
pob& get_root() const {return m_pob_queue.get_root();}
void set_query(func_decl* q) {m_query_pred = q;}

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

@ -1,7 +1,7 @@
#include "muz/spacer/spacer_sat_answer.h"
#include "muz/base/dl_context.h"
#include "muz/base/dl_rule.h"
#include "ast/scoped_proof.h"
#include "smt/smt_solver.h"
namespace spacer {
@ -44,15 +44,16 @@ struct ground_sat_answer_op::frame {
pred_transformer &pt() {return m_pt;}
};
ground_sat_answer_op::ground_sat_answer_op(context &ctx) :
ground_sat_answer_op::ground_sat_answer_op(const context &ctx) :
m_ctx(ctx), m(m_ctx.get_ast_manager()), m_pm(m_ctx.get_manager()),
m_pinned(m) {
m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
}
proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
// -- turn on proof mode so that proof constructing API in ast_manager work correctly
scoped_proof _pf(m);
m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
vector<frame> todo, new_todo;
// -- find substitution for a query if query is not nullary

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

@ -29,9 +29,9 @@ Revision History:
namespace spacer {
class ground_sat_answer_op {
context &m_ctx;
const context &m_ctx;
ast_manager &m;
manager &m_pm;
const manager &m_pm;
expr_ref_vector m_pinned;
obj_map<expr, proof*> m_cache;
@ -46,7 +46,7 @@ class ground_sat_answer_op {
model_ref &mdl, expr_ref_vector &subst);
public:
ground_sat_answer_op(context &ctx);
ground_sat_answer_op(const context &ctx);
proof_ref operator() (pred_transformer &query);
};