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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-27 17:05:52 -07:00
parent 06c9a9f3e1 7844476a7d
commit eabe91cdef
13 changed files with 242 additions and 176 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ast/ast.cpp
View file

@ -1122,11 +1122,11 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : nullptr;
case OP_DISTINCT:
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
case PR_BIND: {
ptr_buffer<sort> sorts;
for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i]));
return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range);
}
case PR_BIND: {
ptr_buffer<sort> sorts;
for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i]));
return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range);
}
default:
break;
}
@ -2847,10 +2847,10 @@ proof * ast_manager::mk_bind_proof(quantifier * q, proof * p) {
}
proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
if (!p) return nullptr;
SASSERT(q1->get_num_decls() == q2->get_num_decls());
SASSERT(has_fact(p));
SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p)));
if (!p) return nullptr;
SASSERT(q1->get_num_decls() == q2->get_num_decls());
SASSERT(has_fact(p));
SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p)));
return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2));
}
@ -2858,7 +2858,7 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof
if (!p) return nullptr;
SASSERT(q1->get_num_decls() == q2->get_num_decls());
SASSERT(has_fact(p));
SASSERT(is_oeq(get_fact(p)));
SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p)));
return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_oeq(q1, q2));
}

13
src/ast/proofs/proof_checker.cpp
View file

@ -335,6 +335,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
return false;
}
case PR_QUANT_INTRO: {
if (match_proof(p, p1) &&
match_fact(p, fact) &&
match_fact(p1.get(), fml) &&
(is_lambda(fact) || is_lambda(fml)))
return true;
if (match_proof(p, p1) &&
match_fact(p, fact) &&
match_fact(p1.get(), fml) &&
@ -361,6 +367,13 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
UNREACHABLE();
return false;
}
case PR_BIND:
// it is a lambda expression returning a proof object.
if (!is_lambda(to_app(p)->get_arg(0)))
return false;
// check that body is a proof object.
return true;
case PR_DISTRIBUTIVITY: {
if (match_fact(p, fact) &&
match_proof(p) &&

4
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -480,11 +480,9 @@ public:
solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null);
solver_ref sNotB = sf(m, p, false /* no proofs */, true, true, symbol::null);
sA->assert_expr(a);
sNotA->assert_expr(m.mk_not(a));
sB->assert_expr(b);
sNotB->assert_expr(m.mk_not(b));
qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get());
qe::euf_arith_mbi_plugin pB(sB.get(), sNotB.get());
qe::prop_mbi_plugin pB(sB.get());
pA.set_shared(vars);
pB.set_shared(vars);
lbool res = mbi.pogo(pA, pB, itp);

7
src/math/simplex/model_based_opt.cpp
View file

@ -266,6 +266,7 @@ namespace opt {
void model_based_opt::update_value(unsigned x, rational const& val) {
rational old_val = m_var2value[x];
m_var2value[x] = val;
SASSERT(val.is_int() || !is_int(x));
unsigned_vector const& row_ids = m_var2row_ids[x];
for (unsigned row_id : row_ids) {
rational coeff = get_coefficient(row_id, x);
@ -530,6 +531,7 @@ namespace opt {
SASSERT(t_le == dst.m_type && t_le == src.m_type);
SASSERT(src_c.is_int());
SASSERT(dst_c.is_int());
SASSERT(m_var2value[x].is_int());
rational abs_src_c = abs(src_c);
rational abs_dst_c = abs(dst_c);
@ -805,6 +807,7 @@ namespace opt {
unsigned v = m_var2value.size();
m_var2value.push_back(value);
m_var2is_int.push_back(is_int);
SASSERT(value.is_int() || !is_int);
m_var2row_ids.push_back(unsigned_vector());
return v;
}
@ -1017,7 +1020,6 @@ namespace opt {
else {
result = def(m_rows[glb_index], x);
}
m_var2value[x] = eval(result);
}
// The number of matching lower and upper bounds is small.
@ -1114,8 +1116,7 @@ namespace opt {
}
def result = project(y, compute_def);
if (compute_def) {
result = (result * D) + u;
m_var2value[x] = eval(result);
result = (result * D) + u;
}
SASSERT(!compute_def || eval(result) == eval(x));
return result;

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

@ -690,7 +690,7 @@ namespace {
qe::term_graph egraph(out.m());
for (expr* e : v) egraph.add_lit(to_app(e));
tout << "Reduced app:\n"
<< mk_pp(egraph.to_app(), out.m()) << "\n";);
<< mk_pp(egraph.to_expr(), out.m()) << "\n";);
out = mk_and(v);
}
}

1
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -23,7 +23,6 @@ Author:
#include "ast/ast_pp.h"
#include "tactic/generic_model_converter.h"
#include "ast/ast_util.h"
#include "tactic/extension_model_converter.h"
namespace datalog {
rule_set * mk_coi_filter::operator()(rule_set const & source) {

11
src/qe/qe_arith.cpp
View file

@ -41,7 +41,7 @@ namespace qe {
bool m_check_purified; // check that variables are properly pure
void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
// TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
rational w;
if (ts.find(x, w)) {
ts.insert(x, w + v);
@ -92,8 +92,8 @@ namespace qe {
rational r1, r2;
expr_ref val1 = eval(e1);
expr_ref val2 = eval(e2);
TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";);
TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";);
//TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";);
//TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";);
if (!a.is_numeral(val1, r1)) return false;
if (!a.is_numeral(val2, r2)) return false;
SASSERT(r1 != r2);
@ -306,14 +306,14 @@ namespace qe {
return vector<def>();
}
model_evaluator eval(model);
TRACE("qe", model_smt2_pp(tout, m, model, 0););
TRACE("qe", tout << model;);
// eval.set_model_completion(true);
opt::model_based_opt mbo;
obj_map<expr, unsigned> tids;
expr_ref_vector pinned(m);
unsigned j = 0;
TRACE("qe", tout << "fmls: " << fmls << "\n";);
TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr * fml = fmls.get(i);
if (!linearize(mbo, eval, fml, fmls, tids)) {
@ -325,7 +325,6 @@ namespace qe {
}
}
fmls.shrink(j);
TRACE("qe", tout << "linearized: " << fmls << "\n";);
// fmls holds residue,
// mbo holds linear inequalities that are in scope

113
src/qe/qe_mbi.cpp
View file

@ -25,52 +25,6 @@ Notes:
Other theories: DT, ARR reduced to EUF
BV is EUF/Boolean.
Purify EUF1 & LIRA1 & EUF2 & LIRA2
Then EUF1 & EUF2 |- false
LIRA1 & LIRA2 |- false
Sketch of approach by example:
A: s <= 2a <= t & f(a) = q
B: t <= 2b <= s + 1 & f(b) != q
1. Extract arithmetic consequences of A over shared vocabulary.
A -> s <= t & (even(t) | s < t)
2a. Send to B, have B solve shared variables with EUF_B.
epsilon b . B & A_pure
epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t)
= t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t)
= even(t) & t = s
b := t div 2
B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1
3a. Send purified result to A
A & B_pure -> false
Invoke the ping-pong principle to extract interpolant.
2b. Solve for shared variables with EUF.
epsilon a . A
= a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q
3b. Send to B. Produces core
s < t & f((s + 1) div 2) = q
4b Solve again in arithmetic for shared variables with EUF.
epsion a . A & (s >= t | f((s + 1) div 2) != q)
a := t div 2 | s = t & f(t div 2) = q & even(t)
Send to B, produces core (s != t | f(t div 2) != q)
5b. There is no longer a solution for A. A is unsat.
--*/
@ -240,15 +194,24 @@ namespace qe {
// euf_arith_mbi
struct euf_arith_mbi_plugin::is_atom_proc {
ast_manager& m;
expr_ref_vector& m_atoms;
is_atom_proc(expr_ref_vector& atoms): m(atoms.m()), m_atoms(atoms) {}
ast_manager& m;
expr_ref_vector& m_atoms;
obj_hashtable<expr>& m_atom_set;
is_atom_proc(expr_ref_vector& atoms, obj_hashtable<expr>& atom_set):
m(atoms.m()), m_atoms(atoms), m_atom_set(atom_set) {}
void operator()(app* a) {
if (m.is_eq(a)) {
if (m_atom_set.contains(a)) {
// continue
}
else if (m.is_eq(a)) {
m_atoms.push_back(a);
m_atom_set.insert(a);
}
else if (m.is_bool(a) && a->get_family_id() != m.get_basic_family_id()) {
m_atoms.push_back(a);
m_atom_set.insert(a);
}
}
void operator()(expr*) {}
@ -275,38 +238,44 @@ namespace qe {
euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot):
mbi_plugin(s->get_manager()),
m_atoms(m),
m_fmls(m),
m_solver(s),
m_dual_solver(sNot) {
params_ref p;
p.set_bool("core.minimize", true);
m_solver->updt_params(p);
m_dual_solver->updt_params(p);
expr_ref_vector fmls(m);
m_solver->get_assertions(fmls);
m_solver->get_assertions(m_fmls);
collect_atoms(m_fmls);
}
void euf_arith_mbi_plugin::collect_atoms(expr_ref_vector const& fmls) {
expr_fast_mark1 marks;
is_atom_proc proc(m_atoms);
is_atom_proc proc(m_atoms, m_atom_set);
for (expr* e : fmls) {
quick_for_each_expr(proc, marks, e);
}
}
bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) {
model_evaluator mev(*mdl.get());
lits.reset();
for (expr* e : m_atoms) {
if (mev.is_true(e)) {
lits.push_back(e);
}
else if (mev.is_false(e)) {
lits.push_back(m.mk_not(e));
}
lits.reset();
for (expr* e : m_atoms) {
if (mdl->is_true(e)) {
lits.push_back(e);
}
TRACE("qe", tout << "atoms from model: " << lits << "\n";);
lbool r = m_dual_solver->check_sat(lits);
else if (mdl->is_false(e)) {
lits.push_back(m.mk_not(e));
}
}
TRACE("qe", tout << "atoms from model: " << lits << "\n";);
solver_ref dual = m_dual_solver->translate(m, m_dual_solver->get_params());
dual->assert_expr(mk_not(mk_and(m_fmls)));
lbool r = dual->check_sat(lits);
TRACE("qe", dual->display(tout << "dual result " << r << "\n"););
if (l_false == r) {
// use the dual solver to find a 'small' implicant
lits.reset();
m_dual_solver->get_unsat_core(lits);
// use the dual solver to find a 'small' implicant
lits.reset();
dual->get_unsat_core(lits);
return true;
}
else {
@ -351,15 +320,15 @@ namespace qe {
for (auto const& def : defs) {
lits.push_back(m.mk_eq(def.var, def.term));
}
TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";);
TRACE("qe", tout << "# arith defs " << defs.size() << " avars: " << avars << " " << lits << "\n";);
// 3. Project the remaining literals with respect to EUF.
term_graph tg(m);
tg.set_vars(m_shared, false);
tg.add_lits(lits);
lits.reset();
lits.append(tg.project(*mdl));
//lits.append(tg.project());
//lits.append(tg.project(*mdl));
lits.append(tg.project());
TRACE("qe", tout << "project: " << lits << "\n";);
return mbi_sat;
}
@ -374,7 +343,9 @@ namespace qe {
}
void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) {
m_solver->assert_expr(mk_not(mk_and(lits)));
collect_atoms(lits);
m_fmls.push_back(mk_not(mk_and(lits)));
m_solver->assert_expr(m_fmls.back());
}

12
src/qe/qe_mbi.h
View file

@ -104,17 +104,19 @@ namespace qe {
};
class euf_arith_mbi_plugin : public mbi_plugin {
expr_ref_vector m_atoms;
solver_ref m_solver;
solver_ref m_dual_solver;
expr_ref_vector m_atoms;
obj_hashtable<expr> m_atom_set;
expr_ref_vector m_fmls;
solver_ref m_solver;
solver_ref m_dual_solver;
struct is_atom_proc;
struct is_arith_var_proc;
app_ref_vector get_arith_vars(expr_ref_vector const& lits);
bool get_literals(model_ref& mdl, expr_ref_vector& lits);
void collect_atoms(expr_ref_vector const& fmls);
public:
euf_arith_mbi_plugin(solver* s, solver* sNot);
euf_arith_mbi_plugin(solver* s, solver* emptySolver);
~euf_arith_mbi_plugin() override {}
mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
void block(expr_ref_vector const& lits) override;

2
src/qe/qe_solve_plugin.cpp
View file

@ -99,7 +99,7 @@ namespace qe {
v = e;
a_val = rational(1)/a_val;
t = mk_term(is_int, a_val, sign, done);
TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << e << " := " << t << "\n";);
TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << t << "\n";);
return true;
}
else {

182
src/qe/qe_term_graph.cpp
View file

@ -125,7 +125,7 @@ namespace qe {
children(term const* _t):t(*_t) {}
ptr_vector<term>::const_iterator begin() const { return t.m_children.begin(); }
ptr_vector<term>::const_iterator end() const { return t.m_children.end(); }
};
};
// Congruence table hash function is based on
// roots of children and function declaration.
@ -198,8 +198,22 @@ namespace qe {
}
while (curr != this);
}
std::ostream& display(std::ostream& out) const {
out << get_id() << ": " << m_expr << " - ";
term const* r = &this->get_next();
while (r != this) {
out << r->get_id() << " ";
r = &r->get_next();
}
out << "\n";
return out;
}
};
static std::ostream& operator<<(std::ostream& out, term const& t) {
return t.display(out);
}
bool term_graph::is_variable_proc::operator()(const expr * e) const {
if (!is_app(e)) return false;
@ -516,10 +530,7 @@ namespace qe {
void term_graph::display(std::ostream &out) {
for (term * t : m_terms) {
out << mk_pp(t->get_expr(), m) << " is root " << t->is_root()
<< " cls sz " << t->get_class_size()
<< " term " << t
<< "\n";
out << *t;
}
}
@ -542,7 +553,7 @@ namespace qe {
}
}
expr_ref term_graph::to_app() {
expr_ref term_graph::to_expr() {
expr_ref_vector lits(m);
to_lits(lits);
return mk_and(lits);
@ -575,8 +586,15 @@ namespace qe {
app* a = ::to_app(e);
expr_ref_buffer kids(m);
for (term* ch : term::children(t)) {
if (!m_root2rep.find(ch->get_root().get_id(), e)) return nullptr;
kids.push_back(e);
// prefer a node that resembles current child,
// otherwise, pick a root representative, if present.
if (m_term2app.find(ch->get_id(), e))
kids.push_back(e);
else if (m_root2rep.find(ch->get_root().get_id(), e))
kids.push_back(e);
else
return nullptr;
TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";);
}
expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.c_ptr());
m_pinned.push_back(pure);
@ -590,6 +608,12 @@ namespace qe {
return m.is_unique_value(t1) && !m.is_unique_value(t2);
}
struct term_depth {
bool operator()(term const* t1, term const* t2) const {
return get_depth(t1->get_expr()) < get_depth(t2->get_expr());
}
};
void purify() {
// - propagate representatives up over parents.
// use work-list + marking to propagate.
@ -603,12 +627,14 @@ namespace qe {
worklist.push_back(t);
t->set_mark(true);
}
// traverse worklist in order of depth.
term_depth td;
std::sort(worklist.begin(), worklist.end(), td);
while (!worklist.empty()) {
term* t = worklist.back();
worklist.pop_back();
for (unsigned i = 0; i < worklist.size(); ++i) {
term* t = worklist[i];
t->set_mark(false);
if (m_term2app.contains(t->get_id()))
if (m_term2app.contains(t->get_id()))
continue;
if (!t->is_theory() && is_projected(*t))
continue;
@ -617,8 +643,8 @@ namespace qe {
if (!pure) continue;
m_term2app.insert(t->get_id(), pure);
expr* rep = nullptr;
// ensure that the root has a representative
TRACE("qe_verbose", tout << "purified " << *t << " " << mk_pp(pure, m) << "\n";);
expr* rep = nullptr; // ensure that the root has a representative
m_root2rep.find(t->get_root().get_id(), rep);
// update rep with pure if it is better
@ -641,6 +667,7 @@ namespace qe {
// and can be mined using other means, such as theory
// aware core minimization
m_tg.reset_marks();
TRACE("qe", display(tout << "after purify\n"););
}
void solve_core() {
@ -651,10 +678,11 @@ namespace qe {
worklist.push_back(t);
t->set_mark(true);
}
term_depth td;
std::sort(worklist.begin(), worklist.end(), td);
while (!worklist.empty()) {
term* t = worklist.back();
worklist.pop_back();
for (unsigned i = 0; i < worklist.size(); ++i) {
term* t = worklist[i];
t->set_mark(false);
if (m_term2app.contains(t->get_id()))
continue;
@ -682,11 +710,16 @@ namespace qe {
}
bool find_app(term &t, expr *&res) {
return m_root2rep.find(t.get_root().get_id(), res);
return
m_term2app.find(t.get_id(), res) ||
m_root2rep.find(t.get_root().get_id(), res);
}
bool find_app(expr *lit, expr *&res) {
return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res);
term const* t = m_tg.get_term(lit);
return
m_term2app.find(t->get_id(), res) ||
m_root2rep.find(t->get_root().get_id(), res);
}
void mk_lits(expr_ref_vector &res) {
@ -695,6 +728,91 @@ namespace qe {
if (!m.is_eq(lit) && find_app(lit, e))
res.push_back(e);
}
TRACE("qe", tout << "literals: " << res << "\n";);
}
void lits2pure(expr_ref_vector& res) {
expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr;
for (auto *lit : m_tg.m_lits) {
if (m.is_eq(lit, e1, e2)) {
if (find_app(e1, p1) && find_app(e2, p2)) {
if (p1 != p2)
res.push_back(m.mk_eq(p1, p2));
}
else {
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
}
else if (m.is_distinct(lit)) {
ptr_buffer<expr> diff;
for (expr* arg : *to_app(lit)) {
if (find_app(arg, p1)) {
diff.push_back(p1);
}
}
if (diff.size() > 1) {
res.push_back(m.mk_distinct(diff.size(), diff.c_ptr()));
}
else {
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
}
else if (find_app(lit, p1)) {
res.push_back(p1);
}
else {
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
}
TRACE("qe", tout << "literals: " << res << "\n";);
}
void mk_distinct(expr_ref_vector& res) {
vector<ptr_vector<term>> decl2terms; // terms that use function f
ptr_vector<func_decl> decls;
decl2terms.reset();
// Collect the projected function symbols.
for (term *t : m_tg.m_terms) {
expr* e = t->get_expr();
if (!is_app(e)) continue;
if (!is_projected(*t)) continue;
app* a = to_app(e);
func_decl* d = a->get_decl();
if (d->get_arity() == 0) continue;
unsigned id = d->get_decl_id();
decl2terms.reserve(id+1);
if (decl2terms[id].empty()) decls.push_back(d);
decl2terms[id].push_back(t);
}
//
// for each projected function that occurs
// (may occur) in multiple congruence classes,
// produce assertions that non-congruent arguments
// are forced distinct.
//
for (func_decl* d : decls) {
unsigned id = d->get_decl_id();
ptr_vector<term> const& terms = decl2terms[id];
if (terms.size() <= 1) continue;
unsigned arity = d->get_arity();
for (unsigned i = 0; i < arity; ++i) {
obj_hashtable<expr> roots;
for (term* t : terms) {
expr* arg = to_app(t->get_expr())->get_arg(i);
term const& root = m_tg.get_term(arg)->get_root();
roots.insert(root.get_expr());
}
if (roots.size() > 1) {
ptr_buffer<expr> args;
for (expr* r : roots) {
args.push_back(r);
}
res.push_back(m.mk_distinct(args.size(), args.c_ptr()));
}
}
}
TRACE("qe", tout << res << "\n";);
}
void mk_pure_equalities(const term &t, expr_ref_vector &res) {
@ -736,7 +854,8 @@ namespace qe {
while (r != &t);
}
void mk_equalities(bool pure, expr_ref_vector &res) {
template<bool pure>
void mk_equalities(expr_ref_vector &res) {
for (term *t : m_tg.m_terms) {
if (!t->is_root()) continue;
if (!m_root2rep.contains(t->get_id())) continue;
@ -745,14 +864,15 @@ namespace qe {
else
mk_unpure_equalities(*t, res);
}
TRACE("qe", tout << "literals: " << res << "\n";);
}
void mk_pure_equalities(expr_ref_vector &res) {
return mk_equalities(true, res);
mk_equalities<true>(res);
}
void mk_unpure_equalities(expr_ref_vector &res) {
return mk_equalities(false, res);
mk_equalities<false>(res);
}
// TBD: generalize for also the case of a (:var n)
@ -813,6 +933,19 @@ namespace qe {
TRACE("qe", tout << "after distinct: " << res << "\n";);
}
std::ostream& display(std::ostream& out) const {
m_tg.display(out);
out << "term2app:\n";
for (auto const& kv : m_term2app) {
out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n";
}
out << "root2rep:\n";
for (auto const& kv : m_root2rep) {
out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n";
}
return out;
}
public:
projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}
@ -828,9 +961,8 @@ namespace qe {
expr_ref_vector project() {
expr_ref_vector res(m);
purify();
mk_lits(res);
mk_pure_equalities(res);
model_complete(res);
lits2pure(res);
mk_distinct(res);
reset();
return res;
}

2
src/qe/qe_term_graph.h
View file

@ -102,7 +102,7 @@ namespace qe {
// deprecate?
void to_lits(expr_ref_vector &lits, bool all_equalities = false);
expr_ref to_app();
expr_ref to_expr();
/**
* Return literals obtained by projecting added literals

49
src/tactic/extension_model_converter.h
View file

@ -1,49 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
extension_model_converter.h
Abstract:
Model converter that introduces new interpretations into a model.
It used to be called elim_var_model_converter
Author:
Leonardo (leonardo) 2011-10-21
Notes:
--*/
#ifndef EXTENSION_MODEL_CONVERTER_H_
#define EXTENSION_MODEL_CONVERTER_H_
#include "ast/ast.h"
#include "tactic/model_converter.h"
class extension_model_converter : public model_converter {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;
public:
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) {
}
~extension_model_converter() override;
ast_manager & m() const { return m_vars.get_manager(); }
void operator()(model_ref & md) override;
void display(std::ostream & out) override;
// register a variable that was eliminated
void insert(func_decl * v, expr * def);
model_converter * translate(ast_translation & translator) override;
};
#endif