mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Moving things around. Adding tactic just for ackermannization.

Browse source
This commit is contained in:
Mikolas Janota 2016-01-26 17:02:30 +00:00
parent 470f8bca73
commit 0dc8dc4d8e
12 changed files with 0 additions and 1370 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ackr/ackr.pyg
View file

@ -1,8 +0,0 @@
def_module_params('ackr',
description='solving UF via ackermannization (currently for QF_AUFBV)',
export=True,
params=(
('eager', BOOL, True, 'eagerly instantiate all congruence rules'),
('sat_backend', BOOL, False, 'use SAT rather than SMT'),
))

107
src/ackr/ackr_info.h
View file

@ -1,107 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
ackr_info.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef ACKR_INFO_H_12278
#define ACKR_INFO_H_12278
#include"obj_hashtable.h"
#include"ast.h"
#include"ref.h"
#include"expr_replacer.h"
/** \brief
Information about how a formula is being converted into
a formula without uninterpreted function symbols via ackermannization.
The intended use is that new terms are added via set_abstr.
Once all terms are abstracted, call seal.
The function abstract may only be called when sealed.
The class enables reference counting.
**/
class ackr_info {
public:
ackr_info(ast_manager& m)
: m_m(m)
, m_consts(m)
, m_er(mk_default_expr_replacer(m))
, m_subst(m_m)
, m_ref_count(0)
, m_sealed(false)
{}
virtual ~ackr_info() {
m_consts.reset();
}
inline void set_abstr(app* term, app* c) {
SASSERT(!m_sealed);
SASSERT(c);
m_t2c.insert(term,c);
m_c2t.insert(c->get_decl(),term);
m_subst.insert(term, c);
m_consts.push_back(c);
}
inline void abstract(expr * e, expr_ref& res) {
SASSERT(m_sealed);
(*m_er)(e, res);
}
inline app* find_term(func_decl* c) const {
app * rv = 0;
m_c2t.find(c,rv);
return rv;
}
inline app* get_abstr(app* term) const {
app * const rv = m_t2c.find(term);
SASSERT(rv);
return rv;
}
inline void seal() {
m_sealed=true;
m_er->set_substitution(&m_subst);
}
//
// Reference counting
//
void inc_ref() { ++m_ref_count; }
void dec_ref() {
--m_ref_count;
if (m_ref_count == 0) {
dealloc(this);
}
}
private:
typedef obj_map<app, app*> t2ct;
typedef obj_map<func_decl, app*> c2tt;
ast_manager& m_m;
t2ct m_t2c; // terms to constants
c2tt m_c2t; // constants to terms (inversion of m_t2c)
expr_ref_vector m_consts; // the constants introduced during abstraction
// replacer and substitution used to compute abstractions
scoped_ptr<expr_replacer> m_er;
expr_substitution m_subst;
unsigned m_ref_count; // reference counting
bool m_sealed; // debugging
};
typedef ref<ackr_info> ackr_info_ref;
#endif /* ACKR_INFO_H_12278 */

294
src/ackr/lackr.cpp
View file

@ -1,294 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr.cpp
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
///////////////
#include"lackr.h"
#include"ackr_params.hpp"
#include"tactic.h"
#include"lackr_model_constructor.h"
#include"ackr_info.h"
#include"for_each_expr.h"
///////////////
#include"inc_sat_solver.h"
#include"qfaufbv_tactic.h"
#include"qfbv_tactic.h"
#include"tactic2solver.h"
///////////////
#include"model_smt2_pp.h"
///////////////
lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas)
: m_m(m)
, m_p(p)
, m_formulas(formulas)
, m_abstr(m)
, m_sat(0)
, m_bvutil(m)
, m_simp(m)
, m_ackrs(m)
, m_st(st)
{
updt_params(p);
}
lackr::~lackr() {
const fun2terms_map::iterator e = m_fun2terms.end();
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
dealloc(i->get_value());
}
}
lbool lackr::operator() () {
setup_sat();
init();
const lbool rv = m_eager ? eager() : lazy();
if (rv == l_true) m_sat->get_model(m_model);
CTRACE("lackr", rv == l_true,
model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
return rv;
}
void lackr::mk_ackermann(/*out*/goal_ref& g) {
init();
eager_enc();
for (unsigned i = 0; i < m_abstr.size(); ++i) g->assert_expr(m_abstr.get(i));
for (unsigned i = 0; i < m_ackrs.size(); ++i) g->assert_expr(m_ackrs.get(i));
}
void lackr::init() {
params_ref simp_p(m_p);
m_simp.updt_params(simp_p);
m_info = alloc(ackr_info, m_m);
collect_terms();
abstract();
}
//
// Introduce ackermann lemma for the two given terms.
//
bool lackr::ackr(app * const t1, app * const t2) {
TRACE("lackr", tout << "ackr "
<< mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
const unsigned sz = t1->get_num_args();
SASSERT(t2->get_num_args() == sz);
expr_ref_vector eqs(m_m);
for (unsigned gi = 0; gi < sz; ++gi) {
expr * const arg1 = t1->get_arg(gi);
expr * const arg2 = t2->get_arg(gi);
if (arg1 == arg2) continue;
if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) {
// quickly abort if there are two distinct numerals
SASSERT(arg1 != arg2);
TRACE("lackr", tout << "never eq\n";);
return false;
}
eqs.push_back(m_m.mk_eq(arg1, arg2));
}
app * const a1 = m_info->get_abstr(t1);
app * const a2 = m_info->get_abstr(t2);
SASSERT(a1 && a2);
TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
expr_ref lhs(m_m.mk_and(eqs.size(), eqs.c_ptr()), m_m);
TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
expr_ref rhs(m_m.mk_eq(a1, a2),m_m);
TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
expr_ref cg(m_m.mk_implies(lhs, rhs), m_m);
TRACE("lackr", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
expr_ref cga(m_m);
m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications
m_simp(cga);
TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
if (m_m.is_true(cga)) return false;
m_st.m_ackrs_sz++;
m_ackrs.push_back(cga);
return true;
}
//
// Introduce the ackermann lemma for each pair of terms.
//
void lackr::eager_enc() {
const fun2terms_map::iterator e = m_fun2terms.end();
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
checkpoint();
func_decl* const fd = i->m_key;
app_set * const ts = i->get_value();
const app_set::iterator r = ts->end();
for (app_set::iterator j = ts->begin(); j != r; ++j) {
app_set::iterator k = j;
++k;
for (; k != r; ++k) {
app * const t1 = *j;
app * const t2 = *k;
SASSERT(t1->get_decl() == fd);
SASSERT(t2->get_decl() == fd);
if (t1 == t2) continue;
ackr(t1,t2);
}
}
}
}
void lackr::abstract() {
const fun2terms_map::iterator e = m_fun2terms.end();
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
func_decl* const fd = i->m_key;
app_set * const ts = i->get_value();
sort* const s = fd->get_range();
const app_set::iterator r = ts->end();
for (app_set::iterator j = ts->begin(); j != r; ++j) {
app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s);
app * const t = *j;
SASSERT(t->get_decl() == fd);
m_info->set_abstr(t, fc);
TRACE("lackr", tout << "abstr term "
<< mk_ismt2_pp(t, m_m, 2)
<< " -> "
<< mk_ismt2_pp(fc, m_m, 2)
<< "\n";);
}
}
m_info->seal();
// perform abstraction of the formulas
const unsigned sz = m_formulas.size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref a(m_m);
m_info->abstract(m_formulas.get(i), a);
m_abstr.push_back(a);
}
}
void lackr::add_term(app* a) {
if (a->get_num_args() == 0) return;
func_decl* const fd = a->get_decl();
if (!is_uninterp(a)) return;
SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a));
app_set* ts = 0;
if (!m_fun2terms.find(fd, ts)) {
ts = alloc(app_set);
m_fun2terms.insert(fd, ts);
}
TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
ts->insert(a);
}
void lackr::push_abstraction() {
const unsigned sz = m_abstr.size();
for (unsigned i = 0; i < sz; ++i) {
m_sat->assert_expr(m_abstr.get(i));
}
}
lbool lackr::eager() {
push_abstraction();
TRACE("lackr", tout << "run sat 0\n"; );
const lbool rv0 = m_sat->check_sat(0, 0);
if (rv0 == l_false) return l_false;
eager_enc();
expr_ref all(m_m);
all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
m_simp(all);
m_sat->assert_expr(all);
TRACE("lackr", tout << "run sat all\n"; );
return m_sat->check_sat(0, 0);
}
lbool lackr::lazy() {
lackr_model_constructor mc(m_m, m_info);
push_abstraction();
unsigned ackr_head = 0;
while (1) {
m_st.m_it++;
checkpoint();
TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
const lbool r = m_sat->check_sat(0, 0);
if (r == l_undef) return l_undef; // give up
if (r == l_false) return l_false; // abstraction unsat
// reconstruct model
model_ref am;
m_sat->get_model(am);
const bool mc_res = mc.check(am);
if (mc_res) return l_true; // model okay
// refine abstraction
const lackr_model_constructor::conflict_list conflicts = mc.get_conflicts();
for (lackr_model_constructor::conflict_list::const_iterator i = conflicts.begin();
i != conflicts.end(); ++i) {
ackr(i->first, i->second);
}
while (ackr_head < m_ackrs.size()) {
m_sat->assert_expr(m_ackrs.get(ackr_head++));
}
}
}
void lackr::setup_sat() {
if (m_use_sat) {
tactic_ref t = mk_qfbv_tactic(m_m, m_p);
m_sat = mk_tactic2solver(m_m, t.get(), m_p);
}
else {
tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
m_sat = mk_tactic2solver(m_m, t.get(), m_p);
}
SASSERT(m_sat);
m_sat->set_produce_models(true);
}
//
// Collect all uninterpreted terms, skipping 0-arity.
//
void lackr::collect_terms() {
ptr_vector<expr> stack;
expr * curr;
expr_mark visited;
for(unsigned i = 0; i < m_formulas.size(); ++i) {
stack.push_back(m_formulas.get(i));
}
while (!stack.empty()) {
curr = stack.back();
if (visited.is_marked(curr)) {
stack.pop_back();
continue;
}
switch (curr->get_kind()) {
case AST_VAR:
visited.mark(curr, true);
stack.pop_back();
break;
case AST_APP:
{
app * const a = to_app(curr);
if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) {
visited.mark(curr, true);
stack.pop_back();
add_term(a);
}
}
break;
case AST_QUANTIFIER:
UNREACHABLE();
break;
default:
UNREACHABLE();
return;
}
}
visited.reset();
}

125
src/ackr/lackr.h
View file

@ -1,125 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef LACKR_H_15079
#define LACKR_H_15079
///////////////
#include"ackr_info.h"
#include"ackr_params.hpp"
#include"th_rewriter.h"
#include"cooperate.h"
#include"bv_decl_plugin.h"
#include"lbool.h"
#include"model.h"
#include"solver.h"
#include"util.h"
#include"tactic_exception.h"
#include"goal.h"
struct lackr_stats {
lackr_stats() : m_it(0), m_ackrs_sz(0) {}
void reset() { m_it = m_ackrs_sz = 0; }
unsigned m_it; // number of lazy iterations
unsigned m_ackrs_sz; // number of congruence constraints
};
/** \brief
A class to encode or directly solve problems with uninterpreted functions via ackermannization.
Currently, solving is supported only for QF_UFBV.
**/
class lackr {
public:
lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas);
~lackr();
void updt_params(params_ref const & _p) {
ackr_params p(_p);
m_eager = p.eager();
m_use_sat = p.sat_backend();
}
/** \brief
* Solve the formula that the class was initialized with.
**/
lbool operator() ();
/** \brief
* Converts function occurrences to constants and encodes all congruence ackermann lemmas.
* This guarantees a equisatisfiability with the input formula. It has a worst-case quadratic blowup.
**/
void mk_ackermann(/*out*/goal_ref& g);
//
// getters
//
inline ackr_info_ref get_info() { return m_info; }
inline model_ref get_model() { return m_model; }
//
// timeout mechanism
//
void checkpoint() {
if (m_m.canceled()) {
throw tactic_exception(TACTIC_CANCELED_MSG);
}
cooperate("lackr");
}
private:
typedef obj_hashtable<app> app_set;
typedef obj_map<func_decl, app_set*> fun2terms_map;
ast_manager& m_m;
params_ref m_p;
expr_ref_vector m_formulas;
expr_ref_vector m_abstr;
fun2terms_map m_fun2terms;
ackr_info_ref m_info;
scoped_ptr<solver> m_sat;
bv_util m_bvutil;
th_rewriter m_simp;
expr_ref_vector m_ackrs;
model_ref m_model;
bool m_eager;
bool m_use_sat;
lackr_stats& m_st;
void init();
void setup_sat();
lbool eager();
lbool lazy();
//
// Introduce congruence ackermann lemma for the two given terms.
//
bool ackr(app * const t1, app * const t2);
//
// Introduce the ackermann lemma for each pair of terms.
//
void eager_enc();
void abstract();
void push_abstraction();
void add_term(app* a);
//
// Collect all uninterpreted terms, skipping 0-arity.
//
void collect_terms();
};
#endif /* LACKR_H_15079 */

379
src/ackr/lackr_model_constructor.cpp
View file

@ -1,379 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
model_constructor.cpp
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#include"lackr_model_constructor.h"
#include"model_evaluator.h"
#include"ast_smt2_pp.h"
#include"ackr_info.h"
#include"for_each_expr.h"
#include"bv_rewriter.h"
#include"bool_rewriter.h"
struct lackr_model_constructor::imp {
public:
imp(ast_manager& m,
ackr_info_ref info,
model_ref& abstr_model,
conflict_list& conflicts)
: m_m(m)
, m_info(info)
, m_abstr_model(abstr_model)
, m_conflicts(conflicts)
, m_b_rw(m)
, m_bv_rw(m)
, m_empty_model(m)
{}
~imp() {
{
values2val_t::iterator i = m_values2val.begin();
const values2val_t::iterator e = m_values2val.end();
for (; i != e; ++i) {
m_m.dec_ref(i->m_key);
m_m.dec_ref(i->m_value.value);
m_m.dec_ref(i->m_value.source_term);
}
}
{
app2val_t::iterator i = m_app2val.begin();
const app2val_t::iterator e = m_app2val.end();
for (; i != e; ++i) {
m_m.dec_ref(i->m_value);
m_m.dec_ref(i->m_key);
}
}
}
//
// Returns true iff model was successfully constructed.
//
bool check() {
for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
func_decl * const c = m_abstr_model->get_constant(i);
app * const term = m_info->find_term(c);
if (term) m_stack.push_back(term);
else m_stack.push_back(m_m.mk_const(c));
}
return run();
}
void make_model(model_ref& destination) {
{
for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) {
sort * const s = m_abstr_model->get_uninterpreted_sort(i);
ptr_vector<expr> u = m_abstr_model->get_universe(s);
destination->register_usort(s, u.size(), u.c_ptr());
}
}
{
const app2val_t::iterator e = m_app2val.end();
app2val_t::iterator i = m_app2val.end();
for (; i != e; ++i) {
app * a = i->m_key;
if (a->get_num_args()) continue;
destination->register_decl(a->get_decl(), i->m_value);
}
}
obj_map<func_decl, func_interp*> interpretations;
{
const values2val_t::iterator e = m_values2val.end();
values2val_t::iterator i = m_values2val.end();
for (; i != e; ++i) add_entry(i->m_key, i->m_value.value, interpretations);
}
{
obj_map<func_decl, func_interp*>::iterator ie = interpretations.end();
obj_map<func_decl, func_interp*>::iterator ii = interpretations.begin();
for (; ii != ie; ++ii) {
func_decl* const fd = ii->m_key;
func_interp* const fi = ii->get_value();
fi->set_else(m_m.get_some_value(fd->get_range()));
destination->register_decl(fd, fi);
}
}
}
void add_entry(app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations) {
func_interp* fi = 0;
func_decl * const declaration = term->get_decl();
const unsigned sz = declaration->get_arity();
SASSERT(sz == term->get_num_args());
if (!interpretations.find(declaration, fi)) {
fi = alloc(func_interp, m_m, sz);
interpretations.insert(declaration, fi);
}
fi->insert_new_entry(term->get_args(), value);
}
private:
ast_manager& m_m;
ackr_info_ref m_info;
model_ref& m_abstr_model;
conflict_list& m_conflicts;
bool_rewriter m_b_rw;
bv_rewriter m_bv_rw;
scoped_ptr<model_evaluator> m_evaluator;
model m_empty_model;
private:
struct val_info { expr * value; app * source_term; };
typedef obj_map<app, expr *> app2val_t;
typedef obj_map<app, val_info> values2val_t;
values2val_t m_values2val;
app2val_t m_app2val;
ptr_vector<expr> m_stack;
static inline val_info mk_val_info(expr* value, app* source_term) {
val_info rv;
rv.value = value;
rv.source_term = source_term;
return rv;
}
//
// Performs congruence check on terms on the stack.
// (Currently stops upon the first failure).
// Returns true if and only if congruence check succeeded.
bool run() {
m_evaluator = alloc(model_evaluator, m_empty_model);
expr_mark visited;
expr * curr;
while (!m_stack.empty()) {
curr = m_stack.back();
if (visited.is_marked(curr)) {
m_stack.pop_back();
continue;
}
switch (curr->get_kind()) {
case AST_VAR:
UNREACHABLE();
return false;
case AST_APP: {
app * a = to_app(curr);
if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) {
visited.mark(a, true);
m_stack.pop_back();
if (!mk_value(a)) return false;
}
}
break;
case AST_QUANTIFIER:
UNREACHABLE();
return false;
default:
UNREACHABLE();
return false;
}
}
return true;
}
inline bool is_val(expr * e) {
if (!is_app(e)) return false;
return is_val(to_app(e));
}
inline bool is_val(app * a) {
const family_id fid = a->get_decl()->get_family_id();
const bool rv = fid != null_family_id && a->get_num_args() == 0;
SASSERT(rv == (m_bv_rw.is_numeral(a) || m_m.is_true(a) || m_m.is_false(a)));
return rv;
}
inline bool eval_cached(app * a, expr *& val) {
if (is_val(a)) { val = a; return true; }
return m_app2val.find(a, val);
}
bool evaluate(app * const a, expr_ref& result) {
SASSERT(!is_val(a));
const unsigned num = a->get_num_args();
if (num == 0) { // handle constants
make_value_constant(a, result);
return true;
}
// evaluate arguments
expr_ref_vector values(m_m);
values.reserve(num);
expr * const * args = a->get_args();
for (unsigned i = 0; i < num; ++i) {
expr * val;
const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); );
TRACE("model_constructor", tout <<
"arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
<< " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );
SASSERT(b);
values[i] = val;
}
// handle functions
if (a->get_family_id() == null_family_id) { // handle uninterpreted
app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m);
if (!make_value_uninterpreted_function(a, values, key.get(), result)) {
return false;
}
}
else { // handle interpreted
make_value_interpreted_function(a, values, result);
}
return true;
}
//
// Check and record the value for a given term, given that all arguments are already checked.
//
bool mk_value(app * a) {
if (is_val(a)) return true; // skip numerals
TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
SASSERT(!m_app2val.contains(a));
const unsigned num = a->get_num_args();
expr_ref result(m_m);
if (!evaluate(a, result)) return false;
SASSERT(is_val(result));
TRACE("model_constructor",
tout << "map term(\n" << mk_ismt2_pp(a, m_m, 2) << "\n->"
<< mk_ismt2_pp(result.get(), m_m, 2)<< ")\n"; );
CTRACE("model_constructor",
!is_val(result.get()),
tout << "eval fail\n" << mk_ismt2_pp(a, m_m, 2) << mk_ismt2_pp(result, m_m, 2) << "\n";
);
SASSERT(is_val(result.get()));
m_app2val.insert(a, result.get()); // memoize
m_m.inc_ref(a);
m_m.inc_ref(result.get());
return true;
}
// Constants from the abstract model are directly mapped to the concrete one.
void make_value_constant(app * const a, expr_ref& result) {
SASSERT(a->get_num_args() == 0);
func_decl * const fd = a->get_decl();
expr * val = m_abstr_model->get_const_interp(fd);
if (val == 0) { // TODO: avoid model completetion?
sort * s = fd->get_range();
val = m_abstr_model->get_some_value(s);
}
result = val;
}
bool make_value_uninterpreted_function(app* a,
expr_ref_vector& values,
app* key,
expr_ref& result) {
// get ackermann constant
app * const ac = m_info->get_abstr(a);
func_decl * const a_fd = a->get_decl();
SASSERT(ac->get_num_args() == 0);
SASSERT(a_fd->get_range() == ac->get_decl()->get_range());
expr_ref value(m_m);
value = m_abstr_model->get_const_interp(ac->get_decl());
// get ackermann constant's interpretation
if (value.get() == 0) { // TODO: avoid model completion?
sort * s = a_fd->get_range();
value = m_abstr_model->get_some_value(s);
}
// check congruence
val_info vi;
if(m_values2val.find(key,vi)) { // already is mapped to a value
SASSERT(vi.source_term);
const bool ok = vi.value == value;
if (!ok) {
TRACE("model_constructor",
tout << "already mapped by(\n" << mk_ismt2_pp(vi.source_term, m_m, 2) << "\n->"
<< mk_ismt2_pp(vi.value, m_m, 2) << ")\n"; );
m_conflicts.push_back(std::make_pair(a, vi.source_term));
}
result = vi.value;
return ok;
} else { // new value
result = value;
vi.value = value;
vi.source_term = a;
m_values2val.insert(key,vi);
m_m.inc_ref(vi.source_term);
m_m.inc_ref(vi.value);
m_m.inc_ref(key);
return true;
}
UNREACHABLE();
}
void make_value_interpreted_function(app* a,
expr_ref_vector& values,
expr_ref& result) {
const unsigned num = values.size();
func_decl * const fd = a->get_decl();
const family_id fid = fd->get_family_id();
expr_ref term(m_m);
term = m_m.mk_app(a->get_decl(), num, values.c_ptr());
m_evaluator->operator() (term, result);
TRACE("model_constructor",
tout << "eval(\n" << mk_ismt2_pp(term.get(), m_m, 2) << "\n->"
<< mk_ismt2_pp(result.get(), m_m, 2) << ")\n"; );
return;
if (fid == m_b_rw.get_fid()) {
decl_kind k = fd->get_decl_kind();
if (k == OP_EQ) {
// theory dispatch for =
SASSERT(num == 2);
family_id s_fid = m_m.get_sort(values.get(0))->get_family_id();
br_status st = BR_FAILED;
if (s_fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
} else {
br_status st = m_b_rw.mk_app_core(fd, num, values.c_ptr(), result);
}
} else {
br_status st = BR_FAILED;
if (fid == m_bv_rw.get_fid()) {
st = m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result);
}
else {
UNREACHABLE();
}
}
}
};
lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref info)
: m_imp(0)
, m_m(m)
, m_state(UNKNOWN)
, m_info(info)
, m_ref_count(0)
{}
lackr_model_constructor::~lackr_model_constructor() {
if (m_imp) dealloc(m_imp);
}
bool lackr_model_constructor::check(model_ref& abstr_model) {
m_conflicts.reset();
if (m_imp) {
dealloc(m_imp);
m_imp = 0;
}
m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts);
const bool rv = m_imp->check();
m_state = rv ? CHECKED : CONFLICT;
return rv;
}
void lackr_model_constructor::make_model(model_ref& model) {
SASSERT(m_state == CHECKED);
m_imp->make_model(model);
}

57
src/ackr/lackr_model_constructor.h
View file

@ -1,57 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
model_constructor.h
Abstract:
Given a propositional abstraction, attempt to construct a model.
Author:
Mikolas Janota
Revision History:
--*/
#ifndef LACKR_MODEL_CONSTRUCTOR_H_626
#define LACKR_MODEL_CONSTRUCTOR_H_626
#include"ast.h"
#include"ackr_info.h"
#include"model.h"
class lackr_model_constructor {
public:
typedef std::pair<app *, app *> app_pair;
typedef vector<app_pair> conflict_list;
lackr_model_constructor(ast_manager& m, ackr_info_ref info);
~lackr_model_constructor();
bool check(model_ref& abstr_model);
const conflict_list& get_conflicts() {
SASSERT(m_state == CONFLICT);
return m_conflicts;
}
void make_model(model_ref& model);
//
// Reference counting
//
void inc_ref() { ++m_ref_count; }
void dec_ref() {
--m_ref_count;
if (m_ref_count == 0) {
dealloc(this);
}
}
private:
struct imp;
imp * m_imp;
enum {CHECKED, CONFLICT, UNKNOWN} m_state;
conflict_list m_conflicts;
ast_manager& m_m;
const ackr_info_ref m_info;
unsigned m_ref_count; // reference counting
};
typedef ref<lackr_model_constructor> lackr_model_constructor_ref;
#endif /* MODEL_CONSTRUCTOR_H_626 */

138
src/ackr/lackr_model_converter.cpp
View file

@ -1,138 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_model_converter.cpp
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#include"lackr_model_converter.h"
#include"model_evaluator.h"
#include"ast_smt2_pp.h"
#include"ackr_info.h"
class lackr_model_converter : public model_converter {
public:
lackr_model_converter(ast_manager & m,
const ackr_info_ref& info,
model_ref& abstr_model)
: m(m)
, info(info)
, abstr_model(abstr_model)
{ }
virtual ~lackr_model_converter() { }
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
SASSERT(abstr_model.get());
model * new_model = alloc(model, m);
convert(abstr_model.get(), new_model);
md = new_model;
}
virtual void operator()(model_ref & md) {
operator()(md, 0);
}
//void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator) {
NOT_IMPLEMENTED_YET();
}
protected:
ast_manager& m;
const ackr_info_ref info;
model_ref abstr_model;
void convert(model * source, model * destination);
void add_entry(model_evaluator & evaluator,
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations);
void convert_sorts(model * source, model * destination);
void convert_constants(model * source, model * destination);
};
void lackr_model_converter::convert(model * source, model * destination) {
SASSERT(source->get_num_functions() == 0);
convert_constants(source,destination);
convert_sorts(source,destination);
}
void lackr_model_converter::convert_constants(model * source, model * destination) {
TRACE("lackr_model", tout << "converting constants\n";);
obj_map<func_decl, func_interp*> interpretations;
model_evaluator evaluator(*source);
for (unsigned i = 0; i < source->get_num_constants(); i++) {
func_decl * const c = source->get_constant(i);
app * const term = info->find_term(c);
expr * value = source->get_const_interp(c);
if(!term) {
destination->register_decl(c, value);
} else {
add_entry(evaluator, term, value, interpretations);
}
}
obj_map<func_decl, func_interp*>::iterator e = interpretations.end();
for (obj_map<func_decl, func_interp*>::iterator i = interpretations.begin();
i!=e; ++i) {
func_decl* const fd = i->m_key;
func_interp* const fi = i->get_value();
fi->set_else(m.get_some_value(fd->get_range()));
destination->register_decl(fd, fi);
}
}
void lackr_model_converter::add_entry(model_evaluator & evaluator,
app* term, expr* value,
obj_map<func_decl, func_interp*>& interpretations) {
TRACE("lackr_model", tout << "add_entry"
<< mk_ismt2_pp(term, m, 2)
<< "->"
<< mk_ismt2_pp(value, m, 2) << "\n";
);
func_interp* fi = 0;
func_decl * const declaration = term->get_decl();
const unsigned sz = declaration->get_arity();
SASSERT(sz == term->get_num_args());
if (!interpretations.find(declaration, fi)) {
fi = alloc(func_interp,m,sz);
interpretations.insert(declaration, fi);
}
expr_ref_vector args(m);
for (unsigned gi = 0; gi < sz; ++gi) {
expr * const arg = term->get_arg(gi);
expr_ref aarg(m);
info->abstract(arg, aarg);
expr_ref arg_value(m);
evaluator(aarg,arg_value);
args.push_back(arg_value);
}
if (fi->get_entry(args.c_ptr()) == 0) {
fi->insert_new_entry(args.c_ptr(), value);
} else {
TRACE("lackr_model", tout << "entry already present\n";);
}
}
void lackr_model_converter::convert_sorts(model * source, model * destination) {
for (unsigned i = 0; i < source->get_num_uninterpreted_sorts(); i++) {
sort * const s = source->get_uninterpreted_sort(i);
ptr_vector<expr> u = source->get_universe(s);
destination->register_usort(s, u.size(), u.c_ptr());
}
}
model_converter * mk_lackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) {
return alloc(lackr_model_converter, m, info, abstr_model);
}

22
src/ackr/lackr_model_converter.h
View file

@ -1,22 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_model_converter.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef LACKR_MODEL_CONVERTER_H_5814
#define LACKR_MODEL_CONVERTER_H_5814
#include"model_converter.h"
#include"ackr_info.h"
model_converter * mk_lackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
#endif /* LACKR_MODEL_CONVERTER_H_5814 */

60
src/ackr/lackr_model_converter_lazy.cpp
View file

@ -1,60 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_model_converter_lazy.cpp
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#include"lackr_model_converter_lazy.h"
#include"model_evaluator.h"
#include"ast_smt2_pp.h"
#include"ackr_info.h"
#include"lackr_model_constructor.h"
class lackr_model_converter_lazy : public model_converter {
public:
lackr_model_converter_lazy(ast_manager & m,
const lackr_model_constructor_ref& lmc)
: m(m)
, model_constructor(lmc)
{ }
virtual ~lackr_model_converter_lazy() { }
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
SASSERT(model_constructor.get());
model * new_model = alloc(model, m);
md = new_model;
model_constructor->make_model(md);
}
virtual void operator()(model_ref & md) {
operator()(md, 0);
}
//void display(std::ostream & out);
virtual model_converter * translate(ast_translation & translator) {
NOT_IMPLEMENTED_YET();
}
protected:
ast_manager& m;
const lackr_model_constructor_ref model_constructor;
};
model_converter * mk_lackr_model_converter_lazy(ast_manager & m,
const lackr_model_constructor_ref& model_constructor) {
return alloc(lackr_model_converter_lazy, m, model_constructor);
}

23
src/ackr/lackr_model_converter_lazy.h
View file

@ -1,23 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_model_converter_lazy.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef LACKR_MODEL_CONVERTER_LAZY_H_14201
#define LACKR_MODEL_CONVERTER_LAZY_H_14201
#include"model_converter.h"
#include"ackr_info.h"
model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
#endif /* LACKR_MODEL_CONVERTER_LAZY_H_14201 */

129
src/ackr/lackr_tactic.cpp
View file

@ -1,129 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_tactic.cpp
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#include"tactical.h"
///////////////
#include"solve_eqs_tactic.h"
#include"simplify_tactic.h"
#include"propagate_values_tactic.h"
#include"bit_blaster_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"max_bv_sharing_tactic.h"
#include"bv_size_reduction_tactic.h"
#include"ctx_simplify_tactic.h"
#include"nnf_tactic.h"
///////////////
#include"model_smt2_pp.h"
#include"cooperate.h"
#include"lackr.h"
#include"ackr_params.hpp"
#include"lackr_model_converter.h"
class lackr_tactic : public tactic {
public:
lackr_tactic(ast_manager& m, params_ref const& p)
: m_m(m)
, m_p(p)
{}
virtual ~lackr_tactic() { }
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0;
ast_manager& m(g->m());
TRACE("lackr", g->display(tout << "Goal:\n"););
// running implementation
expr_ref_vector flas(m);
const unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas);
const lbool o = imp->operator()();
flas.reset();
// report result
goal_ref resg(alloc(goal, *g, true));
if (o == l_false) resg->assert_expr(m.mk_false());
if (o != l_undef) result.push_back(resg.get());
// report model
if (g->models_enabled() && (o == l_true)) {
model_ref abstr_model = imp->get_model();
mc = mk_lackr_model_converter(m, imp->get_info(), abstr_model);
}
}
virtual void collect_statistics(statistics & st) const {
ackr_params p(m_p);
if (!p.eager()) st.update("lackr-its", m_st.m_it);
st.update("ackr-constraints", m_st.m_ackrs_sz);
}
virtual void reset_statistics() { m_st.reset(); }
virtual void cleanup() { }
virtual tactic* translate(ast_manager& m) {
return alloc(lackr_tactic, m, m_p);
}
private:
ast_manager& m_m;
params_ref m_p;
lackr_stats m_st;
};
tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p) {
//return and_then(mk_nnf_tactic(m_m, m_p), alloc(lackr_tactic, m_m, m_p));
//return alloc(lackr_tactic, m_m, m_p);
//params_ref main_p;
//main_p.set_bool("elim_and", true);
//main_p.set_bool("sort_store", true);
//main_p.set_bool("expand_select_store", true);
//main_p.set_bool("expand_store_eq", true);
params_ref simp2_p = p;
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("ite_extra_rules", true);
//simp2_p.set_bool("blast_eq_value", true);
//simp2_p.set_bool("bv_sort_ac", true);
params_ref ctx_simp_p;
ctx_simp_p.set_uint("max_depth", 32);
ctx_simp_p.set_uint("max_steps", 5000000);
tactic * const preamble_t = and_then(
mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
//using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
mk_solve_eqs_tactic(m),
mk_elim_uncnstr_tactic(m),
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
mk_max_bv_sharing_tactic(m),
//mk_macro_finder_tactic(m, p),
using_params(mk_simplify_tactic(m), simp2_p)
//, mk_simplify_tactic(m)
//mk_nnf_tactic(m_m, m_p)
);
return and_then(
preamble_t,
alloc(lackr_tactic, m, p));
}

28
src/ackr/lackr_tactic.h
View file

@ -1,28 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr_tactic.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef _LACKR_TACTIC_H_
#define _LACKR_TACTIC_H_
#include"tactical.h"
tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("lackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_lackr_tactic(m, p)")
*/
#endif