3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00

add fd solver for finite domain queries

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-18 22:34:34 -04:00
parent 948a1e600e
commit d060359f01
16 changed files with 676 additions and 204 deletions

View file

@ -29,6 +29,7 @@ Revision History:
#include "extension_model_converter.h"
#include "var_subst.h"
#include "ast_util.h"
#include "fd_rewriter.h"
class dt2bv_tactic : public tactic {
@ -39,177 +40,8 @@ class dt2bv_tactic : public tactic {
bv_util m_bv;
obj_hashtable<sort> m_fd_sorts;
obj_hashtable<sort> m_non_fd_sorts;
expr_ref_vector m_bounds;
ref<extension_model_converter> m_ext;
ref<filter_model_converter> m_filter;
unsigned m_num_translated;
obj_map<func_decl, expr*>* m_translate;
struct rw_cfg : public default_rewriter_cfg {
dt2bv_tactic& m_t;
ast_manager& m;
params_ref m_params;
obj_map<expr, expr*> m_cache;
expr_ref_vector m_trail;
rw_cfg(dt2bv_tactic& t, ast_manager & m, params_ref const & p) :
m_t(t),
m(m),
m_params(p),
m_trail(m)
{}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
expr_ref a0(m), a1(m);
expr_ref_vector _args(m);
if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) {
result = m.mk_eq(a0, a1);
return BR_DONE;
}
else if (m.is_distinct(f) && reduce_args(num, args, _args)) {
result = m.mk_distinct(_args.size(), _args.c_ptr());
return BR_DONE;
}
else if (m_t.m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
unsigned idx = m_t.m_dt.get_recognizer_constructor_idx(f);
a1 = m_t.m_bv.mk_numeral(rational(idx), get_sort(a0));
result = m.mk_eq(a0, a1);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
bool reduce_args(unsigned sz, expr*const* as, expr_ref_vector& result) {
expr_ref tmp(m);
for (unsigned i = 0; i < sz; ++i) {
if (!reduce_arg(as[i], tmp)) return false;
result.push_back(tmp);
}
return true;
}
bool reduce_arg(expr* a, expr_ref& result) {
expr* b;
if (m_cache.find(a, b)) {
result = b;
return true;
}
sort* s = get_sort(a);
if (!m_t.m_fd_sorts.contains(s)) {
return false;
}
unsigned bv_size = get_bv_size(s);
if (is_var(a)) {
result = m.mk_var(to_var(a)->get_idx(), m_t.m_bv.mk_sort(bv_size));
return true;
}
SASSERT(is_app(a));
func_decl* f = to_app(a)->get_decl();
if (m_t.m_dt.is_constructor(f)) {
unsigned idx = m_t.m_dt.get_constructor_idx(f);
result = m_t.m_bv.mk_numeral(idx, bv_size);
}
else if (is_uninterp_const(a)) {
// create a fresh variable, add bounds constraints for it.
unsigned nc = m_t.m_dt.get_datatype_num_constructors(s);
result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size));
if (!is_power_of_two(nc)) {
m_t.m_bounds.push_back(m_t.m_bv.mk_ule(result, m_t.m_bv.mk_numeral(nc-1, bv_size)));
}
expr_ref f_def(m);
ptr_vector<func_decl> const& cs = *m_t.m_dt.get_datatype_constructors(s);
f_def = m.mk_const(cs[nc-1]);
for (unsigned i = nc - 1; i > 0; ) {
--i;
f_def = m.mk_ite(m.mk_eq(result, m_t.m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def);
}
// update model converters.
m_t.m_ext->insert(f, f_def);
m_t.m_filter->insert(to_app(result)->get_decl());
if (m_t.m_translate) {
m_t.m_translate->insert(f, result);
}
}
else {
return false;
}
m_cache.insert(a, result);
++m_t.m_num_translated;
return true;
}
ptr_buffer<sort> m_sorts;
bool reduce_quantifier(
quantifier * q,
expr * old_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
m_sorts.reset();
expr_ref_vector bounds(m);
bool found = false;
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
sort* s = q->get_decl_sort(i);
if (m_t.m_fd_sorts.contains(s)) {
unsigned bv_size = get_bv_size(s);
m_sorts.push_back(m_t.m_bv.mk_sort(bv_size));
unsigned nc = m_t.m_dt.get_datatype_num_constructors(s);
if (!is_power_of_two(nc)) {
bounds.push_back(m_t.m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_t.m_bv.mk_numeral(nc, bv_size)));
}
found = true;
}
else {
m_sorts.push_back(s);
}
}
if (!found) {
return false;
}
expr_ref new_body_ref(old_body, m), tmp(m);
if (!bounds.empty()) {
if (q->is_forall()) {
new_body_ref = m.mk_implies(mk_and(bounds), new_body_ref);
}
else {
bounds.push_back(new_body_ref);
new_body_ref = mk_and(bounds);
}
}
result = m.mk_quantifier(q->is_forall(), q->get_num_decls(), m_sorts.c_ptr(), q->get_decl_names(), new_body_ref,
q->get_weight(), q->get_qid(), q->get_skid(),
q->get_num_patterns(), new_patterns,
q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
return true;
}
unsigned get_bv_size(sort* s) {
unsigned nc = m_t.m_dt.get_datatype_num_constructors(s);
unsigned bv_size = 1;
while ((unsigned)(1 << bv_size) < nc) {
++bv_size;
}
return bv_size;
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(dt2bv_tactic& t, ast_manager & m, params_ref const & p) :
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(t, m, p) {
}
};
obj_map<func_decl, func_decl*>* m_translate;
bool is_fd(expr* a) { return is_fd(get_sort(a)); }
bool is_fd(sort* a) { return m_dt.is_enum_sort(a); }
@ -255,10 +87,20 @@ class dt2bv_tactic : public tactic {
void operator()(quantifier* q) {}
};
struct sort_pred : public i_sort_pred {
dt2bv_tactic& m_t;
sort_pred(dt2bv_tactic& t): m_t(t) {}
virtual ~sort_pred() {}
virtual bool operator()(sort* s) {
return m_t.m_fd_sorts.contains(s);
}
};
sort_pred m_is_fd;
public:
dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map<func_decl, expr*>* tr):
m(m), m_params(p), m_dt(m), m_bv(m), m_bounds(m), m_translate(tr) {}
dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map<func_decl, func_decl*>* tr):
m(m), m_params(p), m_dt(m), m_bv(m), m_translate(tr), m_is_fd(*this) {}
virtual tactic * translate(ast_manager & m) {
return alloc(dt2bv_tactic, m, m_params, 0);
@ -289,26 +131,43 @@ public:
m_fd_sorts.remove(*it);
}
if (!m_fd_sorts.empty()) {
m_bounds.reset();
m_num_translated = 0;
m_ext = alloc(extension_model_converter, m);
m_filter = alloc(filter_model_converter, m);
scoped_ptr<rw> r = alloc(rw, *this, m, m_params);
ref<extension_model_converter> ext = alloc(extension_model_converter, m);
ref<filter_model_converter> filter = alloc(filter_model_converter, m);
fd_rewriter rw(m, m_params);
rw.set_is_fd(&m_is_fd);
expr_ref new_curr(m);
proof_ref new_pr(m);
for (unsigned idx = 0; idx < size; idx++) {
(*r)(g->form(idx), new_curr, new_pr);
rw(g->form(idx), new_curr, new_pr);
if (produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
for (unsigned i = 0; i < m_bounds.size(); ++i) {
g->assert_expr(m_bounds[i].get());
expr_ref_vector bounds(m);
rw.flush_side_constraints(bounds);
for (unsigned i = 0; i < bounds.size(); ++i) {
g->assert_expr(bounds[i].get());
}
mc = concat(m_filter.get(), m_ext.get());
report_tactic_progress(":fd-num-translated", m_num_translated);
{
obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
for (; it != end; ++it) {
filter->insert(it->m_value);
if (m_translate) {
m_translate->insert(it->m_key, it->m_value);
}
}
}
{
obj_map<func_decl, expr*>::iterator it = rw.enum2def().begin(), end = rw.enum2def().end();
for (; it != end; ++it) {
ext->insert(it->m_key, it->m_value);
}
}
mc = concat(filter.get(), ext.get());
report_tactic_progress(":fd-num-translated", rw.num_translated());
}
g->inc_depth();
result.push_back(g.get());
@ -319,11 +178,10 @@ public:
virtual void cleanup() {
m_fd_sorts.reset();
m_non_fd_sorts.reset();
m_bounds.reset();
}
};
tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map<func_decl, expr*>* tr) {
tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map<func_decl, func_decl*>* tr) {
return alloc(dt2bv_tactic, m, p, tr);
}

View file

@ -24,7 +24,7 @@ Revision History:
class ast_manager;
class tactic;
tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map<func_decl, expr*>* tr = 0);
tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map<func_decl, func_decl*>* tr = 0);
/*
ADD_TACTIC("dt2bv", "eliminate finite domain data-types. Replace by bit-vectors.", "mk_dt2bv_tactic(m, p)")

View file

@ -71,7 +71,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
void extension_model_converter::insert(func_decl * v, expr * def) {
m_vars.push_back(v);
m_defs.push_back(def);
m_defs.push_back(def);
}

View file

@ -0,0 +1,161 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
fd_solver.cpp
Abstract:
Finite domain solver.
Enumeration data-types are translated into bit-vectors, and then
the incremental sat-solver is applied to the resulting assertions.
Author:
Nikolaj Bjorner (nbjorner) 2016-10-17
Notes:
--*/
#include "fd_solver.h"
#include "solver_na2as.h"
#include "tactic.h"
#include "inc_sat_solver.h"
#include "bv_decl_plugin.h"
#include "datatype_decl_plugin.h"
#include "fd_rewriter.h"
#include "extension_model_converter.h"
#include "filter_model_converter.h"
#include "ast_pp.h"
#include "model_smt2_pp.h"
class fd_solver : public solver_na2as {
ast_manager& m;
params_ref m_params;
ref<solver> m_solver;
fd_rewriter m_rewriter;
public:
fd_solver(ast_manager& m, params_ref const& p):
solver_na2as(m),
m(m),
m_params(p),
m_solver(mk_inc_sat_solver(m, p)),
m_rewriter(m, p)
{
}
virtual ~fd_solver() {}
virtual solver* translate(ast_manager& m, params_ref const& p) {
return alloc(fd_solver, m, p);
}
virtual void assert_expr(expr * t) {
expr_ref tmp(t, m);
expr_ref_vector bounds(m);
proof_ref tmp_proof(m);
m_rewriter(t, tmp, tmp_proof);
m_solver->assert_expr(tmp);
m_rewriter.flush_side_constraints(bounds);
m_solver->assert_expr(bounds);
}
virtual void push_core() {
m_rewriter.push();
m_solver->push();
}
virtual void pop_core(unsigned n) {
m_solver->pop(n);
m_rewriter.pop(n);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
return m_solver->check_sat(num_assumptions, assumptions);
}
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); }
virtual void get_unsat_core(ptr_vector<expr> & r) { m_solver->get_unsat_core(r); }
virtual void get_model(model_ref & mdl) {
m_solver->get_model(mdl);
if (mdl) {
extend_model(mdl);
filter_model(mdl);
}
}
virtual proof * get_proof() { return m_solver->get_proof(); }
virtual std::string reason_unknown() const { return m_solver->reason_unknown(); }
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
datatype_util dt(m);
bv_util bv(m);
// translate enumeration constants to bit-vectors.
expr_ref_vector bvars(m), conseq(m);
for (unsigned i = 0; i < vars.size(); ++i) {
func_decl* f;
if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
bvars.push_back(m.mk_const(f));
}
else {
bvars.push_back(vars[i]);
}
}
lbool r = m_solver->get_consequences(asms, bvars, consequences);
// translate bit-vector consequences back to enumeration types
for (unsigned i = 0; i < consequences.size(); ++i) {
expr* a, *b, *u, *v;
func_decl* f;
rational num;
unsigned bvsize;
VERIFY(m.is_implies(consequences[i].get(), a, b));
if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
SASSERT(num.is_unsigned());
expr_ref head(m);
ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
consequences[i] = m.mk_implies(a, head);
}
}
return r;
}
void filter_model(model_ref& mdl) {
filter_model_converter filter(m);
obj_map<func_decl, func_decl*>::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end();
for (; it != end; ++it) {
filter.insert(it->m_value);
}
filter(mdl, 0);
}
void extend_model(model_ref& mdl) {
extension_model_converter ext(m);
obj_map<func_decl, expr*>::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end();
for (; it != end; ++it) {
ext.insert(it->m_key, it->m_value);
}
ext(mdl, 0);
}
};
solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
return alloc(fd_solver, m, p);
}

View file

@ -0,0 +1,29 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
fd_solver.h
Abstract:
Finite domain solver.
Author:
Nikolaj Bjorner (nbjorner) 2016-10-17
Notes:
--*/
#ifndef FD_SOLVER_H_
#define FD_SOLVER_H_
#include"ast.h"
#include"params.h"
class solver;
solver * mk_fd_solver(ast_manager & m, params_ref const & p);
#endif

View file

@ -38,6 +38,7 @@ Notes:
#include"horn_tactic.h"
#include"smt_solver.h"
#include"inc_sat_solver.h"
#include"fd_solver.h"
#include"bv_rewriter.h"
@ -98,6 +99,8 @@ static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol
bv_rewriter rw(m);
if (logic == "QF_BV" && rw.hi_div0())
return mk_inc_sat_solver(m, p);
if (logic == "QF_FD")
return mk_fd_solver(m, p);
return mk_smt_solver(m, p, logic);
}
@ -116,7 +119,6 @@ public:
tactic * t = mk_tactic_for_logic(m, p, l);
return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l),
mk_solver_for_logic(m, p, l),
//mk_smt_solver(m, p, l),
p);
}
};