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

move proof utils under ast

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-24 09:59:55 -07:00
parent 1315c8d7de
commit fc822af707
12 changed files with 722 additions and 869 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

676
src/ast/proofs/proof_utils.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/proofs/proof_utils.h" #include "ast/proofs/proof_utils.h"
#include "ast/proofs/proof_checker.h" #include "ast/proofs/proof_checker.h"
#include "util/container_util.h"
@ -331,3 +332,678 @@ void reduce_hypotheses(proof_ref &pr) {
SASSERT(pc.check(pr, side)); SASSERT(pc.check(pr, side));
); );
} }
#include "ast/ast_smt2_pp.h"
#include "ast/rewriter/var_subst.h"
class reduce_hypotheses0 {
typedef obj_hashtable<expr> expr_set;
ast_manager& m;
// reference for any expression created by the tranformation
expr_ref_vector m_refs;
// currently computed result
obj_map<proof,proof*> m_cache;
// map conclusions to closed proofs that derive them
obj_map<expr, proof*> m_units;
// currently active units
ptr_vector<expr> m_units_trail;
// size of m_units_trail at the last push
unsigned_vector m_limits;
// map from proofs to active hypotheses
obj_map<proof, expr_set*> m_hypmap;
// refernce train for hypotheses sets
ptr_vector<expr_set> m_hyprefs;
ptr_vector<expr> m_literals;
void reset() {
m_refs.reset();
m_cache.reset();
m_units.reset();
m_units_trail.reset();
m_limits.reset();
std::for_each(m_hyprefs.begin(), m_hyprefs.end(), delete_proc<expr_set>());
m_hypmap.reset();
m_hyprefs.reset();
m_literals.reset();
}
void push() {
m_limits.push_back(m_units_trail.size());
}
void pop() {
unsigned sz = m_limits.back();
while (m_units_trail.size() > sz) {
m_units.remove(m_units_trail.back());
m_units_trail.pop_back();
}
m_limits.pop_back();
}
void get_literals(expr* clause) {
m_literals.reset();
if (m.is_or(clause)) {
m_literals.append(to_app(clause)->get_num_args(), to_app(clause)->get_args());
}
else {
m_literals.push_back(clause);
}
}
void add_hypotheses(proof* p) {
expr_set* hyps = 0;
bool inherited = false;
if (p->get_decl_kind() == PR_HYPOTHESIS) {
hyps = alloc(expr_set);
hyps->insert(m.get_fact(p));
m_hyprefs.push_back(hyps);
}
else {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
expr_set* hyps1 = m_hypmap.find(m.get_parent(p, i));
if (hyps1) {
if (!hyps) {
hyps = hyps1;
inherited = true;
continue;
}
if (inherited) {
hyps = alloc(expr_set,*hyps);
m_hyprefs.push_back(hyps);
inherited = false;
}
set_union(*hyps, *hyps1);
}
}
}
m_hypmap.insert(p, hyps);
}
expr_ref complement_lit(expr* e) {
expr* e1;
if (m.is_not(e, e1)) {
return expr_ref(e1, m);
}
else {
return expr_ref(m.mk_not(e), m);
}
}
bool in_hypotheses(expr* e, expr_set* hyps) {
if (!hyps) {
return false;
}
expr_ref not_e = complement_lit(e);
return hyps->contains(not_e);
}
bool contains_hypothesis(proof* p) {
ptr_vector<proof> todo;
ast_mark visit;
todo.push_back(p);
while (!todo.empty()) {
p = todo.back();
todo.pop_back();
if (visit.is_marked(p)) {
continue;
}
visit.mark(p, true);
if (PR_HYPOTHESIS == p->get_decl_kind()) {
return true;
}
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
todo.push_back(m.get_parent(p, i));
}
}
return false;
}
bool is_closed(proof* p) {
expr_set* hyps = m_hypmap.find(p);
return !hyps || hyps->empty();
}
public:
reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
void operator()(proof_ref& pr) {
proof_ref tmp(m);
tmp = pr;
elim(pr);
reset();
CTRACE("proof_utils", contains_hypothesis(pr),
tout << "Contains hypothesis:\n";
tout << mk_ismt2_pp(tmp, m) << "\n====>\n";
tout << mk_ismt2_pp(pr, m) << "\n";);
}
void elim(proof_ref& p) {
proof_ref tmp(m);
proof* result = p.get();
if (m_cache.find(p, result)) {
p = result;
return;
}
//SASSERT (p.get () == result);
switch(p->get_decl_kind()) {
case PR_HYPOTHESIS:
// replace result by m_units[m.get_fact (p)] if defined
// AG: This is the main step. Replace a hypothesis by a derivation of its consequence
if (!m_units.find(m.get_fact(p), result)) {
// restore ther result back to p
result = p.get();
}
// compute hypothesis of the result
// not clear what 'result' is at this point.
// probably the proof at the top of the call
// XXX not clear why this is re-computed each time
// XXX moreover, m_units are guaranteed to be closed!
// XXX so no hypotheses are needed for them
add_hypotheses(result);
break;
case PR_LEMMA: {
SASSERT(m.get_num_parents(p) == 1);
tmp = m.get_parent(p, 0);
// eliminate hypothesis recursively in the proof of the lemma
elim(tmp);
expr_set* hyps = m_hypmap.find(tmp);
expr_set* new_hyps = 0;
// XXX if the proof is correct, the hypotheses of the tmp
// XXX should be exactly those of the consequence of the lemma
// XXX but if this code actually eliminates hypotheses, the set might be a subset
if (hyps) {
new_hyps = alloc(expr_set, *hyps);
}
expr* fact = m.get_fact(p);
// when hypothesis is a single literal of the form
// (or A B), and the fact of p is (or A B).
if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
m_literals.reset();
m_literals.push_back(fact);
}
else {
get_literals(fact);
}
// go over all the literals in the consequence of the lemma
for (unsigned i = 0; i < m_literals.size(); ++i) {
expr* e = m_literals[i];
// if the literal is not in hypothesis, skip it
if (!in_hypotheses(e, hyps)) {
m_literals[i] = m_literals.back();
m_literals.pop_back();
--i;
}
// if the literal is in hypothesis remove it because
// it is not in hypothesis set of the lemma
// XXX but we assume that lemmas have empty hypothesis set.
// XXX eventually every element of new_hyps must be removed!
else {
SASSERT(new_hyps);
expr_ref not_e = complement_lit(e);
SASSERT(new_hyps->contains(not_e));
new_hyps->remove(not_e);
}
}
// killed all hypotheses, so can stop at the lemma since
// we have a closed pf of false
if (m_literals.empty()) {
result = tmp;
}
else {
// create a new lemma, but might be re-creating existing one
expr_ref clause(m);
if (m_literals.size() == 1) {
clause = m_literals[0];
}
else {
clause = m.mk_or(m_literals.size(), m_literals.c_ptr());
}
tmp = m.mk_lemma(tmp, clause);
m_refs.push_back(tmp);
result = tmp;
}
if (new_hyps && new_hyps->empty()) {
dealloc(new_hyps);
new_hyps = 0;
}
m_hypmap.insert(result, new_hyps);
// might push 0 into m_hyprefs. No reason for that
m_hyprefs.push_back(new_hyps);
TRACE("proof_utils",
tout << "New lemma: " << mk_pp(m.get_fact(p), m)
<< "\n==>\n"
<< mk_pp(m.get_fact(result), m) << "\n";
if (hyps) {
expr_set::iterator it = hyps->begin();
expr_set::iterator end = hyps->end();
for (; it != end; ++it) {
tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
}
});
break;
}
case PR_UNIT_RESOLUTION: {
proof_ref_vector parents(m);
// get the clause being resolved with
parents.push_back(m.get_parent(p, 0));
// save state
push();
bool found_false = false;
// for every derivation of a unit literal
for (unsigned i = 1; i < m.get_num_parents(p); ++i) {
// see if it derives false
tmp = m.get_parent(p, i);
elim(tmp);
if (m.is_false(m.get_fact(tmp))) {
// if derived false, the whole pf is false and we can bail out
result = tmp;
found_false = true;
break;
}
// -- otherwise, the fact has not changed. nothing to simplify
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
parents.push_back(tmp);
// remember that we have this derivation while we have not poped the trail
// but only if the proof is closed (i.e., a real unit)
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
m_units.insert(m.get_fact(tmp), tmp);
m_units_trail.push_back(m.get_fact(tmp));
}
}
if (found_false) {
pop();
break;
}
// look at the clause being resolved with
tmp = m.get_parent(p, 0);
// remember its fact
expr* old_clause = m.get_fact(tmp);
// attempt to reduce its fact
elim(tmp);
// update parents
parents[0] = tmp;
// if the new fact is false, bail out
expr* clause = m.get_fact(tmp);
if (m.is_false(clause)) {
m_refs.push_back(tmp);
result = tmp;
pop();
break;
}
//
// case where clause is a literal in the old clause.
// i.e., reduce multi-literal clause to a unit
//
if (is_literal_in_clause(clause, old_clause)) {
// if the resulting literal was resolved, get a pf of false and bail out
bool found = false;
for (unsigned i = 1; !found && i < parents.size(); ++i) {
if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
parents[1] = parents[i].get();
parents.resize(2);
result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
m_refs.push_back(result);
add_hypotheses(result);
found = true;
}
}
// else if the resulting literal is not resolved, it is the new consequence
if (!found) {
result = parents[0].get();
}
pop();
break;
}
//
// case where new clause is a subset of old clause.
// the literals in clause should be a subset of literals in old_clause.
//
get_literals(clause);
for (unsigned i = 1; i < parents.size(); ++i) {
bool found = false;
for (unsigned j = 0; j < m_literals.size(); ++j) {
if (m.is_complement(m_literals[j], m.get_fact(parents[i].get()))) {
found = true;
break;
}
}
if (!found) {
// literal was removed as hypothesis.
parents[i] = parents.back();
parents.pop_back();
--i;
}
}
if (parents.size() == 1) {
result = parents[0].get();
}
else {
result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
m_refs.push_back(result);
add_hypotheses(result);
}
pop();
break;
}
default: {
ptr_buffer<expr> args;
bool change = false;
bool found_false = false;
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
tmp = m.get_parent(p, i);
elim(tmp);
if (m.is_false(m.get_fact(tmp))) {
result = tmp;
found_false = true;
break;
}
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
change = change || (tmp != m.get_parent(p, i));
args.push_back(tmp);
}
if (found_false) {
break;
}
if (m.has_fact(p)) {
args.push_back(m.get_fact(p));
}
if (change) {
tmp = m.mk_app(p->get_decl(), args.size(), args.c_ptr());
m_refs.push_back(tmp);
}
else {
tmp = p;
}
result = tmp;
add_hypotheses(result);
break;
}
}
SASSERT(m_hypmap.contains(result));
m_cache.insert(p, result);
p = result;
}
bool is_literal_in_clause(expr* fml, expr* clause) {
if (!m.is_or(clause)) {
return false;
}
app* cl = to_app(clause);
for (unsigned i = 0; i < cl->get_num_args(); ++i) {
if (cl->get_arg(i) == fml) {
return true;
}
}
return false;
}
};
void proof_utils::reduce_hypotheses(proof_ref& pr) {
ast_manager& m = pr.get_manager();
class reduce_hypotheses0 reduce(m);
reduce(pr);
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
}
class proof_is_closed {
ast_manager& m;
ptr_vector<expr> m_literals;
ast_mark m_visit;
void reset() {
m_literals.reset();
m_visit.reset();
}
bool check(proof* p) {
// really just a partial check because nodes may be visited
// already under a different lemma scope.
if (m_visit.is_marked(p)) {
return true;
}
bool result = false;
m_visit.mark(p, true);
switch(p->get_decl_kind()) {
case PR_LEMMA: {
unsigned sz = m_literals.size();
expr* cls = m.get_fact(p);
m_literals.push_back(cls);
if (m.is_or(cls)) {
m_literals.append(to_app(cls)->get_num_args(), to_app(cls)->get_args());
}
SASSERT(m.get_num_parents(p) == 1);
result = check(m.get_parent(p, 0));
m_literals.resize(sz);
break;
}
case PR_HYPOTHESIS: {
expr* fact = m.get_fact(p);
for (unsigned i = 0; i < m_literals.size(); ++i) {
if (m.is_complement(m_literals[i], fact)) {
result = true;
break;
}
}
break;
}
default:
result = true;
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
if (!check(m.get_parent(p, i))) {
result = false;
break;
}
}
break;
}
return result;
}
public:
proof_is_closed(ast_manager& m): m(m) {}
bool operator()(proof *p) {
bool ok = check(p);
reset();
return ok;
}
};
bool proof_utils::is_closed(ast_manager& m, proof* p) {
proof_is_closed checker(m);
return checker(p);
}
static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
ast_manager& m = pr.get_manager();
proof* pr2 = 0;
proof_ref_vector parents(m);
proof_ref prNew(pr);
if (cache.find(pr, pr2)) {
pr = pr2;
return;
}
for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
prNew = m.get_parent(pr, i);
permute_unit_resolution(refs, cache, prNew);
parents.push_back(prNew);
}
prNew = pr;
if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
parents[0]->get_decl_kind() == PR_TH_LEMMA) {
/*
Unit resolution:
T1: (or l_1 ... l_n l_1' ... l_m')
T2: (not l_1)
...
T(n+1): (not l_n)
[unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
Th lemma:
T1: (not l_1)
...
Tn: (not l_n)
[th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
Implement conversion:
T1 |- not l_1 ... Tn |- not l_n
------------------------------- TH_LEMMA
(or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m
-------------------------------------------------------------- UNIT_RESOLUTION
(or j_1 .. j_m)
|->
T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
---------------------------------------------------------------- TH_LEMMA
(or j_1 .. j_m)
*/
proof_ref_vector premises(m);
proof* thLemma = parents[0].get();
for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
premises.push_back(m.get_parent(thLemma, i));
}
for (unsigned i = 1; i < parents.size(); ++i) {
premises.push_back(parents[i].get());
}
parameter const* params = thLemma->get_decl()->get_parameters();
unsigned num_params = thLemma->get_decl()->get_num_parameters();
SASSERT(params[0].is_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
// AG: This can break a theory lemma. In particular, for Farkas lemmas the coefficients
// AG: for the literals propagated from the unit resolution are missing.
// AG: Why is this a good thing to do?
// AG: This can lead to merging of the units with other terms in interpolation,
// AG: but without farkas coefficients this does not make sense
prNew = m.mk_th_lemma(tid, m.get_fact(pr),
premises.size(), premises.c_ptr(), num_params-1, params+1);
}
else {
ptr_vector<expr> args;
for (unsigned i = 0; i < parents.size(); ++i) {
args.push_back(parents[i].get());
}
if (m.has_fact(pr)) {
args.push_back(m.get_fact(pr));
}
prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
}
cache.insert(pr, prNew);
refs.push_back(prNew);
pr = prNew;
}
// permute unit resolution over Theory lemmas to track premises.
void proof_utils::permute_unit_resolution(proof_ref& pr) {
expr_ref_vector refs(pr.get_manager());
obj_map<proof,proof*> cache;
::permute_unit_resolution(refs, cache, pr);
}
class push_instantiations_up_cl {
ast_manager& m;
public:
push_instantiations_up_cl(ast_manager& m): m(m) {}
void operator()(proof_ref& p) {
expr_ref_vector s0(m);
p = push(p, s0);
}
private:
proof* push(proof* p, expr_ref_vector const& sub) {
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
for (unsigned i = 0; i < premises.size(); ++i) {
compose(substs[i], sub);
premises[i] = push(premises[i].get(), substs[i]);
substs[i].reset();
}
instantiate(sub, conclusion);
return
m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion,
positions,
substs);
}
if (sub.empty()) {
return p;
}
if (m.is_modus_ponens(p)) {
SASSERT(m.get_num_parents(p) == 2);
proof* p0 = m.get_parent(p, 0);
proof* p1 = m.get_parent(p, 1);
if (m.get_fact(p0) == m.get_fact(p)) {
return push(p0, sub);
}
expr* e1, *e2;
if (m.is_rewrite(p1, e1, e2) &&
is_quantifier(e1) && is_quantifier(e2) &&
to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
expr_ref r1(e1,m), r2(e2,m);
instantiate(sub, r1);
instantiate(sub, r2);
p1 = m.mk_rewrite(r1, r2);
return m.mk_modus_ponens(push(p0, sub), p1);
}
}
premises.push_back(p);
substs.push_back(sub);
conclusion = m.get_fact(p);
instantiate(sub, conclusion);
return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
}
void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
for (unsigned i = 0; i < sub.size(); ++i) {
expr_ref e(m);
var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
sub[i] = e;
}
}
void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
if (sub.empty()) {
return;
}
if (!is_forall(fml)) {
return;
}
quantifier* q = to_quantifier(fml);
if (q->get_num_decls() != sub.size()) {
TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
tout << mk_pp(q, m) << "\n";
tout << sub.size() << "\n";);
return;
}
var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
}
};
void proof_utils::push_instantiations_up(proof_ref& pr) {
push_instantiations_up_cl push(pr.get_manager());
push(pr);
}

31
src/ast/proofs/proof_utils.h
View file

@ -16,8 +16,8 @@ Revision History:
--*/ --*/
#ifndef _PROOF_UTILS_H_ #ifndef PROOF_UTILS_H_
#define _PROOF_UTILS_H_ #define PROOF_UTILS_H_
#include "ast/ast.h" #include "ast/ast.h"
/* /*
@ -39,4 +39,31 @@ private:
void reduce_hypotheses(proof_ref &pr); void reduce_hypotheses(proof_ref &pr);
class proof_utils {
public:
/**
\brief reduce the set of hypotheses used in the proof.
*/
static void reduce_hypotheses(proof_ref& pr);
/**
\brief Check that a proof does not contain open hypotheses.
*/
static bool is_closed(ast_manager& m, proof* p);
/**
\brief Permute unit resolution rule with th-lemma
*/
static void permute_unit_resolution(proof_ref& pr);
/**
\brief Push instantiations created in hyper-resolutions up to leaves.
This produces a "ground" proof where leaves are annotated by instantiations.
*/
static void push_instantiations_up(proof_ref& pr);
};
#endif #endif

1
src/muz/base/CMakeLists.txt
View file

@ -10,7 +10,6 @@ z3_add_component(muz
dl_rule_transformer.cpp dl_rule_transformer.cpp
dl_util.cpp dl_util.cpp
hnf.cpp hnf.cpp
proof_utils.cpp
rule_properties.cpp rule_properties.cpp
COMPONENT_DEPENDENCIES COMPONENT_DEPENDENCIES
aig_tactic aig_tactic

2
src/muz/base/dl_boogie_proof.cpp
View file

@ -53,7 +53,7 @@ Example from Boogie:
#include "muz/base/dl_boogie_proof.h" #include "muz/base/dl_boogie_proof.h"
#include "model/model_pp.h" #include "model/model_pp.h"
#include "muz/base/proof_utils.h" #include "ast/proofs/proof_utils.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"

128
src/muz/base/dl_util.h
View file

@ -11,7 +11,7 @@ Abstract:
Author: Author:
Leonardo de Moura (leonardo) 2010-05-20. Krystof Hoder 2010
Revision History: Revision History:
@ -31,6 +31,7 @@ Revision History:
#include "util/statistics.h" #include "util/statistics.h"
#include "util/stopwatch.h" #include "util/stopwatch.h"
#include "util/lbool.h" #include "util/lbool.h"
#include "util/container_util.h"
namespace datalog { namespace datalog {
@ -381,129 +382,6 @@ namespace datalog {
*/ */
void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub); void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub);
// -----------------------------------
//
// container functions
//
// -----------------------------------
template<class Set1, class Set2>
void set_intersection(Set1 & tgt, const Set2 & src) {
svector<typename Set1::data> to_remove;
typename Set1::iterator vit = tgt.begin();
typename Set1::iterator vend = tgt.end();
for(;vit!=vend;++vit) {
typename Set1::data itm=*vit;
if(!src.contains(itm)) {
to_remove.push_back(itm);
}
}
while(!to_remove.empty()) {
tgt.remove(to_remove.back());
to_remove.pop_back();
}
}
template<class Set>
void set_difference(Set & tgt, const Set & to_remove) {
typename Set::iterator vit = to_remove.begin();
typename Set::iterator vend = to_remove.end();
for(;vit!=vend;++vit) {
typename Set::data itm=*vit;
tgt.remove(itm);
}
}
template<class Set1, class Set2>
void set_union(Set1 & tgt, const Set2 & to_add) {
typename Set2::iterator vit = to_add.begin();
typename Set2::iterator vend = to_add.end();
for(;vit!=vend;++vit) {
typename Set1::data itm=*vit;
tgt.insert(itm);
}
}
void idx_set_union(idx_set & tgt, const idx_set & src);
template<class T>
void unite_disjoint_maps(T & tgt, const T & src) {
typename T::iterator it = src.begin();
typename T::iterator end = src.end();
for(; it!=end; ++it) {
SASSERT(!tgt.contains(it->m_key));
tgt.insert(it->m_key, it->m_value);
}
}
template<class T, class U>
void collect_map_range(T & acc, const U & map) {
typename U::iterator it = map.begin();
typename U::iterator end = map.end();
for(; it!=end; ++it) {
acc.push_back(it->m_value);
}
}
template<class T>
void print_container(const T & begin, const T & end, std::ostream & out) {
T it = begin;
out << "(";
bool first = true;
for(; it!=end; ++it) {
if(first) { first = false; } else { out << ","; }
out << (*it);
}
out << ")";
}
template<class T>
void print_container(const T & cont, std::ostream & out) {
print_container(cont.begin(), cont.end(), out);
}
template<class T, class M>
void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
}
template<class T>
void print_map(const T & cont, std::ostream & out) {
typename T::iterator it = cont.begin();
typename T::iterator end = cont.end();
out << "(";
bool first = true;
for(; it!=end; ++it) {
if(first) { first = false; } else { out << ","; }
out << it->m_key << "->" << it->m_value;
}
out << ")";
}
template<class It, class V>
unsigned find_index(const It & begin, const It & end, const V & val) {
unsigned idx = 0;
It it = begin;
for(; it!=end; it++, idx++) {
if(*it==val) {
return idx;
}
}
return UINT_MAX;
}
template<class T, class U>
bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
T it1 = begin1;
U it2 = begin2;
for(; it1!=end1 && it2!=end2; ++it1, ++it2) {
if(*it1!=*it2) {
return false;
}
}
return it1==end1 && it2==end2;
}
template<class T, class U> template<class T, class U>
bool vectors_equal(const T & c1, const U & c2) { bool vectors_equal(const T & c1, const U & c2) {
@ -521,6 +399,8 @@ namespace datalog {
return true; return true;
} }
void idx_set_union(idx_set & tgt, const idx_set & src);
template<class T> template<class T>
struct default_obj_chash { struct default_obj_chash {
unsigned operator()(T const& cont, unsigned i) const { unsigned operator()(T const& cont, unsigned i) const {

680
src/muz/base/proof_utils.cpp
View file

@ -1,680 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
#include "muz/base/dl_util.h"
#include "muz/base/proof_utils.h"
#include "ast/ast_smt2_pp.h"
#include "ast/rewriter/var_subst.h"
class reduce_hypotheses0 {
typedef obj_hashtable<expr> expr_set;
ast_manager& m;
// reference for any expression created by the tranformation
expr_ref_vector m_refs;
// currently computed result
obj_map<proof,proof*> m_cache;
// map conclusions to closed proofs that derive them
obj_map<expr, proof*> m_units;
// currently active units
ptr_vector<expr> m_units_trail;
// size of m_units_trail at the last push
unsigned_vector m_limits;
// map from proofs to active hypotheses
obj_map<proof, expr_set*> m_hypmap;
// refernce train for hypotheses sets
ptr_vector<expr_set> m_hyprefs;
ptr_vector<expr> m_literals;
void reset() {
m_refs.reset();
m_cache.reset();
m_units.reset();
m_units_trail.reset();
m_limits.reset();
std::for_each(m_hyprefs.begin(), m_hyprefs.end(), delete_proc<expr_set>());
m_hypmap.reset();
m_hyprefs.reset();
m_literals.reset();
}
void push() {
m_limits.push_back(m_units_trail.size());
}
void pop() {
unsigned sz = m_limits.back();
while (m_units_trail.size() > sz) {
m_units.remove(m_units_trail.back());
m_units_trail.pop_back();
}
m_limits.pop_back();
}
void get_literals(expr* clause) {
m_literals.reset();
if (m.is_or(clause)) {
m_literals.append(to_app(clause)->get_num_args(), to_app(clause)->get_args());
}
else {
m_literals.push_back(clause);
}
}
void add_hypotheses(proof* p) {
expr_set* hyps = 0;
bool inherited = false;
if (p->get_decl_kind() == PR_HYPOTHESIS) {
hyps = alloc(expr_set);
hyps->insert(m.get_fact(p));
m_hyprefs.push_back(hyps);
}
else {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
expr_set* hyps1 = m_hypmap.find(m.get_parent(p, i));
if (hyps1) {
if (!hyps) {
hyps = hyps1;
inherited = true;
continue;
}
if (inherited) {
hyps = alloc(expr_set,*hyps);
m_hyprefs.push_back(hyps);
inherited = false;
}
datalog::set_union(*hyps, *hyps1);
}
}
}
m_hypmap.insert(p, hyps);
}
expr_ref complement_lit(expr* e) {
expr* e1;
if (m.is_not(e, e1)) {
return expr_ref(e1, m);
}
else {
return expr_ref(m.mk_not(e), m);
}
}
bool in_hypotheses(expr* e, expr_set* hyps) {
if (!hyps) {
return false;
}
expr_ref not_e = complement_lit(e);
return hyps->contains(not_e);
}
bool contains_hypothesis(proof* p) {
ptr_vector<proof> todo;
ast_mark visit;
todo.push_back(p);
while (!todo.empty()) {
p = todo.back();
todo.pop_back();
if (visit.is_marked(p)) {
continue;
}
visit.mark(p, true);
if (PR_HYPOTHESIS == p->get_decl_kind()) {
return true;
}
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
todo.push_back(m.get_parent(p, i));
}
}
return false;
}
bool is_closed(proof* p) {
expr_set* hyps = m_hypmap.find(p);
return !hyps || hyps->empty();
}
public:
reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
void operator()(proof_ref& pr) {
proof_ref tmp(m);
tmp = pr;
elim(pr);
reset();
CTRACE("proof_utils", contains_hypothesis(pr),
tout << "Contains hypothesis:\n";
tout << mk_ismt2_pp(tmp, m) << "\n====>\n";
tout << mk_ismt2_pp(pr, m) << "\n";);
}
void elim(proof_ref& p) {
proof_ref tmp(m);
proof* result = p.get();
if (m_cache.find(p, result)) {
p = result;
return;
}
//SASSERT (p.get () == result);
switch(p->get_decl_kind()) {
case PR_HYPOTHESIS:
// replace result by m_units[m.get_fact (p)] if defined
// AG: This is the main step. Replace a hypothesis by a derivation of its consequence
if (!m_units.find(m.get_fact(p), result)) {
// restore ther result back to p
result = p.get();
}
// compute hypothesis of the result
// not clear what 'result' is at this point.
// probably the proof at the top of the call
// XXX not clear why this is re-computed each time
// XXX moreover, m_units are guaranteed to be closed!
// XXX so no hypotheses are needed for them
add_hypotheses(result);
break;
case PR_LEMMA: {
SASSERT(m.get_num_parents(p) == 1);
tmp = m.get_parent(p, 0);
// eliminate hypothesis recursively in the proof of the lemma
elim(tmp);
expr_set* hyps = m_hypmap.find(tmp);
expr_set* new_hyps = 0;
// XXX if the proof is correct, the hypotheses of the tmp
// XXX should be exactly those of the consequence of the lemma
// XXX but if this code actually eliminates hypotheses, the set might be a subset
if (hyps) {
new_hyps = alloc(expr_set, *hyps);
}
expr* fact = m.get_fact(p);
// when hypothesis is a single literal of the form
// (or A B), and the fact of p is (or A B).
if (hyps && hyps->size() == 1 && in_hypotheses(fact, hyps)) {
m_literals.reset();
m_literals.push_back(fact);
}
else {
get_literals(fact);
}
// go over all the literals in the consequence of the lemma
for (unsigned i = 0; i < m_literals.size(); ++i) {
expr* e = m_literals[i];
// if the literal is not in hypothesis, skip it
if (!in_hypotheses(e, hyps)) {
m_literals[i] = m_literals.back();
m_literals.pop_back();
--i;
}
// if the literal is in hypothesis remove it because
// it is not in hypothesis set of the lemma
// XXX but we assume that lemmas have empty hypothesis set.
// XXX eventually every element of new_hyps must be removed!
else {
SASSERT(new_hyps);
expr_ref not_e = complement_lit(e);
SASSERT(new_hyps->contains(not_e));
new_hyps->remove(not_e);
}
}
// killed all hypotheses, so can stop at the lemma since
// we have a closed pf of false
if (m_literals.empty()) {
result = tmp;
}
else {
// create a new lemma, but might be re-creating existing one
expr_ref clause(m);
if (m_literals.size() == 1) {
clause = m_literals[0];
}
else {
clause = m.mk_or(m_literals.size(), m_literals.c_ptr());
}
tmp = m.mk_lemma(tmp, clause);
m_refs.push_back(tmp);
result = tmp;
}
if (new_hyps && new_hyps->empty()) {
dealloc(new_hyps);
new_hyps = 0;
}
m_hypmap.insert(result, new_hyps);
// might push 0 into m_hyprefs. No reason for that
m_hyprefs.push_back(new_hyps);
TRACE("proof_utils",
tout << "New lemma: " << mk_pp(m.get_fact(p), m)
<< "\n==>\n"
<< mk_pp(m.get_fact(result), m) << "\n";
if (hyps) {
expr_set::iterator it = hyps->begin();
expr_set::iterator end = hyps->end();
for (; it != end; ++it) {
tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
}
});
break;
}
case PR_UNIT_RESOLUTION: {
proof_ref_vector parents(m);
// get the clause being resolved with
parents.push_back(m.get_parent(p, 0));
// save state
push();
bool found_false = false;
// for every derivation of a unit literal
for (unsigned i = 1; i < m.get_num_parents(p); ++i) {
// see if it derives false
tmp = m.get_parent(p, i);
elim(tmp);
if (m.is_false(m.get_fact(tmp))) {
// if derived false, the whole pf is false and we can bail out
result = tmp;
found_false = true;
break;
}
// -- otherwise, the fact has not changed. nothing to simplify
SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
parents.push_back(tmp);
// remember that we have this derivation while we have not poped the trail
// but only if the proof is closed (i.e., a real unit)
if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
m_units.insert(m.get_fact(tmp), tmp);
m_units_trail.push_back(m.get_fact(tmp));
}
}
if (found_false) {
pop();
break;
}
// look at the clause being resolved with
tmp = m.get_parent(p, 0);
// remember its fact
expr* old_clause = m.get_fact(tmp);
// attempt to reduce its fact
elim(tmp);
// update parents
parents[0] = tmp;
// if the new fact is false, bail out
expr* clause = m.get_fact(tmp);
if (m.is_false(clause)) {
m_refs.push_back(tmp);
result = tmp;
pop();
break;
}
//
// case where clause is a literal in the old clause.
// i.e., reduce multi-literal clause to a unit
//
if (is_literal_in_clause(clause, old_clause)) {
// if the resulting literal was resolved, get a pf of false and bail out
bool found = false;
for (unsigned i = 1; !found && i < parents.size(); ++i) {
if (m.is_complement(clause, m.get_fact(parents[i].get()))) {
parents[1] = parents[i].get();
parents.resize(2);
result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
m_refs.push_back(result);
add_hypotheses(result);
found = true;
}
}
// else if the resulting literal is not resolved, it is the new consequence
if (!found) {
result = parents[0].get();
}
pop();
break;
}
//
// case where new clause is a subset of old clause.
// the literals in clause should be a subset of literals in old_clause.
//
get_literals(clause);
for (unsigned i = 1; i < parents.size(); ++i) {
bool found = false;
for (unsigned j = 0; j < m_literals.size(); ++j) {
if (m.is_complement(m_literals[j], m.get_fact(parents[i].get()))) {
found = true;
break;
}
}
if (!found) {
// literal was removed as hypothesis.
parents[i] = parents.back();
parents.pop_back();
--i;
}
}
if (parents.size() == 1) {
result = parents[0].get();
}
else {
result = m.mk_unit_resolution(parents.size(), parents.c_ptr());
m_refs.push_back(result);
add_hypotheses(result);
}
pop();
break;
}
default: {
ptr_buffer<expr> args;
bool change = false;
bool found_false = false;
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
tmp = m.get_parent(p, i);
elim(tmp);
if (m.is_false(m.get_fact(tmp))) {
result = tmp;
found_false = true;
break;
}
// SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
change = change || (tmp != m.get_parent(p, i));
args.push_back(tmp);
}
if (found_false) {
break;
}
if (m.has_fact(p)) {
args.push_back(m.get_fact(p));
}
if (change) {
tmp = m.mk_app(p->get_decl(), args.size(), args.c_ptr());
m_refs.push_back(tmp);
}
else {
tmp = p;
}
result = tmp;
add_hypotheses(result);
break;
}
}
SASSERT(m_hypmap.contains(result));
m_cache.insert(p, result);
p = result;
}
bool is_literal_in_clause(expr* fml, expr* clause) {
if (!m.is_or(clause)) {
return false;
}
app* cl = to_app(clause);
for (unsigned i = 0; i < cl->get_num_args(); ++i) {
if (cl->get_arg(i) == fml) {
return true;
}
}
return false;
}
};
void proof_utils::reduce_hypotheses(proof_ref& pr) {
ast_manager& m = pr.get_manager();
class reduce_hypotheses0 reduce(m);
reduce(pr);
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
}
class proof_is_closed {
ast_manager& m;
ptr_vector<expr> m_literals;
ast_mark m_visit;
void reset() {
m_literals.reset();
m_visit.reset();
}
bool check(proof* p) {
// really just a partial check because nodes may be visited
// already under a different lemma scope.
if (m_visit.is_marked(p)) {
return true;
}
bool result = false;
m_visit.mark(p, true);
switch(p->get_decl_kind()) {
case PR_LEMMA: {
unsigned sz = m_literals.size();
expr* cls = m.get_fact(p);
m_literals.push_back(cls);
if (m.is_or(cls)) {
m_literals.append(to_app(cls)->get_num_args(), to_app(cls)->get_args());
}
SASSERT(m.get_num_parents(p) == 1);
result = check(m.get_parent(p, 0));
m_literals.resize(sz);
break;
}
case PR_HYPOTHESIS: {
expr* fact = m.get_fact(p);
for (unsigned i = 0; i < m_literals.size(); ++i) {
if (m.is_complement(m_literals[i], fact)) {
result = true;
break;
}
}
break;
}
default:
result = true;
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
if (!check(m.get_parent(p, i))) {
result = false;
break;
}
}
break;
}
return result;
}
public:
proof_is_closed(ast_manager& m): m(m) {}
bool operator()(proof *p) {
bool ok = check(p);
reset();
return ok;
}
};
bool proof_utils::is_closed(ast_manager& m, proof* p) {
proof_is_closed checker(m);
return checker(p);
}
static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
ast_manager& m = pr.get_manager();
proof* pr2 = 0;
proof_ref_vector parents(m);
proof_ref prNew(pr);
if (cache.find(pr, pr2)) {
pr = pr2;
return;
}
for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
prNew = m.get_parent(pr, i);
permute_unit_resolution(refs, cache, prNew);
parents.push_back(prNew);
}
prNew = pr;
if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
parents[0]->get_decl_kind() == PR_TH_LEMMA) {
/*
Unit resolution:
T1: (or l_1 ... l_n l_1' ... l_m')
T2: (not l_1)
...
T(n+1): (not l_n)
[unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
Th lemma:
T1: (not l_1)
...
Tn: (not l_n)
[th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
Implement conversion:
T1 |- not l_1 ... Tn |- not l_n
------------------------------- TH_LEMMA
(or k_1 .. k_m j_1 ... j_m) S1 |- not k_1 ... Sm |- not k_m
-------------------------------------------------------------- UNIT_RESOLUTION
(or j_1 .. j_m)
|->
T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
---------------------------------------------------------------- TH_LEMMA
(or j_1 .. j_m)
*/
proof_ref_vector premises(m);
proof* thLemma = parents[0].get();
for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
premises.push_back(m.get_parent(thLemma, i));
}
for (unsigned i = 1; i < parents.size(); ++i) {
premises.push_back(parents[i].get());
}
parameter const* params = thLemma->get_decl()->get_parameters();
unsigned num_params = thLemma->get_decl()->get_num_parameters();
SASSERT(params[0].is_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
// AG: This can break a theory lemma. In particular, for Farkas lemmas the coefficients
// AG: for the literals propagated from the unit resolution are missing.
// AG: Why is this a good thing to do?
// AG: This can lead to merging of the units with other terms in interpolation,
// AG: but without farkas coefficients this does not make sense
prNew = m.mk_th_lemma(tid, m.get_fact(pr),
premises.size(), premises.c_ptr(), num_params-1, params+1);
}
else {
ptr_vector<expr> args;
for (unsigned i = 0; i < parents.size(); ++i) {
args.push_back(parents[i].get());
}
if (m.has_fact(pr)) {
args.push_back(m.get_fact(pr));
}
prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
}
cache.insert(pr, prNew);
refs.push_back(prNew);
pr = prNew;
}
// permute unit resolution over Theory lemmas to track premises.
void proof_utils::permute_unit_resolution(proof_ref& pr) {
expr_ref_vector refs(pr.get_manager());
obj_map<proof,proof*> cache;
::permute_unit_resolution(refs, cache, pr);
}
class push_instantiations_up_cl {
ast_manager& m;
public:
push_instantiations_up_cl(ast_manager& m): m(m) {}
void operator()(proof_ref& p) {
expr_ref_vector s0(m);
p = push(p, s0);
}
private:
proof* push(proof* p, expr_ref_vector const& sub) {
proof_ref_vector premises(m);
expr_ref conclusion(m);
svector<std::pair<unsigned, unsigned> > positions;
vector<expr_ref_vector> substs;
if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
for (unsigned i = 0; i < premises.size(); ++i) {
compose(substs[i], sub);
premises[i] = push(premises[i].get(), substs[i]);
substs[i].reset();
}
instantiate(sub, conclusion);
return
m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion,
positions,
substs);
}
if (sub.empty()) {
return p;
}
if (m.is_modus_ponens(p)) {
SASSERT(m.get_num_parents(p) == 2);
proof* p0 = m.get_parent(p, 0);
proof* p1 = m.get_parent(p, 1);
if (m.get_fact(p0) == m.get_fact(p)) {
return push(p0, sub);
}
expr* e1, *e2;
if (m.is_rewrite(p1, e1, e2) &&
is_quantifier(e1) && is_quantifier(e2) &&
to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
expr_ref r1(e1,m), r2(e2,m);
instantiate(sub, r1);
instantiate(sub, r2);
p1 = m.mk_rewrite(r1, r2);
return m.mk_modus_ponens(push(p0, sub), p1);
}
}
premises.push_back(p);
substs.push_back(sub);
conclusion = m.get_fact(p);
instantiate(sub, conclusion);
return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
}
void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
for (unsigned i = 0; i < sub.size(); ++i) {
expr_ref e(m);
var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
sub[i] = e;
}
}
void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
if (sub.empty()) {
return;
}
if (!is_forall(fml)) {
return;
}
quantifier* q = to_quantifier(fml);
if (q->get_num_decls() != sub.size()) {
TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
tout << mk_pp(q, m) << "\n";
tout << sub.size() << "\n";);
return;
}
var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
}
};
void proof_utils::push_instantiations_up(proof_ref& pr) {
push_instantiations_up_cl push(pr.get_manager());
push(pr);
}

48
src/muz/base/proof_utils.h
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
proof_utils.h
Abstract:
Utilities for transforming proofs.
Author:
Nikolaj Bjorner (nbjorner) 2012-10-12.
Revision History:
--*/
#ifndef PROOF_UTILS_H_
#define PROOF_UTILS_H_
class proof_utils {
public:
/**
\brief reduce the set of hypotheses used in the proof.
*/
static void reduce_hypotheses(proof_ref& pr);
/**
\brief Check that a proof does not contain open hypotheses.
*/
static bool is_closed(ast_manager& m, proof* p);
/**
\brief Permute unit resolution rule with th-lemma
*/
static void permute_unit_resolution(proof_ref& pr);
/**
\brief Push instantiations created in hyper-resolutions up to leaves.
This produces a "ground" proof where leaves are annotated by instantiations.
*/
static void push_instantiations_up(proof_ref& pr);
};
#endif

1
src/muz/pdr/pdr_context.cpp
View file

@ -43,7 +43,6 @@ Notes:
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/proofs/proof_checker.h" #include "ast/proofs/proof_checker.h"
#include "smt/smt_value_sort.h" #include "smt/smt_value_sort.h"
#include "muz/base/proof_utils.h"
#include "muz/base/dl_boogie_proof.h" #include "muz/base/dl_boogie_proof.h"
#include "ast/scoped_proof.h" #include "ast/scoped_proof.h"
#include "tactic/core/blast_term_ite_tactic.h" #include "tactic/core/blast_term_ite_tactic.h"

8
src/muz/pdr/pdr_farkas_learner.cpp
View file

@ -31,7 +31,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "tactic/arith/arith_bounds_tactic.h" #include "tactic/arith/arith_bounds_tactic.h"
#include "muz/base/proof_utils.h" #include "ast/proofs/proof_utils.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
@ -733,8 +733,8 @@ namespace pdr {
} }
else { else {
expr_set* hyps3 = alloc(expr_set); expr_set* hyps3 = alloc(expr_set);
datalog::set_union(*hyps3, *hyps); set_union(*hyps3, *hyps);
datalog::set_union(*hyps3, *hyps2); set_union(*hyps3, *hyps2);
hyps = hyps3; hyps = hyps3;
hyprefs.push_back(hyps); hyprefs.push_back(hyps);
} }
@ -795,7 +795,7 @@ namespace pdr {
case PR_LEMMA: { case PR_LEMMA: {
expr_set* hyps2 = alloc(expr_set); expr_set* hyps2 = alloc(expr_set);
hyprefs.push_back(hyps2); hyprefs.push_back(hyps2);
datalog::set_union(*hyps2, *hyps); set_union(*hyps2, *hyps);
hyps = hyps2; hyps = hyps2;
expr* fml = m.get_fact(p); expr* fml = m.get_fact(p);
hyps->remove(fml); hyps->remove(fml);

6
src/muz/pdr/pdr_generalizers.cpp
View file

@ -81,7 +81,7 @@ namespace pdr {
m_gen(n, core0, uses_level1); m_gen(n, core0, uses_level1);
new_cores.push_back(std::make_pair(core0, uses_level1)); new_cores.push_back(std::make_pair(core0, uses_level1));
obj_hashtable<expr> core_exprs, core1_exprs; obj_hashtable<expr> core_exprs, core1_exprs;
datalog::set_union(core_exprs, core0); set_union(core_exprs, core0);
for (unsigned i = 0; i < old_core.size(); ++i) { for (unsigned i = 0; i < old_core.size(); ++i) {
expr* lit = old_core[i].get(); expr* lit = old_core[i].get();
if (core_exprs.contains(lit)) { if (core_exprs.contains(lit)) {
@ -94,8 +94,8 @@ namespace pdr {
if (core1.size() < old_core.size()) { if (core1.size() < old_core.size()) {
new_cores.push_back(std::make_pair(core1, uses_level1)); new_cores.push_back(std::make_pair(core1, uses_level1));
core1_exprs.reset(); core1_exprs.reset();
datalog::set_union(core1_exprs, core1); set_union(core1_exprs, core1);
datalog::set_intersection(core_exprs, core1_exprs); set_intersection(core_exprs, core1_exprs);
} }
} }
} }

8
src/muz/spacer/spacer_farkas_learner.cpp
View file

@ -31,7 +31,7 @@ Revision History:
#include "muz/spacer/spacer_farkas_learner.h" #include "muz/spacer/spacer_farkas_learner.h"
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "muz/base/proof_utils.h" #include "ast/proofs/proof_utils.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
#include "smt/smt_farkas_util.h" #include "smt/smt_farkas_util.h"
@ -231,8 +231,8 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
hyps = hyps2; hyps = hyps2;
} else { } else {
expr_set* hyps3 = alloc(expr_set); expr_set* hyps3 = alloc(expr_set);
datalog::set_union(*hyps3, *hyps); set_union(*hyps3, *hyps);
datalog::set_union(*hyps3, *hyps2); set_union(*hyps3, *hyps2);
hyps = hyps3; hyps = hyps3;
hyprefs.push_back(hyps); hyprefs.push_back(hyps);
} }
@ -291,7 +291,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
case PR_LEMMA: { case PR_LEMMA: {
expr_set* hyps2 = alloc(expr_set); expr_set* hyps2 = alloc(expr_set);
hyprefs.push_back(hyps2); hyprefs.push_back(hyps2);
datalog::set_union(*hyps2, *hyps); set_union(*hyps2, *hyps);
hyps = hyps2; hyps = hyps2;
expr* fml = m.get_fact(p); expr* fml = m.get_fact(p);
hyps->remove(fml); hyps->remove(fml);

2
src/muz/spacer/spacer_legacy_frames.cpp
View file

@ -25,7 +25,7 @@
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/proofs/proof_checker.h" #include "ast/proofs/proof_checker.h"
#include "smt/smt_value_sort.h" #include "smt/smt_value_sort.h"
#include "muz/base/proof_utils.h" #include "ast/proofs/proof_utils.h"
#include "ast/scoped_proof.h" #include "ast/scoped_proof.h"
#include "muz/spacer/spacer_qe_project.h" #include "muz/spacer/spacer_qe_project.h"
#include "tactic/core/blast_term_ite_tactic.h" #include "tactic/core/blast_term_ite_tactic.h"