mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Adding ackr component.

Browse source
This commit is contained in:
Mikolas Janota 2015-12-15 18:43:36 +00:00
parent 90b1b07af4
commit c6e66ebc3a
11 changed files with 1236 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -76,10 +76,11 @@ def init_project_def():
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt')
add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')
add_lib('ackr', ['smt', 'smtlogic_tactics', 'sat_solver'], 'ackr')
API_files = ['z3_api.h', 'z3_ast_containers.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_fixedpoint.h', 'z3_optimization.h', 'z3_interp.h', 'z3_fpa.h']
add_lib('api', ['portfolio', 'smtparser', 'realclosure', 'interp', 'opt'],
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
add_exe('shell', ['api', 'sat', 'extra_cmds','opt','ackr'], exe_name='z3')
add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False)
_libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
reexports=['api'],

8
src/ackr/ackr.pyg Normal file
View file

@ -0,0 +1,8 @@
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'),
))

106
src/ackr/ackr_info.h Normal file
View file

@ -0,0 +1,106 @@
/*++
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"
//
// Information about how a formula was extracted into
// a formula without uninterpreted function symbols.
//
// The intended use is that new terms are added via set_abstr.
// Once all terms are abstracted, call seal.
// 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;
bool m_sealed; // debugging
unsigned m_ref_count; // reference counting
};
typedef ref<ackr_info> ackr_info_ref;
#endif /* ACKR_INFO_H_12278 */

337
src/ackr/lackr.cpp Normal file
View file

@ -0,0 +1,337 @@
/*++
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"array_decl_plugin.h"
#include"simplifier_plugin.h"
#include"basic_simplifier_plugin.h"
#include"array_simplifier_params.h"
#include"array_simplifier_plugin.h"
#include"bv_simplifier_plugin.h"
#include"bool_rewriter.h"
///////////////
#include"th_rewriter.h"
///////////////
#include"cooperate.h"
///////////////
#include"model_smt2_pp.h"
///////////////
struct simp_wrap {
inline void operator() (expr * s, expr_ref & r) {
proof_ref dummy(m);
simp(s, r, dummy);
}
simp_wrap(ast_manager& m)
: m(m)
, simp(m)
, bsp(m)
, bvsp(m, bsp, bv_par)
, asp(m, bsp, simp, ar_par)
{
params_ref p;
p.set_bool("local_ctx", true);
p.set_uint("local_ctx_limit", 10000000);
p.set_bool("ite_extra_rules", true);
bsp.get_rewriter().updt_params(p);
simp.register_plugin(&bsp);
simp.register_plugin(&bvsp);
}
~simp_wrap() {
simp.release_plugins();
}
ast_manager& m;
simplifier simp;
basic_simplifier_plugin bsp;
bv_simplifier_params bv_par;
bv_simplifier_plugin bvsp;
array_simplifier_params ar_par;
array_simplifier_plugin asp;
};
lackr::lackr(ast_manager& m, params_ref p, expr_ref _f)
: m_m(m)
, m_p(p)
, m_fla(m)
, m_abstr(m)
, m_sat(0)
, m_bvutil(m)
, m_simp(m)
, m_ackrs(m)
, m_cancel(0)
{
m_fla = _f;
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();
const bool ok = init();
if (!ok) return l_undef;
TRACE("lackr", tout << "sat goal\n"; m_sat->display(tout););
const lbool rv = m_eager ? eager() : lazy();
if (rv == l_true) m_sat->get_model(m_model);
TRACE("lackr", tout << "sat:" << rv << '\n'; );
CTRACE("lackr", rv == l_true,
model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
return rv;
}
bool lackr::init() {
params_ref simp_p(m_p);
m_simp.updt_params(simp_p);
m_info = alloc(ackr_info, m_m);
bool iok = collect_terms() && abstract();
if (!iok) return false;
return true;
}
//
// 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();
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)) {
SASSERT(arg1 != arg2);
TRACE("lackr", tout << "never eq\n";);
return true;
}
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);
SASSERT(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);
m_simp(cga);
TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
if (!m_m.is_true(cga)) m_ackrs.push_back(cga);
return true;
}
//
// Introduce the ackermann lemma for each pair of terms.
//
bool 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;
if (!ackr(t1,t2)) return false;
}
}
}
return true;
}
bool 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();
m_info->abstract(m_fla.get(), m_abstr);
TRACE("lackr", tout << "abs(\n" << mk_ismt2_pp(m_abstr.get(), m_m, 2) << ")\n";);
return true;
}
void lackr::add_term(app* a) {
//TRACE("lackr", tout << "inspecting term(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
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);
}
lbool lackr::eager() {
if (!eager_enc()) return l_undef;
m_sat->assert_expr(m_abstr);
TRACE("lackr", tout << "run sat 0\n"; );
if (m_sat->check_sat(0, 0) == l_false)
return l_false;
checkpoint();
expr_ref all(m_m);
all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
m_simp(all);
TRACE("lackr", tout << "run sat\n"; );
m_sat->assert_expr(all);
return m_sat->check_sat(0, 0);
}
lbool lackr::lazy() {
lackr_model_constructor mc(m_m, m_info);
m_sat->assert_expr(m_abstr);
unsigned ackr_head = 0;
unsigned it = 0;
while (1) {
checkpoint();
//std::cout << "it: " << ++it << "\n";
TRACE("lackr", tout << "lazy check\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) {
//std::cout << "; qfbv sat\n";
tactic_ref t = mk_qfbv_tactic(m_m, m_p);
m_sat = mk_tactic2solver(m_m, t.get(), m_p);
}
else {
//std::cout << "; smt sat\n";
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.
//
bool lackr::collect_terms() {
ptr_vector<expr> stack;
expr * curr;
expr_mark visited;
stack.push_back(m_fla.get());
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:
if (for_each_expr_args(stack, visited,
to_app(curr)->get_num_args(), to_app(curr)->get_args())) {
visited.mark(curr, true);
stack.pop_back();
add_term(to_app(curr));
}
break;
case AST_QUANTIFIER:
if (visited.is_marked(to_quantifier(curr)->get_expr())) {
visited.mark(curr, true);
stack.pop_back();
}
else {
stack.push_back(to_quantifier(curr)->get_expr());
}
break;
default:
UNREACHABLE();
return false;
}
}
visited.reset();
return true;
}

106
src/ackr/lackr.h Normal file
View file

@ -0,0 +1,106 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
lackr.h
Abstract:
Author:
Mikolas Janota
Revision History:
--*/
#ifndef LACKR_H_15079
#define LACKR_H_15079
///////////////
#include"inc_sat_solver.h"
#include"qfaufbv_tactic.h"
#include"qfbv_tactic.h"
#include"tactic2solver.h"
#include"ackr_info.h"
#include"ackr_params.hpp"
#include"tactic_exception.h"
#include"th_rewriter.h"
#include"bv_decl_plugin.h"
#include"cooperate.h"
class lackr {
public:
lackr(ast_manager& m, params_ref p, expr_ref _f);
lbool operator() ();
~lackr();
inline ackr_info_ref get_info() { return m_info; }
inline model_ref get_model() { return m_model; }
void updt_params(params_ref const & _p) {
ackr_params p(_p);
m_eager = p.eager();
m_use_sat = p.sat_backend();
}
//
// timeout mechanisms
//
void checkpoint() {
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
cooperate("lackr");
}
//virtual void set_cancel(bool f) {
// //#pragma omp critical (lackr_cancel)
// {
// m_cancel = f;
// if (m_sat == NULL) return;
// if (f) m_sat->cancel();
// else m_sat->reset_cancel();
// }
//}
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 m_fla;
expr_ref 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;
volatile bool m_cancel;
bool m_eager;
bool m_use_sat;
bool init();
void setup_sat();
lbool eager();
lbool lazy();
//
// Introduce ackermann lemma for the two given terms.
//
bool ackr(app * const t1, app * const t2);
//
// Introduce the ackermann lemma for each pair of terms.
//
bool eager_enc();
bool abstract();
void add_term(app* a);
//
// Collect all uninterpreted terms.
//
bool collect_terms();
};
#endif /* LACKR_H_15079 */

313
src/ackr/lackr_model_constructor.cpp Normal file
View file

@ -0,0 +1,313 @@
/*++
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,
vector<std::pair<app*,app*>>& 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();
}
private:
ast_manager& m_m;
ackr_info_ref m_info;
model_ref& m_abstr_model;
vector<std::pair<app*,app*>>& 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(m)
, state(UNKNOWN)
, info(info)
{}
bool lackr_model_constructor::check(model_ref& abstr_model) {
conflicts.reset();
lackr_model_constructor::imp i(m, info, abstr_model, conflicts);
const bool rv = i.check();
state = rv ? CHECKED : CONFLICT;
return rv;
}

40
src/ackr/lackr_model_constructor.h Normal file
View file

@ -0,0 +1,40 @@
/*++
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);
bool check(model_ref& abstr_model);
const conflict_list& get_conflicts() {
SASSERT(state == CONFLICT);
return conflicts;
}
private:
struct imp;
enum {CHECKED, CONFLICT, UNKNOWN} state;
conflict_list conflicts;
ast_manager& m;
const ackr_info_ref info;
};
#endif /* MODEL_CONSTRUCTOR_H_626 */

138
src/ackr/lackr_model_converter.cpp Normal file
View file

@ -0,0 +1,138 @@
/*++
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 Normal file
View file

@ -0,0 +1,22 @@
/*++
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 */

136
src/ackr/lackr_tactic.cpp Normal file
View file

@ -0,0 +1,136 @@
/*++
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"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)
, m_imp(0)
{}
virtual ~lackr_tactic() {
if (m_imp) dealloc(m_imp);
}
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"););
// conflate all assertions into one conjunction
ptr_vector<expr> flas;
g->get_formulas(flas);
expr_ref f(m);
f = m.mk_and(flas.size(), flas.c_ptr());
// running implementation
m_imp = alloc(lackr, m, m_p, f);
const lbool o = m_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 = m_imp->get_model();
mc = mk_lackr_model_converter(m, m_imp->get_info(), abstr_model);
}
// clenup
lackr * d = m_imp;
#pragma omp critical (lackr)
{
m_imp = 0;
}
dealloc(d);
}
virtual void cleanup() { }
virtual tactic* translate(ast_manager& m) {
return alloc(lackr_tactic, m, m_p);
}
// Currently tactics are not cancelable.
//virtual void set_cancel(bool f) {
// if (m_imp) m_imp->set_cancel(f);
//}
private:
ast_manager& m_m;
params_ref m_p;
lackr* m_imp;
};
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_nnf_tactic(m_m, m_p)
);
return and_then(
preamble_t,
alloc(lackr_tactic, m, p));
}

28
src/ackr/lackr_tactic.h Normal file
View file

@ -0,0 +1,28 @@
/*++
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", "lackr.", "mk_lackr_tactic(m, p)")
*/
#endif