mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
Further refactoring ackermannization.
This commit is contained in:
mikolas
parent
f3240024e7
commit
faa620f673
|
|
@ -36,6 +36,7 @@ def init_project_def():
|
||||||
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
|
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
|
||||||
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
|
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
|
||||||
add_lib('solver', ['model', 'tactic'])
|
add_lib('solver', ['model', 'tactic'])
|
||||||
|
add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
|
||||||
add_lib('interp', ['solver'])
|
add_lib('interp', ['solver'])
|
||||||
add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
|
add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
|
||||||
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
||||||
|
|
@ -52,7 +53,6 @@ def init_project_def():
|
||||||
add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
|
add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
|
||||||
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
|
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
|
||||||
'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
|
'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
|
||||||
add_lib('ackr', ['smt'], 'tactic/ackr')
|
|
||||||
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
|
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
|
||||||
add_lib('fuzzing', ['ast'], 'test/fuzzing')
|
add_lib('fuzzing', ['ast'], 'test/fuzzing')
|
||||||
add_lib('smt_tactic', ['smt'], 'smt/tactic')
|
add_lib('smt_tactic', ['smt'], 'smt/tactic')
|
||||||
|
|
@ -73,7 +73,7 @@ def init_project_def():
|
||||||
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
|
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
|
||||||
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
||||||
add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
|
add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
|
||||||
add_lib('smtlogic_tactics', ['ackr', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
|
add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
|
||||||
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
|
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
|
||||||
add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
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('smtparser', ['portfolio'], 'parsers/smt')
|
||||||
|
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
def_module_params('ackermannization',
|
|
||||||
description='solving UF via ackermannization',
|
|
||||||
export=True,
|
|
||||||
params=(
|
|
||||||
('eager', BOOL, True, 'eagerly instantiate all congruence rules'),
|
|
||||||
))
|
|
||||||
|
|
||||||
|
|
@ -1,22 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackermannize_bv_model_converter.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota (MikolasJanota)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#include"ackr_model_converter.h"
|
|
||||||
#include"ackermannize_bv_model_converter.h"
|
|
||||||
|
|
||||||
model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info) {
|
|
||||||
return mk_ackr_model_converter(m, info);
|
|
||||||
}
|
|
||||||
|
|
@ -1,25 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackermannize_bv_model_converter.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota (MikolasJanota)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef ACKERMANNIZE_BV_MODEL_CONVERTER_H_
|
|
||||||
#define ACKERMANNIZE_BV_MODEL_CONVERTER_H_
|
|
||||||
|
|
||||||
#include"model_converter.h"
|
|
||||||
#include"ackr_info.h"
|
|
||||||
|
|
||||||
model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info);
|
|
||||||
|
|
||||||
#endif /* ACKERMANNIZE_BV_MODEL_CONVERTER_H_ */
|
|
||||||
|
|
@ -1,99 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackermannize_bv_tactic.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#include"ackermannize_bv_tactic.h"
|
|
||||||
#include"tactical.h"
|
|
||||||
#include"lackr.h"
|
|
||||||
#include"ackr_params.hpp"
|
|
||||||
#include"model_smt2_pp.h"
|
|
||||||
#include"ackr_bound_probe.h"
|
|
||||||
#include"ackermannize_bv_tactic_params.hpp"
|
|
||||||
#include"ackermannize_bv_model_converter.h"
|
|
||||||
|
|
||||||
|
|
||||||
class ackermannize_bv_tactic : public tactic {
|
|
||||||
public:
|
|
||||||
ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
|
|
||||||
: m_m(m)
|
|
||||||
, m_p(p)
|
|
||||||
{}
|
|
||||||
|
|
||||||
virtual ~ackermannize_bv_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());
|
|
||||||
tactic_report report("ackermannize", *g);
|
|
||||||
fail_if_unsat_core_generation("ackermannize", g);
|
|
||||||
fail_if_proof_generation("ackermannize", g);
|
|
||||||
|
|
||||||
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, NULL);
|
|
||||||
flas.reset();
|
|
||||||
// mk result
|
|
||||||
goal_ref resg(alloc(goal, *g, true));
|
|
||||||
const bool success = imp->mk_ackermann(resg, m_lemma_limit);
|
|
||||||
if (!success) { // Just pass on the input unchanged
|
|
||||||
result.reset();
|
|
||||||
result.push_back(g.get());
|
|
||||||
mc = 0;
|
|
||||||
pc = 0;
|
|
||||||
core = 0;
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
result.push_back(resg.get());
|
|
||||||
// report model
|
|
||||||
if (g->models_enabled()) {
|
|
||||||
mc = mk_ackermannize_bv_model_converter(m, imp->get_info());
|
|
||||||
}
|
|
||||||
|
|
||||||
resg->inc_depth();
|
|
||||||
TRACE("ackermannize", resg->display(tout););
|
|
||||||
SASSERT(resg->is_well_sorted());
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void updt_params(params_ref const & _p) {
|
|
||||||
ackermannize_bv_tactic_params p(_p);
|
|
||||||
m_lemma_limit = p.div0_ackermann_limit();
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual void collect_statistics(statistics & st) const {
|
|
||||||
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(ackermannize_bv_tactic, m, m_p);
|
|
||||||
}
|
|
||||||
private:
|
|
||||||
ast_manager& m_m;
|
|
||||||
params_ref m_p;
|
|
||||||
lackr_stats m_st;
|
|
||||||
double m_lemma_limit;
|
|
||||||
};
|
|
||||||
|
|
||||||
tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p) {
|
|
||||||
return alloc(ackermannize_bv_tactic, m, p);
|
|
||||||
}
|
|
||||||
|
|
@ -1,28 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackermannize_bv_tactic.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#ifndef _ACKERMANNIZE_TACTIC_H_
|
|
||||||
#define _ACKERMANNIZE_TACTIC_H_
|
|
||||||
#include"tactical.h"
|
|
||||||
|
|
||||||
tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p);
|
|
||||||
|
|
||||||
/*
|
|
||||||
ADD_TACTIC("ackermannize_bv", "A tactic for performing full Ackermannization on bv instances.", "mk_ackermannize_bv_tactic(m, p)")
|
|
||||||
*/
|
|
||||||
|
|
||||||
#endif
|
|
||||||
|
|
||||||
|
|
@ -1,8 +0,0 @@
|
||||||
def_module_params(module_name='rewriter',
|
|
||||||
class_name='ackermannize_bv_tactic_params',
|
|
||||||
export=True,
|
|
||||||
params=(
|
|
||||||
("div0_ackermann_limit", UINT, 1000, "a bound for number of congruence Ackermann lemmas for div0 modelling"),
|
|
||||||
)
|
|
||||||
)
|
|
||||||
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
def_module_params('ackr',
|
|
||||||
description='solving UF via ackermannization',
|
|
||||||
export=True,
|
|
||||||
params=(
|
|
||||||
('eager', BOOL, True, 'eagerly instantiate all congruence rules'),
|
|
||||||
))
|
|
||||||
|
|
||||||
|
|
@ -1,77 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_bound_probe.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#include"ackr_helper.h"
|
|
||||||
#include"ackr_bound_probe.h"
|
|
||||||
#include"ast_smt2_pp.h"
|
|
||||||
|
|
||||||
/*
|
|
||||||
For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
|
|
||||||
The probe then sums up these for all functions.
|
|
||||||
This upper bound might be crude because some congruence lemmas trivially simplify to true.
|
|
||||||
*/
|
|
||||||
class ackr_bound_probe : public probe {
|
|
||||||
struct proc {
|
|
||||||
typedef ackr_helper::fun2terms_map fun2terms_map;
|
|
||||||
typedef ackr_helper::app_set app_set;
|
|
||||||
ast_manager& m_m;
|
|
||||||
fun2terms_map m_fun2terms; // a map from functions to occurrences
|
|
||||||
ackr_helper m_ackr_helper;
|
|
||||||
|
|
||||||
proc(ast_manager & m) : m_m(m), m_ackr_helper(m) { }
|
|
||||||
|
|
||||||
~proc() {
|
|
||||||
fun2terms_map::iterator it = m_fun2terms.begin();
|
|
||||||
const fun2terms_map::iterator end = m_fun2terms.end();
|
|
||||||
for (; it != end; ++it) dealloc(it->get_value());
|
|
||||||
}
|
|
||||||
|
|
||||||
void operator()(quantifier *) {}
|
|
||||||
void operator()(var *) {}
|
|
||||||
void operator()(app * a) {
|
|
||||||
if (a->get_num_args() == 0) return;
|
|
||||||
if (!m_ackr_helper.should_ackermannize(a)) return;
|
|
||||||
func_decl* const fd = a->get_decl();
|
|
||||||
app_set* ts = 0;
|
|
||||||
if (!m_fun2terms.find(fd, ts)) {
|
|
||||||
ts = alloc(app_set);
|
|
||||||
m_fun2terms.insert(fd, ts);
|
|
||||||
}
|
|
||||||
ts->insert(a);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
public:
|
|
||||||
ackr_bound_probe() {}
|
|
||||||
|
|
||||||
virtual result operator()(goal const & g) {
|
|
||||||
proc p(g.m());
|
|
||||||
unsigned sz = g.size();
|
|
||||||
expr_fast_mark1 visited;
|
|
||||||
for (unsigned i = 0; i < sz; i++) {
|
|
||||||
for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
|
|
||||||
}
|
|
||||||
const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
|
|
||||||
TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
|
|
||||||
return result(total);
|
|
||||||
}
|
|
||||||
|
|
||||||
inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
|
|
||||||
};
|
|
||||||
|
|
||||||
probe * mk_ackr_bound_probe() {
|
|
||||||
return alloc(ackr_bound_probe);
|
|
||||||
}
|
|
||||||
|
|
@ -1,29 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_bound_probe.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef ACKR_BOUND_PROBE_H_
|
|
||||||
#define ACKR_BOUND_PROBE_H_
|
|
||||||
|
|
||||||
#include"probe.h"
|
|
||||||
|
|
||||||
probe * mk_ackr_bound_probe();
|
|
||||||
|
|
||||||
/*
|
|
||||||
ADD_PROBE("ackr-bound-probe", "A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.", "mk_ackr_bound_probe()")
|
|
||||||
*/
|
|
||||||
|
|
||||||
#endif /* ACKR_BOUND_PROBE_H_ */
|
|
||||||
|
|
@ -1,29 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_helper.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota (MikolasJanota)
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#include"ackr_helper.h"
|
|
||||||
|
|
||||||
double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) {
|
|
||||||
fun2terms_map::iterator it = occurrences.begin();
|
|
||||||
const fun2terms_map::iterator end = occurrences.end();
|
|
||||||
double total = 0;
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
const unsigned fsz = it->m_value->size();
|
|
||||||
const double n2 = n_choose_2_chk(fsz);
|
|
||||||
total += n2;
|
|
||||||
}
|
|
||||||
return total;
|
|
||||||
}
|
|
||||||
|
|
@ -1,69 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2016 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_helper.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef ACKR_HELPER_H_
|
|
||||||
#define ACKR_HELPER_H_
|
|
||||||
|
|
||||||
#include"bv_decl_plugin.h"
|
|
||||||
|
|
||||||
class ackr_helper {
|
|
||||||
public:
|
|
||||||
typedef obj_hashtable<app> app_set;
|
|
||||||
typedef obj_map<func_decl, app_set*> fun2terms_map;
|
|
||||||
|
|
||||||
ackr_helper(ast_manager& m) : m_bvutil(m) {}
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Determines if a given function should be Ackermannized.
|
|
||||||
|
|
||||||
This includes all uninterpreted functions but also "special" functions, e.g. OP_BSMOD0,
|
|
||||||
which are not marked as uninterpreted but effectively are.
|
|
||||||
*/
|
|
||||||
inline bool should_ackermannize(app const * a) const {
|
|
||||||
if (a->get_family_id() == m_bvutil.get_family_id()) {
|
|
||||||
switch (a->get_decl_kind()) {
|
|
||||||
case OP_BSDIV0:
|
|
||||||
case OP_BUDIV0:
|
|
||||||
case OP_BSREM0:
|
|
||||||
case OP_BUREM0:
|
|
||||||
case OP_BSMOD0:
|
|
||||||
return true;
|
|
||||||
default:
|
|
||||||
return is_uninterp(a);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return (is_uninterp(a));
|
|
||||||
}
|
|
||||||
|
|
||||||
inline bv_util& bvutil() { return m_bvutil; }
|
|
||||||
|
|
||||||
/**
|
|
||||||
\brief Calculates an upper bound for congruence lemmas given a map of function of occurrences.
|
|
||||||
*/
|
|
||||||
static double calculate_lemma_bound(fun2terms_map& occurrences);
|
|
||||||
|
|
||||||
/** \brief Calculate n choose 2. **/
|
|
||||||
inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
|
|
||||||
|
|
||||||
/** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
|
|
||||||
inline static double n_choose_2_chk(unsigned n) {
|
|
||||||
SASSERT(std::numeric_limits<unsigned>().max() & 32);
|
|
||||||
return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
|
|
||||||
}
|
|
||||||
private:
|
|
||||||
bv_util m_bvutil;
|
|
||||||
};
|
|
||||||
#endif /* ACKR_HELPER_H_6475 */
|
|
||||||
|
|
@ -1,109 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2015 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_info.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef ACKR_INFO_H_
|
|
||||||
#define ACKR_INFO_H_
|
|
||||||
|
|
||||||
#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_ */
|
|
||||||
|
|
@ -1,153 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2015 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_model_converter.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#include"ackr_model_converter.h"
|
|
||||||
#include"model_evaluator.h"
|
|
||||||
#include"ast_smt2_pp.h"
|
|
||||||
#include"ackr_info.h"
|
|
||||||
|
|
||||||
|
|
||||||
class ackr_model_converter : public model_converter {
|
|
||||||
public:
|
|
||||||
ackr_model_converter(ast_manager & m,
|
|
||||||
const ackr_info_ref& info,
|
|
||||||
model_ref& abstr_model)
|
|
||||||
: m(m)
|
|
||||||
, info(info)
|
|
||||||
, abstr_model(abstr_model)
|
|
||||||
, fixed_model(true)
|
|
||||||
{ }
|
|
||||||
|
|
||||||
ackr_model_converter(ast_manager & m,
|
|
||||||
const ackr_info_ref& info)
|
|
||||||
: m(m)
|
|
||||||
, info(info)
|
|
||||||
, fixed_model(false)
|
|
||||||
{ }
|
|
||||||
|
|
||||||
virtual ~ackr_model_converter() { }
|
|
||||||
|
|
||||||
virtual void operator()(model_ref & md, unsigned goal_idx) {
|
|
||||||
SASSERT(goal_idx == 0);
|
|
||||||
SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
|
|
||||||
model_ref& old_model = fixed_model ? abstr_model : md;
|
|
||||||
SASSERT(old_model.get());
|
|
||||||
model * new_model = alloc(model, m);
|
|
||||||
convert(old_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;
|
|
||||||
bool fixed_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 ackr_model_converter::convert(model * source, model * destination) {
|
|
||||||
//SASSERT(source->get_num_functions() == 0);
|
|
||||||
for (unsigned i = 0; i < source->get_num_functions(); i++) {
|
|
||||||
func_decl * const fd = source->get_function(i);
|
|
||||||
func_interp * const fi = source->get_func_interp(fd);
|
|
||||||
destination->register_decl(fd, fi);
|
|
||||||
}
|
|
||||||
convert_constants(source,destination);
|
|
||||||
convert_sorts(source,destination);
|
|
||||||
}
|
|
||||||
|
|
||||||
void ackr_model_converter::convert_constants(model * source, model * destination) {
|
|
||||||
TRACE("ackr_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 ackr_model_converter::add_entry(model_evaluator & evaluator,
|
|
||||||
app* term, expr* value,
|
|
||||||
obj_map<func_decl, func_interp*>& interpretations) {
|
|
||||||
TRACE("ackr_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("ackr_model", tout << "entry already present\n";);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void ackr_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_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) {
|
|
||||||
return alloc(ackr_model_converter, m, info);
|
|
||||||
}
|
|
||||||
|
|
||||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) {
|
|
||||||
return alloc(ackr_model_converter, m, info, abstr_model);
|
|
||||||
}
|
|
||||||
|
|
@ -1,25 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2015 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
ackr_model_converter.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef ACKR_MODEL_CONVERTER_H_
|
|
||||||
#define ACKR_MODEL_CONVERTER_H_
|
|
||||||
|
|
||||||
#include"model_converter.h"
|
|
||||||
#include"ackr_info.h"
|
|
||||||
|
|
||||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
|
|
||||||
model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info);
|
|
||||||
|
|
||||||
#endif /* LACKR_MODEL_CONVERTER_H_ */
|
|
||||||
|
|
@ -1,285 +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"model_smt2_pp.h"
|
|
||||||
|
|
||||||
lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas,
|
|
||||||
solver * uffree_solver)
|
|
||||||
: m_m(m)
|
|
||||||
, m_p(p)
|
|
||||||
, m_formulas(formulas)
|
|
||||||
, m_abstr(m)
|
|
||||||
, m_sat(uffree_solver)
|
|
||||||
, m_ackr_helper(m)
|
|
||||||
, m_simp(m)
|
|
||||||
, m_ackrs(m)
|
|
||||||
, m_st(st)
|
|
||||||
, m_is_init(false)
|
|
||||||
{
|
|
||||||
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() () {
|
|
||||||
SASSERT(m_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;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
|
|
||||||
if (lemmas_upper_bound <= 0) return false;
|
|
||||||
init();
|
|
||||||
if (lemmas_upper_bound != std::numeric_limits<double>::infinity()) {
|
|
||||||
const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms);
|
|
||||||
if (lemmas_bound > lemmas_upper_bound) return false;
|
|
||||||
}
|
|
||||||
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));
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
void lackr::init() {
|
|
||||||
SASSERT(!m_is_init);
|
|
||||||
m_is_init = true;
|
|
||||||
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 i = 0; i < sz; ++i) {
|
|
||||||
expr * const arg1 = t1->get_arg(i);
|
|
||||||
expr * const arg2 = t2->get_arg(i);
|
|
||||||
if (arg1 == arg2) continue; // quickly skip syntactically equal
|
|
||||||
if (m_ackr_helper.bvutil().is_numeral(arg1) && m_ackr_helper.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() {
|
|
||||||
TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;);
|
|
||||||
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;
|
|
||||||
if (!m_ackr_helper.should_ackermannize(a)) return;
|
|
||||||
func_decl* const fd = a->get_decl();
|
|
||||||
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++));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//
|
|
||||||
// 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));
|
|
||||||
TRACE("lackr", tout << "infla: " <<mk_ismt2_pp(m_formulas.get(i), m_m, 2) << "\n";);
|
|
||||||
}
|
|
||||||
|
|
||||||
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();
|
|
||||||
}
|
|
||||||
|
|
@ -1,127 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2015 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
lackr.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Mikolas Janota
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
--*/
|
|
||||||
#ifndef LACKR_H_
|
|
||||||
#define LACKR_H_
|
|
||||||
|
|
||||||
#include"ackr_info.h"
|
|
||||||
#include"ackr_helper.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, solver * uffree_solver);
|
|
||||||
~lackr();
|
|
||||||
void updt_params(params_ref const & _p) {
|
|
||||||
ackr_params p(_p);
|
|
||||||
m_eager = p.eager();
|
|
||||||
}
|
|
||||||
|
|
||||||
/** \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 procedure guarantees a equisatisfiability with the input formula and it has a worst-case quadratic blowup.
|
|
||||||
Before ackermannization an upper bound on congruence lemmas is computed and tested against \p lemmas_upper_bound.
|
|
||||||
If this bound is exceeded, the function returns false, it returns true otherwise.
|
|
||||||
**/
|
|
||||||
bool mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound);
|
|
||||||
|
|
||||||
//
|
|
||||||
// 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 ackr_helper::fun2terms_map fun2terms_map;
|
|
||||||
typedef ackr_helper::app_set app_set;
|
|
||||||
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;
|
|
||||||
solver* m_sat;
|
|
||||||
ackr_helper m_ackr_helper;
|
|
||||||
th_rewriter m_simp;
|
|
||||||
expr_ref_vector m_ackrs;
|
|
||||||
model_ref m_model;
|
|
||||||
bool m_eager;
|
|
||||||
lackr_stats& m_st;
|
|
||||||
bool m_is_init;
|
|
||||||
|
|
||||||
void init();
|
|
||||||
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_ */
|
|
||||||
|
|
@ -1,377 +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)
|
|
||||||
, m_ackr_helper(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());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
|
|
||||||
func_decl * const fd = m_abstr_model->get_function(i);
|
|
||||||
func_interp * const fi = m_abstr_model->get_func_interp(fd);
|
|
||||||
destination->register_decl(fd, fi);
|
|
||||||
}
|
|
||||||
|
|
||||||
{
|
|
||||||
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;
|
|
||||||
ackr_helper m_ackr_helper;
|
|
||||||
|
|
||||||
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) { return m_m.is_value(e); }
|
|
||||||
|
|
||||||
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 (m_ackr_helper.should_ackermannize(a)) { // 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);
|
|
||||||
}
|
|
||||||
|
|
@ -1,61 +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_
|
|
||||||
#define LACKR_MODEL_CONSTRUCTOR_H_
|
|
||||||
|
|
||||||
#include"ast.h"
|
|
||||||
#include"ackr_info.h"
|
|
||||||
#include"ackr_helper.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_ */
|
|
||||||
|
|
@ -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);
|
|
||||||
}
|
|
||||||
|
|
@ -1,25 +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_
|
|
||||||
#define LACKR_MODEL_CONVERTER_LAZY_H_
|
|
||||||
|
|
||||||
#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_ */
|
|
||||||
|
|
@ -32,6 +32,7 @@ Notes:
|
||||||
#include"model_smt2_pp.h"
|
#include"model_smt2_pp.h"
|
||||||
#include"cooperate.h"
|
#include"cooperate.h"
|
||||||
#include"lackr.h"
|
#include"lackr.h"
|
||||||
|
#include"ackermannization_params.hpp"
|
||||||
#include"qfufbv_ackr_model_converter.h"
|
#include"qfufbv_ackr_model_converter.h"
|
||||||
///////////////
|
///////////////
|
||||||
#include"inc_sat_solver.h"
|
#include"inc_sat_solver.h"
|
||||||
|
|
@ -87,7 +88,7 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
virtual void collect_statistics(statistics & st) const {
|
virtual void collect_statistics(statistics & st) const {
|
||||||
ackr_params p(m_p);
|
ackermannization_params p(m_p);
|
||||||
if (!p.eager()) st.update("lackr-its", m_st.m_it);
|
if (!p.eager()) st.update("lackr-its", m_st.m_it);
|
||||||
st.update("ackr-constraints", m_st.m_ackrs_sz);
|
st.update("ackr-constraints", m_st.m_ackrs_sz);
|
||||||
}
|
}
|
||||||
|
|
@ -172,9 +173,7 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
|
||||||
tactic * const preamble_st = mk_qfufbv_preamble(m, p);
|
tactic * const preamble_st = mk_qfufbv_preamble(m, p);
|
||||||
|
|
||||||
tactic * st = using_params(and_then(preamble_st,
|
tactic * st = using_params(and_then(preamble_st,
|
||||||
cond(mk_is_qfbv_probe(),
|
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic())),
|
||||||
mk_qfbv_tactic(m),
|
|
||||||
mk_smt_tactic())),
|
|
||||||
main_p);
|
main_p);
|
||||||
|
|
||||||
st->updt_params(p);
|
st->updt_params(p);
|
||||||
|
|
@ -187,4 +186,4 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
|
||||||
tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
|
tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
|
||||||
return and_then(preamble_t,
|
return and_then(preamble_t,
|
||||||
cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
|
cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue