mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Cleanup in lackr.
This commit is contained in:
Mikolas Janota
parent
3dbc307ecd
commit
0fd61eee1f
3 changed files with 56 additions and 161 deletions
|
|
@ -22,57 +22,13 @@
|
|||
#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"inc_sat_solver.h"
|
||||
#include"qfaufbv_tactic.h"
|
||||
#include"qfbv_tactic.h"
|
||||
#include"tactic2solver.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, lackr_stats& st, expr_ref _f)
|
||||
: m_m(m)
|
||||
, m_p(p)
|
||||
|
|
@ -81,8 +37,7 @@ lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref _f)
|
|||
, m_sat(0)
|
||||
, m_bvutil(m)
|
||||
, m_simp(m)
|
||||
, m_ackrs(m)
|
||||
, m_cancel(0)
|
||||
, m_ackrs(m)
|
||||
, m_st(st)
|
||||
{
|
||||
m_fla = _f;
|
||||
|
|
@ -96,30 +51,22 @@ lackr::~lackr() {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
lbool lackr::operator() () {
|
||||
setup_sat();
|
||||
const bool ok = init();
|
||||
if (!ok) return l_undef;
|
||||
TRACE("lackr", tout << "sat goal\n"; m_sat->display(tout););
|
||||
init();
|
||||
const lbool rv = m_eager ? eager() : lazy();
|
||||
std::cout << "res: " << rv << "\n";
|
||||
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() {
|
||||
void 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;
|
||||
collect_terms();
|
||||
abstract();
|
||||
}
|
||||
|
||||
//
|
||||
|
|
@ -127,10 +74,9 @@ bool lackr::init() {
|
|||
//
|
||||
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";);
|
||||
<< mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
|
||||
const unsigned sz = t1->get_num_args();
|
||||
SASSERT(t2->get_num_args() == sz);
|
||||
expr_ref_vector eqs(m_m);
|
||||
for (unsigned gi = 0; gi < sz; ++gi) {
|
||||
expr * const arg1 = t1->get_arg(gi);
|
||||
|
|
@ -139,14 +85,13 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) {
|
||||
SASSERT(arg1 != arg2);
|
||||
TRACE("lackr", tout << "never eq\n";);
|
||||
return true;
|
||||
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);
|
||||
SASSERT(a2);
|
||||
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);
|
||||
|
|
@ -156,10 +101,10 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
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_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 true;
|
||||
if (m_m.is_true(cga)) return false;
|
||||
m_st.m_ackrs_sz++;
|
||||
m_ackrs.push_back(cga);
|
||||
return true;
|
||||
|
|
@ -168,12 +113,12 @@ bool lackr::ackr(app * const t1, app * const t2) {
|
|||
//
|
||||
// Introduce the ackermann lemma for each pair of terms.
|
||||
//
|
||||
bool lackr::eager_enc() {
|
||||
void lackr::eager_enc() {
|
||||
const fun2terms_map::iterator e = m_fun2terms.end();
|
||||
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
|
||||
checkpoint();
|
||||
func_decl* const fd = i->m_key;
|
||||
app_set * const ts = i->get_value();
|
||||
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;
|
||||
|
|
@ -184,14 +129,13 @@ bool lackr::eager_enc() {
|
|||
SASSERT(t1->get_decl() == fd);
|
||||
SASSERT(t2->get_decl() == fd);
|
||||
if (t1 == t2) continue;
|
||||
if (!ackr(t1,t2)) return false;
|
||||
ackr(t1,t2);
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool lackr::abstract() {
|
||||
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;
|
||||
|
|
@ -212,12 +156,10 @@ bool lackr::abstract() {
|
|||
}
|
||||
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;
|
||||
TRACE("lackr", tout << "abs(\n" << mk_ismt2_pp(m_abstr.get(), m_m, 2) << ")\n";);
|
||||
}
|
||||
|
||||
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;
|
||||
|
|
@ -235,25 +177,17 @@ void lackr::add_term(app* a) {
|
|||
lbool lackr::eager() {
|
||||
m_sat->assert_expr(m_abstr);
|
||||
TRACE("lackr", tout << "run sat 0\n"; );
|
||||
std::cout << "++sat call\n";
|
||||
const lbool rv0 = m_sat->check_sat(0, 0);
|
||||
std::cout << "--sat call\n";
|
||||
if (rv0 == l_false) return l_false;
|
||||
checkpoint();
|
||||
if (!eager_enc()) return l_undef;
|
||||
checkpoint();
|
||||
eager_enc();
|
||||
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_simp(all);
|
||||
m_sat->assert_expr(all);
|
||||
std::cout << "++sat call\n";
|
||||
const lbool rv = m_sat->check_sat(0, 0);
|
||||
std::cout << "--sat call\n";
|
||||
return rv;
|
||||
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);
|
||||
m_sat->assert_expr(m_abstr);
|
||||
|
|
@ -284,12 +218,10 @@ lbool lackr::lazy() {
|
|||
|
||||
void lackr::setup_sat() {
|
||||
if (m_use_sat) {
|
||||
//tactic_ref t = mk_qfbv_tactic(m_m, m_p);
|
||||
//m_sat = mk_tactic2solver(m_m, t.get(), m_p);
|
||||
m_sat = mk_inc_sat_solver(m_m, m_p);
|
||||
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);
|
||||
}
|
||||
|
|
@ -299,9 +231,9 @@ void lackr::setup_sat() {
|
|||
|
||||
|
||||
//
|
||||
// Collect all uninterpreted terms.
|
||||
// Collect all uninterpreted terms, skipping 0-arity.
|
||||
//
|
||||
bool lackr::collect_terms() {
|
||||
void lackr::collect_terms() {
|
||||
ptr_vector<expr> stack;
|
||||
expr * curr;
|
||||
expr_mark visited;
|
||||
|
|
@ -318,30 +250,23 @@ bool lackr::collect_terms() {
|
|||
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())) {
|
||||
{
|
||||
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(to_app(curr));
|
||||
checkpoint();
|
||||
add_term(a);
|
||||
}
|
||||
}
|
||||
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());
|
||||
}
|
||||
UNREACHABLE();
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
return;
|
||||
}
|
||||
}
|
||||
visited.reset();
|
||||
return true;
|
||||
visited.reset();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -17,16 +17,16 @@
|
|||
#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"
|
||||
#include"bv_decl_plugin.h"
|
||||
#include"lbool.h"
|
||||
#include"model.h"
|
||||
#include"solver.h"
|
||||
#include"util.h"
|
||||
#include"tactic_exception.h"
|
||||
|
||||
struct lackr_stats {
|
||||
lackr_stats() : m_it(0), m_ackrs_sz(0) {}
|
||||
|
|
@ -37,8 +37,7 @@ struct lackr_stats {
|
|||
|
||||
class lackr {
|
||||
public:
|
||||
lackr(ast_manager& m, params_ref p,lackr_stats& st,
|
||||
expr_ref _f);
|
||||
lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref _f);
|
||||
~lackr();
|
||||
void updt_params(params_ref const & _p) {
|
||||
ackr_params p(_p);
|
||||
|
|
@ -54,26 +53,14 @@ class lackr {
|
|||
inline model_ref get_model() { return m_model; }
|
||||
|
||||
//
|
||||
// timeout mechanisms
|
||||
// timeout mechanism
|
||||
//
|
||||
void checkpoint() {
|
||||
//std::cout << "chk\n";
|
||||
if (m_m.canceled()) {
|
||||
std::cout << "canceled\n";
|
||||
if (m_m.canceled()) {
|
||||
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;
|
||||
|
|
@ -88,33 +75,32 @@ class lackr {
|
|||
th_rewriter m_simp;
|
||||
expr_ref_vector m_ackrs;
|
||||
model_ref m_model;
|
||||
volatile bool m_cancel;
|
||||
bool m_eager;
|
||||
bool m_use_sat;
|
||||
lackr_stats& m_st;
|
||||
|
||||
bool init();
|
||||
void init();
|
||||
void setup_sat();
|
||||
lbool eager();
|
||||
lbool lazy();
|
||||
|
||||
//
|
||||
// Introduce ackermann lemma for the two given terms.
|
||||
// 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.
|
||||
//
|
||||
bool eager_enc();
|
||||
void eager_enc();
|
||||
|
||||
bool abstract();
|
||||
void abstract();
|
||||
|
||||
void add_term(app* a);
|
||||
|
||||
//
|
||||
// Collect all uninterpreted terms.
|
||||
// Collect all uninterpreted terms, skipping 0-arity.
|
||||
//
|
||||
bool collect_terms();
|
||||
void collect_terms();
|
||||
};
|
||||
#endif /* LACKR_H_15079 */
|
||||
|
|
|
|||
|
|
@ -36,12 +36,9 @@ 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 ~lackr_tactic() { }
|
||||
|
||||
virtual void operator()(goal_ref const & g,
|
||||
goal_ref_buffer & result,
|
||||
|
|
@ -57,8 +54,8 @@ public:
|
|||
expr_ref f(m);
|
||||
f = m.mk_and(flas.size(), flas.c_ptr());
|
||||
// running implementation
|
||||
m_imp = alloc(lackr, m, m_p, m_st, f);
|
||||
const lbool o = m_imp->operator()();
|
||||
scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, f);
|
||||
const lbool o = imp->operator()();
|
||||
flas.reset();
|
||||
// report result
|
||||
goal_ref resg(alloc(goal, *g, true));
|
||||
|
|
@ -66,16 +63,9 @@ public:
|
|||
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);
|
||||
model_ref abstr_model = imp->get_model();
|
||||
mc = mk_lackr_model_converter(m, imp->get_info(), abstr_model);
|
||||
}
|
||||
// cleanup
|
||||
lackr * d = m_imp;
|
||||
#pragma omp critical (lackr)
|
||||
{
|
||||
m_imp = 0;
|
||||
}
|
||||
dealloc(d);
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
|
|
@ -91,15 +81,9 @@ public:
|
|||
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;
|
||||
lackr_stats m_st;
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue