mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-02 08:10:43 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-10-29 08:07:40 -07:00
commit 99e94e3263
131 changed files with 1027 additions and 6914 deletions
Download patch file Download diff file Expand all files Collapse all files

239
src/muz_qe/qe.cpp
View file

@ -45,6 +45,7 @@ Revision History:
#include "cooperate.h"
#include "tactical.h"
#include "model_v2_pp.h"
#include "obj_hashtable.h"
namespace qe {
@ -723,6 +724,85 @@ namespace qe {
}
};
// ----------------------------
// def_vector
void def_vector::normalize() {
// apply nested definitions into place.
ast_manager& m = m_vars.get_manager();
expr_substitution sub(m);
scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
if (size() <= 1) {
return;
}
for (unsigned i = size(); i > 0; ) {
--i;
expr_ref e(m);
e = def(i);
rep->set_substitution(&sub);
(*rep)(e);
sub.insert(m.mk_const(var(i)), e);
def_ref(i) = e;
}
}
void def_vector::project(unsigned num_vars, app* const* vars) {
obj_hashtable<func_decl> fns;
for (unsigned i = 0; i < num_vars; ++i) {
fns.insert(vars[i]->get_decl());
}
for (unsigned i = 0; i < size(); ++i) {
if (fns.contains(m_vars[i].get())) {
//
// retain only first occurrence of eliminated variable.
// later occurrences are just recycling the name.
//
fns.remove(m_vars[i].get());
}
else {
for (unsigned j = i+1; j < size(); ++j) {
m_vars.set(j-1, m_vars.get(j));
m_defs.set(j-1, m_defs.get(j));
}
m_vars.pop_back();
m_defs.pop_back();
--i;
}
}
}
// ----------------------------
// guarded_defs
std::ostream& guarded_defs::display(std::ostream& out) const {
ast_manager& m = m_guards.get_manager();
for (unsigned i = 0; i < size(); ++i) {
for (unsigned j = 0; j < defs(i).size(); ++j) {
out << defs(i).var(j)->get_name() << " := " << mk_pp(defs(i).def(j), m) << "\n";
}
out << "if " << mk_pp(guard(i), m) << "\n";
}
return out;
}
bool guarded_defs::inv() {
return m_defs.size() == m_guards.size();
}
void guarded_defs::add(expr* guard, def_vector const& defs) {
SASSERT(inv());
m_defs.push_back(defs);
m_guards.push_back(guard);
m_defs.back().normalize();
SASSERT(inv());
}
void guarded_defs::project(unsigned num_vars, app* const* vars) {
for (unsigned i = 0; i < size(); ++i) {
m_defs[i].project(num_vars, vars);
}
}
// ----------------------------
// Obtain atoms in NNF formula.
@ -810,7 +890,7 @@ namespace qe {
virtual lbool eliminate_exists(
unsigned num_vars, app* const* vars,
expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) = 0;
expr_ref& fml, app_ref_vector& free_vars, bool get_first, guarded_defs* defs) = 0;
virtual void set_assumption(expr* fml) = 0;
@ -918,40 +998,25 @@ namespace qe {
}
}
bool get_leaf_rec(expr_ref& fml, def_vector& defs) {
void get_leaves_rec(def_vector& defs, guarded_defs& gdefs) {
expr* f = this->fml();
unsigned sz = defs.size();
defs.append(def());
if (m_children.empty() && f && !m.is_false(f) &&
m_vars.empty() && !has_var()) {
fml = f;
return true;
gdefs.add(f, defs);
}
unsigned sz = defs.size();
for (unsigned i = 0; i < m_children.size(); ++i) {
search_tree* st = m_children[i];
defs.append(st->def());
if (st->get_leaf_rec(fml, defs)) {
return true;
else {
for (unsigned i = 0; i < m_children.size(); ++i) {
m_children[i]->get_leaves_rec(defs, gdefs);
}
defs.shrink(sz);
}
return false;
defs.shrink(sz);
}
void get_leaf(expr_ref& fml, def_vector& defs) {
get_leaf_rec(fml, defs);
// apply nested definitions into place.
expr_substitution sub(m);
scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
for (unsigned i = defs.size(); i > 0; ) {
--i;
expr_ref e(m);
e = defs.def(i);
rep->set_substitution(&sub);
(*rep)(e);
sub.insert(m.mk_const(defs.var(i)), e);
defs.def_ref(i) = e;
}
void get_leaves(guarded_defs& gdefs) {
def_vector defs(m);
get_leaves_rec(defs, gdefs);
}
void reset() {
@ -1248,7 +1313,7 @@ namespace qe {
app_ref_vector m_new_vars; // variables added by solvers
bool m_get_first; // get first satisfying branch.
def_vector* m_defs;
guarded_defs* m_defs;
nnf_normalizer m_nnf; // nnf conversion
@ -1311,7 +1376,7 @@ namespace qe {
void check(unsigned num_vars, app* const* vars,
expr* assumption, expr_ref& fml, bool get_first,
app_ref_vector& free_vars, def_vector* defs) {
app_ref_vector& free_vars, guarded_defs* defs) {
reset();
m_solver.push();
@ -1366,9 +1431,11 @@ namespace qe {
expr_ref_vector result(m);
m_root.get_leaves(result);
m_bool_rewriter.mk_or(result.size(), result.c_ptr(), fml);
}
else if (defs) {
m_root.get_leaf(fml, *defs);
}
if (defs) {
m_root.get_leaves(*defs);
defs->project(num_vars, vars);
}
TRACE("qe",
@ -1401,7 +1468,7 @@ namespace qe {
private:
void final_check(model_evaluator& model_eval) {
TRACE("qe", tout << (m_fml?"fml":"null") << "\n";);
TRACE("qe", tout << "\n";);
while (can_propagate_assignment(model_eval)) {
propagate_assignment(model_eval);
}
@ -1480,7 +1547,7 @@ namespace qe {
m_qe.eliminate_exists(1, &var, fml, m_free_vars, false, 0);
}
lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, def_vector* defs) {
lbool eliminate_exists(unsigned num_vars, app* const* vars, expr_ref& fml, bool get_first, guarded_defs* defs) {
return m_qe.eliminate_exists(num_vars, vars, fml, m_free_vars, get_first, defs);
}
@ -1700,7 +1767,7 @@ namespace qe {
void propagate_assignment(model_evaluator& model_eval) {
if (m_fml) {
update_current(model_eval, true);
update_status st = update_current(model_eval, true);
}
}
@ -1982,7 +2049,7 @@ namespace qe {
virtual lbool eliminate_exists(
unsigned num_vars, app* const* vars, expr_ref& fml,
app_ref_vector& free_vars, bool get_first, def_vector* defs) {
app_ref_vector& free_vars, bool get_first, guarded_defs* defs) {
if (get_first) {
return eliminate_block(num_vars, vars, fml, free_vars, get_first, defs);
}
@ -2008,7 +2075,7 @@ namespace qe {
lbool eliminate_block(
unsigned num_vars, app* const* vars, expr_ref& fml,
app_ref_vector& free_vars, bool get_first, def_vector* defs) {
app_ref_vector& free_vars, bool get_first, guarded_defs* defs) {
checkpoint();
@ -2094,54 +2161,6 @@ namespace qe {
};
#if 0
//
// Instantiation based quantifier elimination procedure.
// try a few loops of checking satisfiability.
// substitute in model values for bound variables.
//
class quant_elim_inst : public quant_elim {
ast_manager&
public:
quant_elim_inst(ast_manager& m): m(m) {}
virtual lbool eliminate_exists(
unsigned num_vars, app* const* vars,
expr_ref& fml, app_ref_vector& free_vars, bool get_first, def_vector* defs) {
}
virtual void set_assumption(expr* fml) {}
virtual void collect_statistics(statistics & st) const {
m_solver.collect_statistics(st);
}
virtual void eliminate(bool is_forall, unsigned num_vars, app* const* vars, expr_ref& fml) {
if (is_forall) {
fml = m.mk_not(fml);
r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs);
fml = m.mk_not(fml);
}
else {
r = eliminate_exists(num_vars, vars, fml, free_vars, false, defs);
}
}
virtual void set_cancel(bool f) {
m_solver.set_cancel(f);
}
virtual void updt_params(params_ref const& p) {
m_solver.updt_params(p);
}
};
#endif
// ------------------------------------------------
// expr_quant_elim
@ -2310,40 +2329,28 @@ namespace qe {
lbool expr_quant_elim::first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) {
app_ref_vector fvs(m);
init_qe();
return m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &defs);
}
bool expr_quant_elim::solve_for_var(app* var, expr* _fml, expr_ref_vector& terms, expr_ref_vector& fmls) {
expr_ref assms(m.mk_true(), m);
func_decl* v = var->get_decl();
init_qe();
while (true) {
def_vector defs(m);
app_ref_vector fvs(m);
m_qe->set_assumption(assms);
expr_ref fml(_fml, m);
lbool is_sat = m_qe->eliminate_exists(1, &var, fml, fvs, true, &defs);
switch (is_sat) {
case l_false: return true;
case l_undef: return false;
default: break;
}
bool found = false;
for (unsigned i = 0; !found && i < defs.size(); ++i) {
if (defs.var(i) == v) {
terms.push_back(defs.def(i));
fmls.push_back(fml);
found = true;
}
}
if (!found) {
NOT_IMPLEMENTED_YET();
}
assms = m.mk_and(assms, m.mk_not(fml));
guarded_defs gdefs(m);
lbool res = m_qe->eliminate_exists(num_vars, vars, fml, fvs, true, &gdefs);
if (gdefs.size() > 0) {
defs.reset();
defs.append(gdefs.defs(0));
fml = gdefs.guard(0);
}
return true;
return res;
}
bool expr_quant_elim::solve_for_var(app* var, expr* fml, guarded_defs& defs) {
return solve_for_vars(1,&var, fml, defs);
}
bool expr_quant_elim::solve_for_vars(unsigned num_vars, app* const* vars, expr* _fml, guarded_defs& defs) {
app_ref_vector fvs(m);
expr_ref fml(_fml, m);
TRACE("qe", tout << mk_pp(fml, m) << "\n";);
init_qe();
lbool is_sat = m_qe->eliminate_exists(num_vars, vars, fml, fvs, false, &defs);
return is_sat != l_undef;
}
void expr_quant_elim::set_cancel(bool f) {
if (m_qe) {

37
src/muz_qe/qe.h
View file

@ -226,8 +226,10 @@ namespace qe {
class def_vector {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;
def_vector& operator=(def_vector const& other);
public:
def_vector(ast_manager& m): m_vars(m), m_defs(m) {}
def_vector(def_vector const& other): m_vars(other.m_vars), m_defs(other.m_defs) {}
void push_back(func_decl* v, expr* e) {
m_vars.push_back(v);
m_defs.push_back(e);
@ -240,6 +242,33 @@ namespace qe {
func_decl* var(unsigned i) const { return m_vars[i]; }
expr* def(unsigned i) const { return m_defs[i]; }
expr_ref_vector::element_ref def_ref(unsigned i) { return m_defs[i]; }
void normalize();
void project(unsigned num_vars, app* const* vars);
};
/**
\brief Guarded definitions.
A realizer to a an existential quantified formula is a disjunction
together with a substitution from the existentially quantified variables
to terms such that:
1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
2. Each guard is equivalent to fml where 'vars' are replaced by the substitution associated
with the guard.
*/
class guarded_defs {
expr_ref_vector m_guards;
vector<def_vector> m_defs;
bool inv();
public:
guarded_defs(ast_manager& m): m_guards(m) { SASSERT(inv()); }
void add(expr* guard, def_vector const& defs);
unsigned size() const { return m_guards.size(); }
def_vector const& defs(unsigned i) const { return m_defs[i]; }
expr* guard(unsigned i) const { return m_guards[i]; }
std::ostream& display(std::ostream& out) const;
void project(unsigned num_vars, app* const* vars);
};
class quant_elim;
@ -277,10 +306,12 @@ namespace qe {
\brief solve for (exists (var) fml).
Return false if operation failed.
Return true and list of pairs (t_i, fml_i) in <terms, fmls>
such that fml[t_1] \/ ... \/ fml[t_n] == (exists (var) fml)
and fml_i == fml[t_1]
such that fml_1 \/ ... \/ fml_n == (exists (var) fml)
and fml_i => fml[t_i]
*/
bool solve_for_var(app* var, expr* fml, expr_ref_vector& terms, expr_ref_vector& fmls);
bool solve_for_var(app* var, expr* fml, guarded_defs& defs);
bool solve_for_vars(unsigned num_vars, app* const* vars, expr* fml, guarded_defs& defs);
void set_cancel(bool f);

138
src/muz_qe/qe_arith_plugin.cpp
View file

@ -367,16 +367,6 @@ namespace qe {
simplify(result);
}
expr_ref mk_idiv(expr* a, numeral const & k) {
if (k.is_one()) {
return expr_ref(a, m);
}
expr_ref result(m);
result = m_arith.mk_idiv(a, m_arith.mk_numeral(k, true));
simplify(result);
return result;
}
expr* mk_numeral(numeral const& k, bool is_int = true) { return m_arith.mk_numeral(k, is_int); }
expr* mk_numeral(int k, bool is_int) { return mk_numeral(numeral(k),is_int); }
@ -1699,6 +1689,40 @@ public:
private:
/**
\brief Compute least upper/greatest lower bounds for x.
Assume:
(not (= k 0))
(<= 0 (mod m k))
(< (mod m k) (abs k))
(= m (+ (* k (div m k)) (mod m k)))
i.e.
k * (e div k) + (e mod k) = e
When k is positive, least upper bound
for x such that: k*x <= e is e div k
When k is negative, greatest lower bound
for x such that k*x <= e is e div k
k * (e div k) + (e mod k) = e
*/
expr_ref mk_idiv(expr* e, numeral k) {
SASSERT(!k.is_zero());
arith_util& a = m_util.m_arith;
if (k.is_one()) {
return expr_ref(e, m);
}
if (k.is_minus_one()) {
return expr_ref(a.mk_uminus(e), m);
}
SASSERT(a.is_int(e));
return expr_ref(a.mk_idiv(e, a.mk_numeral(k, true)), m);
}
void get_def(contains_app& contains_x, unsigned v, expr* fml, expr_ref& def) {
app* x = contains_x.x();
x_subst x_t(m_util);
@ -1730,35 +1754,30 @@ public:
// a*x + term <= 0
expr_ref term(bounds.exprs(is_strict, !is_lower)[i], m);
rational a = bounds.coeffs(is_strict, !is_lower)[i];
if (x_t.get_term()) {
// a*(c*x' + s) + term <= 0
// term <- a*s + term
// a <- a*c
term = m_util.mk_add(m_util.mk_mul(a,x_t.get_term()), term);
a = a * x_t.get_coeff();
// x := coeff * x' + s
// solve instead for
// a*coeff*x' + term + a*s <= 0
TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + "
<< mk_pp(x_t.get_term(), m) << "\n";);
SASSERT(x_t.get_coeff().is_pos());
term = m_util.mk_add(term, m_util.mk_mul(a, x_t.get_term()));
a = a * x_t.get_coeff();
}
TRACE("qe", tout << a << "* " << mk_pp(x,m) << " + " << mk_pp(term, m) << " <= 0\n";);
SASSERT(a.is_int());
if (is_lower) {
// a*x + t <= 0
// <=
// x <= -t div a
SASSERT(a.is_pos());
term = m_util.mk_idiv(m_util.mk_uminus(term), a);
}
else {
// -a*x + t <= 0
// <=>
// t <= a*x
// <=
// ((div t a) + 1) <= x
term = m_util.mk_idiv(term, abs(a));
if (!(abs(a).is_one())) {
term = m_util.mk_add(term, m_util.mk_one(x));
}
}
terms.push_back(term);
SASSERT(is_lower == a.is_pos());
TRACE("qe", tout << is_lower << " " << a << " " << mk_pp(term, m) << "\n";);
// a*x + t <= 0
// <=
// x <= -t div a + 1
term = m_util.mk_uminus(term);
term = mk_idiv(term, a);
terms.push_back(term);
TRACE("qe", tout << "a: " << a << " term: " << mk_pp(term, m) << "\n";);
}
is_strict = true;
sz = bounds.size(is_strict, !is_lower);
@ -1788,14 +1807,11 @@ public:
}
if (x_t.get_term()) {
//
// x = x_t.get_coeff()*x' + x_t.get_term()
// =>
// x' = (x - x_t.get_term()) div x_t.get_coeff()
//
def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff());
// x := coeff * x + s
TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + "
<< mk_pp(x_t.get_term(), m) << "\n";);
def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
}
m_util.simplify(def);
return;
}
@ -1822,25 +1838,39 @@ public:
// assert v => (x <= t_i)
//
SASSERT(v < bounds.size(is_strict, is_lower));
expr_ref t(bounds.exprs(is_strict, is_lower)[v], m);
def = bounds.exprs(is_strict, is_lower)[v];
rational a = bounds.coeffs(is_strict, is_lower)[v];
t = x_t.mk_term(a, t);
a = x_t.mk_coeff(a);
def = t;
if (a.is_pos()) {
def = m_util.mk_uminus(def);
}
if (x_t.get_term()) {
def = m_util.mk_idiv(m_util.mk_sub(def, x_t.get_term()), x_t.get_coeff());
// x := coeff * x' + s
// solve instead for
// a*coeff*x' + term + a*s <= 0
TRACE("qe", tout << x_t.get_coeff() << "* " << mk_pp(x,m) << " + "
<< mk_pp(x_t.get_term(), m) << "\n";);
SASSERT(x_t.get_coeff().is_pos());
def = m_util.mk_add(def, m_util.mk_mul(a, x_t.get_term()));
a = a * x_t.get_coeff();
}
if (!a.is_one()) {
def = m_util.mk_idiv(def, a);
SASSERT(a.is_int());
SASSERT(is_lower != a.is_pos());
// a*x + t <= 0
// <=
// x <= -t div a
def = m_util.mk_uminus(def);
def = mk_idiv(def, a);
if (x_t.get_term()) {
// x := coeff * x + s
def = m_util.mk_add(m_util.mk_mul(x_t.get_coeff(), def), x_t.get_term());
}
m_util.simplify(def);
TRACE("qe", tout << "TBD: " << a << " " << mk_pp(t, m) << "\n";);
TRACE("qe", tout << "TBD: " << a << " " << mk_pp(def, m) << "\n";);
}
expr_ref mk_not(expr* e) {

28
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -467,10 +467,10 @@ namespace qe {
SASSERT(m_datatype_util.is_datatype(s));
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
if (m_datatype_util.is_recursive(s)) {
subst_rec(x, vl, fml);
subst_rec(x, vl, fml, def);
}
else {
subst_nonrec(x, vl, fml);
subst_nonrec(x, vl, fml, def);
}
if (def) {
*def = 0; // TBD
@ -501,14 +501,21 @@ namespace qe {
private:
void add_def(expr* term, expr_ref* def) {
if (def) {
*def = term;
}
}
//
// replace x by C(y1,..,yn) where y1,..,yn are fresh variables.
//
void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml) {
void subst_constructor(contains_app& x, func_decl* c, expr_ref& fml, expr_ref* def) {
subst_clos* sub = 0;
if (m_subst_cache.find(x.x(), c, sub)) {
m_replace->apply_substitution(x.x(), sub->first, 0, fml);
add_def(sub->first, def);
for (unsigned i = 0; i < sub->second.size(); ++i) {
m_ctx.add_var(sub->second[i]);
}
@ -529,6 +536,7 @@ namespace qe {
m_trail.push_back(c);
m_trail.push_back(t);
add_def(t, def);
m_replace->apply_substitution(x.x(), t, 0, fml);
sub->first = t;
m_subst_cache.insert(x.x(), c, sub);
@ -643,7 +651,7 @@ namespace qe {
}
}
void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml) {
void subst_rec(contains_app& contains_x, rational const& vl, expr_ref& fml, expr_ref* def) {
app* x = contains_x.x();
sort* s = x->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
@ -661,6 +669,7 @@ namespace qe {
app_ref fresh_x(m.mk_fresh_const("x", s), m);
m_ctx.add_var(fresh_x);
m_replace->apply_substitution(x, fresh_x, 0, fml);
add_def(fresh_x, def);
TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
return;
}
@ -668,7 +677,7 @@ namespace qe {
if (has_selector(contains_x, fml, c)) {
TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
subst_constructor(contains_x, c, fml);
subst_constructor(contains_x, c, fml, def);
return;
}
@ -697,6 +706,7 @@ namespace qe {
if (idx < eqs.num_eqs()) {
expr* t = eqs.eq(idx);
expr* c = eqs.eq_cond(idx);
add_def(t, def);
m_replace->apply_substitution(x, t, fml);
if (!m.is_true(c)) {
fml = m.mk_and(c, fml);
@ -710,6 +720,10 @@ namespace qe {
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
}
if (def) {
NOT_IMPLEMENTED_YET();
// you need to create a diagonal term
}
}
TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
}
@ -753,7 +767,7 @@ namespace qe {
m_ctx.add_constraint(true, is_c);
}
virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml) {
virtual void subst_nonrec(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
sort* s = x.x()->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
SASSERT(!m_datatype_util.is_recursive(s));
@ -767,7 +781,7 @@ namespace qe {
SASSERT(vl.get_unsigned() < sz);
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
}
subst_constructor(x, c, fml);
subst_constructor(x, c, fml, def);
}