mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Nikolaj Bjorner
GitHub
commit
2eea7709e0
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
};
|
||||
|
|
|
|||
Loading…
Reference in a new issue