mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +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-19 08:33:57 -07:00
parent ccb50f5d8a 28a4f51ea5
commit 36f7bad1da
8 changed files with 622 additions and 187 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

103
lib/pdr_context.cpp
View file

@ -395,7 +395,6 @@ namespace pdr {
lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
if (is_sat == l_true && core) {
core->reset();
model2cube(*model,*core);
n.set_model(model);
}
return is_sat;
@ -697,34 +696,6 @@ namespace pdr {
}
}
void pred_transformer::model2cube(app* c, expr* val, expr_ref_vector& res) const {
if (m.is_bool(val)) {
res.push_back(m.is_true(val)?c:m.mk_not(c));
}
else {
res.push_back(m.mk_eq(c, val));
}
}
void pred_transformer::model2cube(const model_core& mdl, func_decl * d, expr_ref_vector& res) const {
expr_ref interp(m);
get_value_from_model(mdl, d, interp);
app* c = m.mk_const(d);
model2cube(c, interp, res);
}
void pred_transformer::model2cube(const model_core & mdl, expr_ref_vector & res) const {
unsigned sz = mdl.get_num_constants();
for (unsigned i = 0; i < sz; i++) {
func_decl * d = mdl.get_constant(i);
SASSERT(d->get_arity()==0);
if (!m_solver.is_aux_symbol(d)) {
model2cube(mdl, d, res);
}
}
}
// ----------------
// model_node
@ -1103,11 +1074,9 @@ namespace pdr {
m_inductive_lvl(0),
m_cancel(false)
{
m_use_model_generalizer = m_params.get_bool("use-model-generalizer", false);
}
context::~context() {
reset_model_generalizers();
reset_core_generalizers();
reset();
}
@ -1169,7 +1138,6 @@ namespace pdr {
void context::update_rules(datalog::rule_set& rules) {
decl2rel rels;
init_model_generalizers(rules);
init_core_generalizers(rules);
init_rules(rules, rels);
decl2rel::iterator it = rels.begin(), end = rels.end();
@ -1294,18 +1262,6 @@ namespace pdr {
};
void context::reset_model_generalizers() {
std::for_each(m_model_generalizers.begin(), m_model_generalizers.end(), delete_proc<model_generalizer>());
m_model_generalizers.reset();
}
void context::init_model_generalizers(datalog::rule_set& rules) {
reset_model_generalizers();
if (m_use_model_generalizer) {
m_model_generalizers.push_back(alloc(model_evaluation_generalizer, *this, m));
}
}
void context::reset_core_generalizers() {
std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
m_core_generalizers.reset();
@ -1552,11 +1508,7 @@ namespace pdr {
}
else {
TRACE("pdr", tout << "node: " << &n << "\n";);
for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
(*m_model_generalizers[i])(n, cube);
}
create_children(n, m_pm.mk_and(cube));
create_children(n);
}
break;
case l_false: {
@ -1627,45 +1579,6 @@ namespace pdr {
}
}
// create children states from model cube.
void context::create_children(model_node& n, expr* model) {
if (!m_use_model_generalizer) {
create_children2(n);
return;
}
expr_ref_vector literals(m), sub_lits(m);
expr_ref o_cube(m), n_cube(m);
datalog::flatten_and(model, literals);
ptr_vector<func_decl> preds;
unsigned level = n.level();
SASSERT(level > 0);
n.pt().find_predecessors(n.model(), preds);
n.pt().remove_predecessors(literals);
TRACE("pdr",
model_v2_pp(tout, n.model());
tout << "Model cube\n";
tout << mk_pp(model, m) << "\n";
tout << "Predecessors\n";
for (unsigned i = 0; i < preds.size(); ++i) {
tout << preds[i]->get_name() << "\n";
}
);
for (unsigned i = 0; i < preds.size(); ++i) {
pred_transformer& pt = *m_rels.find(preds[i]);
SASSERT(pt.head() == preds[i]);
assign_ref_vector(sub_lits, literals);
m_pm.filter_o_atoms(sub_lits, i);
o_cube = m_pm.mk_and(sub_lits);
m_pm.formula_o2n(o_cube, n_cube, i);
model_node* child = alloc(model_node, &n, n_cube, pt, level-1);
++m_stats.m_num_nodes;
m_search.add_leaf(*child);
}
check_pre_closed(n);
TRACE("pdr", m_search.display(tout););
}
/**
\brief create children states from model cube.
@ -1707,7 +1620,7 @@ namespace pdr {
- Create sub-goals for L0 and L1.
*/
void context::create_children2(model_node& n) {
void context::create_children(model_node& n) {
SASSERT(n.level() > 0);
pred_transformer& pt = n.pt();
@ -1723,12 +1636,17 @@ namespace pdr {
verbose_stream() << "Phi:\n" << mk_pp(phi, m) << "\n";);
model_evaluator mev(m);
expr_ref_vector mdl(m), forms(m);
expr_ref_vector mdl(m), forms(m), Phi(m);
forms.push_back(T);
forms.push_back(phi);
datalog::flatten_and(forms);
ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
expr_ref_vector Phi = mev.minimize_literals(forms1, M);
if (m_params.get_bool(":use-model-generalizer", false)) {
Phi.append(mev.minimize_model(forms1, M));
}
else {
Phi.append(mev.minimize_literals(forms1, M));
}
ptr_vector<func_decl> preds;
pt.find_predecessors(r, preds);
pt.remove_predecessors(Phi);
@ -1834,9 +1752,6 @@ namespace pdr {
st.update("PDR max depth", m_stats.m_max_depth);
m_pm.collect_statistics(st);
for (unsigned i = 0; i < m_model_generalizers.size(); ++i) {
m_model_generalizers[i]->collect_statistics(st);
}
for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
m_core_generalizers[i]->collect_statistics(st);
}

24
lib/pdr_context.h
View file

@ -98,9 +98,6 @@ namespace pdr {
void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
void model2cube(const model_core& md, func_decl * d, expr_ref_vector& res) const;
void model2cube(app* c, expr* val, expr_ref_vector& res) const;
void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
// Debugging
@ -157,8 +154,6 @@ namespace pdr {
manager& get_pdr_manager() const { return pm; }
ast_manager& get_manager() const { return m; }
void model2cube(const model_core & mdl, expr_ref_vector & res) const;
void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
void close(expr* e);
@ -266,18 +261,6 @@ namespace pdr {
class context;
// 'state' is satisifiable with predecessor 'cube'.
// Generalize predecessor still forcing satisfiability.
class model_generalizer {
protected:
context& m_ctx;
public:
model_generalizer(context& ctx): m_ctx(ctx) {}
virtual ~model_generalizer() {}
virtual void operator()(model_node& n, expr_ref_vector& cube) = 0;
virtual void collect_statistics(statistics& st) {}
};
// 'state' is unsatisfiable at 'level' with 'core'.
// Minimize or weaken core.
class core_generalizer {
@ -317,9 +300,7 @@ namespace pdr {
pred_transformer* m_query;
model_search m_search;
lbool m_last_result;
bool m_use_model_generalizer;
unsigned m_inductive_lvl;
ptr_vector<model_generalizer> m_model_generalizers;
ptr_vector<core_generalizer> m_core_generalizers;
stats m_stats;
volatile bool m_cancel;
@ -336,8 +317,7 @@ namespace pdr {
void check_pre_closed(model_node& n);
void expand_node(model_node& n);
lbool expand_state(model_node& n, expr_ref_vector& cube);
void create_children(model_node& n, expr* model);
void create_children2(model_node& n);
void create_children(model_node& n);
expr_ref mk_sat_answer() const;
expr_ref mk_unsat_answer() const;
@ -347,7 +327,6 @@ namespace pdr {
// Initialization
class classifier_proc;
void init_model_generalizers(datalog::rule_set& rules);
void init_core_generalizers(datalog::rule_set& rules);
bool check_invariant(unsigned lvl);
@ -359,7 +338,6 @@ namespace pdr {
void simplify_formulas();
void reset_model_generalizers();
void reset_core_generalizers();
public:

13
lib/pdr_generalizers.cpp
View file

@ -29,19 +29,6 @@ Revision History:
namespace pdr {
//
// eliminate conjuncts from cube as long as state is satisfied.
//
void model_evaluation_generalizer::operator()(model_node& n, expr_ref_vector& cube) {
expr_ref_vector forms(cube.get_manager());
forms.push_back(n.state());
forms.push_back(n.pt().transition());
datalog::flatten_and(forms);
ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
model_ref mdl = n.model_ptr();
m_model_evaluator.minimize_model(forms1, mdl, cube);
}
//
// main propositional induction generalizer.
// drop literals one by one from the core and check if the core is still inductive.

8
lib/pdr_generalizers.h
View file

@ -25,14 +25,6 @@ Revision History:
namespace pdr {
class model_evaluation_generalizer : public model_generalizer {
model_evaluator m_model_evaluator;
public:
model_evaluation_generalizer(context& ctx, ast_manager& m) : model_generalizer(ctx), m_model_evaluator(m) {}
virtual ~model_evaluation_generalizer() {}
virtual void operator()(model_node& n, expr_ref_vector& cube);
};
class core_bool_inductive_generalizer : public core_generalizer {
unsigned m_failure_limit;
public:

59
lib/pdr_util.cpp
View file

@ -90,33 +90,6 @@ std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
//
bool model_evaluator::get_assignment(expr* e, expr*& var, expr*& val) {
if (m.is_eq(e, var, val)) {
if (!is_uninterp(var)) {
std::swap(var, val);
}
if (m.is_true(val) || m.is_false(val) || m_arith.is_numeral(val)) {
return true;
}
TRACE("pdr_verbose", tout << "no value for " << mk_pp(val, m) << "\n";);
return false;
}
else if (m.is_not(e, var)) {
val = m.mk_false();
return true;
}
else if (m.is_bool(e)) {
val = m.mk_true();
var = e;
return true;
}
else {
TRACE("pdr_verbose", tout << "no value set of " << mk_pp(e, m) << "\n";);
return false;
}
}
void model_evaluator::assign_value(expr* e, expr* val) {
rational r;
if (m.is_true(val)) {
@ -166,7 +139,7 @@ void model_evaluator::reset() {
m_model = 0;
}
void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl, expr_ref_vector & model) {
expr_ref_vector model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl) {
setup_model(mdl);
TRACE("pdr_verbose",
@ -174,7 +147,7 @@ void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_re
for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
);
prune_by_cone_of_influence(formulas, model);
expr_ref_vector model = prune_by_cone_of_influence(formulas);
TRACE("pdr_verbose",
tout << "pruned model:\n";
for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";);
@ -185,6 +158,8 @@ void model_evaluator::minimize_model(ptr_vector<expr> const & formulas, model_re
setup_model(mdl);
VERIFY(check_model(formulas));
reset(););
return model;
}
expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formulas, model_ref& mdl) {
@ -340,7 +315,7 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
m_visited.reset();
}
void model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model) {
expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formulas) {
ptr_vector<expr> tocollect;
collect(formulas, tocollect);
m1.reset();
@ -349,19 +324,23 @@ void model_evaluator::prune_by_cone_of_influence(ptr_vector<expr> const & formul
TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";);
for_each_expr(*this, m_visited, tocollect[i]);
}
unsigned sz1 = model.size();
for (unsigned i = 0; i < model.size(); ++i) {
expr* e = model[i].get(), *var, *val;
if (get_assignment(e, var, val)) {
if (!m_visited.is_marked(var)) {
model[i] = model.back();
model.pop_back();
--i;
}
unsigned sz = m_model->get_num_constants();
expr_ref e(m), eq(m);
expr_ref_vector model(m);
bool_rewriter rw(m);
for (unsigned i = 0; i < sz; i++) {
func_decl * d = m_model->get_constant(i);
expr* val = m_model->get_const_interp(d);
e = m.mk_const(d);
if (m_visited.is_marked(e)) {
rw.mk_eq(e, val, eq);
model.push_back(eq);
}
}
m_visited.reset();
TRACE("pdr", tout << sz1 << " ==> " << model.size() << "\n";);
TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";);
return model;
}
void model_evaluator::eval_arith(app* e) {

17
lib/pdr_util.h
View file

@ -194,10 +194,9 @@ class model_evaluator {
void reset();
void setup_model(model_ref& model);
void assign_value(expr* e, expr* v);
bool get_assignment(expr* e, expr*& var, expr*& val);
void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
void prune_by_cone_of_influence(ptr_vector<expr> const & formulas, expr_ref_vector& model);
expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
void eval_arith(app* e);
void eval_basic(app* e);
void eval_iff(app* e, expr* arg1, expr* arg2);
@ -230,7 +229,13 @@ protected:
public:
model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_refs(m) {}
virtual void minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl, expr_ref_vector& model);
/**
\brief extract equalities from model that suffice to satisfy formula.
\pre model satisfies formulas
*/
expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
\brief extract literals from formulas that satisfy formulas.
@ -239,12 +244,6 @@ public:
*/
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
/**
\brief extract literals from formulas that satisfy formulas.
\pre model satisfies formulas
*/
expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, expr_ref_vector const & model);
// for_each_expr visitor.
void operator()(expr* e) {}

536
lib/qe_lite.cpp Normal file
View file

@ -0,0 +1,536 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
qe_lite.cpp
Abstract:
Light weight partial quantifier-elimination procedure
Author:
Nikolaj Bjorner (nbjorner) 2012-10-17
Revision History:
- TBD: integrate Fourier Motzkin elimination
integrate Gaussean elimination
--*/
#include "qe_lite.h"
#include "expr_abstract.h"
#include "used_vars.h"
#include"occurs.h"
#include"for_each_expr.h"
#include"rewriter_def.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"ast_smt2_pp.h"
#include"tactical.h"
#include"bool_rewriter.h"
#include"var_subst.h"
class der2 {
ast_manager & m;
var_subst m_subst;
expr_ref_buffer m_new_exprs;
ptr_vector<expr> m_map;
int_vector m_pos2var;
ptr_vector<var> m_inx2var;
unsigned_vector m_order;
expr_ref_vector m_subst_map;
expr_ref_buffer m_new_args;
/**
\brief Return true if e can be viewed as a variable disequality.
Store the variable id in v and the definition in t.
For example:
if e is (not (= (VAR 1) T)), then v assigned to 1, and t to T.
if e is (iff (VAR 2) T), then v is assigned to 2, and t to (not T).
(not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))),
and can be viewed as a disequality.
*/
bool is_var_diseq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
/**
\brief Return true if e can be viewed as a variable equality.
*/
bool is_var_eq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
bool is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t);
void get_elimination_order();
void create_substitution(unsigned sz);
void apply_substitution(quantifier * q, expr_ref & r);
void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr);
void elim_unused_vars(expr_ref& r, proof_ref &pr);
public:
der2(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {}
void operator()(quantifier * q, expr_ref & r, proof_ref & pr);
void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr);
ast_manager& get_manager() const { return m; }
};
static bool is_var(expr * e, unsigned num_decls) {
return is_var(e) && to_var(e)->get_idx() < num_decls;
}
static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
expr* e1;
return m.is_not(e, e1) && is_var(e1, num_decls);
}
bool der2::is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t) {
if (check_eq) {
return is_var_eq(e, num_decls, v, t);
}
else {
return is_var_diseq(e, num_decls, v, t);
}
}
bool der2::is_var_eq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
expr* lhs, *rhs;
// (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases
if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
// (iff (not VAR) t) (iff t (not VAR)) cases
if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls) && m.is_bool(lhs)) {
if (!is_neg_var(m, lhs, num_decls)) {
std::swap(lhs, rhs);
}
if (!is_neg_var(m, lhs, num_decls)) {
return false;
}
v = to_var(lhs);
t = m.mk_not(rhs);
m_new_exprs.push_back(t);
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true;
}
if (!is_var(lhs, num_decls))
std::swap(lhs, rhs);
if (!is_var(lhs, num_decls))
return false;
v = to_var(lhs);
t = rhs;
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true;
}
// (ite cond (= VAR t) (= VAR t2)) case
expr* cond, *e2, *e3;
if (m.is_ite(e, cond, e2, e3)) {
if (is_var_eq(e2, num_decls, v, t)) {
expr_ref t2(m);
var* v2;
if (is_var_eq(e3, num_decls, v2, t2) && v2 == v) {
t = m.mk_ite(cond, t, t2);
m_new_exprs.push_back(t);
return true;
}
}
return false;
}
// VAR = true case
if (is_var(e, num_decls)) {
t = m.mk_true();
v = to_var(e);
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true;
}
// VAR = false case
if (is_neg_var(m, e, num_decls)) {
t = m.mk_false();
v = to_var(to_app(e)->get_arg(0));
TRACE("der", tout << mk_pp(e, m) << "\n";);
return true;
}
return false;
}
/**
\brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or
(iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)).
The last case can be viewed
*/
bool der2::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
expr* e1;
if (m.is_not(e, e1)) {
return is_var_eq(e, num_decls, v, t);
}
else if (is_var_eq(e, num_decls, v, t) && m.is_bool(v)) {
bool_rewriter(m).mk_not(t, t);
m_new_exprs.push_back(t);
return true;
}
else {
return false;
}
}
void der2::elim_unused_vars(expr_ref& r, proof_ref& pr) {
if (is_quantifier(r)) {
quantifier * q = to_quantifier(r);
::elim_unused_vars(m, q, r);
if (m.proofs_enabled()) {
proof * p1 = m.mk_elim_unused_vars(q, r);
pr = m.mk_transitivity(pr, p1);
}
}
}
/**
Reduce the set of definitions in quantifier.
Then eliminate variables that have become unused
*/
void der2::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
TRACE("der", tout << mk_pp(q, m) << "\n";);
pr = 0;
r = q;
reduce_quantifier(q, r, pr);
if (r != q) {
elim_unused_vars(r, pr);
}
}
void der2::reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
// Keep applying reduce_quantifier1 until r doesn't change anymore
do {
proof_ref curr_pr(m);
q = to_quantifier(r);
reduce_quantifier1(q, r, curr_pr);
if (m.proofs_enabled()) {
pr = m.mk_transitivity(pr, curr_pr);
}
} while (q != r && is_quantifier(r));
m_new_exprs.reset();
}
void der2::reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) {
expr * e = q->get_expr();
unsigned num_decls = q->get_num_decls();
var * v = 0;
expr_ref t(m);
unsigned num_args = 1;
expr* const* args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();
args = to_app(e)->get_args();
}
unsigned def_count = 0;
unsigned largest_vinx = 0;
m_map.reset();
m_pos2var.reset();
m_inx2var.reset();
m_pos2var.reserve(num_args, -1);
// Find all definitions
for (unsigned i = 0; i < num_args; i++) {
if (is_var_def(q->is_exists(), args[i], num_decls, v, t)) {
unsigned idx = v->get_idx();
if(m_map.get(idx, 0) == 0) {
m_map.reserve(idx + 1, 0);
m_inx2var.reserve(idx + 1, 0);
m_map[idx] = t;
m_inx2var[idx] = v;
m_pos2var[i] = idx;
def_count++;
largest_vinx = std::max(idx, largest_vinx);
}
}
}
if (def_count > 0) {
get_elimination_order();
SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
if (!m_order.empty()) {
create_substitution(largest_vinx + 1);
apply_substitution(q, r);
}
else {
r = q;
}
}
else {
TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
r = q;
}
if (m.proofs_enabled()) {
pr = r == q ? 0 : m.mk_der(q, r);
}
}
static void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
order.reset();
// eliminate self loops, and definitions containing quantifiers.
bool found = false;
for (unsigned i = 0; i < definitions.size(); i++) {
var * v = vars[i];
expr * t = definitions[i];
if (t == 0 || has_quantifiers(t) || occurs(v, t))
definitions[i] = 0;
else
found = true; // found at least one candidate
}
if (!found)
return;
typedef std::pair<expr *, unsigned> frame;
svector<frame> todo;
expr_fast_mark1 visiting;
expr_fast_mark2 done;
unsigned vidx, num;
for (unsigned i = 0; i < definitions.size(); i++) {
if (definitions[i] == 0)
continue;
var * v = vars[i];
SASSERT(v->get_idx() == i);
SASSERT(todo.empty());
todo.push_back(frame(v, 0));
while (!todo.empty()) {
start:
frame & fr = todo.back();
expr * t = fr.first;
if (t->get_ref_count() > 1 && done.is_marked(t)) {
todo.pop_back();
continue;
}
switch (t->get_kind()) {
case AST_VAR:
vidx = to_var(t)->get_idx();
if (fr.second == 0) {
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
// Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
if (definitions.get(vidx, 0) != 0) {
if (visiting.is_marked(t)) {
// cycle detected: remove t
visiting.reset_mark(t);
definitions[vidx] = 0;
}
else {
visiting.mark(t);
fr.second = 1;
todo.push_back(frame(definitions[vidx], 0));
goto start;
}
}
}
else {
SASSERT(fr.second == 1);
if (definitions.get(vidx, 0) != 0) {
visiting.reset_mark(t);
order.push_back(vidx);
}
else {
// var was removed from the list of candidate vars to elim cycle
// do nothing
}
}
if (t->get_ref_count() > 1)
done.mark(t);
todo.pop_back();
break;
case AST_QUANTIFIER:
UNREACHABLE();
todo.pop_back();
break;
case AST_APP:
num = to_app(t)->get_num_args();
while (fr.second < num) {
expr * arg = to_app(t)->get_arg(fr.second);
fr.second++;
if (arg->get_ref_count() > 1 && done.is_marked(arg))
continue;
todo.push_back(frame(arg, 0));
goto start;
}
if (t->get_ref_count() > 1)
done.mark(t);
todo.pop_back();
break;
default:
UNREACHABLE();
todo.pop_back();
break;
}
}
}
}
void der2::get_elimination_order() {
m_order.reset();
TRACE("top_sort",
tout << "DEFINITIONS: " << std::endl;
for(unsigned i = 0; i < m_map.size(); i++)
if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl;
);
// der2::top_sort ts(m);
der_sort_vars(m_inx2var, m_map, m_order);
TRACE("der",
tout << "Elimination m_order:" << std::endl;
for(unsigned i=0; i<m_order.size(); i++)
{
if (i != 0) tout << ",";
tout << m_order[i];
}
tout << std::endl;
);
}
void der2::create_substitution(unsigned sz) {
m_subst_map.reset();
m_subst_map.resize(sz, 0);
for(unsigned i = 0; i < m_order.size(); i++) {
expr_ref cur(m_map[m_order[i]], m);
// do all the previous substitutions before inserting
expr_ref r(m);
m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
unsigned inx = sz - m_order[i]- 1;
SASSERT(m_subst_map[inx]==0);
m_subst_map[inx] = r;
}
}
void der2::apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args=to_app(e)->get_num_args();
bool_rewriter rw(m);
// get a new expression
m_new_args.reset();
for(unsigned i = 0; i < num_args; i++) {
int x = m_pos2var[i];
if (x != -1 && m_map[x] != 0)
continue; // this is a disequality with definition (vanishes)
m_new_args.push_back(to_app(e)->get_arg(i));
}
expr_ref t(m);
if (q->is_forall()) {
rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t);
}
else {
rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t);
}
expr_ref new_e(m);
m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
// don't forget to update the quantifier patterns
expr_ref_buffer new_patterns(m);
expr_ref_buffer new_no_patterns(m);
for (unsigned j = 0; j < q->get_num_patterns(); j++) {
expr_ref new_pat(m);
m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat);
new_patterns.push_back(new_pat);
}
for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
expr_ref new_nopat(m);
m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat);
new_no_patterns.push_back(new_nopat);
}
r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(),
new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
}
class qe_lite::impl {
ast_manager& m;
der2 m_der;
public:
impl(ast_manager& m): m(m), m_der(m) {}
void operator()(app_ref_vector& vars, expr_ref& fml) {
expr_ref tmp(fml);
quantifier_ref q(m);
proof_ref pr(m);
symbol qe_lite("QE");
expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), fml, tmp);
ptr_vector<sort> sorts;
svector<symbol> names;
for (unsigned i = 0; i < vars.size(); ++i) {
sorts.push_back(m.get_sort(vars[i].get()));
names.push_back(vars[i]->get_decl()->get_name());
}
q = m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qe_lite);
m_der.reduce_quantifier(q, tmp, pr);
// assumes m_der just updates the quantifier and does not change things more.
if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) {
used_vars used;
tmp = to_quantifier(tmp)->get_expr();
used.process(tmp);
var_subst vs(m, true);
vs(tmp, vars.size(), (expr*const*)vars.c_ptr(), fml);
// collect set of variables that were used.
unsigned j = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
if (used.contains(vars.size()-i-1)) {
vars[j] = vars[i];
++j;
}
}
vars.resize(j);
}
else {
fml = tmp;
}
}
void operator()(expr_ref& fml, proof_ref& pr) {
// TODO apply der everywhere as a rewriting rule.
// TODO add cancel method.
if (is_quantifier(fml)) {
m_der(to_quantifier(fml), fml, pr);
}
}
};
qe_lite::qe_lite(ast_manager& m) {
m_impl = alloc(impl, m);
}
qe_lite::~qe_lite() {
dealloc(m_impl);
}
void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
(*m_impl)(vars, fml);
}
void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
(*m_impl)(fml, pr);
}

49
lib/qe_lite.h Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2010 Microsoft Corporation
Module Name:
qe_lite.h
Abstract:
Light weight partial quantifier-elimination procedures
Author:
Nikolaj Bjorner (nbjorner) 2012-10-17
Revision History:
--*/
#ifndef __QE_LITE_H__
#define __QE_LITE_H__
#include "ast.h"
class qe_lite {
class impl;
impl * m_impl;
public:
qe_lite(ast_manager& m);
~qe_lite();
/**
\brief
Apply light-weight quantifier elimination
on constants provided as vector of variables.
Return the updated formula and updated set of variables that were not eliminated.
*/
void operator()(app_ref_vector& vars, expr_ref& fml);
/**
\brief full rewriting based light-weight quantifier elimination round.
*/
void operator()(expr_ref& fml, proof_ref& pr);
};
#endif __QE_LITE_H__