mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
split muz_qe into two directories
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
d795792304
commit
137339a2e1
174 changed files with 242 additions and 174 deletions
2023
src/qe/nlarith_util.cpp
Normal file
2023
src/qe/nlarith_util.cpp
Normal file
File diff suppressed because it is too large
Load diff
151
src/qe/nlarith_util.h
Normal file
151
src/qe/nlarith_util.h
Normal file
|
|
@ -0,0 +1,151 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
nlarith_util.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Utilities for nln-linear arithmetic quantifier elimination and
|
||||
solving.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj (nbjorner) 2011-05-13
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _NLARITH_UTIL_H_
|
||||
#define _NLARITH_UTIL_H_
|
||||
|
||||
#include "ast.h"
|
||||
#include "lbool.h"
|
||||
|
||||
namespace nlarith {
|
||||
|
||||
/**
|
||||
\brief A summary for branch side conditions and substitutions.
|
||||
|
||||
Each branch in a split comprises of:
|
||||
- preds - a sequence of predicates used for the branching.
|
||||
- branches - a sequence of branch side conditions
|
||||
- subst - a sequence of substitutions that replace 'preds' by formulas
|
||||
not containing the eliminated variable
|
||||
- constraints - a sequence of side constraints to add to the main formula.
|
||||
*/
|
||||
class branch_conditions {
|
||||
expr_ref_vector m_branches;
|
||||
expr_ref_vector m_preds;
|
||||
vector<expr_ref_vector> m_subst;
|
||||
expr_ref_vector m_constraints;
|
||||
expr_ref_vector m_defs;
|
||||
expr_ref_vector m_a;
|
||||
expr_ref_vector m_b;
|
||||
expr_ref_vector m_c;
|
||||
|
||||
public:
|
||||
branch_conditions(ast_manager& m) : m_branches(m), m_preds(m), m_constraints(m), m_defs(m), m_a(m), m_b(m), m_c(m) {}
|
||||
void add_pred(expr* p) { m_preds.push_back(p); }
|
||||
void add_branch(expr* branch, expr* cond, expr_ref_vector const& subst, expr* def, expr* a, expr* b, expr* c) {
|
||||
m_branches.push_back(branch);
|
||||
m_constraints.push_back(cond);
|
||||
m_subst.push_back(subst);
|
||||
m_defs.push_back(def);
|
||||
m_a.push_back(a);
|
||||
m_b.push_back(b);
|
||||
m_c.push_back(c);
|
||||
}
|
||||
expr* preds(unsigned i) const { return m_preds[i]; }
|
||||
expr* branches(unsigned i) const { return m_branches[i]; }
|
||||
expr* constraints(unsigned i) const { return m_constraints[i]; }
|
||||
expr* def(unsigned i) const { return m_defs[i]; }
|
||||
expr* a(unsigned i) const { return m_a[i]; }
|
||||
expr* b(unsigned i) const { return m_b[i]; }
|
||||
expr* c(unsigned i) const { return m_c[i]; }
|
||||
expr_ref_vector const& subst(unsigned i) const { return m_subst[i]; }
|
||||
expr_ref_vector const& branches() const { return m_branches; }
|
||||
expr_ref_vector const& preds() const { return m_preds; }
|
||||
vector<expr_ref_vector> const& subst() const { return m_subst; }
|
||||
expr_ref_vector const& constraints() const { return m_constraints; }
|
||||
void reset() {
|
||||
m_branches.reset(); m_preds.reset(); m_subst.reset();
|
||||
m_constraints.reset(); m_defs.reset();
|
||||
m_a.reset(); m_b.reset(); m_c.reset();
|
||||
}
|
||||
|
||||
unsigned size() const { return branches().size(); }
|
||||
unsigned num_preds() const { return preds().size(); }
|
||||
};
|
||||
|
||||
class util {
|
||||
class imp;
|
||||
imp* m_imp;
|
||||
public:
|
||||
util(ast_manager& m);
|
||||
~util();
|
||||
|
||||
/**
|
||||
\brief Enable handling of linear variables.
|
||||
*/
|
||||
void set_enable_linear(bool enable_linear);
|
||||
|
||||
/**
|
||||
\brief Create branches for non-linear variable x.
|
||||
*/
|
||||
bool create_branches(app* x, unsigned nl, expr* const* lits, branch_conditions& bc);
|
||||
/**
|
||||
\brief Extract non-linear variables from ground formula.
|
||||
|
||||
\requires a ground formula.
|
||||
*/
|
||||
void extract_non_linear(expr* e, ptr_vector<app>& nl_vars);
|
||||
|
||||
/**
|
||||
\brief literal sets. Opaque state.
|
||||
*/
|
||||
|
||||
class literal_set;
|
||||
|
||||
static void deallocate(literal_set* lits);
|
||||
|
||||
|
||||
|
||||
/**
|
||||
\brief Sign-based branching. v2.
|
||||
*/
|
||||
typedef obj_hashtable<app> atoms;
|
||||
|
||||
class eval {
|
||||
public:
|
||||
virtual ~eval() {}
|
||||
virtual lbool operator()(app* a) = 0;
|
||||
};
|
||||
|
||||
enum atom_update { INSERT, REMOVE };
|
||||
|
||||
class branch {
|
||||
public:
|
||||
virtual ~branch() {}
|
||||
virtual app* get_constraint() = 0;
|
||||
virtual void get_updates(ptr_vector<app>& atoms, svector<atom_update>& updates) = 0;
|
||||
};
|
||||
|
||||
/**
|
||||
\brief select literals that contain non-linear variables.
|
||||
*/
|
||||
bool get_sign_literals(atoms const& atoms, eval& eval, literal_set*& lits);
|
||||
|
||||
/**
|
||||
\brief given selected literals, generate branch conditions.
|
||||
*/
|
||||
void get_sign_branches(literal_set& lits, eval& eval, ptr_vector<branch>& branches);
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
2622
src/qe/qe.cpp
Normal file
2622
src/qe/qe.cpp
Normal file
File diff suppressed because it is too large
Load diff
388
src/qe/qe.h
Normal file
388
src/qe/qe.h
Normal file
|
|
@ -0,0 +1,388 @@
|
|||
/*++
|
||||
Copyright (c) 2010 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Quantifier-elimination procedures
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2010-02-19
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef __QE_H__
|
||||
#define __QE_H__
|
||||
|
||||
#include "ast.h"
|
||||
#include "smt_params.h"
|
||||
#include "statistics.h"
|
||||
#include "lbool.h"
|
||||
#include "expr_functors.h"
|
||||
#include "simplifier.h"
|
||||
#include "rewriter.h"
|
||||
#include "model.h"
|
||||
#include "params.h"
|
||||
|
||||
namespace qe {
|
||||
|
||||
|
||||
class i_nnf_atom {
|
||||
public:
|
||||
virtual void operator()(expr* e, bool pol, expr_ref& result) = 0;
|
||||
};
|
||||
|
||||
typedef obj_hashtable<app> atom_set;
|
||||
|
||||
class qe_solver_plugin;
|
||||
|
||||
|
||||
class i_solver_context {
|
||||
protected:
|
||||
class is_relevant : public i_expr_pred {
|
||||
i_solver_context& m_s;
|
||||
public:
|
||||
is_relevant(i_solver_context& s):m_s(s) {}
|
||||
virtual bool operator()(expr* e);
|
||||
};
|
||||
class mk_atom_fn : public i_nnf_atom {
|
||||
i_solver_context& m_s;
|
||||
public:
|
||||
mk_atom_fn(i_solver_context& s) : m_s(s) {}
|
||||
void operator()(expr* e, bool p, expr_ref& result);
|
||||
};
|
||||
|
||||
is_relevant m_is_relevant;
|
||||
mk_atom_fn m_mk_atom;
|
||||
ptr_vector<qe_solver_plugin> m_plugins; // fid -> plugin
|
||||
|
||||
public:
|
||||
i_solver_context():m_is_relevant(*this), m_mk_atom(*this) {}
|
||||
|
||||
virtual ~i_solver_context();
|
||||
|
||||
void add_plugin(qe_solver_plugin* p);
|
||||
|
||||
bool has_plugin(app* x);
|
||||
|
||||
qe_solver_plugin& plugin(app* x);
|
||||
|
||||
qe_solver_plugin& plugin(unsigned fid) { return *m_plugins[fid]; }
|
||||
|
||||
void mk_atom(expr* e, bool p, expr_ref& result);
|
||||
|
||||
virtual ast_manager& get_manager() = 0;
|
||||
|
||||
// set of atoms in current formula.
|
||||
virtual atom_set const& pos_atoms() const = 0;
|
||||
virtual atom_set const& neg_atoms() const = 0;
|
||||
|
||||
// Access current set of variables to solve
|
||||
virtual unsigned get_num_vars() const = 0;
|
||||
virtual app* get_var(unsigned idx) const = 0;
|
||||
virtual app*const* get_vars() const = 0;
|
||||
virtual bool is_var(expr* e, unsigned& idx) const;
|
||||
virtual contains_app& contains(unsigned idx) = 0;
|
||||
|
||||
// callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml'
|
||||
virtual void elim_var(unsigned idx, expr* fml, expr* def) = 0;
|
||||
|
||||
// callback to add new variable to branch.
|
||||
virtual void add_var(app* x) = 0;
|
||||
|
||||
// callback to add constraints in branch.
|
||||
virtual void add_constraint(bool use_var, expr* l1 = 0, expr* l2 = 0, expr* l3 = 0) = 0;
|
||||
|
||||
// eliminate finite domain variable 'var' from fml.
|
||||
virtual void blast_or(app* var, expr_ref& fml) = 0;
|
||||
|
||||
i_expr_pred& get_is_relevant() { return m_is_relevant; }
|
||||
|
||||
i_nnf_atom& get_mk_atom() { return m_mk_atom; }
|
||||
};
|
||||
|
||||
class conj_enum {
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_conjs;
|
||||
public:
|
||||
conj_enum(ast_manager& m, expr* e);
|
||||
|
||||
class iterator {
|
||||
conj_enum* m_super;
|
||||
unsigned m_index;
|
||||
public:
|
||||
iterator(conj_enum& c, bool first) : m_super(&c), m_index(first?0:c.m_conjs.size()) {}
|
||||
expr* operator*() { return m_super->m_conjs[m_index].get(); }
|
||||
iterator& operator++() { m_index++; return *this; }
|
||||
bool operator==(iterator const& it) const { return m_index == it.m_index; }
|
||||
bool operator!=(iterator const& it) const { return m_index != it.m_index; }
|
||||
};
|
||||
|
||||
void extract_equalities(expr_ref_vector& eqs);
|
||||
|
||||
iterator begin() { return iterator(*this, true); }
|
||||
iterator end() { return iterator(*this, false); }
|
||||
};
|
||||
|
||||
|
||||
//
|
||||
// interface for plugins to eliminate quantified variables.
|
||||
//
|
||||
class qe_solver_plugin {
|
||||
protected:
|
||||
ast_manager& m;
|
||||
family_id m_fid;
|
||||
i_solver_context& m_ctx;
|
||||
public:
|
||||
qe_solver_plugin(ast_manager& m, family_id fid, i_solver_context& ctx) :
|
||||
m(m),
|
||||
m_fid(fid),
|
||||
m_ctx(ctx)
|
||||
{}
|
||||
|
||||
virtual ~qe_solver_plugin() {}
|
||||
|
||||
family_id get_family_id() { return m_fid; }
|
||||
|
||||
/**
|
||||
\brief Return number of case splits for variable x in fml.
|
||||
*/
|
||||
virtual bool get_num_branches(contains_app& x, expr* fml, rational& num_branches) = 0;
|
||||
|
||||
/**
|
||||
\brief Given a case split index 'vl' assert the constraints associated with it.
|
||||
*/
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) = 0;
|
||||
|
||||
|
||||
/**
|
||||
\brief The case splits associated with 'vl' are satisfiable.
|
||||
Apply the elimination for fml corresponding to case split.
|
||||
If def is non-null, then retrieve the realizer corresponding to the case split.
|
||||
*/
|
||||
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) = 0;
|
||||
|
||||
|
||||
/**
|
||||
\brief solve quantified variable.
|
||||
*/
|
||||
virtual bool solve(conj_enum& conjs, expr* fml) = 0;
|
||||
|
||||
/**
|
||||
\brief project variable x for fml given model.
|
||||
|
||||
Assumption: model |= fml[x]
|
||||
|
||||
Projection updates fml to fml', such that:
|
||||
|
||||
- fml' -> fml
|
||||
- model |= fml'
|
||||
- fml' does not contain x
|
||||
|
||||
return false if the method is not implemented.
|
||||
*/
|
||||
virtual bool project(contains_app& x, model_ref& model, expr_ref& fml) { return false; }
|
||||
|
||||
/**
|
||||
\brief assign branching penalty to variable x for 'fml'.
|
||||
*/
|
||||
virtual unsigned get_weight(contains_app& x, expr* fml) { return UINT_MAX; }
|
||||
|
||||
/**
|
||||
\brief simplify formula.
|
||||
*/
|
||||
virtual bool simplify(expr_ref& fml) { return false; }
|
||||
|
||||
/**
|
||||
\brief Normalize literal during NNF conversion.
|
||||
*/
|
||||
virtual bool mk_atom(expr* e, bool p, expr_ref& result) { return false; }
|
||||
|
||||
/**
|
||||
\brief Determine whether sub-term is uninterpreted with respect to quantifier elimination.
|
||||
*/
|
||||
virtual bool is_uninterpreted(app* f) { return true; }
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_datatype_plugin(i_solver_context& ctx);
|
||||
|
||||
qe_solver_plugin* mk_bool_plugin(i_solver_context& ctx);
|
||||
|
||||
qe_solver_plugin* mk_bv_plugin(i_solver_context& ctx);
|
||||
|
||||
qe_solver_plugin* mk_dl_plugin(i_solver_context& ctx);
|
||||
|
||||
qe_solver_plugin* mk_array_plugin(i_solver_context& ctx);
|
||||
|
||||
qe_solver_plugin* mk_arith_plugin(i_solver_context& ctx, bool produce_models, smt_params& p);
|
||||
|
||||
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);
|
||||
}
|
||||
void reset() { m_vars.reset(); m_defs.reset(); }
|
||||
void append(def_vector const& o) { m_vars.append(o.m_vars); m_defs.append(o.m_defs); }
|
||||
unsigned size() const { return m_defs.size(); }
|
||||
void shrink(unsigned sz) { m_vars.shrink(sz); m_defs.shrink(sz); }
|
||||
bool empty() const { return m_defs.empty(); }
|
||||
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;
|
||||
|
||||
class expr_quant_elim {
|
||||
ast_manager& m;
|
||||
smt_params const& m_fparams;
|
||||
params_ref m_params;
|
||||
expr_ref_vector m_trail;
|
||||
obj_map<expr,expr*> m_visited;
|
||||
quant_elim* m_qe;
|
||||
expr* m_assumption;
|
||||
bool m_use_new_qe;
|
||||
public:
|
||||
expr_quant_elim(ast_manager& m, smt_params const& fp, params_ref const& p = params_ref());
|
||||
~expr_quant_elim();
|
||||
|
||||
void operator()(expr* assumption, expr* fml, expr_ref& result);
|
||||
|
||||
void collect_statistics(statistics & st) const;
|
||||
|
||||
void updt_params(params_ref const& p);
|
||||
|
||||
void collect_param_descrs(param_descrs& r);
|
||||
|
||||
/**
|
||||
\brief try to eliminate 'vars' and find first satisfying assignment.
|
||||
|
||||
return l_true if satisfiable, l_false if unsatisfiable, l_undef if
|
||||
the formula could not be satisfied modulo eliminating the quantified variables.
|
||||
*/
|
||||
lbool first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs);
|
||||
|
||||
/**
|
||||
\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_1 \/ ... \/ fml_n == (exists (var) fml)
|
||||
and fml_i => fml[t_i]
|
||||
*/
|
||||
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);
|
||||
|
||||
private:
|
||||
void instantiate_expr(expr_ref_vector& bound, expr_ref& fml);
|
||||
void abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml);
|
||||
void elim(expr_ref& result);
|
||||
void init_qe();
|
||||
};
|
||||
|
||||
class expr_quant_elim_star1 : public simplifier {
|
||||
protected:
|
||||
expr_quant_elim m_quant_elim;
|
||||
expr* m_assumption;
|
||||
virtual bool visit_quantifier(quantifier * q);
|
||||
virtual void reduce1_quantifier(quantifier * q);
|
||||
virtual bool is_target(quantifier * q) const { return q->get_num_patterns() == 0 && q->get_num_no_patterns() == 0; }
|
||||
public:
|
||||
expr_quant_elim_star1(ast_manager & m, smt_params const& p);
|
||||
virtual ~expr_quant_elim_star1() {}
|
||||
|
||||
void collect_statistics(statistics & st) const {
|
||||
m_quant_elim.collect_statistics(st);
|
||||
}
|
||||
|
||||
void reduce_with_assumption(expr* ctx, expr* fml, expr_ref& result);
|
||||
|
||||
lbool first_elim(unsigned num_vars, app* const* vars, expr_ref& fml, def_vector& defs) {
|
||||
return m_quant_elim.first_elim(num_vars, vars, fml, defs);
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {} // TBD: replace simplifier by rewriter
|
||||
|
||||
};
|
||||
|
||||
void hoist_exists(expr_ref& fml, app_ref_vector& vars);
|
||||
|
||||
void mk_exists(unsigned num_vars, app* const* vars, expr_ref& fml);
|
||||
|
||||
void get_nnf(expr_ref& fml, i_expr_pred& pred, i_nnf_atom& mk_atom, atom_set& pos, atom_set& neg);
|
||||
|
||||
class simplify_rewriter_cfg : public default_rewriter_cfg {
|
||||
class impl;
|
||||
impl* imp;
|
||||
public:
|
||||
simplify_rewriter_cfg(ast_manager& m);
|
||||
|
||||
~simplify_rewriter_cfg();
|
||||
|
||||
bool reduce_quantifier(
|
||||
quantifier * old_q,
|
||||
expr * new_body,
|
||||
expr * const * new_patterns,
|
||||
expr * const * new_no_patterns,
|
||||
expr_ref & result,
|
||||
proof_ref & result_pr);
|
||||
|
||||
bool pre_visit(expr* e);
|
||||
|
||||
};
|
||||
|
||||
class simplify_rewriter_star : public rewriter_tpl<simplify_rewriter_cfg> {
|
||||
simplify_rewriter_cfg m_cfg;
|
||||
public:
|
||||
simplify_rewriter_star(ast_manager& m):
|
||||
rewriter_tpl<simplify_rewriter_cfg>(m, false, m_cfg),
|
||||
m_cfg(m) {}
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
||||
2574
src/qe/qe_arith_plugin.cpp
Normal file
2574
src/qe/qe_arith_plugin.cpp
Normal file
File diff suppressed because it is too large
Load diff
299
src/qe/qe_array_plugin.cpp
Normal file
299
src/qe/qe_array_plugin.cpp
Normal file
|
|
@ -0,0 +1,299 @@
|
|||
|
||||
#include "qe.h"
|
||||
#include "array_decl_plugin.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "ast_pp.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
|
||||
namespace qe {
|
||||
// ---------------------
|
||||
// arrays
|
||||
|
||||
class array_plugin : public qe_solver_plugin {
|
||||
|
||||
expr_safe_replace m_replace;
|
||||
|
||||
public:
|
||||
|
||||
array_plugin(i_solver_context& ctx, ast_manager& m) :
|
||||
qe_solver_plugin(m, m.mk_family_id("array"), ctx),
|
||||
m_replace(m)
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~array_plugin() {}
|
||||
|
||||
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
virtual bool get_num_branches( contains_app& x, expr* fml, rational& num_branches) {
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
|
||||
virtual bool solve(conj_enum& conjs, expr* fml) {
|
||||
|
||||
conj_enum::iterator it = conjs.begin(), end = conjs.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
if (m.is_eq(e) && solve_eq(to_app(e), fml)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
expr_ref_vector eqs(m);
|
||||
conjs.extract_equalities(eqs);
|
||||
for (unsigned i = 0; i < eqs.size(); ++i) {
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(eqs[i].get(), m) << "\n";);
|
||||
expr* e = eqs[i].get();
|
||||
if (solve_eq_zero(e, fml)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual bool is_uninterpreted(app* f) {
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
private:
|
||||
|
||||
bool solve_eq(app* eq, expr* fml) {
|
||||
SASSERT(m.is_eq(eq));
|
||||
expr* arg1 = eq->get_arg(0);
|
||||
expr* arg2 = eq->get_arg(1);
|
||||
return solve_eq(arg1, arg2, fml) || solve_eq(arg2, arg1, fml);
|
||||
}
|
||||
|
||||
bool solve_eq_zero(expr* e, expr* fml) {
|
||||
arith_util arith(m);
|
||||
if (arith.is_add(e)) {
|
||||
app* a = to_app(e);
|
||||
expr* e1, *e2;
|
||||
unsigned sz = a->get_num_args();
|
||||
expr_ref_vector args(m);
|
||||
expr_ref lhs(m), rhs(m);
|
||||
rational r;
|
||||
args.append(sz, a->get_args());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref save(m);
|
||||
save = lhs = args[i].get();
|
||||
args[i] = arith.mk_numeral(rational(0), m.get_sort(lhs));
|
||||
rhs = arith.mk_uminus(arith.mk_add(args.size(), args.c_ptr()));
|
||||
if (arith.is_mul(lhs, e1, e2) &&
|
||||
arith.is_numeral(e1, r) &&
|
||||
r.is_minus_one()) {
|
||||
lhs = to_app(e2);
|
||||
rhs = arith.mk_uminus(rhs);
|
||||
}
|
||||
if (solve_eq(lhs, rhs, fml)) {
|
||||
return true;
|
||||
}
|
||||
args[i] = save;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool solve_eq(expr* lhs, expr* rhs, expr* fml) {
|
||||
|
||||
if (!is_app(lhs)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
TRACE("qe_verbose",
|
||||
tout << mk_pp(lhs, m) <<
|
||||
" == " << mk_pp(rhs, m) << "\n";);
|
||||
expr_ref tmp(m);
|
||||
app* a = to_app(lhs);
|
||||
//
|
||||
// A = t, A not in t.
|
||||
//
|
||||
unsigned idx = 0;
|
||||
if (m_ctx.is_var(a, idx) &&
|
||||
!m_ctx.contains(idx)(rhs)) {
|
||||
expr_ref result(fml, m);
|
||||
m_replace.apply_substitution(a, rhs, result);
|
||||
m_ctx.elim_var(idx, result, rhs);
|
||||
return true;
|
||||
}
|
||||
if (solve_store(a, rhs, fml)) {
|
||||
return true;
|
||||
}
|
||||
if (solve_select(a, rhs, fml)) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solve_select2(app* lhs, expr* rhs, expr* fml) {
|
||||
//
|
||||
// (select (select A i) j) = t, A not in i, j, t
|
||||
// A |-> (store B' j (store B i t)), where B, B' are fresh.
|
||||
//
|
||||
// TBD
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solve_select(app* lhs, expr* rhs, expr* fml) {
|
||||
//
|
||||
// (select A i) = t, A not in i, v, t
|
||||
// A |-> (store B i t), where B is fresh.
|
||||
//
|
||||
unsigned idx = 0;
|
||||
vector<ptr_vector<expr> > args;
|
||||
if (is_select(lhs, idx, rhs, args) && args.size() == 1) {
|
||||
contains_app& contains_A = m_ctx.contains(idx);
|
||||
app* A = contains_A.x();
|
||||
app_ref B(m);
|
||||
expr_ref store_B_i_t(m);
|
||||
|
||||
unsigned num_args = args[0].size();
|
||||
B = m.mk_fresh_const("B", m.get_sort(A));
|
||||
ptr_buffer<expr> args2;
|
||||
args2.push_back(B);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
args2.push_back(args[0][i]);
|
||||
}
|
||||
args2.push_back(rhs);
|
||||
|
||||
store_B_i_t = m.mk_app(m_fid, OP_STORE, args2.size(), args2.c_ptr());
|
||||
|
||||
TRACE("qe",
|
||||
tout << "fml: " << mk_pp(fml, m) << "\n";
|
||||
tout << "solved form: " << mk_pp(store_B_i_t, m) << "\n";
|
||||
tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
|
||||
);
|
||||
expr_ref result(fml, m);
|
||||
m_replace.apply_substitution(A, store_B_i_t, result);
|
||||
m_ctx.add_var(B);
|
||||
m_ctx.elim_var(idx, result, store_B_i_t);
|
||||
return true;
|
||||
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool is_array_app_of(app* a, unsigned& idx, expr* t, decl_kind k) {
|
||||
if (!is_app_of(a, m_fid, k)) {
|
||||
return false;
|
||||
}
|
||||
expr* v = a->get_arg(0);
|
||||
if (!m_ctx.is_var(v, idx)) {
|
||||
return false;
|
||||
}
|
||||
contains_app& contains_v = m_ctx.contains(idx);
|
||||
|
||||
for (unsigned i = 1; i < a->get_num_args(); ++i) {
|
||||
if (contains_v(a->get_arg(i))) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
if (contains_v(t)) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool solve_store(app* lhs, expr* rhs, expr* fml) {
|
||||
//
|
||||
// store(store(A, j, u), i, v) = t, A not in i, j, u, v, t
|
||||
// ->
|
||||
// A |-> store(store(t, i, w), j, w') where w, w' are fresh.
|
||||
// t[i] = v
|
||||
// store(t, i, v)[j] = u
|
||||
//
|
||||
unsigned idx = 0;
|
||||
vector<ptr_vector<expr> > args;
|
||||
if (is_store_update(lhs, idx, rhs, args)) {
|
||||
contains_app& contains_A = m_ctx.contains(idx);
|
||||
app* A = contains_A.x();
|
||||
app_ref w(m);
|
||||
|
||||
expr_ref store_t(rhs, m), store_T(rhs, m), select_t(m);
|
||||
ptr_vector<expr> args2;
|
||||
for (unsigned i = args.size(); i > 0; ) {
|
||||
--i;
|
||||
args2.reset();
|
||||
w = m.mk_fresh_const("w", m.get_sort(args[i].back()));
|
||||
args2.push_back(store_T);
|
||||
args2.append(args[i]);
|
||||
|
||||
select_t = m.mk_app(m_fid, OP_SELECT, args2.size()-1, args2.c_ptr());
|
||||
fml = m.mk_and(fml, m.mk_eq(select_t, args2.back()));
|
||||
store_T = m.mk_app(m_fid, OP_STORE, args2.size(), args2.c_ptr());
|
||||
|
||||
args2[0] = store_t;
|
||||
args2.back() = w;
|
||||
store_t = m.mk_app(m_fid, OP_STORE, args2.size(), args2.c_ptr());
|
||||
|
||||
m_ctx.add_var(w);
|
||||
}
|
||||
|
||||
TRACE("qe",
|
||||
tout << "Variable: " << mk_pp(A, m) << "\n";
|
||||
tout << "fml: " << mk_pp(fml, m) << "\n";
|
||||
tout << "solved form: " << mk_pp(store_t, m) << "\n";
|
||||
tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
|
||||
);
|
||||
expr_ref result(fml, m);
|
||||
m_replace.apply_substitution(A, store_t, result);
|
||||
m_ctx.elim_var(idx, result, store_t);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool is_array_app_of(app* a, unsigned& idx, expr* t, decl_kind k, vector<ptr_vector<expr> >& args) {
|
||||
if (m_ctx.is_var(a, idx)) {
|
||||
contains_app& contains_v = m_ctx.contains(idx);
|
||||
if (args.empty() || contains_v(t)) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
for (unsigned j = 0; j < args[i].size(); ++j) {
|
||||
if (contains_v(args[i][j])) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
if (!is_app_of(a, m_fid, k)) {
|
||||
return false;
|
||||
}
|
||||
args.push_back(ptr_vector<expr>());
|
||||
for (unsigned i = 1; i < a->get_num_args(); ++i) {
|
||||
args.back().push_back(a->get_arg(i));
|
||||
}
|
||||
if (!is_app(a->get_arg(0))) {
|
||||
return false;
|
||||
}
|
||||
return is_array_app_of(to_app(a->get_arg(0)), idx, t, k, args);
|
||||
}
|
||||
|
||||
bool is_store_update(app* a, unsigned& idx, expr* t, vector<ptr_vector<expr> >& args) {
|
||||
return is_array_app_of(a, idx, t, OP_STORE, args);
|
||||
}
|
||||
|
||||
bool is_select(app* a, unsigned& idx, expr* t, vector<ptr_vector<expr> >& args) {
|
||||
return is_array_app_of(a, idx, t, OP_SELECT, args);
|
||||
}
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_array_plugin(i_solver_context& ctx) {
|
||||
return alloc(array_plugin, ctx, ctx.get_manager());
|
||||
}
|
||||
|
||||
}
|
||||
180
src/qe/qe_bool_plugin.cpp
Normal file
180
src/qe/qe_bool_plugin.cpp
Normal file
|
|
@ -0,0 +1,180 @@
|
|||
/*++
|
||||
Copyright (c) 2010 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_bool_plugin.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Eliminate Boolean variable from formula
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2010-02-19
|
||||
|
||||
Revision History:
|
||||
|
||||
Notes:
|
||||
|
||||
The procedure is a bit naive.
|
||||
Consider a co-factoring approach that eliminates all Boolean
|
||||
variables in scope in one shot, similar to what we do with
|
||||
BDDs.
|
||||
|
||||
--*/
|
||||
|
||||
#include "qe.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "ast_pp.h"
|
||||
#include "model_evaluator.h"
|
||||
|
||||
|
||||
namespace qe {
|
||||
class bool_plugin : public qe_solver_plugin {
|
||||
expr_safe_replace m_replace;
|
||||
public:
|
||||
bool_plugin(i_solver_context& ctx, ast_manager& m):
|
||||
qe_solver_plugin(m, m.get_basic_family_id(), ctx),
|
||||
m_replace(m)
|
||||
{}
|
||||
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
|
||||
SASSERT(vl.is_zero() || vl.is_one());
|
||||
}
|
||||
|
||||
virtual bool get_num_branches(contains_app& x, expr* fml, rational& nb) {
|
||||
nb = rational(2);
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
|
||||
SASSERT(vl.is_one() || vl.is_zero());
|
||||
expr* tf = (vl.is_one())?m.mk_true():m.mk_false();
|
||||
m_replace.apply_substitution(x.x(), tf, fml);
|
||||
if (def) {
|
||||
*def = tf;
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool project(contains_app& x, model_ref& model, expr_ref& fml) {
|
||||
model_evaluator model_eval(*model);
|
||||
expr_ref val_x(m);
|
||||
rational val;
|
||||
model_eval(x.x(), val_x);
|
||||
CTRACE("qe", (!m.is_true(val_x) && !m.is_false(val_x)),
|
||||
tout << "Boolean is a don't care: " << mk_pp(x.x(), m) << "\n";);
|
||||
val = m.is_true(val_x)?rational::one():rational::zero();
|
||||
subst(x, val, fml, 0);
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual unsigned get_weight(contains_app& contains_x, expr* fml) {
|
||||
app* x = contains_x.x();
|
||||
bool p = m_ctx.pos_atoms().contains(x);
|
||||
bool n = m_ctx.neg_atoms().contains(x);
|
||||
if (p && n) {
|
||||
return 3;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual bool solve(conj_enum& conjs,expr* fml) {
|
||||
return
|
||||
solve_units(conjs, fml) ||
|
||||
solve_polarized(fml);
|
||||
}
|
||||
|
||||
virtual bool is_uninterpreted(app* a) {
|
||||
return false;
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
bool solve_units(conj_enum& conjs, expr* _fml) {
|
||||
expr_ref fml(_fml, m);
|
||||
conj_enum::iterator it = conjs.begin(), end = conjs.end();
|
||||
unsigned idx;
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
if (!is_app(e)) {
|
||||
continue;
|
||||
}
|
||||
app* a = to_app(e);
|
||||
expr* e1;
|
||||
if (m_ctx.is_var(a, idx)) {
|
||||
m_replace.apply_substitution(a, m.mk_true(), fml);
|
||||
m_ctx.elim_var(idx, fml, m.mk_true());
|
||||
return true;
|
||||
}
|
||||
else if (m.is_not(e, e1) && m_ctx.is_var(e1, idx)) {
|
||||
m_replace.apply_substitution(to_app(e1), m.mk_false(), fml);
|
||||
m_ctx.elim_var(idx, fml, m.mk_false());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solve_polarized(expr* _fml) {
|
||||
unsigned num_vars = m_ctx.get_num_vars();
|
||||
expr_ref fml(_fml, m), def(m);
|
||||
for (unsigned i = 0; i < num_vars; ++i) {
|
||||
if (m.is_bool(m_ctx.get_var(i)) &&
|
||||
solve_polarized(m_ctx.contains(i), fml, def)) {
|
||||
m_ctx.elim_var(i, fml, def);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solve_polarized( contains_app& contains_x, expr_ref& fml, expr_ref& def) {
|
||||
app* x = contains_x.x();
|
||||
bool p = m_ctx.pos_atoms().contains(x);
|
||||
bool n = m_ctx.neg_atoms().contains(x);
|
||||
TRACE("quant_elim", tout << mk_pp(x, m) << " " << mk_pp(fml, m) << "\n";);
|
||||
if (p && n) {
|
||||
return false;
|
||||
}
|
||||
else if (p && !n) {
|
||||
atom_set::iterator it = m_ctx.pos_atoms().begin(), end = m_ctx.pos_atoms().end();
|
||||
for (; it != end; ++it) {
|
||||
if (x != *it && contains_x(*it)) return false;
|
||||
}
|
||||
it = m_ctx.neg_atoms().begin(), end = m_ctx.neg_atoms().end();
|
||||
for (; it != end; ++it) {
|
||||
if (contains_x(*it)) return false;
|
||||
}
|
||||
// only occurrences of 'x' must be in positive atoms
|
||||
def = m.mk_true();
|
||||
m_replace.apply_substitution(x, def, fml);
|
||||
return true;
|
||||
}
|
||||
else if (!p && n) {
|
||||
atom_set::iterator it = m_ctx.pos_atoms().begin(), end = m_ctx.pos_atoms().end();
|
||||
for (; it != end; ++it) {
|
||||
if (contains_x(*it)) return false;
|
||||
}
|
||||
it = m_ctx.neg_atoms().begin(), end = m_ctx.neg_atoms().end();
|
||||
for (; it != end; ++it) {
|
||||
if (x != *it && contains_x(*it)) return false;
|
||||
}
|
||||
def = m.mk_false();
|
||||
m_replace.apply_substitution(x, def, fml);
|
||||
return true;
|
||||
}
|
||||
else if (contains_x(fml)) {
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
def = m.mk_false();
|
||||
return true;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_bool_plugin(i_solver_context& ctx) {
|
||||
return alloc(bool_plugin, ctx, ctx.get_manager());
|
||||
}
|
||||
}
|
||||
97
src/qe/qe_bv_plugin.cpp
Normal file
97
src/qe/qe_bv_plugin.cpp
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
/*++
|
||||
Copyright (c) 2010 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bv_plugin.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Eliminate Bit-vector variable from formula
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2010-02-19
|
||||
|
||||
Revision History:
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "qe.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
#include "model_evaluator.h"
|
||||
|
||||
namespace qe {
|
||||
|
||||
class bv_plugin : public qe_solver_plugin {
|
||||
expr_safe_replace m_replace;
|
||||
bv_util m_bv;
|
||||
public:
|
||||
bv_plugin(i_solver_context& ctx, ast_manager& m):
|
||||
qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
|
||||
m_replace(m),
|
||||
m_bv(m)
|
||||
{}
|
||||
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
|
||||
}
|
||||
|
||||
virtual bool get_num_branches(contains_app& x, expr* fml, rational& nb) {
|
||||
unsigned sz = m_bv.get_bv_size(x.x());
|
||||
nb = power(rational(2), sz);
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
|
||||
app_ref c(m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x())), m);
|
||||
m_replace.apply_substitution(x.x(), c, fml);
|
||||
if (def) {
|
||||
*def = m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x()));
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool project(contains_app& x, model_ref& model, expr_ref& fml) {
|
||||
model_evaluator model_eval(*model);
|
||||
expr_ref val_x(m);
|
||||
rational val(0);
|
||||
unsigned bv_size;
|
||||
model_eval(x.x(), val_x);
|
||||
m_bv.is_numeral(val_x, val, bv_size);
|
||||
subst(x, val, fml, 0);
|
||||
return true;
|
||||
}
|
||||
|
||||
virtual unsigned get_weight(contains_app& contains_x, expr* fml) {
|
||||
return 2;
|
||||
}
|
||||
|
||||
bool solve(conj_enum& conjs, expr* fml) { return false; }
|
||||
|
||||
virtual bool is_uninterpreted(app* f) {
|
||||
switch(f->get_decl_kind()) {
|
||||
case OP_BSDIV0:
|
||||
case OP_BUDIV0:
|
||||
case OP_BSREM0:
|
||||
case OP_BUREM0:
|
||||
case OP_BSMOD0:
|
||||
case OP_BSDIV_I:
|
||||
case OP_BUDIV_I:
|
||||
case OP_BSREM_I:
|
||||
case OP_BUREM_I:
|
||||
case OP_BSMOD_I:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_bv_plugin(i_solver_context& ctx) {
|
||||
return alloc(bv_plugin, ctx, ctx.get_manager());
|
||||
}
|
||||
}
|
||||
64
src/qe/qe_cmd.cpp
Normal file
64
src/qe/qe_cmd.cpp
Normal file
|
|
@ -0,0 +1,64 @@
|
|||
#include "qe_cmd.h"
|
||||
#include "qe.h"
|
||||
#include "cmd_context.h"
|
||||
#include "parametric_cmd.h"
|
||||
|
||||
class qe_cmd : public parametric_cmd {
|
||||
expr * m_target;
|
||||
public:
|
||||
qe_cmd(char const* name = "elim-quantifiers"):parametric_cmd(name) {}
|
||||
|
||||
virtual char const * get_usage() const { return "<term> (<keyword> <value>)*"; }
|
||||
|
||||
virtual char const * get_main_descr() const {
|
||||
return "apply quantifier elimination to the supplied expression";
|
||||
}
|
||||
|
||||
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
|
||||
insert_timeout(p);
|
||||
p.insert("print", CPK_BOOL, "(default: true) print the simplified term.");
|
||||
p.insert("print_statistics", CPK_BOOL, "(default: false) print statistics.");
|
||||
}
|
||||
|
||||
virtual ~qe_cmd() {
|
||||
}
|
||||
|
||||
virtual void prepare(cmd_context & ctx) {
|
||||
parametric_cmd::prepare(ctx);
|
||||
m_target = 0;
|
||||
}
|
||||
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
if (m_target == 0) return CPK_EXPR;
|
||||
return parametric_cmd::next_arg_kind(ctx);
|
||||
}
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
|
||||
m_target = arg;
|
||||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
smt_params par;
|
||||
proof_ref pr(ctx.m());
|
||||
qe::expr_quant_elim_star1 qe(ctx.m(), par);
|
||||
expr_ref result(ctx.m());
|
||||
|
||||
qe(m_target, result, pr);
|
||||
|
||||
if (m_params.get_bool("print", true)) {
|
||||
ctx.display(ctx.regular_stream(), result);
|
||||
ctx.regular_stream() << std::endl;
|
||||
}
|
||||
if (m_params.get_bool("print_statistics", false)) {
|
||||
statistics st;
|
||||
qe.collect_statistics(st);
|
||||
st.display(ctx.regular_stream());
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
void install_qe_cmd(cmd_context & ctx, char const * cmd_name) {
|
||||
ctx.insert(alloc(qe_cmd, cmd_name));
|
||||
}
|
||||
|
||||
25
src/qe/qe_cmd.h
Normal file
25
src/qe/qe_cmd.h
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_cmd.h
|
||||
|
||||
Abstract:
|
||||
SMT2 front-end 'qe' command.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2011-01-11
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _QE_CMD_H_
|
||||
#define _QE_CMD_H_
|
||||
|
||||
class cmd_context;
|
||||
|
||||
void install_qe_cmd(cmd_context & ctx, char const * cmd_name = "elim-quantifiers");
|
||||
|
||||
#endif
|
||||
867
src/qe/qe_datatype_plugin.cpp
Normal file
867
src/qe/qe_datatype_plugin.cpp
Normal file
|
|
@ -0,0 +1,867 @@
|
|||
// ---------------------
|
||||
// datatypes
|
||||
// Quantifier elimination routine for recursive data-types.
|
||||
//
|
||||
|
||||
|
||||
//
|
||||
// reduce implementation is modeled after Hodges:
|
||||
// subst implementation is using QE "for dummies".
|
||||
|
||||
// for dummies:
|
||||
// -----------
|
||||
//
|
||||
// Step 1. ensure x is recognized.
|
||||
//
|
||||
// exists x . phi[x] -> \/_i exists x. R_C(x) & phi[x]
|
||||
//
|
||||
// Step 2. non-recursive data-types
|
||||
//
|
||||
// exists x . R_C(x) & phi[x] -> exists y . phi[C(y)]
|
||||
//
|
||||
// Step 2. recursive data-types, eliminate selectors.
|
||||
//
|
||||
// exists x . R_C(x) & phi[x] -> exists y . phi[C(y)], x occurs with sel^C_i(x)
|
||||
//
|
||||
// Step 3. (recursive data-types)
|
||||
//
|
||||
// Solve equations
|
||||
// . C[t] = C[s] -> t = s
|
||||
// . C[x,t] = y -> x = s1(y) /\ t = s2(y) /\ R_C(y)
|
||||
// . C[x,t] != y -> can remain
|
||||
//
|
||||
// The remaining formula is in NNF where occurrences of 'x' are of the form
|
||||
// x = t_i or t[x] != s_j
|
||||
//
|
||||
// The last normalization step is:
|
||||
//
|
||||
// exists x . R_C(x) & phi[x = t_i, t[x] != s_j]
|
||||
//
|
||||
// -> \/_i R_C(t_i) & phi[t_i/x] \/ phi[false, true]
|
||||
//
|
||||
// Justification:
|
||||
// - We will asume that each of t_i, s_j are constructor terms.
|
||||
// - We can assume that x \notin t_i, x \notin s_j, or otherwise use simplification.
|
||||
// - We can assume that x occurs only in equalities or disequalities, or the recognizer, since
|
||||
// otherwise, we could simplify equalities, or QE does not apply.
|
||||
// - either x = t_i for some positive t_i, or we create
|
||||
// diag = C(t_1, ..., C(t_n, .. C(s_1, .. , C(s_m))))
|
||||
// and x is different from each t_i, s_j.
|
||||
//
|
||||
|
||||
//
|
||||
// reduce:
|
||||
// --------
|
||||
// reduce set of literals containing x. The elimination procedure follows an adaptation of
|
||||
// the proof (with corrections) in Hodges (shorter model theory).
|
||||
//
|
||||
// . x = t - (x \notin t) x is eliminated immediately.
|
||||
//
|
||||
// . x != t1, ..., x != t_n - (x \notin t_i) are collected into distrinct_terms.
|
||||
//
|
||||
// . recognizer(x) - is stored as pos_recognizer.
|
||||
//
|
||||
// . !recognizer(x) - is stored into neg_recognizers.
|
||||
//
|
||||
// . L[constructor(..,x,..)] -
|
||||
// We could assume pre-processing introduces auxiliary
|
||||
// variable y, Is_constructor(y), accessor_j(y) = arg_j.
|
||||
// But we apply the following hack: re-introduce x' into vars,
|
||||
// but also the variable y and the reduced formula.
|
||||
//
|
||||
// . L[accessor_i(x)] - if pos_recognizer(x) matches accessor,
|
||||
// or if complement of neg_recognizers match accessor, then
|
||||
// introduce x_1, .., x_n corresponding to accessor_i(x).
|
||||
//
|
||||
// The only way x is not in the scope of a data-type method is if it is in
|
||||
// an equality or dis-equality of the form:
|
||||
//
|
||||
// . x (!)= acc_1(acc_2(..(acc_i(x)..) - would be false (true) if recognizer(..)
|
||||
// is declared for each sub-term.
|
||||
//
|
||||
//
|
||||
// - otherwise, each x should be in the scope of an accessor.
|
||||
//
|
||||
// Normalized literal elimination:
|
||||
//
|
||||
// . exists x . Lits[accessor_i(x)] & Is_constructor(x)
|
||||
// ->
|
||||
// exists x_1, .., x_n . Lits[x_1, .., x_n] for each accessor_i(x).
|
||||
//
|
||||
|
||||
//
|
||||
// maintain set of equations and disequations with x.
|
||||
//
|
||||
|
||||
#include "qe.h"
|
||||
#include "datatype_decl_plugin.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "obj_pair_hashtable.h"
|
||||
#include "for_each_expr.h"
|
||||
#include "ast_pp.h"
|
||||
#include "ast_ll_pp.h"
|
||||
|
||||
namespace qe {
|
||||
|
||||
class datatype_atoms {
|
||||
ast_manager& m;
|
||||
app_ref_vector m_recognizers;
|
||||
expr_ref_vector m_eqs;
|
||||
expr_ref_vector m_neqs;
|
||||
app_ref_vector m_eq_atoms;
|
||||
app_ref_vector m_neq_atoms;
|
||||
app_ref_vector m_unsat_atoms;
|
||||
expr_ref_vector m_eq_conds;
|
||||
ast_mark m_mark;
|
||||
datatype_util m_util;
|
||||
public:
|
||||
datatype_atoms(ast_manager& m) :
|
||||
m(m),
|
||||
m_recognizers(m),
|
||||
m_eqs(m),
|
||||
m_neqs(m),
|
||||
m_eq_atoms(m), m_neq_atoms(m), m_unsat_atoms(m), m_eq_conds(m),
|
||||
m_util(m) {}
|
||||
|
||||
bool add_atom(contains_app& contains_x, bool is_pos, app* a) {
|
||||
app* x = contains_x.x();
|
||||
SASSERT(contains_x(a));
|
||||
if (m_mark.is_marked(a)) {
|
||||
return true;
|
||||
}
|
||||
m_mark.mark(a, true);
|
||||
func_decl* f = a->get_decl();
|
||||
if (m_util.is_recognizer(f) && a->get_arg(0) == x) {
|
||||
m_recognizers.push_back(a);
|
||||
TRACE("qe", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
|
||||
return true;
|
||||
}
|
||||
if (!m.is_eq(a)) {
|
||||
return false;
|
||||
}
|
||||
if (add_eq(contains_x, is_pos, a->get_arg(0), a->get_arg(1))) {
|
||||
add_atom(a, is_pos);
|
||||
return true;
|
||||
}
|
||||
if (add_eq(contains_x, is_pos, a->get_arg(1), a->get_arg(0))) {
|
||||
add_atom(a, is_pos);
|
||||
return true;
|
||||
}
|
||||
if (add_unsat_eq(contains_x, a, a->get_arg(0), a->get_arg(1))) {
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
unsigned num_eqs() { return m_eqs.size(); }
|
||||
expr* eq(unsigned i) { return m_eqs[i].get(); }
|
||||
expr* eq_cond(unsigned i) { return m_eq_conds[i].get(); }
|
||||
app* eq_atom(unsigned i) { return m_eq_atoms[i].get(); }
|
||||
|
||||
unsigned num_neqs() { return m_neq_atoms.size(); }
|
||||
app* neq_atom(unsigned i) { return m_neq_atoms[i].get(); }
|
||||
|
||||
unsigned num_neq_terms() const { return m_neqs.size(); }
|
||||
expr* neq_term(unsigned i) const { return m_neqs[i]; }
|
||||
expr* const* neq_terms() const { return m_neqs.c_ptr(); }
|
||||
|
||||
unsigned num_recognizers() { return m_recognizers.size(); }
|
||||
app* recognizer(unsigned i) { return m_recognizers[i].get(); }
|
||||
|
||||
unsigned num_unsat() { return m_unsat_atoms.size(); }
|
||||
app* unsat_atom(unsigned i) { return m_unsat_atoms[i].get(); }
|
||||
|
||||
private:
|
||||
|
||||
//
|
||||
// perform occurs check on equality.
|
||||
//
|
||||
bool add_unsat_eq(contains_app& contains_x, app* atom, expr* a, expr* b) {
|
||||
app* x = contains_x.x();
|
||||
if (x != a) {
|
||||
std::swap(a, b);
|
||||
}
|
||||
if (x != a) {
|
||||
return false;
|
||||
}
|
||||
if (!contains_x(b)) {
|
||||
return false;
|
||||
}
|
||||
ptr_vector<expr> todo;
|
||||
ast_mark mark;
|
||||
todo.push_back(b);
|
||||
while (!todo.empty()) {
|
||||
b = todo.back();
|
||||
todo.pop_back();
|
||||
if (mark.is_marked(b)) {
|
||||
continue;
|
||||
}
|
||||
mark.mark(b, true);
|
||||
if (!is_app(b)) {
|
||||
continue;
|
||||
}
|
||||
if (b == x) {
|
||||
m_unsat_atoms.push_back(atom);
|
||||
return true;
|
||||
}
|
||||
app* b_app = to_app(b);
|
||||
if (!m_util.is_constructor(b_app)) {
|
||||
continue;
|
||||
}
|
||||
for (unsigned i = 0; i < b_app->get_num_args(); ++i) {
|
||||
todo.push_back(b_app->get_arg(i));
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void add_atom(app* a, bool is_pos) {
|
||||
TRACE("qe", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
|
||||
if (is_pos) {
|
||||
m_eq_atoms.push_back(a);
|
||||
}
|
||||
else {
|
||||
m_neq_atoms.push_back(a);
|
||||
}
|
||||
}
|
||||
|
||||
bool add_eq(contains_app& contains_x, bool is_pos, expr* a, expr* b) {
|
||||
if (contains_x(b)) {
|
||||
return false;
|
||||
}
|
||||
if (is_pos) {
|
||||
return solve_eq(contains_x, a, b, m.mk_true());
|
||||
}
|
||||
else {
|
||||
return solve_diseq(contains_x, a, b);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool solve_eq(contains_app& contains_x, expr* _a, expr* b, expr* cond0) {
|
||||
SASSERT(contains_x(_a));
|
||||
SASSERT(!contains_x(b));
|
||||
app* x = contains_x.x();
|
||||
if (!is_app(_a)) {
|
||||
return false;
|
||||
}
|
||||
app* a = to_app(_a);
|
||||
if (x == a) {
|
||||
m_eqs.push_back(b);
|
||||
m_eq_conds.push_back(cond0);
|
||||
return true;
|
||||
}
|
||||
if (!m_util.is_constructor(a)) {
|
||||
return false;
|
||||
}
|
||||
func_decl* c = a->get_decl();
|
||||
func_decl* r = m_util.get_constructor_recognizer(c);
|
||||
ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c);
|
||||
SASSERT(acc.size() == a->get_num_args());
|
||||
//
|
||||
// It suffices to solve just the first available equality.
|
||||
// The others are determined by the first.
|
||||
//
|
||||
expr_ref cond(m.mk_and(m.mk_app(r, b), cond0), m);
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
expr* l = a->get_arg(i);
|
||||
if (contains_x(l)) {
|
||||
expr_ref r(m.mk_app(acc[i], b), m);
|
||||
if (solve_eq(contains_x, l, r, cond)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
//
|
||||
// check that some occurrence of 'x' is in a constructor sequence.
|
||||
//
|
||||
bool solve_diseq(contains_app& contains_x, expr* a0, expr* b) {
|
||||
SASSERT(!contains_x(b));
|
||||
SASSERT(contains_x(a0));
|
||||
app* x = contains_x.x();
|
||||
ptr_vector<expr> todo;
|
||||
ast_mark mark;
|
||||
todo.push_back(a0);
|
||||
while (!todo.empty()) {
|
||||
a0 = todo.back();
|
||||
todo.pop_back();
|
||||
if (mark.is_marked(a0)) {
|
||||
continue;
|
||||
}
|
||||
mark.mark(a0, true);
|
||||
if (!is_app(a0)) {
|
||||
continue;
|
||||
}
|
||||
app* a = to_app(a0);
|
||||
if (a == x) {
|
||||
m_neqs.push_back(b);
|
||||
return true;
|
||||
}
|
||||
if (!m_util.is_constructor(a)) {
|
||||
continue;
|
||||
}
|
||||
for (unsigned i = 0; i < a->get_num_args(); ++i) {
|
||||
todo.push_back(a->get_arg(i));
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
//
|
||||
// eliminate foreign variable under datatype functions (constructors).
|
||||
// (= C(x,y) t) -> (R_C(t) && x = s1(t) && x = s2(t))
|
||||
//
|
||||
|
||||
class lift_foreign_vars : public map_proc {
|
||||
ast_manager& m;
|
||||
bool m_change;
|
||||
datatype_util& m_util;
|
||||
i_solver_context& m_ctx;
|
||||
public:
|
||||
lift_foreign_vars(ast_manager& m, datatype_util& util, i_solver_context& ctx):
|
||||
map_proc(m), m(m), m_change(false), m_util(util), m_ctx(ctx) {}
|
||||
|
||||
bool lift(expr_ref& fml) {
|
||||
m_change = false;
|
||||
for_each_expr(*this, fml.get());
|
||||
if (m_change) {
|
||||
fml = get_expr(fml.get());
|
||||
TRACE("qe", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
|
||||
}
|
||||
return m_change;
|
||||
}
|
||||
|
||||
void operator()(var* v) {
|
||||
visit(v);
|
||||
}
|
||||
|
||||
void operator()(quantifier* q) {
|
||||
visit(q);
|
||||
}
|
||||
|
||||
void operator()(app* a) {
|
||||
expr* l, *r;
|
||||
if (m.is_eq(a, l, r)) {
|
||||
if (reduce_eq(a, l, r)) {
|
||||
m_change = true;
|
||||
return;
|
||||
}
|
||||
if (reduce_eq(a, r, l)) {
|
||||
m_change = true;
|
||||
return;
|
||||
}
|
||||
}
|
||||
reconstruct(a);
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
bool reduce_eq(app* a, expr* _l, expr* r) {
|
||||
if (!is_app(_l)) {
|
||||
return false;
|
||||
}
|
||||
app* l = to_app(_l);
|
||||
if (!m_util.is_constructor(l)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if (!contains_foreign(l)) {
|
||||
return false;
|
||||
}
|
||||
func_decl* c = l->get_decl();
|
||||
ptr_vector<func_decl> const& acc = *m_util.get_constructor_accessors(c);
|
||||
func_decl* rec = m_util.get_constructor_recognizer(c);
|
||||
expr_ref_vector conj(m);
|
||||
conj.push_back(m.mk_app(rec, r));
|
||||
for (unsigned i = 0; i < acc.size(); ++i) {
|
||||
expr* r_i = m.mk_app(acc[i], r);
|
||||
expr* l_i = l->get_arg(i);
|
||||
conj.push_back(m.mk_eq(l_i, r_i));
|
||||
}
|
||||
expr* e = m.mk_and(conj.size(), conj.c_ptr());
|
||||
m_map.insert(a, e, 0);
|
||||
TRACE("qe", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool contains_foreign(app* a) {
|
||||
unsigned num_vars = m_ctx.get_num_vars();
|
||||
for (unsigned i = 0; i < num_vars; ++i) {
|
||||
contains_app& v = m_ctx.contains(i);
|
||||
sort* s = v.x()->get_decl()->get_range();
|
||||
|
||||
//
|
||||
// data-type contains arithmetical term or bit-vector.
|
||||
//
|
||||
if (!m_util.is_datatype(s) &&
|
||||
!m.is_bool(s) &&
|
||||
v(a)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
class datatype_plugin : public qe_solver_plugin {
|
||||
typedef std::pair<app*,ptr_vector<app> > subst_clos;
|
||||
typedef obj_pair_map<app, expr, datatype_atoms*> eqs_cache;
|
||||
typedef obj_pair_map<app, func_decl, subst_clos*> subst_map;
|
||||
|
||||
datatype_util m_datatype_util;
|
||||
expr_safe_replace m_replace;
|
||||
eqs_cache m_eqs_cache;
|
||||
subst_map m_subst_cache;
|
||||
ast_ref_vector m_trail;
|
||||
|
||||
public:
|
||||
datatype_plugin(i_solver_context& ctx, ast_manager& m) :
|
||||
qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
|
||||
m_datatype_util(m),
|
||||
m_replace(m),
|
||||
m_trail(m)
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~datatype_plugin() {
|
||||
{
|
||||
eqs_cache::iterator it = m_eqs_cache.begin(), end = m_eqs_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
}
|
||||
{
|
||||
subst_map::iterator it = m_subst_cache.begin(), end = m_subst_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
virtual bool get_num_branches( contains_app& x, expr* fml, rational& num_branches) {
|
||||
sort* s = x.x()->get_decl()->get_range();
|
||||
SASSERT(m_datatype_util.is_datatype(s));
|
||||
if (m_datatype_util.is_recursive(s)) {
|
||||
return get_num_branches_rec(x, fml, num_branches);
|
||||
}
|
||||
else {
|
||||
return get_num_branches_nonrec(x, fml, num_branches);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
|
||||
sort* s = x.x()->get_decl()->get_range();
|
||||
SASSERT(m_datatype_util.is_datatype(s));
|
||||
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
|
||||
if (m_datatype_util.is_recursive(s)) {
|
||||
assign_rec(x, fml, vl);
|
||||
}
|
||||
else {
|
||||
assign_nonrec(x, fml, vl);
|
||||
}
|
||||
}
|
||||
|
||||
virtual void subst(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));
|
||||
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
|
||||
if (m_datatype_util.is_recursive(s)) {
|
||||
subst_rec(x, vl, fml, def);
|
||||
}
|
||||
else {
|
||||
subst_nonrec(x, vl, fml, def);
|
||||
}
|
||||
}
|
||||
|
||||
virtual unsigned get_weight( contains_app& x, expr* fml) {
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
virtual bool solve( conj_enum& conj, expr* fml) {
|
||||
return false;
|
||||
}
|
||||
|
||||
virtual bool simplify( expr_ref& fml) {
|
||||
lift_foreign_vars lift(m, m_datatype_util, m_ctx);
|
||||
return lift.lift(fml);
|
||||
}
|
||||
|
||||
virtual bool mk_atom(expr* e, bool p, expr_ref& result) {
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
virtual rational get_cost(contains_app&, expr* fml) {
|
||||
return rational(0);
|
||||
}
|
||||
|
||||
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, expr_ref* def) {
|
||||
subst_clos* sub = 0;
|
||||
|
||||
if (m_subst_cache.find(x.x(), c, sub)) {
|
||||
m_replace.apply_substitution(x.x(), sub->first, fml);
|
||||
add_def(sub->first, def);
|
||||
for (unsigned i = 0; i < sub->second.size(); ++i) {
|
||||
m_ctx.add_var(sub->second[i]);
|
||||
}
|
||||
return;
|
||||
}
|
||||
sub = alloc(subst_clos);
|
||||
unsigned arity = c->get_arity();
|
||||
expr_ref_vector vars(m);
|
||||
for (unsigned i = 0; i < arity; ++i) {
|
||||
sort* sort_x = c->get_domain()[i];
|
||||
app_ref fresh_x(m.mk_fresh_const("x", sort_x), m);
|
||||
m_ctx.add_var(fresh_x.get());
|
||||
vars.push_back(fresh_x.get());
|
||||
sub->second.push_back(fresh_x.get());
|
||||
}
|
||||
app_ref t(m.mk_app(c, vars.size(), vars.c_ptr()), m);
|
||||
m_trail.push_back(x.x());
|
||||
m_trail.push_back(c);
|
||||
m_trail.push_back(t);
|
||||
|
||||
add_def(t, def);
|
||||
m_replace.apply_substitution(x.x(), t, fml);
|
||||
sub->first = t;
|
||||
m_subst_cache.insert(x.x(), c, sub);
|
||||
}
|
||||
|
||||
void get_recognizers(expr* fml, ptr_vector<app>& recognizers) {
|
||||
conj_enum conjs(m, fml);
|
||||
conj_enum::iterator it = conjs.begin(), end = conjs.end();
|
||||
for (; it != end; ++it) {
|
||||
expr* e = *it;
|
||||
if (is_app(e)) {
|
||||
app* a = to_app(e);
|
||||
func_decl* f = a->get_decl();
|
||||
if (m_datatype_util.is_recognizer(f)) {
|
||||
recognizers.push_back(a);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool has_recognizer(app* x, expr* fml, func_decl*& r, func_decl*& c) {
|
||||
ptr_vector<app> recognizers;
|
||||
get_recognizers(fml, recognizers);
|
||||
for (unsigned i = 0; i < recognizers.size(); ++i) {
|
||||
app* a = recognizers[i];
|
||||
if (a->get_arg(0) == x) {
|
||||
r = a->get_decl();
|
||||
c = m_datatype_util.get_recognizer_constructor(a->get_decl());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool get_num_branches_rec( contains_app& x, expr* fml, rational& num_branches) {
|
||||
sort* s = x.x()->get_decl()->get_range();
|
||||
SASSERT(m_datatype_util.is_datatype(s));
|
||||
SASSERT(m_datatype_util.is_recursive(s));
|
||||
|
||||
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
|
||||
num_branches = rational(sz);
|
||||
func_decl* c = 0, *r = 0;
|
||||
|
||||
//
|
||||
// If 'x' does not yet have a recognizer, then branch according to recognizers.
|
||||
//
|
||||
if (!has_recognizer(x.x(), fml, r, c)) {
|
||||
return true;
|
||||
}
|
||||
//
|
||||
// eliminate 'x' by applying constructor to fresh variables.
|
||||
//
|
||||
if (has_selector(x, fml, c)) {
|
||||
num_branches = rational(1);
|
||||
return true;
|
||||
}
|
||||
|
||||
//
|
||||
// 'x' has a recognizer. Count number of equalities and disequalities.
|
||||
//
|
||||
if (update_eqs(x, fml)) {
|
||||
datatype_atoms& eqs = get_eqs(x.x(), fml);
|
||||
num_branches = rational(eqs.num_eqs() + 1);
|
||||
return true;
|
||||
}
|
||||
TRACE("qe", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
void assign_rec(contains_app& contains_x, expr* fml, rational const& vl) {
|
||||
app* x = contains_x.x();
|
||||
sort* s = x->get_decl()->get_range();
|
||||
func_decl* c = 0, *r = 0;
|
||||
|
||||
//
|
||||
// If 'x' does not yet have a recognizer, then branch according to recognizers.
|
||||
//
|
||||
if (!has_recognizer(x, fml, r, c)) {
|
||||
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
|
||||
r = m_datatype_util.get_constructor_recognizer(c);
|
||||
app* is_c = m.mk_app(r, x);
|
||||
// assert v => r(x)
|
||||
m_ctx.add_constraint(true, is_c);
|
||||
return;
|
||||
}
|
||||
|
||||
//
|
||||
// eliminate 'x' by applying constructor to fresh variables.
|
||||
//
|
||||
if (has_selector(contains_x, fml, c)) {
|
||||
return;
|
||||
}
|
||||
|
||||
//
|
||||
// 'x' has a recognizer. The branch ID id provided by the index of the equality.
|
||||
//
|
||||
datatype_atoms& eqs = get_eqs(x, fml);
|
||||
SASSERT(vl.is_unsigned());
|
||||
unsigned idx = vl.get_unsigned();
|
||||
SASSERT(idx <= eqs.num_eqs());
|
||||
|
||||
if (idx < eqs.num_eqs()) {
|
||||
expr* t = eqs.eq(idx);
|
||||
m_ctx.add_constraint(true, m.mk_eq(x, t));
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
|
||||
expr* t = eqs.eq(i);
|
||||
m_ctx.add_constraint(true, m.mk_not(m.mk_eq(x, t)));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
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));
|
||||
func_decl* c = 0, *r = 0;
|
||||
|
||||
TRACE("qe", tout << mk_pp(x, m) << " " << vl << " " << mk_pp(fml, m) << " " << (def != 0) << "\n";);
|
||||
//
|
||||
// Add recognizer to formula.
|
||||
// Introduce auxiliary variable to eliminate.
|
||||
//
|
||||
if (!has_recognizer(x, fml, r, c)) {
|
||||
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
|
||||
r = m_datatype_util.get_constructor_recognizer(c);
|
||||
app* is_c = m.mk_app(r, x);
|
||||
fml = m.mk_and(is_c, fml);
|
||||
app_ref fresh_x(m.mk_fresh_const("x", s), m);
|
||||
m_ctx.add_var(fresh_x);
|
||||
m_replace.apply_substitution(x, fresh_x, fml);
|
||||
add_def(fresh_x, def);
|
||||
TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
if (has_selector(contains_x, fml, c)) {
|
||||
TRACE("qe", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
|
||||
subst_constructor(contains_x, c, fml, def);
|
||||
return;
|
||||
}
|
||||
|
||||
//
|
||||
// 'x' has a recognizer. The branch ID id provided by the index of the equality.
|
||||
//
|
||||
datatype_atoms& eqs = get_eqs(x, fml);
|
||||
SASSERT(vl.is_unsigned());
|
||||
unsigned idx = vl.get_unsigned();
|
||||
SASSERT(idx <= eqs.num_eqs());
|
||||
|
||||
for (unsigned i = 0; i < eqs.num_recognizers(); ++i) {
|
||||
app* rec = eqs.recognizer(i);
|
||||
if (rec->get_decl() == r) {
|
||||
m_replace.apply_substitution(rec, m.mk_true(), fml);
|
||||
}
|
||||
else {
|
||||
m_replace.apply_substitution(rec, m.mk_false(), fml);
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < eqs.num_unsat(); ++i) {
|
||||
m_replace.apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml);
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
|
||||
m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
|
||||
m_replace.apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
|
||||
}
|
||||
if (def) {
|
||||
sort* s = m.get_sort(x);
|
||||
ptr_vector<sort> sorts;
|
||||
sorts.resize(eqs.num_neq_terms(), s);
|
||||
func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s);
|
||||
expr_ref t(m);
|
||||
t = m.mk_app(diag, eqs.num_neq_terms(), eqs.neq_terms());
|
||||
add_def(t, def);
|
||||
}
|
||||
}
|
||||
TRACE("qe", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
|
||||
}
|
||||
|
||||
bool get_num_branches_nonrec( contains_app& x, expr* fml, rational& num_branches) {
|
||||
sort* s = x.x()->get_decl()->get_range();
|
||||
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
|
||||
num_branches = rational(sz);
|
||||
func_decl* c = 0, *r = 0;
|
||||
|
||||
if (sz != 1 && has_recognizer(x.x(), fml, r, c)) {
|
||||
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
|
||||
num_branches = rational(1);
|
||||
}
|
||||
TRACE("qe", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
|
||||
return true;
|
||||
}
|
||||
|
||||
void assign_nonrec(contains_app& contains_x, expr* fml, rational const& vl) {
|
||||
app* x = contains_x.x();
|
||||
sort* s = x->get_decl()->get_range();
|
||||
SASSERT(m_datatype_util.is_datatype(s));
|
||||
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
|
||||
SASSERT(vl.is_unsigned());
|
||||
SASSERT(vl.get_unsigned() < sz);
|
||||
if (sz == 1) {
|
||||
return;
|
||||
}
|
||||
func_decl* c = 0, *r = 0;
|
||||
if (has_recognizer(x, fml, r, c)) {
|
||||
TRACE("qe", tout << mk_pp(x, m) << " has a recognizer\n";);
|
||||
return;
|
||||
}
|
||||
|
||||
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
|
||||
r = m_datatype_util.get_constructor_recognizer(c);
|
||||
app* is_c = m.mk_app(r, x);
|
||||
|
||||
// assert v => r(x)
|
||||
|
||||
m_ctx.add_constraint(true, is_c);
|
||||
}
|
||||
|
||||
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));
|
||||
func_decl* c = 0, *r = 0;
|
||||
if (has_recognizer(x.x(), fml, r, c)) {
|
||||
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
|
||||
}
|
||||
else {
|
||||
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
|
||||
SASSERT(vl.is_unsigned());
|
||||
SASSERT(vl.get_unsigned() < sz);
|
||||
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
|
||||
}
|
||||
subst_constructor(x, c, fml, def);
|
||||
}
|
||||
|
||||
|
||||
class has_select : public i_expr_pred {
|
||||
app* m_x;
|
||||
func_decl* m_c;
|
||||
datatype_util& m_util;
|
||||
public:
|
||||
has_select(app* x, func_decl* c, datatype_util& u): m_x(x), m_c(c), m_util(u) {}
|
||||
|
||||
virtual bool operator()(expr* e) {
|
||||
if (!is_app(e)) return false;
|
||||
app* a = to_app(e);
|
||||
if (!m_util.is_accessor(a)) return false;
|
||||
if (a->get_arg(0) != m_x) return false;
|
||||
func_decl* f = a->get_decl();
|
||||
return m_c == m_util.get_accessor_constructor(f);
|
||||
}
|
||||
};
|
||||
|
||||
bool has_selector(contains_app& x, expr* fml, func_decl* c) {
|
||||
has_select hs(x.x(), c, m_datatype_util);
|
||||
check_pred ch(hs, m);
|
||||
return ch(fml);
|
||||
}
|
||||
|
||||
datatype_atoms& get_eqs(app* x, expr* fml) {
|
||||
datatype_atoms* eqs = 0;
|
||||
VERIFY (m_eqs_cache.find(x, fml, eqs));
|
||||
return *eqs;
|
||||
}
|
||||
|
||||
bool update_eqs(contains_app& contains_x, expr* fml) {
|
||||
datatype_atoms* eqs = 0;
|
||||
if (m_eqs_cache.find(contains_x.x(), fml, eqs)) {
|
||||
return true;
|
||||
}
|
||||
eqs = alloc(datatype_atoms, m);
|
||||
|
||||
if (!update_eqs(*eqs, contains_x, fml, m_ctx.pos_atoms(), true)) {
|
||||
dealloc(eqs);
|
||||
return false;
|
||||
}
|
||||
if (!update_eqs(*eqs, contains_x, fml, m_ctx.neg_atoms(), false)) {
|
||||
dealloc(eqs);
|
||||
return false;
|
||||
}
|
||||
|
||||
m_trail.push_back(contains_x.x());
|
||||
m_trail.push_back(fml);
|
||||
m_eqs_cache.insert(contains_x.x(), fml, eqs);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool update_eqs(datatype_atoms& eqs, contains_app& contains_x, expr* fml, atom_set const& tbl, bool is_pos) {
|
||||
atom_set::iterator it = tbl.begin(), end = tbl.end();
|
||||
for (; it != end; ++it) {
|
||||
app* e = *it;
|
||||
if (!contains_x(e)) {
|
||||
continue;
|
||||
}
|
||||
if (!eqs.add_atom(contains_x, is_pos, e)) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_datatype_plugin(i_solver_context& ctx) {
|
||||
return alloc(datatype_plugin, ctx, ctx.get_manager());
|
||||
}
|
||||
}
|
||||
231
src/qe/qe_dl_plugin.cpp
Normal file
231
src/qe/qe_dl_plugin.cpp
Normal file
|
|
@ -0,0 +1,231 @@
|
|||
|
||||
#include "qe.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "dl_decl_plugin.h"
|
||||
#include "obj_pair_hashtable.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
|
||||
namespace qe {
|
||||
|
||||
// ---------------------
|
||||
// dl_plugin
|
||||
|
||||
class eq_atoms {
|
||||
expr_ref_vector m_eqs;
|
||||
expr_ref_vector m_neqs;
|
||||
app_ref_vector m_eq_atoms;
|
||||
app_ref_vector m_neq_atoms;
|
||||
public:
|
||||
eq_atoms(ast_manager& m):
|
||||
m_eqs(m),
|
||||
m_neqs(m),
|
||||
m_eq_atoms(m),
|
||||
m_neq_atoms(m) {}
|
||||
|
||||
unsigned num_eqs() const { return m_eqs.size(); }
|
||||
expr* eq(unsigned i) const { return m_eqs[i]; }
|
||||
app* eq_atom(unsigned i) const { return m_eq_atoms[i]; }
|
||||
unsigned num_neqs() const { return m_neqs.size(); }
|
||||
app* neq_atom(unsigned i) const { return m_neq_atoms[i]; }
|
||||
expr* neq(unsigned i) const { return m_neqs[i]; }
|
||||
void add_eq(app* atom, expr * e) { m_eq_atoms.push_back(atom); m_eqs.push_back(e); }
|
||||
void add_neq(app* atom, expr* e) { m_neq_atoms.push_back(atom); m_neqs.push_back(e); }
|
||||
};
|
||||
|
||||
class dl_plugin : public qe_solver_plugin {
|
||||
typedef obj_pair_map<app, expr, eq_atoms*> eqs_cache;
|
||||
expr_safe_replace m_replace;
|
||||
datalog::dl_decl_util m_util;
|
||||
expr_ref_vector m_trail;
|
||||
eqs_cache m_eqs_cache;
|
||||
|
||||
|
||||
public:
|
||||
dl_plugin(i_solver_context& ctx, ast_manager& m) :
|
||||
qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
|
||||
m_replace(m),
|
||||
m_util(m),
|
||||
m_trail(m)
|
||||
{
|
||||
}
|
||||
|
||||
virtual ~dl_plugin() {
|
||||
eqs_cache::iterator it = m_eqs_cache.begin(), end = m_eqs_cache.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->get_value());
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
bool get_num_branches(contains_app & x,expr * fml,rational & num_branches) {
|
||||
if (!update_eqs(x, fml)) {
|
||||
return false;
|
||||
}
|
||||
eq_atoms& eqs = get_eqs(x.x(), fml);
|
||||
uint64 domain_size;
|
||||
if (is_small_domain(x, eqs, domain_size)) {
|
||||
num_branches = rational(domain_size, rational::ui64());
|
||||
}
|
||||
else {
|
||||
num_branches = rational(eqs.num_eqs() + 1);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void assign(contains_app & x,expr * fml,const rational & v) {
|
||||
SASSERT(v.is_unsigned());
|
||||
eq_atoms& eqs = get_eqs(x.x(), fml);
|
||||
unsigned uv = v.get_unsigned();
|
||||
uint64 domain_size;
|
||||
if (is_small_domain(x, eqs, domain_size)) {
|
||||
SASSERT(v < rational(domain_size, rational::ui64()));
|
||||
assign_small_domain(x, eqs, uv);
|
||||
}
|
||||
else {
|
||||
assign_large_domain(x, eqs, uv);
|
||||
}
|
||||
}
|
||||
|
||||
void subst(contains_app & x,const rational & v,expr_ref & fml, expr_ref* def) {
|
||||
SASSERT(v.is_unsigned());
|
||||
eq_atoms& eqs = get_eqs(x.x(), fml);
|
||||
unsigned uv = v.get_unsigned();
|
||||
uint64 domain_size;
|
||||
if (is_small_domain(x, eqs, domain_size)) {
|
||||
SASSERT(uv < domain_size);
|
||||
subst_small_domain(x, eqs, uv, fml);
|
||||
}
|
||||
else {
|
||||
subst_large_domain(x, eqs, uv, fml);
|
||||
}
|
||||
if (def) {
|
||||
*def = 0; // TBD
|
||||
}
|
||||
}
|
||||
|
||||
virtual bool solve(conj_enum& conjs, expr* fml) { return false; }
|
||||
|
||||
private:
|
||||
|
||||
bool is_small_domain(contains_app& x, eq_atoms& eqs, uint64& domain_size) {
|
||||
VERIFY(m_util.try_get_size(m.get_sort(x.x()), domain_size));
|
||||
return domain_size < eqs.num_eqs() + eqs.num_neqs();
|
||||
}
|
||||
|
||||
void assign_small_domain(contains_app & x,eq_atoms& eqs, unsigned value) {
|
||||
expr_ref vl(m_util.mk_numeral(value, m.get_sort(x.x())), m);
|
||||
expr_ref eq(m.mk_eq(x.x(), vl), m);
|
||||
m_ctx.add_constraint(true, eq);
|
||||
}
|
||||
|
||||
void assign_large_domain(contains_app & x,eq_atoms& eqs, unsigned v) {
|
||||
if (v < eqs.num_eqs()) {
|
||||
m_ctx.add_constraint(true, eqs.eq_atom(v));
|
||||
}
|
||||
else {
|
||||
SASSERT(v == eqs.num_eqs());
|
||||
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
|
||||
expr_ref neq(m.mk_not(eqs.eq_atom(i)), m);
|
||||
m_ctx.add_constraint(true, neq);
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
|
||||
expr_ref neq(m.mk_not(eqs.neq_atom(i)), m);
|
||||
m_ctx.add_constraint(true, neq);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) {
|
||||
expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m);
|
||||
m_replace.apply_substitution(x.x(), vl, fml);
|
||||
}
|
||||
|
||||
// assumes that all disequalities can be satisfied.
|
||||
void subst_large_domain(contains_app & x,eq_atoms& eqs, unsigned w,expr_ref & fml) {
|
||||
SASSERT(w <= eqs.num_eqs());
|
||||
if (w < eqs.num_eqs()) {
|
||||
expr* e = eqs.eq(w);
|
||||
m_replace.apply_substitution(x.x(), e, fml);
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
|
||||
m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
|
||||
m_replace.apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
eq_atoms& get_eqs(app* x, expr* fml) {
|
||||
eq_atoms* eqs = 0;
|
||||
VERIFY(m_eqs_cache.find(x, fml, eqs));
|
||||
return *eqs;
|
||||
}
|
||||
|
||||
bool update_eqs(contains_app& contains_x, expr* fml) {
|
||||
eq_atoms* eqs = 0;
|
||||
if (m_eqs_cache.find(contains_x.x(), fml, eqs)) {
|
||||
return true;
|
||||
}
|
||||
eqs = alloc(eq_atoms, m);
|
||||
|
||||
if (!update_eqs(*eqs, contains_x, fml, m_ctx.pos_atoms(), true)) {
|
||||
dealloc(eqs);
|
||||
return false;
|
||||
}
|
||||
if (!update_eqs(*eqs, contains_x, fml, m_ctx.neg_atoms(), false)) {
|
||||
dealloc(eqs);
|
||||
return false;
|
||||
}
|
||||
|
||||
m_trail.push_back(contains_x.x());
|
||||
m_trail.push_back(fml);
|
||||
m_eqs_cache.insert(contains_x.x(), fml, eqs);
|
||||
return true;
|
||||
}
|
||||
|
||||
bool update_eqs(eq_atoms& eqs, contains_app& contains_x, expr* fml, atom_set const& tbl, bool is_pos) {
|
||||
atom_set::iterator it = tbl.begin(), end = tbl.end();
|
||||
expr* x = contains_x.x();
|
||||
for (; it != end; ++it) {
|
||||
app* e = *it;
|
||||
if (!contains_x(e)) {
|
||||
continue;
|
||||
}
|
||||
if (m_util.is_lt(e)) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
expr* e1, *e2;
|
||||
if (!m.is_eq(e, e1, e2)) {
|
||||
TRACE("quant_elim", tout << "Cannot handle: " << mk_pp(e, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (x == e2) {
|
||||
std::swap(e1, e2);
|
||||
}
|
||||
if (contains_x(e2) || x != e1) {
|
||||
TRACE("quant_elim", tout << "Cannot handle: " << mk_pp(e, m) << "\n";);
|
||||
return false;
|
||||
}
|
||||
if (is_pos) {
|
||||
eqs.add_eq(e, e2);
|
||||
}
|
||||
else {
|
||||
eqs.add_neq(e, e2);
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
qe_solver_plugin* mk_dl_plugin(i_solver_context& ctx) {
|
||||
return alloc(dl_plugin, ctx, ctx.get_manager());
|
||||
}
|
||||
}
|
||||
2596
src/qe/qe_lite.cpp
Normal file
2596
src/qe/qe_lite.cpp
Normal file
File diff suppressed because it is too large
Load diff
71
src/qe/qe_lite.h
Normal file
71
src/qe/qe_lite.h
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
/*++
|
||||
Copyright (c) 2012 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"
|
||||
#include "uint_set.h"
|
||||
#include "params.h"
|
||||
|
||||
class tactic;
|
||||
|
||||
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
|
||||
Apply light-weight quantifier elimination to variables present/absent in the index set.
|
||||
If 'index_of_bound' is true, then the index_set is treated as the set of
|
||||
bound variables. if 'index_of_bound' is false, then index_set is treated as the
|
||||
set of variables that are not bound (variables that are not in the index set are bound).
|
||||
*/
|
||||
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);
|
||||
|
||||
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
|
||||
|
||||
/**
|
||||
\brief full rewriting based light-weight quantifier elimination round.
|
||||
*/
|
||||
void operator()(expr_ref& fml, proof_ref& pr);
|
||||
|
||||
void set_cancel(bool f);
|
||||
};
|
||||
|
||||
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
711
src/qe/qe_sat_tactic.cpp
Normal file
711
src/qe/qe_sat_tactic.cpp
Normal file
|
|
@ -0,0 +1,711 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_sat_tactic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Procedure for quantifier satisfiability using quantifier projection.
|
||||
Based on generalizations by Bjorner & Monniaux
|
||||
(see tvm\papers\z3qe\altqe.tex)
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-02-24
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "qe_sat_tactic.h"
|
||||
#include "quant_hoist.h"
|
||||
#include "ast_pp.h"
|
||||
#include "smt_kernel.h"
|
||||
#include "qe.h"
|
||||
#include "cooperate.h"
|
||||
#include "model_v2_pp.h"
|
||||
#include "expr_replacer.h"
|
||||
#include "th_rewriter.h"
|
||||
#include "expr_context_simplifier.h"
|
||||
|
||||
// plugin registration.
|
||||
// solver specific projection operators.
|
||||
// connect goals to tactic
|
||||
|
||||
namespace qe {
|
||||
|
||||
class is_relevant_default : public i_expr_pred {
|
||||
public:
|
||||
bool operator()(expr* e) {
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
||||
class mk_atom_default : public i_nnf_atom {
|
||||
public:
|
||||
virtual void operator()(expr* e, bool pol, expr_ref& result) {
|
||||
if (pol) result = e;
|
||||
else result = result.get_manager().mk_not(e);
|
||||
}
|
||||
};
|
||||
|
||||
class sat_tactic : public tactic {
|
||||
|
||||
// forall x . not forall y . not forall z . not forall u . fml.
|
||||
|
||||
ast_manager& m;
|
||||
expr_ref m_false;
|
||||
volatile bool m_cancel;
|
||||
smt_params m_fparams;
|
||||
params_ref m_params;
|
||||
unsigned m_extrapolate_strategy_param;
|
||||
bool m_projection_mode_param;
|
||||
bool m_strong_context_simplify_param;
|
||||
bool m_ctx_simplify_local_param;
|
||||
vector<app_ref_vector> m_vars;
|
||||
ptr_vector<smt::kernel> m_solvers;
|
||||
smt::kernel m_solver;
|
||||
expr_ref m_fml;
|
||||
expr_ref_vector m_Ms;
|
||||
expr_ref_vector m_assignments;
|
||||
is_relevant_default m_is_relevant;
|
||||
mk_atom_default m_mk_atom;
|
||||
th_rewriter m_rewriter;
|
||||
expr_strong_context_simplifier m_ctx_rewriter;
|
||||
|
||||
class solver_context : public i_solver_context {
|
||||
|
||||
ast_manager& m;
|
||||
sat_tactic& m_super;
|
||||
smt::kernel& m_solver;
|
||||
atom_set m_pos;
|
||||
atom_set m_neg;
|
||||
app_ref_vector m_vars;
|
||||
expr_ref m_fml;
|
||||
ptr_vector<contains_app> m_contains_app;
|
||||
bool m_projection_mode_param;
|
||||
public:
|
||||
solver_context(sat_tactic& s, unsigned idx):
|
||||
m(s.m),
|
||||
m_super(s),
|
||||
m_solver(*s.m_solvers[idx+1]),
|
||||
m_vars(m),
|
||||
m_fml(m),
|
||||
m_projection_mode_param(true) {}
|
||||
|
||||
virtual ~solver_context() {
|
||||
std::for_each(m_contains_app.begin(), m_contains_app.end(), delete_proc<contains_app>());
|
||||
}
|
||||
|
||||
void init(expr* fml, unsigned idx) {
|
||||
m_fml = fml;
|
||||
for (unsigned j = 0; j < m_super.vars(idx).size(); ++j) {
|
||||
add_var(m_super.vars(idx)[j]);
|
||||
}
|
||||
get_nnf(m_fml, get_is_relevant(), get_mk_atom(), m_pos, m_neg);
|
||||
}
|
||||
|
||||
void set_projection_mode(bool p) { m_projection_mode_param = p; }
|
||||
|
||||
ast_manager& get_manager() { return m; }
|
||||
|
||||
expr* fml() { return m_fml; }
|
||||
|
||||
// set of atoms in current formula.
|
||||
virtual atom_set const& pos_atoms() const { return m_pos; }
|
||||
virtual atom_set const& neg_atoms() const { return m_neg; }
|
||||
|
||||
// Access current set of variables to solve
|
||||
virtual unsigned get_num_vars() const { return m_vars.size(); }
|
||||
virtual app* get_var(unsigned idx) const { return m_vars[idx]; }
|
||||
virtual app*const* get_vars() const { return m_vars.c_ptr(); }
|
||||
virtual bool is_var(expr* e, unsigned& idx) const {
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
if (e == m_vars[i]) return (idx = i, true);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
virtual contains_app& contains(unsigned idx) { return *m_contains_app[idx]; }
|
||||
|
||||
// callback to replace variable at index 'idx' with definition 'def' and updated formula 'fml'
|
||||
virtual void elim_var(unsigned idx, expr* fml, expr* def) {
|
||||
m_fml = fml;
|
||||
m_pos.reset();
|
||||
m_neg.reset();
|
||||
get_nnf(m_fml, get_is_relevant(), get_mk_atom(), m_pos, m_neg);
|
||||
m_vars.erase(idx);
|
||||
dealloc(m_contains_app[idx]);
|
||||
m_contains_app.erase(m_contains_app.c_ptr() + idx);
|
||||
}
|
||||
|
||||
// callback to add new variable to branch.
|
||||
virtual void add_var(app* x) {
|
||||
m_vars.push_back(x);
|
||||
m_contains_app.push_back(alloc(contains_app, m, x));
|
||||
}
|
||||
|
||||
// callback to add constraints in branch.
|
||||
virtual void add_constraint(bool use_var, expr* l1 = 0, expr* l2 = 0, expr* l3 = 0) {
|
||||
ptr_buffer<expr> args;
|
||||
if (l1) args.push_back(l1);
|
||||
if (l2) args.push_back(l2);
|
||||
if (l3) args.push_back(l3);
|
||||
expr_ref cnstr(m.mk_or(args.size(), args.c_ptr()), m);
|
||||
m_solver.assert_expr(cnstr);
|
||||
TRACE("qe", tout << "add_constraint " << mk_pp(cnstr,m) << "\n";);
|
||||
}
|
||||
|
||||
// eliminate finite domain variable 'var' from fml.
|
||||
virtual void blast_or(app* var, expr_ref& fml) {
|
||||
expr_ref result(m);
|
||||
expr_quant_elim qelim(m, m_super.m_fparams);
|
||||
qe::mk_exists(1, &var, fml);
|
||||
qelim(m.mk_true(), fml, result);
|
||||
fml = result;
|
||||
TRACE("qe", tout << mk_pp(var, m) << " " << mk_pp(fml, m) << "\n";);
|
||||
}
|
||||
|
||||
void project_var_partial(unsigned i) {
|
||||
app* x = get_var(i);
|
||||
m_super.check_success(has_plugin(x));
|
||||
qe_solver_plugin& p = plugin(m.get_sort(x)->get_family_id());
|
||||
model_ref model;
|
||||
m_solver.get_model(model);
|
||||
m_super.check_success(p.project(contains(i), model, m_fml));
|
||||
m_super.m_rewriter(m_fml);
|
||||
TRACE("qe", model_v2_pp(tout, *model); tout << "\n";
|
||||
tout << mk_pp(m_fml, m) << "\n";);
|
||||
elim_var(i, m_fml, 0);
|
||||
}
|
||||
|
||||
void project_var_full(unsigned i) {
|
||||
expr_ref result(m);
|
||||
app* x = get_var(i);
|
||||
expr_quant_elim qelim(m, m_super.m_fparams);
|
||||
qe::mk_exists(1, &x, m_fml);
|
||||
qelim(m.mk_true(), m_fml, result);
|
||||
m_fml = result;
|
||||
m_super.m_rewriter(m_fml);
|
||||
TRACE("qe", tout << mk_pp(m_fml, m) << "\n";);
|
||||
elim_var(i, m_fml, 0);
|
||||
}
|
||||
|
||||
void project_var(unsigned i) {
|
||||
if (m_projection_mode_param) {
|
||||
project_var_full(i);
|
||||
}
|
||||
else {
|
||||
project_var_partial(i);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
public:
|
||||
sat_tactic(ast_manager& m, params_ref const& p = params_ref()):
|
||||
m(m),
|
||||
m_false(m.mk_false(), m),
|
||||
m_cancel(false),
|
||||
m_params(p),
|
||||
m_extrapolate_strategy_param(0),
|
||||
m_projection_mode_param(true),
|
||||
m_strong_context_simplify_param(true),
|
||||
m_ctx_simplify_local_param(false),
|
||||
m_solver(m, m_fparams),
|
||||
m_fml(m),
|
||||
m_Ms(m),
|
||||
m_assignments(m),
|
||||
m_rewriter(m),
|
||||
m_ctx_rewriter(m_fparams, m) {
|
||||
m_fparams.m_model = true;
|
||||
}
|
||||
|
||||
virtual tactic * translate(ast_manager & m) {
|
||||
return alloc(sat_tactic, m);
|
||||
}
|
||||
|
||||
~sat_tactic() {
|
||||
for (unsigned i = 0; i < m_solvers.size(); ++i) {
|
||||
dealloc(m_solvers[i]);
|
||||
}
|
||||
}
|
||||
|
||||
virtual void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
// not thread-safe when solvers are reset.
|
||||
// TBD: lock - this, reset() and init_Ms.
|
||||
for (unsigned i = 0; i < m_solvers.size(); ++i) {
|
||||
m_solvers[i]->set_cancel(f);
|
||||
}
|
||||
m_solver.set_cancel(f);
|
||||
m_ctx_rewriter.set_cancel(f);
|
||||
}
|
||||
|
||||
virtual void operator()(
|
||||
goal_ref const& goal,
|
||||
goal_ref_buffer& result,
|
||||
model_converter_ref& mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref& core)
|
||||
{
|
||||
try {
|
||||
checkpoint();
|
||||
reset();
|
||||
ptr_vector<expr> fmls;
|
||||
goal->get_formulas(fmls);
|
||||
m_fml = m.mk_and(fmls.size(), fmls.c_ptr());
|
||||
TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";);
|
||||
simplify_rewriter_star rw(m);
|
||||
expr_ref tmp(m);
|
||||
rw(m_fml, tmp);
|
||||
m_fml = tmp;
|
||||
TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";);
|
||||
skolemize_existential_prefix();
|
||||
extract_alt_form(m_fml);
|
||||
model_ref model;
|
||||
expr_ref res = qt(0, m.mk_true(), model);
|
||||
goal->inc_depth();
|
||||
if (m.is_false(res)) {
|
||||
goal->assert_expr(res);
|
||||
}
|
||||
else {
|
||||
goal->reset();
|
||||
// equi-satisfiable. What to do with model?
|
||||
mc = model2model_converter(&*model);
|
||||
}
|
||||
result.push_back(goal.get());
|
||||
}
|
||||
catch (rewriter_exception & ex) {
|
||||
throw tactic_exception(ex.msg());
|
||||
}
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
for (unsigned i = 0; i < m_solvers.size(); ++i) {
|
||||
m_solvers[i]->collect_statistics(st);
|
||||
}
|
||||
m_solver.collect_statistics(st);
|
||||
m_ctx_rewriter.collect_statistics(st);
|
||||
}
|
||||
|
||||
virtual void reset_statistics() {
|
||||
for (unsigned i = 0; i < m_solvers.size(); ++i) {
|
||||
m_solvers[i]->reset_statistics();
|
||||
}
|
||||
m_solver.reset_statistics();
|
||||
m_ctx_rewriter.reset_statistics();
|
||||
}
|
||||
|
||||
virtual void cleanup() {}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_extrapolate_strategy_param = p.get_uint("extrapolate_strategy", m_extrapolate_strategy_param);
|
||||
m_projection_mode_param = p.get_bool("projection_mode", m_projection_mode_param);
|
||||
m_strong_context_simplify_param = p.get_bool("strong_context_simplify", m_strong_context_simplify_param);
|
||||
m_ctx_simplify_local_param = p.get_bool("strong_context_simplify_local", m_ctx_simplify_local_param);
|
||||
}
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
r.insert("extrapolate_strategy",CPK_UINT, "(default: 0 trivial extrapolation) 1 - nnf strengthening 2 - smt-test 3 - nnf_weakening");
|
||||
r.insert("projection_mode", CPK_BOOL, "(default: true - full) false - partial quantifier instantiation");
|
||||
r.insert("strong_context_simplify", CPK_BOOL, "(default: true) use strong context simplifier on result of quantifier elimination");
|
||||
r.insert("strong_context_simplify_local", CPK_BOOL, "(default: false) use strong context simplifier locally on the new formula only");
|
||||
}
|
||||
|
||||
|
||||
private:
|
||||
|
||||
unsigned num_alternations() const { return m_vars.size(); }
|
||||
|
||||
void init_Ms() {
|
||||
for (unsigned i = 0; i < num_alternations(); ++i) {
|
||||
m_Ms.push_back(m.mk_true());
|
||||
m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params));
|
||||
}
|
||||
m_Ms.push_back(m_fml);
|
||||
m_solvers.push_back(alloc(smt::kernel, m, m_fparams, m_params));
|
||||
m_solvers.back()->assert_expr(m_fml);
|
||||
}
|
||||
|
||||
expr* M(unsigned i) { return m_Ms[i].get(); }
|
||||
|
||||
app_ref_vector const& vars(unsigned i) { return m_vars[i]; }
|
||||
|
||||
smt::kernel& solver(unsigned i) { return *m_solvers[i]; }
|
||||
|
||||
void reset() {
|
||||
m_fml = 0;
|
||||
m_Ms.reset();
|
||||
m_vars.reset();
|
||||
}
|
||||
|
||||
void skolemize_existential_prefix() {
|
||||
quantifier_hoister hoist(m);
|
||||
expr_ref result(m);
|
||||
app_ref_vector vars(m);
|
||||
hoist.pull_exists(m_fml, vars, result);
|
||||
m_fml = result;
|
||||
}
|
||||
|
||||
//
|
||||
// fa x ex y fa z . phi
|
||||
// fa x ! fa y ! fa z ! (!phi)
|
||||
//
|
||||
void extract_alt_form(expr* fml) {
|
||||
quantifier_hoister hoist(m);
|
||||
expr_ref result(m);
|
||||
bool is_fa;
|
||||
unsigned parity = 0;
|
||||
m_fml = fml;
|
||||
while (true) {
|
||||
app_ref_vector vars(m);
|
||||
hoist(m_fml, vars, is_fa, result);
|
||||
if (vars.empty()) {
|
||||
break;
|
||||
}
|
||||
SASSERT(((parity & 0x1) == 0) == is_fa);
|
||||
++parity;
|
||||
TRACE("qe", tout << "Hoist " << (is_fa?"fa":"ex") << "\n";
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
tout << mk_pp(vars[i].get(), m) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
tout << mk_pp(result, m) << "\n";);
|
||||
|
||||
m_vars.push_back(vars);
|
||||
m_fml = result;
|
||||
}
|
||||
//
|
||||
// negate formula if the last quantifier is universal.
|
||||
// so that normal form fa x ! fa y ! fa z ! psi
|
||||
// is obtained.
|
||||
//
|
||||
if ((parity & 0x1) == 1) {
|
||||
m_fml = m.mk_not(m_fml);
|
||||
}
|
||||
init_Ms();
|
||||
checkpoint();
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Main quantifier test algorithm loop.
|
||||
|
||||
*/
|
||||
expr_ref qt(unsigned i, expr* ctx, model_ref& model) {
|
||||
model_ref model1;
|
||||
while (true) {
|
||||
IF_VERBOSE(1, verbose_stream() << "qt " << i << "\n";);
|
||||
TRACE("qe",
|
||||
tout << i << " " << mk_pp(ctx, m) << "\n";
|
||||
display(tout););
|
||||
checkpoint();
|
||||
if (is_sat(i, ctx, model)) {
|
||||
expr_ref ctxM = extrapolate(i, ctx, M(i));
|
||||
if (i == num_alternations()) {
|
||||
return ctxM;
|
||||
}
|
||||
expr_ref res = qt(i+1, ctxM, model1);
|
||||
if (m.is_false(res)) {
|
||||
return ctxM;
|
||||
}
|
||||
project(i, res);
|
||||
}
|
||||
else {
|
||||
return m_false;
|
||||
}
|
||||
}
|
||||
UNREACHABLE();
|
||||
return expr_ref(m);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief compute extrapolant
|
||||
|
||||
Assume A & B is sat.
|
||||
Compute C, such that
|
||||
1. A & C is sat,
|
||||
2. not B & C is unsat.
|
||||
(C strengthens B and is still satisfiable with A).
|
||||
*/
|
||||
expr_ref extrapolate(unsigned i, expr* A, expr* B) {
|
||||
switch(m_extrapolate_strategy_param) {
|
||||
case 0: return trivial_extrapolate(i, A, B);
|
||||
case 1: return nnf_strengthening_extrapolate(i, A, B);
|
||||
case 2: return smt_test_extrapolate(i, A, B);
|
||||
case 3: return nnf_weakening_extrapolate(i, A, B);
|
||||
default: return trivial_extrapolate(i, A, B);
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref trivial_extrapolate(unsigned i, expr* A, expr* B) {
|
||||
return expr_ref(B, m);
|
||||
}
|
||||
|
||||
expr_ref conjunction_extrapolate(unsigned i, expr* A, expr* B) {
|
||||
return expr_ref(m.mk_and(A, B), m);
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
Set C = nnf(B), That is, C is the NNF version of B.
|
||||
For each literal in C in order, replace the literal by False and
|
||||
check the conditions for extrapolation:
|
||||
1. not B & C is unsat,
|
||||
2. A & C is sat.
|
||||
The first check holds by construction, so it is redundant.
|
||||
The second is not redundant.
|
||||
Instead of replacing literals in an NNF formula,
|
||||
one simply asserts the negation of that literal.
|
||||
*/
|
||||
expr_ref nnf_strengthening_extrapolate(unsigned i, expr* A, expr* B) {
|
||||
expr_ref Bnnf(B, m);
|
||||
atom_set pos, neg;
|
||||
get_nnf(Bnnf, m_is_relevant, m_mk_atom, pos, neg);
|
||||
expr_substitution sub(m);
|
||||
|
||||
remove_duplicates(pos, neg);
|
||||
|
||||
// Assumption: B is already asserted in solver[i].
|
||||
smt::kernel& solver = *m_solvers[i];
|
||||
solver.push();
|
||||
solver.assert_expr(A);
|
||||
nnf_strengthen(solver, pos, m.mk_false(), sub);
|
||||
nnf_strengthen(solver, neg, m.mk_true(), sub);
|
||||
|
||||
|
||||
solver.pop(1);
|
||||
scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
|
||||
replace->set_substitution(&sub);
|
||||
(*replace)(Bnnf);
|
||||
m_rewriter(Bnnf);
|
||||
TRACE("qe",
|
||||
tout << "A: " << mk_pp(A, m) << "\n";
|
||||
tout << "B: " << mk_pp(B, m) << "\n";
|
||||
tout << "B': " << mk_pp(Bnnf.get(), m) << "\n";
|
||||
// solver.display(tout);
|
||||
);
|
||||
DEBUG_CODE(
|
||||
solver.push();
|
||||
solver.assert_expr(m.mk_not(B));
|
||||
solver.assert_expr(Bnnf);
|
||||
lbool is_sat = solver.check();
|
||||
TRACE("qe", tout << "is sat: " << is_sat << "\n";);
|
||||
SASSERT(is_sat == l_false);
|
||||
solver.pop(1););
|
||||
DEBUG_CODE(
|
||||
solver.push();
|
||||
solver.assert_expr(A);
|
||||
solver.assert_expr(Bnnf);
|
||||
lbool is_sat = solver.check();
|
||||
TRACE("qe", tout << "is sat: " << is_sat << "\n";);
|
||||
SASSERT(is_sat == l_true);
|
||||
solver.pop(1););
|
||||
|
||||
return Bnnf;
|
||||
}
|
||||
|
||||
void nnf_strengthen(smt::kernel& solver, atom_set& atoms, expr* value, expr_substitution& sub) {
|
||||
atom_set::iterator it = atoms.begin(), end = atoms.end();
|
||||
for (; it != end; ++it) {
|
||||
solver.push();
|
||||
solver.assert_expr(m.mk_iff(*it, value));
|
||||
lbool is_sat = solver.check();
|
||||
solver.pop(1);
|
||||
if (is_sat == l_true) {
|
||||
TRACE("qe", tout << "consistent with: " << mk_pp(*it, m) << " " << mk_pp(value, m) << "\n";);
|
||||
sub.insert(*it, value);
|
||||
solver.assert_expr(m.mk_iff(*it, value));
|
||||
}
|
||||
checkpoint();
|
||||
}
|
||||
}
|
||||
|
||||
void remove_duplicates(atom_set& pos, atom_set& neg) {
|
||||
ptr_vector<app> to_delete;
|
||||
atom_set::iterator it = pos.begin(), end = pos.end();
|
||||
for (; it != end; ++it) {
|
||||
if (neg.contains(*it)) {
|
||||
to_delete.push_back(*it);
|
||||
}
|
||||
}
|
||||
for (unsigned j = 0; j < to_delete.size(); ++j) {
|
||||
pos.remove(to_delete[j]);
|
||||
neg.remove(to_delete[j]);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
Set C = nnf(B), That is, C is the NNF version of B.
|
||||
For each literal in C in order, replace the literal by True and
|
||||
check the conditions for extrapolation
|
||||
1. not B & C is unsat,
|
||||
2. A & C is sat.
|
||||
The second holds by construction and is redundant.
|
||||
The first is not redundant.
|
||||
*/
|
||||
expr_ref nnf_weakening_extrapolate(unsigned i, expr* A, expr* B) {
|
||||
expr_ref Bnnf(B, m);
|
||||
atom_set pos, neg;
|
||||
get_nnf(Bnnf, m_is_relevant, m_mk_atom, pos, neg);
|
||||
remove_duplicates(pos, neg);
|
||||
expr_substitution sub(m);
|
||||
|
||||
m_solver.push();
|
||||
m_solver.assert_expr(A);
|
||||
m_solver.assert_expr(m.mk_not(B));
|
||||
nnf_weaken(m_solver, Bnnf, pos, m.mk_true(), sub);
|
||||
nnf_weaken(m_solver, Bnnf, neg, m.mk_false(), sub);
|
||||
scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
|
||||
replace->set_substitution(&sub);
|
||||
(*replace)(Bnnf);
|
||||
m_rewriter(Bnnf);
|
||||
m_solver.pop(1);
|
||||
return Bnnf;
|
||||
}
|
||||
|
||||
void nnf_weaken(smt::kernel& solver, expr_ref& B, atom_set& atoms, expr* value, expr_substitution& sub) {
|
||||
atom_set::iterator it = atoms.begin(), end = atoms.end();
|
||||
for (; it != end; ++it) {
|
||||
solver.push();
|
||||
expr_ref fml = B;
|
||||
mk_default_expr_replacer(m)->apply_substitution(*it, value, fml);
|
||||
solver.assert_expr(fml);
|
||||
if (solver.check() == l_false) {
|
||||
sub.insert(*it, value);
|
||||
B = fml;
|
||||
}
|
||||
solver.pop(1);
|
||||
checkpoint();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
Use the model for A & B to extrapolate.
|
||||
Initially, C is conjunction of literals from B
|
||||
that are in model of A & B.
|
||||
The model is a conjunction of literals.
|
||||
Let us denote this set $C$. We see that the conditions
|
||||
for extrapolation are satisfied. Furthermore,
|
||||
C can be generalized by removing literals
|
||||
from C as long as !B & A & C is unsatisfiable.
|
||||
*/
|
||||
|
||||
expr_ref smt_test_extrapolate(unsigned i, expr* A, expr* B) {
|
||||
expr_ref_vector proxies(m), core(m);
|
||||
obj_map<expr, expr*> proxy_map;
|
||||
|
||||
checkpoint();
|
||||
|
||||
m_solver.push();
|
||||
m_solver.assert_expr(m.mk_not(B));
|
||||
for (unsigned i = 0; i < m_assignments.size(); ++i) {
|
||||
proxies.push_back(m.mk_fresh_const("proxy",m.mk_bool_sort()));
|
||||
proxy_map.insert(proxies.back(), m_assignments[i].get());
|
||||
m_solver.assert_expr(m.mk_iff(proxies.back(), m_assignments[i].get()));
|
||||
TRACE("qe", tout << "assignment: " << mk_pp(m_assignments[i].get(), m) << "\n";);
|
||||
}
|
||||
lbool is_sat = m_solver.check(proxies.size(), proxies.c_ptr());
|
||||
SASSERT(is_sat == l_false);
|
||||
unsigned core_size = m_solver.get_unsat_core_size();
|
||||
for (unsigned i = 0; i < core_size; ++i) {
|
||||
core.push_back(proxy_map.find(m_solver.get_unsat_core_expr(i)));
|
||||
}
|
||||
expr_ref result(m.mk_and(core.size(), core.c_ptr()), m);
|
||||
TRACE("qe", tout << "core: " << mk_pp(result, m) << "\n";
|
||||
tout << mk_pp(A, m) << "\n";
|
||||
tout << mk_pp(B, m) << "\n";);
|
||||
m_solver.pop(1);
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief project vars(idx) from fml relative to M(idx).
|
||||
*/
|
||||
void project(unsigned idx, expr* _fml) {
|
||||
SASSERT(idx < num_alternations());
|
||||
expr_ref fml(_fml, m);
|
||||
if (m_strong_context_simplify_param && m_ctx_simplify_local_param) {
|
||||
m_ctx_rewriter.push();
|
||||
m_ctx_rewriter.assert_expr(M(idx));
|
||||
m_ctx_rewriter(fml);
|
||||
m_ctx_rewriter.pop();
|
||||
TRACE("qe", tout << mk_pp(_fml, m) << "\n-- context simplify -->\n" << mk_pp(fml, m) << "\n";);
|
||||
}
|
||||
solver_context ctx(*this, idx);
|
||||
ctx.add_plugin(mk_arith_plugin(ctx, false, m_fparams));
|
||||
ctx.add_plugin(mk_bool_plugin(ctx));
|
||||
ctx.add_plugin(mk_bv_plugin(ctx));
|
||||
ctx.init(fml, idx);
|
||||
ctx.set_projection_mode(m_projection_mode_param);
|
||||
m_solvers[idx+1]->push();
|
||||
while (ctx.get_num_vars() > 0) {
|
||||
VERIFY(l_true == m_solvers[idx+1]->check());
|
||||
ctx.project_var(ctx.get_num_vars()-1);
|
||||
}
|
||||
m_solvers[idx+1]->pop(1);
|
||||
expr_ref not_fml(m.mk_not(ctx.fml()), m);
|
||||
m_rewriter(not_fml);
|
||||
if (m_strong_context_simplify_param && !m_ctx_simplify_local_param) {
|
||||
m_ctx_rewriter.push();
|
||||
m_ctx_rewriter.assert_expr(M(idx));
|
||||
m_ctx_rewriter(not_fml);
|
||||
m_ctx_rewriter.pop();
|
||||
}
|
||||
expr_ref tmp(m.mk_and(M(idx), not_fml), m);
|
||||
m_rewriter(tmp);
|
||||
m_Ms[idx] = tmp;
|
||||
m_solvers[idx]->assert_expr(not_fml);
|
||||
TRACE("qe",
|
||||
tout << mk_pp(fml, m) << "\n--->\n";
|
||||
tout << mk_pp(tmp, m) << "\n";);
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
if (m_cancel) {
|
||||
throw tactic_exception(TACTIC_CANCELED_MSG);
|
||||
}
|
||||
cooperate("qe-sat");
|
||||
}
|
||||
|
||||
void check_success(bool ok) {
|
||||
if (!ok) {
|
||||
TRACE("qe", tout << "check failed\n";);
|
||||
throw tactic_exception(TACTIC_CANCELED_MSG);
|
||||
}
|
||||
}
|
||||
|
||||
bool is_sat(unsigned i, expr* ctx, model_ref& model) {
|
||||
smt::kernel& solver = *m_solvers[i];
|
||||
solver.push();
|
||||
solver.assert_expr(ctx);
|
||||
lbool r = solver.check();
|
||||
m_assignments.reset();
|
||||
solver.get_assignments(m_assignments);
|
||||
solver.pop(1);
|
||||
check_success(r != l_undef);
|
||||
if (r == l_true && i == 0) solver.get_model(model);
|
||||
return r == l_true;
|
||||
}
|
||||
|
||||
void display(std::ostream& out) {
|
||||
bool is_fa = true;
|
||||
for (unsigned i = 0; i < num_alternations(); ++i) {
|
||||
out << (is_fa?"fa ":"ex ");
|
||||
for (unsigned j = 0; j < vars(i).size(); ++j) {
|
||||
out << mk_pp(m_vars[i][j].get(), m) << " ";
|
||||
}
|
||||
out << "\n";
|
||||
out << mk_pp(m_Ms[i+1].get(), m) << "\n";
|
||||
is_fa = !is_fa;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
tactic * mk_sat_tactic(ast_manager& m, params_ref const& p) {
|
||||
return alloc(sat_tactic, m, p);
|
||||
}
|
||||
|
||||
};
|
||||
36
src/qe/qe_sat_tactic.h
Normal file
36
src/qe/qe_sat_tactic.h
Normal file
|
|
@ -0,0 +1,36 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_sat_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Procedure for quantifier satisfiability using quantifier elimination.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-02-24
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
|
||||
#ifndef __QE_SAT_H__
|
||||
#define __QE_SAT_H__
|
||||
|
||||
#include"tactic.h"
|
||||
|
||||
namespace qe {
|
||||
|
||||
tactic * mk_sat_tactic(ast_manager& m, params_ref const& p = params_ref());
|
||||
|
||||
};
|
||||
/*
|
||||
ADD_TACTIC("qe-sat", "check satisfiability of quantified formulas using quantifier elimination.", "qe::mk_sat_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
153
src/qe/qe_tactic.cpp
Normal file
153
src/qe/qe_tactic.cpp
Normal file
|
|
@ -0,0 +1,153 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_tactic.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Quantifier elimination front-end for tactic framework.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2011-12-28.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"tactical.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"cooperate.h"
|
||||
#include"qe.h"
|
||||
|
||||
class qe_tactic : public tactic {
|
||||
struct imp {
|
||||
ast_manager & m;
|
||||
smt_params m_fparams;
|
||||
volatile bool m_cancel;
|
||||
qe::expr_quant_elim m_qe;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_qe(m, m_fparams) {
|
||||
updt_params(p);
|
||||
m_cancel = false;
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_fparams.m_nlquant_elim = p.get_bool("qe_nonlinear", false);
|
||||
m_qe.updt_params(p);
|
||||
}
|
||||
|
||||
void collect_param_descrs(param_descrs & r) {
|
||||
m_qe.collect_param_descrs(r);
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
m_qe.set_cancel(f);
|
||||
}
|
||||
|
||||
void checkpoint() {
|
||||
if (m_cancel)
|
||||
throw tactic_exception(TACTIC_CANCELED_MSG);
|
||||
cooperate("qe");
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
SASSERT(g->is_well_sorted());
|
||||
mc = 0; pc = 0; core = 0;
|
||||
tactic_report report("qe", *g);
|
||||
m_fparams.m_model = g->models_enabled();
|
||||
proof_ref new_pr(m);
|
||||
expr_ref new_f(m);
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
|
||||
unsigned sz = g->size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
checkpoint();
|
||||
if (g->inconsistent())
|
||||
break;
|
||||
expr * f = g->form(i);
|
||||
if (!has_quantifiers(f))
|
||||
continue;
|
||||
m_qe(m.mk_true(), f, new_f);
|
||||
new_pr = 0;
|
||||
if (produce_proofs) {
|
||||
new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
|
||||
}
|
||||
g->update(i, new_f, new_pr, g->dep(i));
|
||||
}
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
TRACE("qe", g->display(tout););
|
||||
SASSERT(g->is_well_sorted());
|
||||
}
|
||||
};
|
||||
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
qe_tactic(ast_manager & m, params_ref const & p):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
virtual tactic * translate(ast_manager & m) {
|
||||
return alloc(qe_tactic, m, m_params);
|
||||
}
|
||||
|
||||
virtual ~qe_tactic() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
|
||||
virtual void collect_param_descrs(param_descrs & r) {
|
||||
r.insert("qe_nonlinear", CPK_BOOL, "(default: false) enable virtual term substitution.");
|
||||
m_imp->collect_param_descrs(r);
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
goal_ref_buffer & result,
|
||||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
(*m_imp)(in, result, mc, pc, core);
|
||||
}
|
||||
|
||||
virtual void cleanup() {
|
||||
ast_manager & m = m_imp->m;
|
||||
imp * d = m_imp;
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_imp = 0;
|
||||
}
|
||||
dealloc(d);
|
||||
d = alloc(imp, m, m_params);
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_imp = d;
|
||||
}
|
||||
}
|
||||
|
||||
protected:
|
||||
virtual void set_cancel(bool f) {
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
};
|
||||
|
||||
tactic * mk_qe_tactic(ast_manager & m, params_ref const & p) {
|
||||
return clean(alloc(qe_tactic, m, p));
|
||||
}
|
||||
|
||||
30
src/qe/qe_tactic.h
Normal file
30
src/qe/qe_tactic.h
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_tactic.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Quantifier elimination front-end for tactic framework.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2011-12-28.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _QE_TACTIC_H_
|
||||
#define _QE_TACTIC_H_
|
||||
|
||||
#include"params.h"
|
||||
class ast_manager;
|
||||
class tactic;
|
||||
|
||||
tactic * mk_qe_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("qe", "apply quantifier elimination.", "mk_qe_tactic(m, p)")
|
||||
*/
|
||||
#endif
|
||||
116
src/qe/qe_util.cpp
Normal file
116
src/qe/qe_util.cpp
Normal file
|
|
@ -0,0 +1,116 @@
|
|||
#include "qe_util.h"
|
||||
|
||||
namespace qe {
|
||||
void flatten_and(expr_ref_vector& result) {
|
||||
ast_manager& m = result.get_manager();
|
||||
expr* e1, *e2, *e3;
|
||||
for (unsigned i = 0; i < result.size(); ++i) {
|
||||
if (m.is_and(result[i].get())) {
|
||||
app* a = to_app(result[i].get());
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned j = 0; j < num_args; ++j) {
|
||||
result.push_back(a->get_arg(j));
|
||||
}
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
|
||||
result[i] = e2;
|
||||
--i;
|
||||
}
|
||||
else if (m.is_not(result[i].get(), e1) && m.is_or(e1)) {
|
||||
app* a = to_app(e1);
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned j = 0; j < num_args; ++j) {
|
||||
result.push_back(m.mk_not(a->get_arg(j)));
|
||||
}
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_not(result[i].get(), e1) && m.is_implies(e1,e2,e3)) {
|
||||
result.push_back(e2);
|
||||
result[i] = m.mk_not(e3);
|
||||
--i;
|
||||
}
|
||||
else if (m.is_true(result[i].get()) ||
|
||||
(m.is_not(result[i].get(), e1) &&
|
||||
m.is_false(e1))) {
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_false(result[i].get()) ||
|
||||
(m.is_not(result[i].get(), e1) &&
|
||||
m.is_true(e1))) {
|
||||
result.reset();
|
||||
result.push_back(m.mk_false());
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void flatten_and(expr* fml, expr_ref_vector& result) {
|
||||
SASSERT(result.get_manager().is_bool(fml));
|
||||
result.push_back(fml);
|
||||
flatten_and(result);
|
||||
}
|
||||
|
||||
void flatten_or(expr_ref_vector& result) {
|
||||
ast_manager& m = result.get_manager();
|
||||
expr* e1, *e2, *e3;
|
||||
for (unsigned i = 0; i < result.size(); ++i) {
|
||||
if (m.is_or(result[i].get())) {
|
||||
app* a = to_app(result[i].get());
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned j = 0; j < num_args; ++j) {
|
||||
result.push_back(a->get_arg(j));
|
||||
}
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_not(result[i].get(), e1) && m.is_not(e1, e2)) {
|
||||
result[i] = e2;
|
||||
--i;
|
||||
}
|
||||
else if (m.is_not(result[i].get(), e1) && m.is_and(e1)) {
|
||||
app* a = to_app(e1);
|
||||
unsigned num_args = a->get_num_args();
|
||||
for (unsigned j = 0; j < num_args; ++j) {
|
||||
result.push_back(m.mk_not(a->get_arg(j)));
|
||||
}
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_implies(result[i].get(),e2,e3)) {
|
||||
result.push_back(e3);
|
||||
result[i] = m.mk_not(e2);
|
||||
--i;
|
||||
}
|
||||
else if (m.is_false(result[i].get()) ||
|
||||
(m.is_not(result[i].get(), e1) &&
|
||||
m.is_true(e1))) {
|
||||
result[i] = result.back();
|
||||
result.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m.is_true(result[i].get()) ||
|
||||
(m.is_not(result[i].get(), e1) &&
|
||||
m.is_false(e1))) {
|
||||
result.reset();
|
||||
result.push_back(m.mk_true());
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void flatten_or(expr* fml, expr_ref_vector& result) {
|
||||
SASSERT(result.get_manager().is_bool(fml));
|
||||
result.push_back(fml);
|
||||
flatten_or(result);
|
||||
}
|
||||
}
|
||||
37
src/qe/qe_util.h
Normal file
37
src/qe/qe_util.h
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qe_util.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Utilities for quantifiers.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-08-28
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _QE_UTIL_H_
|
||||
#define _QE_UTIL_H_
|
||||
|
||||
#include "ast.h"
|
||||
|
||||
namespace qe {
|
||||
/**
|
||||
\brief Collect top-level conjunctions and disjunctions.
|
||||
*/
|
||||
void flatten_and(expr_ref_vector& result);
|
||||
|
||||
void flatten_and(expr* fml, expr_ref_vector& result);
|
||||
|
||||
void flatten_or(expr_ref_vector& result);
|
||||
|
||||
void flatten_or(expr* fml, expr_ref_vector& result);
|
||||
|
||||
}
|
||||
#endif
|
||||
Loading…
Add table
Add a link
Reference in a new issue