mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
Nikolaj Bjorner
GitHub
commit
a5f4980c92
|
|
@ -33,7 +33,7 @@ public:
|
|||
bool is_h_marked(proof* p) {return m_h_mark.is_marked(p);}
|
||||
|
||||
bool is_b_pure (proof *p) {
|
||||
return !is_h_marked (p) && is_core_pure(m.get_fact (p));
|
||||
return !is_h_marked(p) && !this->is_a_marked(p) && is_core_pure(m.get_fact(p));
|
||||
}
|
||||
|
||||
void display_dot(std::ostream &out);
|
||||
|
|
|
|||
|
|
@ -322,6 +322,24 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
|
|||
// -- new hypothesis reducer
|
||||
else
|
||||
{
|
||||
#if 0
|
||||
static unsigned bcnt = 0;
|
||||
{
|
||||
bcnt++;
|
||||
TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";);
|
||||
if (bcnt == 123) {
|
||||
std::ofstream ofs;
|
||||
ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
|
||||
iuc_proof iuc_pf_before(m, res.get(), core_lits);
|
||||
iuc_pf_before.display_dot(ofs);
|
||||
ofs.close();
|
||||
|
||||
proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
ENSURE(pc.check(res, side));
|
||||
}
|
||||
}
|
||||
#endif
|
||||
scoped_watch _t_ (m_hyp_reduce2_sw);
|
||||
|
||||
// pre-process proof for better iuc extraction
|
||||
|
|
@ -356,6 +374,22 @@ void iuc_solver::get_iuc(expr_ref_vector &core)
|
|||
|
||||
iuc_proof iuc_pf(m, res, core_lits);
|
||||
|
||||
#if 0
|
||||
static unsigned cnt = 0;
|
||||
{
|
||||
cnt++;
|
||||
TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";);
|
||||
if (cnt == 123) {
|
||||
std::ofstream ofs;
|
||||
ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
|
||||
iuc_pf.display_dot(ofs);
|
||||
ofs.close();
|
||||
proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
ENSURE(pc.check(res, side));
|
||||
}
|
||||
}
|
||||
#endif
|
||||
unsat_core_learner learner(m, iuc_pf);
|
||||
|
||||
unsat_core_plugin* plugin;
|
||||
|
|
|
|||
|
|
@ -29,9 +29,9 @@ Revision History:
|
|||
|
||||
namespace spacer {
|
||||
|
||||
// arithmetic lemma recognizer
|
||||
bool is_arith_lemma(ast_manager& m, proof* pr)
|
||||
{
|
||||
// arithmetic lemma recognizer
|
||||
bool is_arith_lemma(ast_manager& m, proof* pr)
|
||||
{
|
||||
// arith lemmas: second parameter specifies exact type of lemma,
|
||||
// could be "farkas", "triangle-eq", "eq-propagate",
|
||||
// "assign-bounds", maybe also something else
|
||||
|
|
@ -43,11 +43,11 @@ bool is_arith_lemma(ast_manager& m, proof* pr)
|
|||
sym == "arith";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
// farkas lemma recognizer
|
||||
bool is_farkas_lemma(ast_manager& m, proof* pr)
|
||||
{
|
||||
// farkas lemma recognizer
|
||||
bool is_farkas_lemma(ast_manager& m, proof* pr)
|
||||
{
|
||||
if (pr->get_decl_kind() == PR_TH_LEMMA)
|
||||
{
|
||||
func_decl* d = pr->get_decl();
|
||||
|
|
@ -57,8 +57,144 @@ bool is_farkas_lemma(ast_manager& m, proof* pr)
|
|||
d->get_parameter(1).is_symbol(sym) && sym == "farkas";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
static bool is_assign_bounds_lemma(ast_manager &m, proof *pr) {
|
||||
if (pr->get_decl_kind() == PR_TH_LEMMA)
|
||||
{
|
||||
func_decl* d = pr->get_decl();
|
||||
symbol sym;
|
||||
return d->get_num_parameters() >= 2 &&
|
||||
d->get_parameter(0).is_symbol(sym) && sym == "arith" &&
|
||||
d->get_parameter(1).is_symbol(sym) && sym == "assign-bounds";
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
||||
class linear_combinator {
|
||||
struct scaled_lit {
|
||||
bool is_pos;
|
||||
app *lit;
|
||||
rational coeff;
|
||||
scaled_lit(bool is_pos, app *lit, const rational &coeff) :
|
||||
is_pos(is_pos), lit(lit), coeff(coeff) {}
|
||||
};
|
||||
ast_manager &m;
|
||||
th_rewriter m_rw;
|
||||
arith_util m_arith;
|
||||
expr_ref m_sum;
|
||||
bool m_is_strict;
|
||||
rational m_lc;
|
||||
vector<scaled_lit> m_lits;
|
||||
public:
|
||||
linear_combinator(ast_manager &m) : m(m), m_rw(m), m_arith(m),
|
||||
m_sum(m), m_is_strict(false),
|
||||
m_lc(1) {}
|
||||
|
||||
void add_lit(app* lit, rational const &coeff, bool is_pos = true) {
|
||||
m_lits.push_back(scaled_lit(is_pos, lit, coeff));
|
||||
}
|
||||
|
||||
void normalize_coeff() {
|
||||
for (auto &lit : m_lits)
|
||||
m_lc = lcm(m_lc, denominator(lit.coeff));
|
||||
if (!m_lc.is_one()) {
|
||||
for (auto &lit : m_lits)
|
||||
lit.coeff *= m_lc;
|
||||
}
|
||||
}
|
||||
|
||||
rational const &lc() const {return m_lc;}
|
||||
|
||||
bool process_lit(scaled_lit &lit0) {
|
||||
arith_util a(m);
|
||||
app* lit = lit0.lit;
|
||||
rational &coeff = lit0.coeff;
|
||||
bool is_pos = lit0.is_pos;
|
||||
|
||||
|
||||
if (m.is_not(lit)) {
|
||||
lit = to_app(lit->get_arg(0));
|
||||
is_pos = !is_pos;
|
||||
}
|
||||
if (!m_arith.is_le(lit) && !m_arith.is_lt(lit) &&
|
||||
!m_arith.is_ge(lit) && !m_arith.is_gt(lit) && !m.is_eq(lit)) {
|
||||
return false;
|
||||
}
|
||||
SASSERT(lit->get_num_args() == 2);
|
||||
sort* s = m.get_sort(lit->get_arg(0));
|
||||
bool is_int = m_arith.is_int(s);
|
||||
if (!is_int && m_arith.is_int_expr(lit->get_arg(0))) {
|
||||
is_int = true;
|
||||
s = m_arith.mk_int();
|
||||
}
|
||||
|
||||
if (!is_int && is_pos && (m_arith.is_gt(lit) || m_arith.is_lt(lit))) {
|
||||
m_is_strict = true;
|
||||
}
|
||||
if (!is_int && !is_pos && (m_arith.is_ge(lit) || m_arith.is_le(lit))) {
|
||||
m_is_strict = true;
|
||||
}
|
||||
|
||||
|
||||
SASSERT(m_arith.is_int(s) || m_arith.is_real(s));
|
||||
expr_ref sign1(m), sign2(m), term(m);
|
||||
sign1 = m_arith.mk_numeral(m.is_eq(lit)?coeff:abs(coeff), s);
|
||||
sign2 = m_arith.mk_numeral(m.is_eq(lit)?-coeff:-abs(coeff), s);
|
||||
if (!m_sum.get()) {
|
||||
m_sum = m_arith.mk_numeral(rational(0), s);
|
||||
}
|
||||
|
||||
expr* a0 = lit->get_arg(0);
|
||||
expr* a1 = lit->get_arg(1);
|
||||
|
||||
if (is_pos && (m_arith.is_ge(lit) || m_arith.is_gt(lit))) {
|
||||
std::swap(a0, a1);
|
||||
}
|
||||
if (!is_pos && (m_arith.is_le(lit) || m_arith.is_lt(lit))) {
|
||||
std::swap(a0, a1);
|
||||
}
|
||||
|
||||
//
|
||||
// Multiplying by coefficients over strict
|
||||
// and non-strict inequalities:
|
||||
//
|
||||
// (a <= b) * 2
|
||||
// (a - b <= 0) * 2
|
||||
// (2a - 2b <= 0)
|
||||
|
||||
// (a < b) * 2 <=>
|
||||
// (a +1 <= b) * 2 <=>
|
||||
// 2a + 2 <= 2b <=>
|
||||
// 2a+2-2b <= 0
|
||||
|
||||
bool strict_ineq =
|
||||
is_pos?(m_arith.is_gt(lit) || m_arith.is_lt(lit)):(m_arith.is_ge(lit) || m_arith.is_le(lit));
|
||||
|
||||
if (is_int && strict_ineq) {
|
||||
m_sum = m_arith.mk_add(m_sum, sign1);
|
||||
}
|
||||
|
||||
term = m_arith.mk_mul(sign1, a0);
|
||||
m_sum = m_arith.mk_add(m_sum, term);
|
||||
term = m_arith.mk_mul(sign2, a1);
|
||||
m_sum = m_arith.mk_add(m_sum, term);
|
||||
|
||||
m_rw(m_sum);
|
||||
return true;
|
||||
}
|
||||
|
||||
expr_ref operator()(){
|
||||
if (!m_sum) normalize_coeff();
|
||||
m_sum.reset();
|
||||
for (auto &lit : m_lits) {
|
||||
if (!process_lit(lit)) return expr_ref(m);
|
||||
}
|
||||
return m_sum;
|
||||
}
|
||||
};
|
||||
|
||||
/*
|
||||
* ====================================
|
||||
|
|
@ -66,13 +202,154 @@ bool is_farkas_lemma(ast_manager& m, proof* pr)
|
|||
* ====================================
|
||||
*/
|
||||
|
||||
void theory_axiom_reducer::reset() {
|
||||
void theory_axiom_reducer::reset() {
|
||||
m_cache.reset();
|
||||
m_pinned.reset();
|
||||
}
|
||||
}
|
||||
|
||||
// -- rewrite theory axioms into theory lemmas
|
||||
proof_ref theory_axiom_reducer::reduce(proof* pr) {
|
||||
static proof_ref mk_th_lemma(ast_manager &m, ptr_buffer<proof> const &parents,
|
||||
unsigned num_params, parameter const *params) {
|
||||
buffer<parameter> v;
|
||||
for (unsigned i = 1; i < num_params; ++i)
|
||||
v.push_back(params[i]);
|
||||
|
||||
SASSERT(params[0].is_symbol());
|
||||
family_id tid = m.mk_family_id(params[0].get_symbol());
|
||||
SASSERT(tid != null_family_id);
|
||||
|
||||
proof_ref pf(m);
|
||||
pf = m.mk_th_lemma(tid, m.mk_false(),
|
||||
parents.size(), parents.c_ptr(),
|
||||
v.size(), v.c_ptr());
|
||||
return pf;
|
||||
}
|
||||
|
||||
static bool match_mul(expr *e, expr_ref &var, expr_ref &val, arith_util &a) {
|
||||
expr *e1 = nullptr, *e2 = nullptr;
|
||||
if (!a.is_mul(e, e1, e2)) {
|
||||
if (a.is_numeral(e)) return false;
|
||||
if (!var || var == e) {
|
||||
var = e;
|
||||
val = a.mk_numeral(rational(1), get_sort(e));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
if (!a.is_numeral(e1)) std::swap(e1, e2);
|
||||
if (!a.is_numeral(e1)) return false;
|
||||
|
||||
// if variable is given, match it as well
|
||||
if (!var || var == e2) {
|
||||
var = e2;
|
||||
val = e1;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static expr_ref get_coeff(expr *lit0, expr_ref &var) {
|
||||
ast_manager &m = var.m();
|
||||
arith_util a(m);
|
||||
|
||||
expr *lit = nullptr;
|
||||
if (!m.is_not(lit0, lit)) lit = lit0;
|
||||
|
||||
expr *e1 = nullptr, *e2 = nullptr;
|
||||
// assume e2 is numeral and ignore it
|
||||
if ((a.is_le(lit, e1, e2) || a.is_lt(lit, e1, e2) ||
|
||||
a.is_ge(lit, e1, e2) || a.is_gt(lit, e1, e2) ||
|
||||
m.is_eq(lit, e1, e2))) {
|
||||
if (a.is_numeral(e1)) std::swap(e1, e2);
|
||||
}
|
||||
else {
|
||||
e1 = lit;
|
||||
}
|
||||
|
||||
expr_ref val(m);
|
||||
if (!a.is_add(e1)) {
|
||||
if (match_mul(e1, var, val, a)) return val;
|
||||
}
|
||||
else {
|
||||
for (auto *arg : *to_app(e1)) {
|
||||
if (match_mul(arg, var, val, a)) return val;
|
||||
}
|
||||
}
|
||||
return expr_ref(m);
|
||||
}
|
||||
|
||||
// convert assign-bounds lemma to a farkas lemma by adding missing coeff
|
||||
// assume that missing coeff is for premise at position 0
|
||||
static proof_ref mk_fk_from_ab(ast_manager &m,
|
||||
ptr_buffer<proof> const &parents,
|
||||
unsigned num_params,
|
||||
parameter const *params) {
|
||||
SASSERT(num_params == parents.size() + 1 /* one param is missing */);
|
||||
|
||||
// compute missing coefficient
|
||||
linear_combinator lcb(m);
|
||||
for (unsigned i = 1, sz = parents.size(); i < sz; ++i) {
|
||||
app *p = to_app(m.get_fact(parents.get(i)));
|
||||
rational const &r = params[i+1].get_rational();
|
||||
lcb.add_lit(p, r);
|
||||
}
|
||||
|
||||
TRACE("spacer.fkab",
|
||||
tout << "lit0 is: " << mk_pp(m.get_fact(parents.get(0)), m) << "\n"
|
||||
<< "LCB is: " << lcb() << "\n";);
|
||||
|
||||
expr_ref var(m), val1(m), val2(m);
|
||||
val1 = get_coeff(m.get_fact(parents.get(0)), var);
|
||||
val2 = get_coeff(lcb(), var);
|
||||
TRACE("spacer.fkab",
|
||||
tout << "var: " << var
|
||||
<< " val1: " << val1 << " val2: " << val2 << "\n";);
|
||||
|
||||
rational rat1, rat2, coeff0;
|
||||
arith_util a(m);
|
||||
CTRACE("spacer.fkab", !(val1 && val2),
|
||||
tout << "Failed to match variables\n";);
|
||||
if (val1 && val2 &&
|
||||
a.is_numeral(val1, rat1) && a.is_numeral(val2, rat2)) {
|
||||
coeff0 = abs(rat2/rat1);
|
||||
coeff0 = coeff0 / lcb.lc();
|
||||
TRACE("spacer.fkab", tout << "coeff0: " << coeff0 << "\n";);
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(1, verbose_stream()
|
||||
<< "\n\n\nFAILED TO FIND COEFFICIENT\n\n\n";);
|
||||
// failed to find a coefficient
|
||||
return proof_ref(m);
|
||||
}
|
||||
|
||||
|
||||
buffer<parameter> v;
|
||||
v.push_back(parameter(symbol("farkas")));
|
||||
v.push_back(parameter(coeff0));
|
||||
for (unsigned i = 2; i < num_params; ++i)
|
||||
v.push_back(params[i]);
|
||||
|
||||
SASSERT(params[0].is_symbol());
|
||||
family_id tid = m.mk_family_id(params[0].get_symbol());
|
||||
SASSERT(tid != null_family_id);
|
||||
|
||||
proof_ref pf(m);
|
||||
pf = m.mk_th_lemma(tid, m.mk_false(),
|
||||
parents.size(), parents.c_ptr(),
|
||||
v.size(), v.c_ptr());
|
||||
|
||||
SASSERT(is_arith_lemma(m, pf));
|
||||
|
||||
DEBUG_CODE(
|
||||
proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
ENSURE(pc.check(pf, side)););
|
||||
return pf;
|
||||
|
||||
}
|
||||
|
||||
/// -- rewrite theory axioms into theory lemmas
|
||||
proof_ref theory_axiom_reducer::reduce(proof* pr) {
|
||||
proof_post_order pit(pr, m);
|
||||
while (pit.hasNext()) {
|
||||
proof* p = pit.next();
|
||||
|
|
@ -108,20 +385,22 @@ proof_ref theory_axiom_reducer::reduce(proof* pr) {
|
|||
hyps.push_back(hyp);
|
||||
}
|
||||
|
||||
// (b) create farkas lemma. Rebuild parameters since
|
||||
// mk_th_lemma() adds tid as first parameter
|
||||
unsigned num_params = p->get_decl()->get_num_parameters();
|
||||
parameter const* params = p->get_decl()->get_parameters();
|
||||
vector<parameter> parameters;
|
||||
for (unsigned i = 1; i < num_params; ++i) parameters.push_back(params[i]);
|
||||
// (b) Create a theory lemma
|
||||
proof_ref th_lemma(m);
|
||||
func_decl *d = p->get_decl();
|
||||
if (is_assign_bounds_lemma(m, p)) {
|
||||
|
||||
SASSERT(params[0].is_symbol());
|
||||
family_id tid = m.mk_family_id(params[0].get_symbol());
|
||||
SASSERT(tid != null_family_id);
|
||||
th_lemma = mk_fk_from_ab(m, hyps,
|
||||
d->get_num_parameters(),
|
||||
d->get_parameters());
|
||||
}
|
||||
|
||||
proof* th_lemma = m.mk_th_lemma(tid, m.mk_false(),
|
||||
hyps.size(), hyps.c_ptr(),
|
||||
num_params-1, parameters.c_ptr());
|
||||
// fall back to th-lemma
|
||||
if (!th_lemma) {
|
||||
th_lemma = mk_th_lemma(m, hyps,
|
||||
d->get_num_parameters(),
|
||||
d->get_parameters());
|
||||
}
|
||||
m_pinned.push_back(th_lemma);
|
||||
SASSERT(is_arith_lemma(m, th_lemma));
|
||||
|
||||
|
|
@ -171,13 +450,13 @@ proof_ref theory_axiom_reducer::reduce(proof* pr) {
|
|||
);
|
||||
|
||||
return proof_ref(res, m);
|
||||
}
|
||||
}
|
||||
|
||||
/* ------------------------------------------------------------------------- */
|
||||
/* hypothesis_reducer */
|
||||
/* ------------------------------------------------------------------------- */
|
||||
|
||||
proof_ref hypothesis_reducer::reduce(proof* pr) {
|
||||
proof_ref hypothesis_reducer::reduce(proof* pr) {
|
||||
compute_hypsets(pr);
|
||||
collect_units(pr);
|
||||
|
||||
|
|
@ -189,9 +468,9 @@ proof_ref hypothesis_reducer::reduce(proof* pr) {
|
|||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(res, side)););
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
void hypothesis_reducer::reset() {
|
||||
void hypothesis_reducer::reset() {
|
||||
m_active_hyps.reset();
|
||||
m_units.reset();
|
||||
m_cache.reset();
|
||||
|
|
@ -201,9 +480,9 @@ void hypothesis_reducer::reset() {
|
|||
m_hyp_mark.reset();
|
||||
m_open_mark.reset();
|
||||
m_visited.reset();
|
||||
}
|
||||
}
|
||||
|
||||
void hypothesis_reducer::compute_hypsets(proof *pr) {
|
||||
void hypothesis_reducer::compute_hypsets(proof *pr) {
|
||||
ptr_buffer<proof> todo;
|
||||
todo.push_back(pr);
|
||||
|
||||
|
|
@ -267,11 +546,11 @@ void hypothesis_reducer::compute_hypsets(proof *pr) {
|
|||
m_active_hyps.insert(p, active_hyps);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// collect all units that are hyp-free and are used as hypotheses somewhere
|
||||
// requires that m_active_hyps has been computed
|
||||
void hypothesis_reducer::collect_units(proof* pr) {
|
||||
void hypothesis_reducer::collect_units(proof* pr) {
|
||||
|
||||
proof_post_order pit(pr, m);
|
||||
while (pit.hasNext()) {
|
||||
|
|
@ -284,12 +563,12 @@ void hypothesis_reducer::collect_units(proof* pr) {
|
|||
m_units.insert(m.get_fact(p), p);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief returns true if p is an ancestor of q
|
||||
*/
|
||||
bool hypothesis_reducer::is_ancestor(proof *p, proof *q) {
|
||||
*/
|
||||
bool hypothesis_reducer::is_ancestor(proof *p, proof *q) {
|
||||
if (p == q) return true;
|
||||
ptr_vector<proof> todo;
|
||||
todo.push_back(q);
|
||||
|
|
@ -310,9 +589,9 @@ bool hypothesis_reducer::is_ancestor(proof *p, proof *q) {
|
|||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
proof* hypothesis_reducer::reduce_core(proof* pf) {
|
||||
proof* hypothesis_reducer::reduce_core(proof* pf) {
|
||||
SASSERT(m.is_false(m.get_fact(pf)));
|
||||
|
||||
proof *res = NULL;
|
||||
|
|
@ -412,9 +691,9 @@ proof* hypothesis_reducer::reduce_core(proof* pf) {
|
|||
}
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
}
|
||||
|
||||
proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
|
||||
proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
|
||||
SASSERT(m.is_false(m.get_fact(premise)));
|
||||
SASSERT(m_active_hyps.contains(premise));
|
||||
|
||||
|
|
@ -448,9 +727,9 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
|
|||
res = m.mk_lemma(premise, lemma);
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures,
|
||||
proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures,
|
||||
ptr_buffer<proof>& args) {
|
||||
// if any literal is false, we don't need a unit resolution step
|
||||
// This can be the case due to some previous transformations
|
||||
|
|
@ -528,9 +807,9 @@ proof* hypothesis_reducer::mk_unit_resolution_core(proof *ures,
|
|||
m_pinned.push_back(res);
|
||||
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
proof* hypothesis_reducer::mk_proof_core(proof* old, ptr_buffer<proof>& args) {
|
||||
proof* hypothesis_reducer::mk_proof_core(proof* old, ptr_buffer<proof>& args) {
|
||||
// if any of the literals are false, we don't need a step
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
if (m.is_false(m.get_fact(args[i]))) {
|
||||
|
|
@ -550,6 +829,6 @@ proof* hypothesis_reducer::mk_proof_core(proof* old, ptr_buffer<proof>& args) {
|
|||
(expr * const*)args.c_ptr());
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -36,28 +36,27 @@ void unsat_core_learner::register_plugin(unsat_core_plugin* plugin) {
|
|||
}
|
||||
|
||||
void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
|
||||
// traverse proof
|
||||
proof_post_order it(m_pr.get(), m);
|
||||
while (it.hasNext()) {
|
||||
proof* currentNode = it.next();
|
||||
proof* curr = it.next();
|
||||
|
||||
if (m.get_num_parents(currentNode) > 0) {
|
||||
bool need_to_mark_closed = true;
|
||||
bool done = is_closed(curr);
|
||||
if (done) continue;
|
||||
|
||||
for (proof* premise : m.get_parents(currentNode)) {
|
||||
need_to_mark_closed &= (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
|
||||
if (m.get_num_parents(curr) > 0) {
|
||||
done = true;
|
||||
for (proof* p : m.get_parents(curr)) done &= !is_b_open(p);
|
||||
set_closed(curr, done);
|
||||
}
|
||||
|
||||
// save result
|
||||
m_closed.mark(currentNode, need_to_mark_closed);
|
||||
// we have now collected all necessary information,
|
||||
// so we can visit the node
|
||||
// if the node mixes A-reasoning and B-reasoning
|
||||
// and contains non-closed premises
|
||||
if (!done) {
|
||||
if (is_a(curr) && is_b(curr)) {
|
||||
compute_partial_core(curr);
|
||||
}
|
||||
|
||||
// we have now collected all necessary information, so we can visit the node
|
||||
// if the node mixes A-reasoning and B-reasoning and contains non-closed premises
|
||||
if (m_pr.is_a_marked(currentNode) &&
|
||||
m_pr.is_b_marked(currentNode) &&
|
||||
!m_closed.is_marked(currentNode)) {
|
||||
compute_partial_core(currentNode); // then we need to compute a partial core
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -74,7 +73,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core) {
|
|||
|
||||
void unsat_core_learner::compute_partial_core(proof* step) {
|
||||
for (unsat_core_plugin* plugin : m_plugins) {
|
||||
if (m_closed.is_marked(step)) break;
|
||||
if (is_closed(step)) break;
|
||||
plugin->compute_partial_core(step);
|
||||
}
|
||||
}
|
||||
|
|
@ -93,9 +92,6 @@ void unsat_core_learner::set_closed(proof* p, bool value) {
|
|||
m_closed.mark(p, value);
|
||||
}
|
||||
|
||||
bool unsat_core_learner::is_b_open(proof *p) {
|
||||
return m_pr.is_b_marked(p) && !is_closed (p);
|
||||
}
|
||||
|
||||
void unsat_core_learner::add_lemma_to_core(expr* lemma) {
|
||||
m_unsat_core.push_back(lemma);
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Revision History:
|
|||
#include "ast/ast.h"
|
||||
#include "muz/spacer/spacer_util.h"
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
|
@ -31,13 +32,32 @@ namespace spacer {
|
|||
class unsat_core_learner {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
||||
ast_manager& m;
|
||||
iuc_proof& m_pr;
|
||||
|
||||
ptr_vector<unsat_core_plugin> m_plugins;
|
||||
ast_mark m_closed;
|
||||
|
||||
expr_ref_vector m_unsat_core;
|
||||
|
||||
public:
|
||||
unsat_core_learner(ast_manager& m, iuc_proof& pr) :
|
||||
m(m), m_pr(pr), m_unsat_core(m) {};
|
||||
virtual ~unsat_core_learner();
|
||||
|
||||
ast_manager& m;
|
||||
iuc_proof& m_pr;
|
||||
ast_manager& get_manager() {return m;}
|
||||
|
||||
|
||||
bool is_a(proof *pr) {
|
||||
// AG: treat hypotheses as A
|
||||
// AG: assume that all B-hyp have been eliminated
|
||||
// AG: this is not yet true in case of arithmetic eq_prop
|
||||
return m_pr.is_a_marked(pr) || is_h(pr);
|
||||
}
|
||||
bool is_b(proof *pr) {return m_pr.is_b_marked(pr);}
|
||||
bool is_h(proof *pr) {return m_pr.is_h_marked(pr);}
|
||||
bool is_b_pure(proof *pr) { return m_pr.is_b_pure(pr);}
|
||||
bool is_b_open(proof *p) {return m_pr.is_b_marked(p) && !is_closed (p);}
|
||||
|
||||
/*
|
||||
* register a plugin for computation of partial unsat cores
|
||||
|
|
@ -59,7 +79,6 @@ namespace spacer {
|
|||
bool is_closed(proof* p);
|
||||
void set_closed(proof* p, bool value);
|
||||
|
||||
bool is_b_open (proof *p);
|
||||
|
||||
/*
|
||||
* adds a lemma to the unsat core
|
||||
|
|
@ -67,14 +86,6 @@ namespace spacer {
|
|||
void add_lemma_to_core(expr* lemma);
|
||||
|
||||
private:
|
||||
ptr_vector<unsat_core_plugin> m_plugins;
|
||||
ast_mark m_closed;
|
||||
|
||||
/*
|
||||
* collects the lemmas of the unsat-core
|
||||
* will at the end be inserted into unsat_core.
|
||||
*/
|
||||
expr_ref_vector m_unsat_core;
|
||||
|
||||
/*
|
||||
* computes partial core for step by delegating computation to plugins
|
||||
|
|
|
|||
|
|
@ -34,27 +34,25 @@ Revision History:
|
|||
|
||||
namespace spacer {
|
||||
|
||||
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& learner):
|
||||
m(learner.m), m_learner(learner) {};
|
||||
unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx):
|
||||
m(ctx.get_manager()), m_ctx(ctx) {};
|
||||
|
||||
void unsat_core_plugin_lemma::compute_partial_core(proof* step) {
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
|
||||
for (proof* premise : m.get_parents(step)) {
|
||||
|
||||
if (m_learner.is_b_open (premise)) {
|
||||
for (auto* p : m.get_parents(step)) {
|
||||
if (m_ctx.is_b_open (p)) {
|
||||
// by IH, premises that are AB marked are already closed
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
add_lowest_split_to_core(premise);
|
||||
SASSERT(!m_ctx.is_a(p));
|
||||
add_lowest_split_to_core(p);
|
||||
}
|
||||
}
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
}
|
||||
|
||||
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const
|
||||
{
|
||||
SASSERT(m_learner.is_b_open(step));
|
||||
void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const {
|
||||
SASSERT(m_ctx.is_b_open(step));
|
||||
|
||||
ptr_buffer<proof> todo;
|
||||
todo.push_back(step);
|
||||
|
|
@ -64,45 +62,46 @@ namespace spacer {
|
|||
todo.pop_back();
|
||||
|
||||
// if current step hasn't been processed,
|
||||
if (!m_learner.is_closed(pf)) {
|
||||
m_learner.set_closed(pf, true);
|
||||
if (!m_ctx.is_closed(pf)) {
|
||||
m_ctx.set_closed(pf, true);
|
||||
// the step is b-marked and not closed.
|
||||
// by I.H. the step must be already visited
|
||||
// so if it is also a-marked, it must be closed
|
||||
SASSERT(m_learner.m_pr.is_b_marked(pf));
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(pf));
|
||||
SASSERT(m_ctx.is_b(pf));
|
||||
SASSERT(!m_ctx.is_a(pf));
|
||||
|
||||
// the current step needs to be interpolated:
|
||||
expr* fact = m.get_fact(pf);
|
||||
// if we trust the current step and we are able to use it
|
||||
if (m_learner.m_pr.is_b_pure (pf) &&
|
||||
(m.is_asserted(pf) || is_literal(m, fact))) {
|
||||
if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || is_literal(m, fact))) {
|
||||
// just add it to the core
|
||||
m_learner.add_lemma_to_core(fact);
|
||||
m_ctx.add_lemma_to_core(fact);
|
||||
}
|
||||
// otherwise recurse on premises
|
||||
else {
|
||||
for (proof* premise : m.get_parents(pf))
|
||||
if (m_learner.is_b_open(premise))
|
||||
if (m_ctx.is_b_open(premise))
|
||||
todo.push_back(premise);
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step)
|
||||
{
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
/***
|
||||
* FARKAS
|
||||
*/
|
||||
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) {
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
// XXX this assertion should be true so there is no need to check for it
|
||||
SASSERT (!m_learner.is_closed (step));
|
||||
SASSERT (!m_ctx.is_closed (step));
|
||||
func_decl* d = step->get_decl();
|
||||
symbol sym;
|
||||
if (!m_learner.is_closed(step) && // if step is not already interpolated
|
||||
is_farkas_lemma(m, step)) {
|
||||
// weaker check: d->get_num_parameters() >= m.get_num_parents(step) + 2
|
||||
TRACE("spacer.farkas",
|
||||
tout << "looking at: " << mk_pp(step, m) << "\n";);
|
||||
if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) {
|
||||
// weaker check : d->get_num_parameters() >= m.get_num_parents(step) + 2
|
||||
|
||||
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
|
||||
SASSERT(m.has_fact(step));
|
||||
|
|
@ -135,32 +134,33 @@ namespace spacer {
|
|||
*/
|
||||
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
|
||||
|
||||
STRACE("spacer.farkas",
|
||||
verbose_stream() << "Farkas input: "<< "\n";
|
||||
TRACE("spacer.farkas",
|
||||
tout << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_learner.m_pr.is_b_pure (prem);
|
||||
verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
bool b_pure = m_ctx.is_b_pure (prem);
|
||||
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
bool can_be_closed = true;
|
||||
bool done = true;
|
||||
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * premise = m.get_parent(step, i);
|
||||
|
||||
if (m_learner.is_b_open (premise)) {
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
if (m_ctx.is_b_open (premise)) {
|
||||
SASSERT(!m_ctx.is_a(premise));
|
||||
|
||||
if (m_learner.m_pr.is_b_pure (step)) {
|
||||
if (m_ctx.is_b_pure (premise)) {
|
||||
if (!m_use_constant_from_a) {
|
||||
rational coefficient = params[i].get_rational();
|
||||
coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise)));
|
||||
}
|
||||
}
|
||||
else {
|
||||
can_be_closed = false;
|
||||
// -- mixed premise, won't be able to close this proof step
|
||||
done = false;
|
||||
|
||||
if (m_use_constant_from_a) {
|
||||
rational coefficient = params[i].get_rational();
|
||||
|
|
@ -176,6 +176,7 @@ namespace spacer {
|
|||
}
|
||||
}
|
||||
|
||||
// TBD: factor into another method
|
||||
if (m_use_constant_from_a) {
|
||||
params += m.get_num_parents(step); // point to the first Farkas coefficient, which corresponds to a formula in the conclusion
|
||||
|
||||
|
|
@ -205,13 +206,12 @@ namespace spacer {
|
|||
}
|
||||
|
||||
// only if all b-premises can be used directly, add the farkas core and close the step
|
||||
if (can_be_closed) {
|
||||
m_learner.set_closed(step, true);
|
||||
|
||||
// AG: this decision needs to be re-evaluated. If the proof cannot be closed, literals above
|
||||
// AG: it will go into the core. However, it does not mean that this literal should/could not be added.
|
||||
m_ctx.set_closed(step, done);
|
||||
expr_ref res = compute_linear_combination(coeff_lits);
|
||||
|
||||
m_learner.add_lemma_to_core(res);
|
||||
}
|
||||
TRACE("spacer.farkas", tout << "Farkas core: " << res << "\n";);
|
||||
m_ctx.add_lemma_to_core(res);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -235,12 +235,12 @@ namespace spacer {
|
|||
|
||||
void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step)
|
||||
{
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
|
||||
func_decl* d = step->get_decl();
|
||||
symbol sym;
|
||||
if (!m_learner.is_closed(step) && // if step is not already interpolated
|
||||
if (!m_ctx.is_closed(step) && // if step is not already interpolated
|
||||
is_farkas_lemma(m, step)) {
|
||||
SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
|
||||
SASSERT(m.has_fact(step));
|
||||
|
|
@ -249,13 +249,13 @@ namespace spacer {
|
|||
|
||||
parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient
|
||||
|
||||
STRACE("spacer.farkas",
|
||||
verbose_stream() << "Farkas input: "<< "\n";
|
||||
TRACE("spacer.farkas",
|
||||
tout << "Farkas input: "<< "\n";
|
||||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * prem = m.get_parent(step, i);
|
||||
rational coef = params[i].get_rational();
|
||||
bool b_pure = m_learner.m_pr.is_b_pure (prem);
|
||||
verbose_stream() << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m_learner.m) << "\n";
|
||||
bool b_pure = m_ctx.is_b_pure (prem);
|
||||
tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
|
||||
}
|
||||
);
|
||||
|
||||
|
|
@ -263,11 +263,11 @@ namespace spacer {
|
|||
for (unsigned i = 0; i < m.get_num_parents(step); ++i) {
|
||||
proof * premise = m.get_parent(step, i);
|
||||
|
||||
if (m_learner.m_pr.is_b_marked(premise) && !m_learner.is_closed(premise))
|
||||
if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise))
|
||||
{
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(premise));
|
||||
SASSERT(!m_ctx.is_a(premise));
|
||||
|
||||
if (m_learner.m_pr.is_b_pure(premise))
|
||||
if (m_ctx.is_b_pure(premise))
|
||||
{
|
||||
rational coefficient = params[i].get_rational();
|
||||
linear_combination.push_back
|
||||
|
|
@ -283,7 +283,7 @@ namespace spacer {
|
|||
// only if all b-premises can be used directly, close the step and add linear combinations for later processing
|
||||
if (can_be_closed)
|
||||
{
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
if (!linear_combination.empty())
|
||||
{
|
||||
m_linear_combinations.push_back(linear_combination);
|
||||
|
|
@ -349,7 +349,7 @@ namespace spacer {
|
|||
SASSERT(!coeff_lits.empty());
|
||||
expr_ref linear_combination = compute_linear_combination(coeff_lits);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
m_ctx.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -480,7 +480,7 @@ namespace spacer {
|
|||
SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already
|
||||
expr_ref linear_combination = compute_linear_combination(coeff_lits);
|
||||
|
||||
m_learner.add_lemma_to_core(linear_combination);
|
||||
m_ctx.add_lemma_to_core(linear_combination);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
|
@ -504,10 +504,10 @@ namespace spacer {
|
|||
{
|
||||
ptr_vector<proof> todo;
|
||||
|
||||
SASSERT(m_learner.m_pr.is_a_marked(step));
|
||||
SASSERT(m_learner.m_pr.is_b_marked(step));
|
||||
SASSERT(m_ctx.is_a(step));
|
||||
SASSERT(m_ctx.is_b(step));
|
||||
SASSERT(m.get_num_parents(step) > 0);
|
||||
SASSERT(!m_learner.is_closed(step));
|
||||
SASSERT(!m_ctx.is_closed(step));
|
||||
todo.push_back(step);
|
||||
|
||||
while (!todo.empty())
|
||||
|
|
@ -516,7 +516,7 @@ namespace spacer {
|
|||
todo.pop_back();
|
||||
|
||||
// if we need to deal with the node and if we haven't added the corresponding edges so far
|
||||
if (!m_learner.is_closed(current) && !m_visited.is_marked(current))
|
||||
if (!m_ctx.is_closed(current) && !m_visited.is_marked(current))
|
||||
{
|
||||
// compute smallest subproof rooted in current, which has only good edges
|
||||
// add an edge from current to each leaf of that subproof
|
||||
|
|
@ -527,7 +527,7 @@ namespace spacer {
|
|||
|
||||
}
|
||||
}
|
||||
m_learner.set_closed(step, true);
|
||||
m_ctx.set_closed(step, true);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -538,7 +538,7 @@ namespace spacer {
|
|||
ptr_buffer<proof> todo_subproof;
|
||||
|
||||
for (proof* premise : m.get_parents(step)) {
|
||||
if (m_learner.m_pr.is_b_marked(premise)) {
|
||||
if (m_ctx.is_b(premise)) {
|
||||
todo_subproof.push_back(premise);
|
||||
}
|
||||
}
|
||||
|
|
@ -548,21 +548,21 @@ namespace spacer {
|
|||
todo_subproof.pop_back();
|
||||
|
||||
// if we need to deal with the node
|
||||
if (!m_learner.is_closed(current))
|
||||
if (!m_ctx.is_closed(current))
|
||||
{
|
||||
SASSERT(!m_learner.m_pr.is_a_marked(current)); // by I.H. the step must be already visited
|
||||
SASSERT(!m_ctx.is_a(current)); // by I.H. the step must be already visited
|
||||
|
||||
// and the current step needs to be interpolated:
|
||||
if (m_learner.m_pr.is_b_marked(current))
|
||||
if (m_ctx.is_b(current))
|
||||
{
|
||||
// if we trust the current step and we are able to use it
|
||||
if (m_learner.m_pr.is_b_pure (current) &&
|
||||
if (m_ctx.is_b_pure (current) &&
|
||||
(m.is_asserted(current) ||
|
||||
is_literal(m, m.get_fact(current))))
|
||||
{
|
||||
// we found a leaf of the subproof, so
|
||||
// 1) we add corresponding edges
|
||||
if (m_learner.m_pr.is_a_marked(step))
|
||||
if (m_ctx.is_a(step))
|
||||
{
|
||||
add_edge(nullptr, current); // current is sink
|
||||
}
|
||||
|
|
@ -684,7 +684,7 @@ namespace spacer {
|
|||
m_min_cut.compute_min_cut(cut_nodes);
|
||||
|
||||
for (unsigned cut_node : cut_nodes) {
|
||||
m_learner.add_lemma_to_core(m_node_to_formula[cut_node]);
|
||||
m_ctx.add_lemma_to_core(m_node_to_formula[cut_node]);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ namespace spacer {
|
|||
virtual void compute_partial_core(proof* step) = 0;
|
||||
virtual void finalize(){};
|
||||
|
||||
unsat_core_learner& m_learner;
|
||||
unsat_core_learner& m_ctx;
|
||||
};
|
||||
|
||||
class unsat_core_plugin_lemma : public unsat_core_plugin {
|
||||
|
|
|
|||
Loading…
Reference in a new issue