mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

bindings --> api; and moved nlsat/sat/subpaving tactics

Browse source
This commit is contained in:
Leonardo de Moura 2012-10-31 13:24:39 -07:00
parent ccdb253b47
commit a274cac2a0
123 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

309
src/tactic/nlsat/goal2nlsat.cpp
View file

@ -1,309 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
goal2nlsat.cpp
Abstract:
"Compile" a goal into the nonlinear arithmetic engine.
Non-arithmetic atoms are "abstracted" into boolean variables.
Non-supported terms are "abstracted" into variables.
The mappings can be used to convert back the state of the
engine into a goal.
Author:
Leonardo (leonardo) 2012-01-02
Notes:
--*/
#include"goal2nlsat.h"
#include"goal.h"
#include"goal_util.h"
#include"nlsat_solver.h"
#include"expr2polynomial.h"
#include"expr2var.h"
#include"arith_decl_plugin.h"
#include"tactic.h"
#include"ast_smt2_pp.h"
struct goal2nlsat::imp {
struct nlsat_expr2polynomial : public expr2polynomial {
nlsat::solver & m_solver;
nlsat_expr2polynomial(nlsat::solver & s, ast_manager & m, polynomial::manager & pm, expr2var * e2v):
expr2polynomial(m, pm, e2v),
m_solver(s) {
}
virtual bool is_int(polynomial::var x) const {
return m_solver.is_int(x);
}
virtual polynomial::var mk_var(bool is_int) {
return m_solver.mk_var(is_int);
}
};
ast_manager & m;
nlsat::solver & m_solver;
polynomial::manager & m_pm;
unsynch_mpq_manager & m_qm;
arith_util m_util;
expr2var & m_a2b;
expr2var & m_t2x;
nlsat_expr2polynomial m_expr2poly;
polynomial::factor_params m_fparams;
unsigned long long m_max_memory;
bool m_factor;
volatile bool m_cancel;
imp(ast_manager & _m, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x):
m(_m),
m_solver(s),
m_pm(s.pm()),
m_qm(s.qm()),
m_util(m),
m_a2b(a2b),
m_t2x(t2x),
m_expr2poly(m_solver, m, m_solver.pm(), &m_t2x) {
updt_params(p);
m_cancel = false;
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_factor = p.get_bool(":factor", true);
m_fparams.updt_params(p);
}
void set_cancel(bool f) {
m_cancel = f;
m_pm.set_cancel(f);
}
nlsat::atom::kind flip(nlsat::atom::kind k) {
switch (k) {
case nlsat::atom::EQ: return k;
case nlsat::atom::LT: return nlsat::atom::GT;
case nlsat::atom::GT: return nlsat::atom::LT;
default:
UNREACHABLE();
return k;
}
}
nlsat::bool_var factor_atom(polynomial::polynomial * p, nlsat::atom::kind k) {
sbuffer<bool> is_even;
ptr_buffer<polynomial::polynomial> ps;
polynomial::factors fs(m_pm);
m_pm.factor(p, fs, m_fparams);
TRACE("goal2nlsat_bug", tout << "factors:\n" << fs << "\n";);
SASSERT(fs.distinct_factors() > 0);
for (unsigned i = 0; i < fs.distinct_factors(); i++) {
ps.push_back(fs[i]);
is_even.push_back(fs.get_degree(i) % 2 == 0);
}
if (m_qm.is_neg(fs.get_constant()))
k = flip(k);
return m_solver.mk_ineq_atom(k, ps.size(), ps.c_ptr(), is_even.c_ptr());
}
nlsat::literal process_atom(app * f, nlsat::atom::kind k) {
SASSERT(f->get_num_args() == 2);
expr * lhs = f->get_arg(0);
expr * rhs = f->get_arg(1);
polynomial_ref p1(m_pm);
polynomial_ref p2(m_pm);
scoped_mpz d1(m_qm);
scoped_mpz d2(m_qm);
m_expr2poly.to_polynomial(lhs, p1, d1);
m_expr2poly.to_polynomial(rhs, p2, d2);
scoped_mpz lcm(m_qm);
m_qm.lcm(d1, d2, lcm);
m_qm.div(lcm, d1, d1);
m_qm.div(lcm, d2, d2);
m_qm.neg(d2);
polynomial_ref p(m_pm);
p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
TRACE("goal2nlsat_bug", tout << "p: " << p << "\nk: " << k << "\n";);
if (is_const(p)) {
int sign;
if (is_zero(p))
sign = 0;
else
sign = m_qm.is_pos(m_pm.coeff(p, 0)) ? 1 : -1;
switch (k) {
case nlsat::atom::EQ: return sign == 0 ? nlsat::true_literal : nlsat::false_literal;
case nlsat::atom::LT: return sign < 0 ? nlsat::true_literal : nlsat::false_literal;
case nlsat::atom::GT: return sign > 0 ? nlsat::true_literal : nlsat::false_literal;
default:
UNREACHABLE();
return nlsat::true_literal;
}
}
if (m_factor) {
return nlsat::literal(factor_atom(p, k), false);
}
else {
bool is_even = false;
polynomial::polynomial * _p = p.get();
return nlsat::literal(m_solver.mk_ineq_atom(k, 1, &_p, &is_even), false);
}
}
nlsat::literal process_eq(app * f) {
return process_atom(f, nlsat::atom::EQ);
}
nlsat::literal process_le(app * f) {
return ~process_atom(f, nlsat::atom::GT);
}
nlsat::literal process_ge(app * f) {
return ~process_atom(f, nlsat::atom::LT);
}
// everything else is compiled as a boolean variable
nlsat::bool_var process_bvar(expr * f) {
if (m_a2b.is_var(f)) {
return static_cast<nlsat::bool_var>(m_a2b.to_var(f));
}
else {
nlsat::bool_var b = m_solver.mk_bool_var();
m_a2b.insert(f, b);
return b;
}
}
nlsat::literal process_atom(expr * f) {
if (m.is_eq(f)) {
if (m_util.is_int_real(to_app(f)->get_arg(0)))
return process_eq(to_app(f));
else
return nlsat::literal(process_bvar(f), false);
}
else if (m_util.is_le(f)) {
return process_le(to_app(f));
}
else if (m_util.is_ge(f)) {
return process_ge(to_app(f));
}
else if (is_app(f)) {
if (to_app(f)->get_family_id() == m.get_basic_family_id()) {
switch (to_app(f)->get_decl_kind()) {
case OP_TRUE:
case OP_FALSE:
TRACE("goal2nlsat", tout << "f: " << mk_ismt2_pp(f, m) << "\n";);
throw tactic_exception("apply simplify before applying nlsat");
case OP_AND:
case OP_OR:
case OP_IFF:
case OP_XOR:
case OP_NOT:
case OP_IMPLIES:
throw tactic_exception("convert goal into cnf before applying nlsat");
case OP_DISTINCT:
throw tactic_exception("eliminate distinct operator (use tactic '(using-params simplify :blast-distinct true)') before applying nlsat");
default:
UNREACHABLE();
return nlsat::literal(nlsat::null_bool_var, false);
}
}
else if (to_app(f)->get_family_id() == m_util.get_family_id()) {
throw tactic_exception("apply purify-arith before applying nlsat");
}
else {
return nlsat::literal(process_bvar(f), false);
}
}
else {
SASSERT(is_quantifier(f));
return nlsat::literal(process_bvar(f), false);
}
}
nlsat::literal process_literal(expr * f) {
bool neg = false;
while (m.is_not(f, f))
neg = !neg;
nlsat::literal l = process_atom(f);
if (neg)
l.neg();
return l;
}
void process(expr * f, expr_dependency * dep) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
sbuffer<nlsat::literal> ls;
for (unsigned i = 0; i < num_lits; i++) {
ls.push_back(process_literal(lits[i]));
}
m_solver.mk_clause(ls.size(), ls.c_ptr(), dep);
}
void operator()(goal const & g) {
if (has_term_ite(g))
throw tactic_exception("eliminate term-ite before applying nlsat");
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
process(g.form(i), g.dep(i));
}
}
};
struct goal2nlsat::scoped_set_imp {
goal2nlsat & m_owner;
scoped_set_imp(goal2nlsat & o, imp & i):m_owner(o) {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = &i;
}
}
~scoped_set_imp() {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = 0;
}
}
};
goal2nlsat::goal2nlsat() {
m_imp = 0;
}
goal2nlsat::~goal2nlsat() {
SASSERT(m_imp == 0);
}
void goal2nlsat::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert(":factor", CPK_BOOL, "(default: true) factor polynomials.");
polynomial::factor_params::get_param_descrs(r);
}
void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x) {
imp local_imp(g.m(), p, s, a2b, t2x);
scoped_set_imp setter(*this, local_imp);
local_imp(g);
}
void goal2nlsat::set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}

75
src/tactic/nlsat/goal2nlsat.h
View file

@ -1,75 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
goal2nlsat.h
Abstract:
"Compile" a goal into the nonlinear arithmetic engine.
Non-arithmetic atoms are "abstracted" into boolean variables.
Non-supported terms are "abstracted" into variables.
The mappings can be used to convert back the state of the
engine into a goal.
Author:
Leonardo (leonardo) 2012-01-02
Notes:
--*/
#ifndef _GOAL2NLSAT_H_
#define _GOAL2NLSAT_H_
#include"nlsat_types.h"
#include"model_converter.h"
class goal;
class expr2var;
class goal2nlsat {
struct imp;
imp * m_imp;
struct scoped_set_imp;
public:
goal2nlsat();
~goal2nlsat();
static void collect_param_descrs(param_descrs & r);
/**
\brief "Compile" the goal into the given nlsat engine.
Store a mapping from atoms to boolean variables into a2b.
Store a mapping from terms into arithmetic variables into t2x.
\remark a2b and t2x m don't need to be empty. The definitions there are reused.
The input is expected to be in CNF
*/
void operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x);
void set_cancel(bool f);
};
class nlsat2goal {
struct imp;
imp * m_imp;
public:
nlsat2goal();
~nlsat2goal();
static void collect_param_descrs(param_descrs & r);
/**
\brief Translate the state of the nlsat engine back into a goal.
*/
void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x,
params_ref const & p, goal & g, model_converter_ref & mc);
void set_cancel(bool f);
};
#endif

259
src/tactic/nlsat/nlsat_tactic.cpp
View file

@ -1,259 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
nlsat_tactic.cpp
Abstract:
Tactic for using nonlinear procedure.
Author:
Leonardo (leonardo) 2012-01-02
Notes:
--*/
#include"tactical.h"
#include"goal2nlsat.h"
#include"nlsat_solver.h"
#include"model.h"
#include"expr2var.h"
#include"arith_decl_plugin.h"
#include"ast_smt2_pp.h"
#include"z3_exception.h"
#include"algebraic_numbers.h"
class nlsat_tactic : public tactic {
struct expr_display_var_proc : public nlsat::display_var_proc {
ast_manager & m;
expr_ref_vector m_var2expr;
expr_display_var_proc(ast_manager & _m):m(_m), m_var2expr(_m) {}
virtual void operator()(std::ostream & out, nlsat::var x) const {
if (x < m_var2expr.size())
out << mk_ismt2_pp(m_var2expr.get(x), m);
else
out << "x!" << x;
}
};
struct imp {
ast_manager & m;
params_ref m_params;
expr_display_var_proc m_display_var;
nlsat::solver m_solver;
goal2nlsat m_g2nl;
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_params(p),
m_display_var(_m),
m_solver(p) {
}
void updt_params(params_ref const & p) {
m_params = p;
m_solver.updt_params(p);
}
void set_cancel(bool f) {
m_solver.set_cancel(f);
m_g2nl.set_cancel(f);
}
bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) {
for (unsigned x = 0; x < x2t.size(); x++) {
if (!is_uninterp_const(x2t.get(x))) {
TRACE("unsupported", tout << "unsupported atom:\n" << mk_ismt2_pp(x2t.get(x), m) << "\n";);
return true;
}
}
for (unsigned b = 0; b < b2a.size(); b++) {
expr * a = b2a.get(b);
if (a == 0)
continue;
if (is_uninterp_const(a))
continue;
if (m_solver.is_interpreted(b))
continue; // arithmetic atom
TRACE("unsupported", tout << "unsupported atom:\n" << mk_ismt2_pp(a, m) << "\n";);
return true; // unsupported
}
return false;
}
// Return false if nlsat assigned noninteger value to an integer variable.
bool mk_model(expr_ref_vector & b2a, expr_ref_vector & x2t, model_converter_ref & mc) {
bool ok = true;
model_ref md = alloc(model, m);
arith_util util(m);
for (unsigned x = 0; x < x2t.size(); x++) {
expr * t = x2t.get(x);
if (!is_uninterp_const(t))
continue;
expr * v;
try {
v = util.mk_numeral(m_solver.value(x), util.is_int(t));
}
catch (z3_error & ex) {
throw ex;
}
catch (z3_exception &) {
v = util.mk_to_int(util.mk_numeral(m_solver.value(x), false));
ok = false;
}
md->register_decl(to_app(t)->get_decl(), v);
}
for (unsigned b = 0; b < b2a.size(); b++) {
expr * a = b2a.get(b);
if (a == 0 || !is_uninterp_const(a))
continue;
lbool val = m_solver.bvalue(b);
if (val == l_undef)
continue; // don't care
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
}
mc = model2model_converter(md.get());
return ok;
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("nlsat", *g);
if (g->is_decided()) {
result.push_back(g.get());
return;
}
fail_if_proof_generation("nlsat", g);
expr2var a2b(m);
expr2var t2x(m);
m_g2nl(*g, m_params, m_solver, a2b, t2x);
m_display_var.m_var2expr.reset();
t2x.mk_inv(m_display_var.m_var2expr);
m_solver.set_display_var(m_display_var);
lbool st = m_solver.check();
if (st == l_undef) {
}
else if (st == l_true) {
expr_ref_vector x2t(m);
expr_ref_vector b2a(m);
a2b.mk_inv(b2a);
t2x.mk_inv(x2t);
if (!contains_unsupported(b2a, x2t)) {
// If mk_model is false it means that the model produced by nlsat
// assigns noninteger values to integer variables
if (mk_model(b2a, x2t, mc)) {
// result goal is trivially SAT
g->reset();
}
}
}
else {
// TODO: extract unsat core
g->assert_expr(m.mk_false(), 0, 0);
}
g->inc_depth();
result.push_back(g.get());
TRACE("nlsat", g->display(tout););
SASSERT(g->is_well_sorted());
}
};
imp * m_imp;
params_ref m_params;
statistics m_stats;
struct scoped_set_imp {
nlsat_tactic & m_owner;
scoped_set_imp(nlsat_tactic & o, imp & i):m_owner(o) {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = &i;
}
}
~scoped_set_imp() {
m_owner.m_imp->m_solver.collect_statistics(m_owner.m_stats);
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = 0;
}
}
};
public:
nlsat_tactic(params_ref const & p):
m_params(p) {
m_imp = 0;
}
virtual tactic * translate(ast_manager & m) {
return alloc(nlsat_tactic, m_params);
}
virtual ~nlsat_tactic() {
SASSERT(m_imp == 0);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
}
virtual void collect_param_descrs(param_descrs & r) {
goal2nlsat::collect_param_descrs(r);
nlsat::solver::collect_param_descrs(r);
algebraic_numbers::manager::collect_param_descrs(r);
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
imp local_imp(in->m(), m_params);
scoped_set_imp setter(*this, local_imp);
local_imp(in, result, mc, pc, core);
}
catch (z3_error & ex) {
throw ex;
}
catch (z3_exception & ex) {
// convert all Z3 exceptions into tactic exceptions.
throw tactic_exception(ex.msg());
}
}
virtual void cleanup() {}
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void reset_statistics() {
m_stats.reset();
}
};
tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(nlsat_tactic, p));
}

32
src/tactic/nlsat/nlsat_tactic.h
View file

@ -1,32 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
nlsat_tactic.h
Abstract:
Tactic for using nonlinear procedure.
Author:
Leonardo (leonardo) 2012-01-02
Notes:
--*/
#ifndef _NLSAT_TACTIC_H_
#define _NLSAT_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC('nlsat', '(try to) solve goal using a nonlinear arithmetic solver.', 'mk_nlsat_tactic(m, p)')
*/
#endif

63
src/tactic/nlsat/qfnra_nlsat_tactic.cpp
View file

@ -1,63 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
qfnra_nlsat_tactic.h
Abstract:
Tactic based on nlsat for solving QF_NRA problems
Author:
Leonardo (leonardo) 2012-01-23
Notes:
--*/
#include"tactical.h"
#include"tseitin_cnf_tactic.h"
#include"degree_shift_tactic.h"
#include"purify_arith_tactic.h"
#include"nlsat_tactic.h"
#include"factor_tactic.h"
#include"simplify_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"propagate_values_tactic.h"
#include"solve_eqs_tactic.h"
#include"elim_term_ite_tactic.h"
tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p = p;
main_p.set_bool(":elim-and", true);
main_p.set_bool(":blast-distinct", true);
params_ref purify_p = p;
purify_p.set_bool(":complete", false); // temporary hack, solver does not support uninterpreted functions for encoding (div0 x) applications. So, we replace it application of this kind with an uninterpreted function symbol.
tactic * factor;
if (p.get_bool(":factor", true))
factor = mk_factor_tactic(m, p);
else
factor = mk_skip_tactic();
return and_then(and_then(using_params(mk_simplify_tactic(m, p),
main_p),
using_params(mk_purify_arith_tactic(m, p),
purify_p),
mk_propagate_values_tactic(m, p),
mk_solve_eqs_tactic(m, p),
mk_elim_uncnstr_tactic(m, p),
mk_elim_term_ite_tactic(m, p)),
and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
factor,
mk_solve_eqs_tactic(m, p),
using_params(mk_simplify_tactic(m, p),
main_p),
mk_tseitin_cnf_core_tactic(m, p),
using_params(mk_simplify_tactic(m, p),
main_p),
mk_nlsat_tactic(m, p)));
}

34
src/tactic/nlsat/qfnra_nlsat_tactic.h
View file

@ -1,34 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
qfnra_nlsat_tactic.h
Abstract:
Tactic based on nlsat for solving QF_NRA problems
Author:
Leonardo (leonardo) 2012-01-23
Notes:
--*/
#ifndef _QFNRA_NLSAT_TACTIC_H_
#define _QFNRA_NLSAT_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p));
/*
ADD_TACTIC("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", "mk_qfnra_nlsat_tactic(m, p)")
*/
#endif

116
src/tactic/sat/atom2bool_var.cpp
View file

@ -1,116 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
atom2bool_var.cpp
Abstract:
The mapping between SAT boolean variables and atoms
Author:
Leonardo (leonardo) 2011-10-25
Notes:
--*/
#include"atom2bool_var.h"
#include"ast_smt2_pp.h"
#include"ref_util.h"
#include"goal.h"
void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
obj_map<expr, var>::iterator it = m_mapping.begin();
obj_map<expr, var>::iterator end = m_mapping.end();
for (; it != end; ++it) {
sat::literal l(static_cast<sat::bool_var>(it->m_value), false);
lit2expr.set(l.index(), it->m_key);
l.neg();
lit2expr.set(l.index(), m().mk_not(it->m_key));
}
}
sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
sat::bool_var v = sat::null_bool_var;
m_mapping.find(n, v);
return v;
}
struct collect_boolean_interface_proc {
struct visitor {
obj_hashtable<expr> & m_r;
visitor(obj_hashtable<expr> & r):m_r(r) {}
void operator()(var * n) {}
void operator()(app * n) { if (is_uninterp_const(n)) m_r.insert(n); }
void operator()(quantifier * n) {}
};
ast_manager & m;
expr_fast_mark2 fvisited;
expr_fast_mark1 tvisited;
ptr_vector<expr> todo;
visitor proc;
collect_boolean_interface_proc(ast_manager & _m, obj_hashtable<expr> & r):
m(_m),
proc(r) {
}
void process(expr * f) {
if (fvisited.is_marked(f))
return;
fvisited.mark(f);
todo.push_back(f);
while (!todo.empty()) {
expr * t = todo.back();
todo.pop_back();
if (is_uninterp_const(t))
continue;
if (is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0) {
decl_kind k = to_app(t)->get_decl_kind();
if (k == OP_OR || k == OP_NOT || k == OP_IFF || ((k == OP_EQ || k == OP_ITE) && m.is_bool(to_app(t)->get_arg(1)))) {
unsigned num = to_app(t)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(t)->get_arg(i);
if (fvisited.is_marked(arg))
continue;
fvisited.mark(arg);
todo.push_back(arg);
}
}
}
else {
quick_for_each_expr(proc, tvisited, t);
}
}
}
template<typename T>
void operator()(T const & g) {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++)
process(g.form(i));
}
void operator()(unsigned sz, expr * const * fs) {
for (unsigned i = 0; i < sz; i++)
process(fs[i]);
}
};
template<typename T>
void collect_boolean_interface_core(T const & s, obj_hashtable<expr> & r) {
collect_boolean_interface_proc proc(s.m(), r);
proc(s);
}
void collect_boolean_interface(goal const & g, obj_hashtable<expr> & r) {
collect_boolean_interface_core(g, r);
}
void collect_boolean_interface(ast_manager & m, unsigned num, expr * const * fs, obj_hashtable<expr> & r) {
collect_boolean_interface_proc proc(m, r);
proc(num, fs);
}

43
src/tactic/sat/atom2bool_var.h
View file

@ -1,43 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
atom2bool_var.h
Abstract:
The mapping between SAT boolean variables and atoms
Author:
Leonardo (leonardo) 2011-10-25
Notes:
--*/
#ifndef _ATOM2BOOL_VAR_H_
#define _ATOM2BOOL_VAR_H_
#include"expr2var.h"
#include"sat_types.h"
/**
\brief Mapping from atoms into SAT boolean variables.
*/
class atom2bool_var : public expr2var {
public:
atom2bool_var(ast_manager & m):expr2var(m) {}
void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); }
sat::bool_var to_bool_var(expr * n) const;
void mk_inv(expr_ref_vector & lit2expr) const;
// return true if the mapping contains uninterpreted atoms.
bool interpreted_atoms() const { return expr2var::interpreted_vars(); }
};
class goal;
void collect_boolean_interface(goal const & g, obj_hashtable<expr> & r);
void collect_boolean_interface(ast_manager & m, unsigned num, expr * const * fs, obj_hashtable<expr> & r);
#endif

711
src/tactic/sat/goal2sat.cpp
View file

@ -1,711 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
goal2sat.cpp
Abstract:
"Compile" a goal into the SAT engine.
Atoms are "abstracted" into boolean variables.
The mapping between boolean variables and atoms
can be used to convert back the state of the
SAT engine into a goal.
The idea is to support scenarios such as:
1) simplify, blast, convert into SAT, and solve
2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
Author:
Leonardo (leonardo) 2011-10-26
Notes:
--*/
#include"goal2sat.h"
#include"ast_smt2_pp.h"
#include"ref_util.h"
#include"cooperate.h"
#include"filter_model_converter.h"
#include"model_evaluator.h"
#include"for_each_expr.h"
#include"model_v2_pp.h"
#include"tactic.h"
struct goal2sat::imp {
struct frame {
app * m_t;
unsigned m_root:1;
unsigned m_sign:1;
unsigned m_idx;
frame(app * t, bool r, bool s, unsigned idx):
m_t(t), m_root(r), m_sign(s), m_idx(idx) {}
};
ast_manager & m;
svector<frame> m_frame_stack;
svector<sat::literal> m_result_stack;
obj_map<app, sat::literal> m_cache;
obj_hashtable<expr> m_interface_vars;
sat::solver & m_solver;
atom2bool_var & m_map;
sat::bool_var m_true;
bool m_ite_extra;
unsigned long long m_max_memory;
volatile bool m_cancel;
imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map):
m(_m),
m_solver(s),
m_map(map) {
updt_params(p);
m_cancel = false;
m_true = sat::null_bool_var;
}
void updt_params(params_ref const & p) {
m_ite_extra = p.get_bool(":ite-extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
}
void throw_op_not_handled() {
throw tactic_exception("operator not supported, apply simplifier before invoking translator");
}
void mk_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
m_solver.mk_clause(1, &l);
}
void mk_clause(sat::literal l1, sat::literal l2) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
m_solver.mk_clause(l1, l2);
}
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
m_solver.mk_clause(l1, l2, l3);
}
void mk_clause(unsigned num, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
m_solver.mk_clause(num, lits);
}
sat::bool_var mk_true() {
// create fake variable to represent true;
if (m_true == sat::null_bool_var) {
m_true = m_solver.mk_var();
mk_clause(sat::literal(m_true, false)); // v is true
}
return m_true;
}
void convert_atom(expr * t, bool root, bool sign) {
SASSERT(m.is_bool(t));
sat::literal l;
sat::bool_var v = m_map.to_bool_var(t);
if (v == sat::null_bool_var) {
if (m.is_true(t)) {
l = sat::literal(mk_true(), sign);
}
else if (m.is_false(t)) {
l = sat::literal(mk_true(), !sign);
}
else {
bool ext = !is_uninterp_const(t) || m_interface_vars.contains(t);
sat::bool_var v = m_solver.mk_var(ext);
m_map.insert(t, v);
l = sat::literal(v, sign);
TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
}
}
else {
SASSERT(v != sat::null_bool_var);
l = sat::literal(v, sign);
}
SASSERT(l != sat::null_literal);
if (root)
mk_clause(l);
else
m_result_stack.push_back(l);
}
bool process_cached(app * t, bool root, bool sign) {
sat::literal l;
if (m_cache.find(t, l)) {
if (sign)
l.neg();
if (root)
mk_clause(l);
else
m_result_stack.push_back(l);
return true;
}
return false;
}
bool visit(expr * t, bool root, bool sign) {
if (!is_app(t)) {
convert_atom(t, root, sign);
return true;
}
if (process_cached(to_app(t), root, sign))
return true;
if (to_app(t)->get_family_id() != m.get_basic_family_id()) {
convert_atom(t, root, sign);
return true;
}
switch (to_app(t)->get_decl_kind()) {
case OP_NOT:
case OP_OR:
case OP_IFF:
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
case OP_ITE:
case OP_EQ:
if (m.is_bool(to_app(t)->get_arg(1))) {
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
}
convert_atom(t, root, sign);
return true;
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
throw_op_not_handled();
default:
convert_atom(t, root, sign);
return true;
}
}
void convert_or(app * t, bool root, bool sign) {
TRACE("goal2sat", tout << "convert_or:\n" << mk_ismt2_pp(t, m) << "\n";);
unsigned num = t->get_num_args();
if (root) {
SASSERT(num == m_result_stack.size());
if (sign) {
// this case should not really happen.
for (unsigned i = 0; i < num; i++) {
sat::literal l = m_result_stack[i];
l.neg();
mk_clause(l);
}
}
else {
mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
m_result_stack.reset();
}
}
else {
SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var();
sat::literal l(k, false);
m_cache.insert(t, l);
sat::literal * lits = m_result_stack.end() - num;
for (unsigned i = 0; i < num; i++) {
mk_clause(~lits[i], l);
}
m_result_stack.push_back(~l);
lits = m_result_stack.end() - num - 1;
// remark: mk_clause may perform destructive updated to lits.
// I have to execute it after the binary mk_clause above.
mk_clause(num+1, lits);
unsigned old_sz = m_result_stack.size() - num - 1;
m_result_stack.shrink(old_sz);
if (sign)
l.neg();
m_result_stack.push_back(l);
}
}
void convert_ite(app * n, bool root, bool sign) {
unsigned sz = m_result_stack.size();
SASSERT(sz >= 3);
sat::literal c = m_result_stack[sz-3];
sat::literal t = m_result_stack[sz-2];
sat::literal e = m_result_stack[sz-1];
if (root) {
SASSERT(sz == 3);
if (sign) {
mk_clause(~c, ~t);
mk_clause(c, ~e);
}
else {
mk_clause(~c, t);
mk_clause(c, e);
}
m_result_stack.reset();
}
else {
sat::bool_var k = m_solver.mk_var();
sat::literal l(k, false);
m_cache.insert(n, l);
mk_clause(~l, ~c, t);
mk_clause(~l, c, e);
mk_clause(l, ~c, ~t);
mk_clause(l, c, ~e);
if (m_ite_extra) {
mk_clause(~t, ~e, l);
mk_clause(t, e, ~l);
}
m_result_stack.shrink(sz-3);
if (sign)
l.neg();
m_result_stack.push_back(l);
}
}
void convert_iff(app * t, bool root, bool sign) {
TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";);
unsigned sz = m_result_stack.size();
SASSERT(sz >= 2);
sat::literal l1 = m_result_stack[sz-1];
sat::literal l2 = m_result_stack[sz-2];
if (root) {
SASSERT(sz == 2);
if (sign) {
mk_clause(l1, l2);
mk_clause(~l1, ~l2);
}
else {
mk_clause(l1, ~l2);
mk_clause(~l1, l2);
}
m_result_stack.reset();
}
else {
sat::bool_var k = m_solver.mk_var();
sat::literal l(k, false);
m_cache.insert(t, l);
mk_clause(~l, l1, ~l2);
mk_clause(~l, ~l1, l2);
mk_clause(l, l1, l2);
mk_clause(l, ~l1, ~l2);
m_result_stack.shrink(sz-2);
if (sign)
l.neg();
m_result_stack.push_back(l);
}
}
void convert(app * t, bool root, bool sign) {
SASSERT(t->get_family_id() == m.get_basic_family_id());
switch (to_app(t)->get_decl_kind()) {
case OP_OR:
convert_or(t, root, sign);
break;
case OP_ITE:
convert_ite(t, root, sign);
break;
case OP_IFF:
case OP_EQ:
convert_iff(t, root, sign);
break;
default:
UNREACHABLE();
}
}
void process(expr * n) {
TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
if (visit(n, true, false)) {
SASSERT(m_result_stack.empty());
return;
}
while (!m_frame_stack.empty()) {
loop:
cooperate("goal2sat");
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
frame & fr = m_frame_stack.back();
app * t = fr.m_t;
bool root = fr.m_root;
bool sign = fr.m_sign;
TRACE("goal2sat_bug", tout << "result stack\n";
tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
tout << "\n";);
if (fr.m_idx == 0 && process_cached(t, root, sign)) {
m_frame_stack.pop_back();
continue;
}
if (m.is_not(t)) {
m_frame_stack.pop_back();
visit(t->get_arg(0), root, !sign);
continue;
}
unsigned num = t->get_num_args();
while (fr.m_idx < num) {
expr * arg = t->get_arg(fr.m_idx);
fr.m_idx++;
if (!visit(arg, false, false))
goto loop;
}
TRACE("goal2sat_bug", tout << "converting\n";
tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
tout << "\n";);
convert(t, root, sign);
m_frame_stack.pop_back();
}
SASSERT(m_result_stack.empty());
}
void operator()(goal const & g) {
m_interface_vars.reset();
collect_boolean_interface(g, m_interface_vars);
unsigned size = g.size();
for (unsigned idx = 0; idx < size; idx++) {
expr * f = g.form(idx);
process(f);
}
}
void operator()(unsigned sz, expr * const * fs) {
m_interface_vars.reset();
collect_boolean_interface(m, sz, fs, m_interface_vars);
for (unsigned i = 0; i < sz; i++)
process(fs[i]);
}
void set_cancel(bool f) { m_cancel = f; }
};
struct unsupported_bool_proc {
struct found {};
ast_manager & m;
unsupported_bool_proc(ast_manager & _m):m(_m) {}
void operator()(var *) {}
void operator()(quantifier *) {}
void operator()(app * n) {
if (n->get_family_id() == m.get_basic_family_id()) {
switch (n->get_decl_kind()) {
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
throw found();
default:
break;
}
}
}
};
/**
\brief Return true if s contains an unsupported Boolean operator.
goal_rewriter (with the following configuration) can be used to
eliminate unsupported operators.
:elim-and true
:blast-distinct true
*/
bool goal2sat::has_unsupported_bool(goal const & g) {
return test<unsupported_bool_proc>(g);
}
goal2sat::goal2sat():m_imp(0) {
}
void goal2sat::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert(":ite-extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
}
struct goal2sat::scoped_set_imp {
goal2sat * m_owner;
scoped_set_imp(goal2sat * o, goal2sat::imp * i):m_owner(o) {
#pragma omp critical (goal2sat)
{
m_owner->m_imp = i;
}
}
~scoped_set_imp() {
#pragma omp critical (goal2sat)
{
m_owner->m_imp = 0;
}
}
};
void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m) {
imp proc(g.m(), p, t, m);
scoped_set_imp set(this, &proc);
proc(g);
}
void goal2sat::set_cancel(bool f) {
#pragma omp critical (goal2sat)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
struct sat2goal::imp {
// Wrapper for sat::model_converter: converts it into an "AST level" model_converter.
class sat_model_converter : public model_converter {
sat::model_converter m_mc;
// TODO: the following mapping is storing a lot of useless information, and may be a performance bottleneck.
// We need to save only the expressions associated with variables that occur in m_mc.
// This information may be stored as a vector of pairs.
// The mapping is only created during the model conversion.
expr_ref_vector m_var2expr;
ref<filter_model_converter> m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
sat_model_converter(ast_manager & m):
m_var2expr(m) {
}
public:
sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
m_mc.copy(s.get_model_converter());
m_fmc = alloc(filter_model_converter, m);
}
ast_manager & m() { return m_var2expr.get_manager(); }
void insert(expr * atom, bool aux) {
m_var2expr.push_back(atom);
if (aux) {
SASSERT(is_uninterp_const(atom));
SASSERT(m().is_bool(atom));
m_fmc->insert(to_app(atom)->get_decl());
}
}
virtual void operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
TRACE("sat_mc", tout << "before sat_mc\n"; model_v2_pp(tout, *md); display(tout););
// REMARK: potential problem
// model_evaluator can't evaluate quantifiers. Then,
// an eliminated variable that depends on a quantified expression can't be recovered.
// A similar problem also affects any model_converter that uses elim_var_model_converter.
//
// Possible solution:
// model_converters reject any variable elimination that depends on a quantified expression.
model_evaluator ev(*md);
ev.set_model_completion(false);
// create a SAT model using md
sat::model sat_md;
unsigned sz = m_var2expr.size();
expr_ref val(m());
for (sat::bool_var v = 0; v < sz; v++) {
expr * atom = m_var2expr.get(v);
ev(atom, val);
if (m().is_true(val))
sat_md.push_back(l_true);
else if (m().is_false(val))
sat_md.push_back(l_false);
else
sat_md.push_back(l_undef);
}
// apply SAT model converter
m_mc(sat_md);
// register value of non-auxiliary boolean variables back into md
sz = m_var2expr.size();
for (sat::bool_var v = 0; v < sz; v++) {
expr * atom = m_var2expr.get(v);
if (is_uninterp_const(atom)) {
func_decl * d = to_app(atom)->get_decl();
lbool new_val = sat_md[v];
if (new_val == l_true)
md->register_decl(d, m().mk_true());
else if (new_val == l_false)
md->register_decl(d, m().mk_false());
}
}
// apply filter model converter
(*m_fmc)(md);
TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md););
}
virtual model_converter * translate(ast_translation & translator) {
sat_model_converter * res = alloc(sat_model_converter, translator.to());
res->m_fmc = static_cast<filter_model_converter*>(m_fmc->translate(translator));
unsigned sz = m_var2expr.size();
for (unsigned i = 0; i < sz; i++)
res->m_var2expr.push_back(translator(m_var2expr.get(i)));
return res;
}
void display(std::ostream & out) {
out << "(sat-model-converter\n";
m_mc.display(out);
sat::bool_var_set vars;
m_mc.collect_vars(vars);
out << "(atoms";
unsigned sz = m_var2expr.size();
for (unsigned i = 0; i < sz; i++) {
if (vars.contains(i)) {
out << "\n (" << i << "\n " << mk_ismt2_pp(m_var2expr.get(i), m(), 2) << ")";
}
}
out << ")\n";
m_fmc->display(out);
out << ")\n";
}
};
ast_manager & m;
expr_ref_vector m_lit2expr;
unsigned long long m_max_memory;
bool m_learned;
volatile bool m_cancel;
imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m), m_cancel(false) {
updt_params(p);
}
void updt_params(params_ref const & p) {
m_learned = p.get_bool(":learned", false);
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
}
void checkpoint() {
if (m_cancel)
throw tactic_exception(TACTIC_CANCELED_MSG);
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
void init_lit2expr(sat::solver const & s, atom2bool_var const & map, model_converter_ref & mc, bool produce_models) {
ref<sat_model_converter> _mc;
if (produce_models)
_mc = alloc(sat_model_converter, m, s);
unsigned num_vars = s.num_vars();
m_lit2expr.resize(num_vars * 2);
map.mk_inv(m_lit2expr);
sort * b = m.mk_bool_sort();
for (sat::bool_var v = 0; v < num_vars; v++) {
checkpoint();
sat::literal l(v, false);
if (m_lit2expr.get(l.index()) == 0) {
SASSERT(m_lit2expr.get((~l).index()) == 0);
app * aux = m.mk_fresh_const(0, b);
if (_mc)
_mc->insert(aux, true);
m_lit2expr.set(l.index(), aux);
m_lit2expr.set((~l).index(), m.mk_not(aux));
}
else {
if (_mc)
_mc->insert(m_lit2expr.get(l.index()), false);
SASSERT(m_lit2expr.get((~l).index()) != 0);
}
}
mc = _mc.get();
}
expr * lit2expr(sat::literal l) {
return m_lit2expr.get(l.index());
}
void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) {
ptr_buffer<expr> lits;
for (sat::clause * const * it = begin; it != end; it++) {
checkpoint();
lits.reset();
sat::clause const & c = *(*it);
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
lits.push_back(lit2expr(c[i]));
}
r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
}
}
void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
if (s.inconsistent()) {
r.assert_expr(m.mk_false());
return;
}
init_lit2expr(s, map, mc, r.models_enabled());
// collect units
unsigned num_vars = s.num_vars();
for (sat::bool_var v = 0; v < num_vars; v++) {
checkpoint();
switch (s.value(v)) {
case l_true:
r.assert_expr(lit2expr(sat::literal(v, false)));
break;
case l_false:
r.assert_expr(lit2expr(sat::literal(v, true)));
break;
case l_undef:
break;
}
}
// collect binary clauses
svector<sat::solver::bin_clause> bin_clauses;
s.collect_bin_clauses(bin_clauses, m_learned);
svector<sat::solver::bin_clause>::iterator it = bin_clauses.begin();
svector<sat::solver::bin_clause>::iterator end = bin_clauses.end();
for (; it != end; ++it) {
checkpoint();
r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
}
// collect clauses
assert_clauses(s.begin_clauses(), s.end_clauses(), r);
if (m_learned)
assert_clauses(s.begin_learned(), s.end_learned(), r);
}
void set_cancel(bool f) { m_cancel = f; }
};
sat2goal::sat2goal():m_imp(0) {
}
void sat2goal::collect_param_descrs(param_descrs & r) {
insert_max_memory(r);
r.insert(":learned", CPK_BOOL, "(default: false) collect also learned clauses.");
}
struct sat2goal::scoped_set_imp {
sat2goal * m_owner;
scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
#pragma omp critical (sat2goal)
{
m_owner->m_imp = i;
}
}
~scoped_set_imp() {
#pragma omp critical (sat2goal)
{
m_owner->m_imp = 0;
}
}
};
void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p,
goal & g, model_converter_ref & mc) {
imp proc(g.m(), p);
scoped_set_imp set(this, &proc);
proc(t, m, g, mc);
}
void sat2goal::set_cancel(bool f) {
#pragma omp critical (sat2goal)
{
if (m_imp)
m_imp->set_cancel(f);
}
}

86
src/tactic/sat/goal2sat.h
View file

@ -1,86 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
goal2sat.h
Abstract:
"Compile" a goal into the SAT engine.
Atoms are "abstracted" into boolean variables.
The mapping between boolean variables and atoms
can be used to convert back the state of the
SAT engine into a goal.
The idea is to support scenarios such as:
1) simplify, blast, convert into SAT, and solve
2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
Author:
Leonardo (leonardo) 2011-10-26
Notes:
--*/
#ifndef _GOAL2SAT_H_
#define _GOAL2SAT_H_
#include"goal.h"
#include"sat_solver.h"
#include"model_converter.h"
#include"atom2bool_var.h"
class goal2sat {
struct imp;
imp * m_imp;
struct scoped_set_imp;
public:
goal2sat();
static void collect_param_descrs(param_descrs & r);
static bool has_unsupported_bool(goal const & s);
/**
\brief "Compile" the goal into the given sat solver.
Store a mapping from atoms to boolean variables into m.
\remark m doesn't need to be empty. the definitions there are
reused.
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
*/
void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m);
void set_cancel(bool f);
};
class sat2goal {
struct imp;
imp * m_imp;
struct scoped_set_imp;
public:
sat2goal();
static void collect_param_descrs(param_descrs & r);
/**
\brief Translate the state of the SAT engine back into a goal.
The SAT solver may use variables that are not in \c m. The translator
creates fresh boolean AST variables for them. They are stored in fvars.
\warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
or memory consumption limit is reached (set with param :max-memory).
*/
void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, goal & s, model_converter_ref & mc);
void set_cancel(bool f);
};
#endif

218
src/tactic/sat/sat_tactic.cpp
View file

@ -1,218 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_tactic.cpp
Abstract:
Tactic for using the SAT solver and its preprocessing capabilities.
Author:
Leonardo (leonardo) 2011-10-25
Notes:
--*/
#include"tactical.h"
#include"goal2sat.h"
#include"sat_solver.h"
#include"filter_model_converter.h"
#include"ast_smt2_pp.h"
#include"model_v2_pp.h"
class sat_tactic : public tactic {
struct imp {
ast_manager & m;
goal2sat m_goal2sat;
sat2goal m_sat2goal;
sat::solver m_solver;
params_ref m_params;
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_solver(p, 0),
m_params(p) {
SASSERT(!m.proofs_enabled());
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
fail_if_proof_generation("sat", g);
fail_if_unsat_core_generation("sat", g);
bool produce_models = g->models_enabled();
TRACE("before_sat_solver", g->display(tout););
g->elim_redundancies();
atom2bool_var map(m);
m_goal2sat(*g, m_params, m_solver, map);
TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
atom2bool_var::iterator it = map.begin();
atom2bool_var::iterator end = map.end();
for (; it != end; ++it) {
if (!is_uninterp_const(it->m_key))
tout << mk_ismt2_pp(it->m_key, m) << "\n";
});
g->reset();
g->m().compact_memory();
CASSERT("sat_solver", m_solver.check_invariant());
IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
lbool r = m_solver.check();
if (r == l_false) {
g->assert_expr(m.mk_false(), 0, 0);
}
else if (r == l_true && !map.interpreted_atoms()) {
// register model
if (produce_models) {
model_ref md = alloc(model, m);
sat::model const & ll_m = m_solver.get_model();
TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";);
atom2bool_var::iterator it = map.begin();
atom2bool_var::iterator end = map.end();
for (; it != end; ++it) {
expr * n = it->m_key;
sat::bool_var v = it->m_value;
TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, m) << "\nvar: " << v << "\n";);
switch (sat::value_at(v, ll_m)) {
case l_true:
md->register_decl(to_app(n)->get_decl(), m.mk_true());
break;
case l_false:
md->register_decl(to_app(n)->get_decl(), m.mk_false());
break;
default:
break;
}
}
TRACE("sat_tactic", model_v2_pp(tout, *md););
mc = model2model_converter(md.get());
}
}
else {
// get simplified problem.
#if 0
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";);
#endif
m_solver.pop(m_solver.scope_lvl());
m_sat2goal(m_solver, map, m_params, *(g.get()), mc);
}
g->inc_depth();
result.push_back(g.get());
}
void set_cancel(bool f) {
m_goal2sat.set_cancel(f);
m_sat2goal.set_cancel(f);
m_solver.set_cancel(f);
}
};
struct scoped_set_imp {
sat_tactic * m_owner;
scoped_set_imp(sat_tactic * o, imp * i):m_owner(o) {
#pragma omp critical (sat_tactic)
{
m_owner->m_imp = i;
}
}
~scoped_set_imp() {
#pragma omp critical (sat_tactic)
{
m_owner->m_imp = 0;
}
}
};
imp * m_imp;
params_ref m_params;
statistics m_stats;
public:
sat_tactic(ast_manager & m, params_ref const & p):
m_imp(0),
m_params(p) {
}
virtual tactic * translate(ast_manager & m) {
return alloc(sat_tactic, m, m_params);
}
virtual ~sat_tactic() {
SASSERT(m_imp == 0);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
}
virtual void collect_param_descrs(param_descrs & r) {
goal2sat::collect_param_descrs(r);
sat2goal::collect_param_descrs(r);
sat::solver::collect_param_descrs(r);
}
void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
imp proc(g->m(), m_params);
scoped_set_imp set(this, &proc);
try {
proc(g, result, mc, pc, core);
proc.m_solver.collect_statistics(m_stats);
}
catch (sat::solver_exception & ex) {
proc.m_solver.collect_statistics(m_stats);
throw tactic_exception(ex.msg());
}
TRACE("sat_stats", m_stats.display_smt2(tout););
}
virtual void cleanup() {
SASSERT(m_imp == 0);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void reset_statistics() {
m_stats.reset();
}
protected:
virtual void set_cancel(bool f) {
#pragma omp critical (sat_tactic)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
};
tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(sat_tactic, m, p));
}
tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
params_ref p_aux;
p_aux.set_uint(":max-conflicts", 0);
tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux));
t->updt_params(p);
return t;
}

35
src/tactic/sat/sat_tactic.h
View file

@ -1,35 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_tactic.cpp
Abstract:
Tactic for using the SAT solver and its preprocessing capabilities.
Author:
Leonardo (leonardo) 2011-10-26
Notes:
--*/
#ifndef _SAT_TACTIC_H_
#define _SAT_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_sat_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC('sat', '(try to) solve goal using a SAT solver.', 'mk_sat_tactic(m, p)')
ADD_TACTIC('sat-preprocess', 'Apply SAT solver preprocessing procedures (bounded resolution, Boolean constant propagation, 2-SAT, subsumption, subsumption resolution).', 'mk_sat_preprocessor_tactic(m, p)')
*/
#endif

395
src/tactic/subpaving/expr2subpaving.cpp
View file

@ -1,395 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
expr2subpaving.cpp
Abstract:
Translator from Z3 expressions into generic subpaving data-structure.
Author:
Leonardo (leonardo) 2012-08-08
Notes:
--*/
#include"expr2subpaving.h"
#include"expr2var.h"
#include"ref_util.h"
#include"z3_exception.h"
#include"cooperate.h"
#include"arith_decl_plugin.h"
#include"scoped_numeral_buffer.h"
struct expr2subpaving::imp {
struct frame {
app * m_curr;
unsigned m_idx;
frame():m_curr(0), m_idx(0) {}
frame(app * t):m_curr(t), m_idx(0) {}
};
ast_manager & m_manager;
subpaving::context & m_subpaving;
unsynch_mpq_manager & m_qm;
arith_util m_autil;
expr2var * m_expr2var;
bool m_expr2var_owner;
expr_ref_vector m_var2expr;
typedef svector<subpaving::var> var_vector;
obj_map<expr, unsigned> m_cache;
var_vector m_cached_vars;
scoped_mpz_vector m_cached_numerators;
scoped_mpz_vector m_cached_denominators;
obj_map<expr, subpaving::ineq*> m_lit_cache;
volatile bool m_cancel;
imp(ast_manager & m, subpaving::context & s, expr2var * e2v):
m_manager(m),
m_subpaving(s),
m_qm(s.qm()),
m_autil(m),
m_var2expr(m),
m_cached_numerators(m_qm),
m_cached_denominators(m_qm) {
if (e2v == 0) {
m_expr2var = alloc(expr2var, m);
m_expr2var_owner = true;
}
else {
m_expr2var = e2v;
m_expr2var_owner = false;
}
m_cancel = false;
}
~imp() {
reset_cache();
if (m_expr2var_owner)
dealloc(m_expr2var);
}
ast_manager & m() { return m_manager; }
subpaving::context & s() { return m_subpaving; }
unsynch_mpq_manager & qm() const { return m_qm; }
void reset_cache() {
dec_ref_map_keys(m(), m_cache);
m_cached_vars.reset();
m_cached_numerators.reset();
m_cached_denominators.reset();
dec_ref_map_key_values(m(), s(), m_lit_cache);
}
void checkpoint() {
if (m_cancel)
throw default_exception("canceled");
cooperate("expr2subpaving");
}
subpaving::var mk_var_for(expr * t) {
SASSERT(!m_autil.is_numeral(t));
subpaving::var x = m_expr2var->to_var(t);
if (x == subpaving::null_var) {
bool is_int = m_autil.is_int(t);
x = s().mk_var(is_int);
m_expr2var->insert(t, x);
if (x >= m_var2expr.size())
m_var2expr.resize(x+1, 0);
m_var2expr.set(x, t);
}
return x;
}
void found_non_simplified() {
throw default_exception("you must apply simplifier before internalizing expressions into the subpaving module.");
}
bool is_cached(expr * t) {
return t->get_ref_count() > 1 && m_cache.contains(t);
}
bool is_int_real(expr * t) {
return m_autil.is_int_real(t);
}
void cache_result(expr * t, subpaving::var x, mpz const & n, mpz const & d) {
SASSERT(!m_cache.contains(t));
SASSERT(m_cached_numerators.size() == m_cached_vars.size());
SASSERT(m_cached_denominators.size() == m_cached_vars.size());
if (t->get_ref_count() <= 1)
return;
unsigned idx = m_cached_vars.size();
m_cache.insert(t, idx);
m().inc_ref(t);
m_cached_vars.push_back(x);
m_cached_numerators.push_back(n);
m_cached_denominators.push_back(d);
}
subpaving::var process_num(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
VERIFY(m_autil.is_numeral(t, k));
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
return subpaving::null_var;
}
// Put t as a^k.
void as_power(expr * t, expr * & a, unsigned & k) {
if (!m_autil.is_power(t)) {
a = t;
k = 1;
return;
}
rational _k;
if (!m_autil.is_numeral(to_app(t)->get_arg(1), _k) || !_k.is_int() || !_k.is_unsigned()) {
a = t;
k = 1;
return;
}
a = to_app(t)->get_arg(0);
k = _k.get_unsigned();
}
subpaving::var process_mul(app * t, unsigned depth, mpz & n, mpz & d) {
unsigned num_args = t->get_num_args();
if (num_args <= 1)
found_non_simplified();
rational k;
expr * m;
if (m_autil.is_numeral(t->get_arg(0), k)) {
if (num_args != 2)
found_non_simplified();
qm().set(n, k.to_mpq().numerator());
qm().set(d, k.to_mpq().denominator());
m = t->get_arg(1);
}
else {
qm().set(n, 1);
qm().set(d, 1);
m = t;
}
expr * const * margs;
unsigned sz;
if (m_autil.is_mul(m)) {
margs = to_app(m)->get_args();
sz = to_app(m)->get_num_args();
}
else {
margs = &m;
sz = 1;
}
scoped_mpz n_arg(qm());
scoped_mpz d_arg(qm());
sbuffer<subpaving::power> pws;
for (unsigned i = 0; i < sz; i++) {
expr * arg = margs[i];
unsigned k;
as_power(arg, arg, k);
subpaving::var x_arg = process(arg, depth+1, n_arg, d_arg);
qm().power(n_arg, k, n_arg);
qm().power(d_arg, k, d_arg);
qm().mul(n, n_arg, n);
qm().mul(d, d_arg, d);
if (x_arg != subpaving::null_var)
pws.push_back(subpaving::power(x_arg, k));
}
subpaving::var x;
if (pws.empty())
x = subpaving::null_var;
else if (pws.size() == 1 && pws[0].degree() == 1)
x = pws[0].get_var();
else
x = s().mk_monomial(pws.size(), pws.c_ptr());
cache_result(t, x, n, d);
return x;
}
typedef _scoped_numeral_buffer<unsynch_mpz_manager> mpz_buffer;
typedef sbuffer<subpaving::var> var_buffer;
subpaving::var process_add(app * t, unsigned depth, mpz & n, mpz & d) {
unsigned num_args = t->get_num_args();
mpz_buffer ns(qm()), ds(qm());
var_buffer xs;
scoped_mpq c(qm()), c_arg(qm());
scoped_mpz n_arg(qm()), d_arg(qm());
for (unsigned i = 0; i < num_args; i++) {
expr * arg = t->get_arg(i);
subpaving::var x_arg = process(arg, depth+1, n_arg, d_arg);
if (x_arg == subpaving::null_var) {
qm().set(c_arg, n_arg, d_arg);
qm().add(c, c_arg, c);
}
else {
xs.push_back(x_arg);
ns.push_back(n_arg);
ds.push_back(d_arg);
}
}
qm().set(d, c.get().denominator());
unsigned sz = xs.size();
for (unsigned i = 0; i < sz; i++) {
qm().lcm(d, ds[i], d);
}
scoped_mpz & k = d_arg;
qm().div(d, c.get().denominator(), k);
scoped_mpz sum_c(qm());
qm().mul(c.get().numerator(), k, sum_c);
for (unsigned i = 0; i < sz; i++) {
qm().div(d, ds[i], k);
qm().mul(ns[i], k, ns[i]);
}
subpaving::var x;
if (sz == 0) {
qm().set(n, sum_c);
x = subpaving::null_var;
}
else {
x = s().mk_sum(sum_c, sz, ns.c_ptr(), xs.c_ptr());
qm().set(n, 1);
}
cache_result(t, x, n, d);
return x;
}
subpaving::var process_power(app * t, unsigned depth, mpz & n, mpz & d) {
rational k;
SASSERT(t->get_num_args() == 2);
if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
unsigned _k = k.get_unsigned();
subpaving::var x = process(t->get_arg(0), depth+1, n, d);
if (x != subpaving::null_var) {
subpaving::power p(x, _k);
x = s().mk_monomial(1, &p);
}
qm().power(n, _k, n);
qm().power(d, _k, d);
cache_result(t, x, n, d);
return x;
}
subpaving::var process_arith_app(app * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(m_autil.is_arith_expr(t));
switch (t->get_decl_kind()) {
case OP_NUM:
return process_num(t, depth, n, d);
case OP_ADD:
return process_add(t, depth, n, d);
case OP_MUL:
return process_mul(t, depth, n, d);
case OP_POWER:
return process_power(t, depth, n, d);
case OP_TO_REAL:
return process(t->get_arg(0), depth+1, n, d);
case OP_SUB:
case OP_UMINUS:
found_non_simplified();
break;
case OP_TO_INT:
case OP_DIV:
case OP_IDIV:
case OP_MOD:
case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");
case OP_SIN:
case OP_COS:
case OP_TAN:
case OP_ASIN:
case OP_ACOS:
case OP_ATAN:
case OP_SINH:
case OP_COSH:
case OP_TANH:
case OP_ASINH:
case OP_ACOSH:
case OP_ATANH:
// TODO
throw default_exception("transcendental and hyperbolic functions are not supported yet.");
default:
UNREACHABLE();
}
return subpaving::null_var;
}
subpaving::var process(expr * t, unsigned depth, mpz & n, mpz & d) {
SASSERT(is_int_real(t));
checkpoint();
if (is_cached(t)) {
unsigned idx = m_cache.find(t);
qm().set(n, m_cached_numerators[idx]);
qm().set(d, m_cached_denominators[idx]);
return m_cached_vars[idx];
}
SASSERT(!is_quantifier(t));
if (::is_var(t) || !m_autil.is_arith_expr(t)) {
qm().set(n, 1);
qm().set(d, 1);
return mk_var_for(t);
}
return process_arith_app(to_app(t), depth, n, d);
}
bool is_var(expr * t) const {
return m_expr2var->is_var(t);
}
void set_cancel(bool f) {
m_cancel = f;
}
subpaving::var internalize_term(expr * t, mpz & n, mpz & d) {
return process(t, 0, n, d);
}
};
expr2subpaving::expr2subpaving(ast_manager & m, subpaving::context & s, expr2var * e2v) {
m_imp = alloc(imp, m, s, e2v);
}
expr2subpaving::~expr2subpaving() {
dealloc(m_imp);
}
ast_manager & expr2subpaving::m() const {
return m_imp->m();
}
subpaving::context & expr2subpaving::s() const {
return m_imp->s();
}
bool expr2subpaving::is_var(expr * t) const {
return m_imp->is_var(t);
}
void expr2subpaving::set_cancel(bool f) {
m_imp->set_cancel(f);
}
subpaving::var expr2subpaving::internalize_term(expr * t, mpz & n, mpz & d) {
return m_imp->internalize_term(t, n, d);
}

58
src/tactic/subpaving/expr2subpaving.h
View file

@ -1,58 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
expr2subpaving.h
Abstract:
Translator from Z3 expressions into generic subpaving data-structure.
Author:
Leonardo (leonardo) 2012-08-08
Notes:
--*/
#ifndef _EXPR2SUBPAVING_H_
#define _EXPR2SUBPAVING_H_
#include"ast.h"
#include"subpaving.h"
class expr2var;
class expr2subpaving {
struct imp;
imp * m_imp;
public:
expr2subpaving(ast_manager & m, subpaving::context & s, expr2var * e2v = 0);
~expr2subpaving();
ast_manager & m() const;
subpaving::context & s() const;
/**
\brief Return true if t was encoded as a variable by the translator.
*/
bool is_var(expr * t) const;
/**
\brief Cancel/Interrupt execution.
*/
void set_cancel(bool f);
/**
\brief Internalize a Z3 arithmetical expression into the subpaving data-structure.
\remark throws subpaving::exception there is a translation error (when using imprecise representations, i.e. floats, in the subpaving module)
*/
subpaving::var internalize_term(expr * t, /* out */ mpz & n, /* out */ mpz & d);
};
#endif

314
src/tactic/subpaving/subpaving_tactic.cpp
View file

@ -1,314 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_tactic.cpp
Abstract:
"Fake" tactic used to test subpaving module.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#include"tactical.h"
#include"simplify_tactic.h"
#include"expr2subpaving.h"
#include"expr2var.h"
#include"arith_decl_plugin.h"
#include"ast_smt2_pp.h"
#include"hwf.h"
#include"mpff.h"
#include"mpfx.h"
#include"f2n.h"
class subpaving_tactic : public tactic {
struct display_var_proc : public subpaving::display_var_proc {
expr_ref_vector m_inv;
display_var_proc(expr2var & e2v):m_inv(e2v.m()) {
e2v.mk_inv(m_inv);
}
ast_manager & m() const { return m_inv.get_manager(); }
virtual void operator()(std::ostream & out, subpaving::var x) const {
expr * t = m_inv.get(x, 0);
if (t != 0)
out << mk_ismt2_pp(t, m());
else
out << "k!" << x;
}
};
struct imp {
enum engine_kind { MPQ, MPF, HWF, MPFF, MPFX, NONE };
ast_manager & m_manager;
unsynch_mpq_manager m_qm;
mpf_manager m_fm_core;
f2n<mpf_manager> m_fm;
hwf_manager m_hm_core;
f2n<hwf_manager> m_hm;
mpff_manager m_ffm;
mpfx_manager m_fxm;
arith_util m_autil;
engine_kind m_kind;
scoped_ptr<subpaving::context> m_ctx;
scoped_ptr<display_var_proc> m_proc;
expr2var m_e2v;
scoped_ptr<expr2subpaving> m_e2s;
bool m_display;
imp(ast_manager & m, params_ref const & p):
m_manager(m),
m_fm(m_fm_core),
m_hm(m_hm_core),
m_autil(m),
m_kind(NONE),
m_e2v(m) {
updt_params(p);
}
ast_manager & m() const { return m_manager; }
void collect_param_descrs(param_descrs & r) {
m_ctx->collect_param_descrs(r);
// #ifndef _EXTERNAL_RELEASE
r.insert(":numeral", CPK_SYMBOL, "(default: mpq) options: mpq, mpf, hwf, mpff, mpfx.");
r.insert(":print-nodes", CPK_BOOL, "(default: false) display subpaving tree leaves.");
// #endif
}
void updt_params(params_ref const & p) {
m_display = p.get_bool(":print-nodes", false);
symbol engine = p.get_sym(":numeral", symbol("mpq"));
engine_kind new_kind;
if (engine == "mpq")
new_kind = MPQ;
else if (engine == "mpf")
new_kind = MPF;
else if (engine == "mpff")
new_kind = MPFF;
else if (engine == "mpfx")
new_kind = MPFX;
else
new_kind = HWF;
if (m_kind != new_kind) {
m_kind = new_kind;
switch (m_kind) {
case MPQ: m_ctx = subpaving::mk_mpq_context(m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m_fxm, m_qm); break;
default: UNREACHABLE(); break;
}
m_e2s = alloc(expr2subpaving, m_manager, *m_ctx, &m_e2v);
}
m_ctx->updt_params(p);
}
void collect_statistics(statistics & st) const {
m_ctx->collect_statistics(st);
}
void reset_statistics() {
m_ctx->reset_statistics();
}
void set_cancel(bool f) {
m_e2s->set_cancel(f);
m_ctx->set_cancel(f);
}
subpaving::ineq * mk_ineq(expr * a) {
bool neg = false;
while (m().is_not(a, a))
neg = !neg;
bool lower;
bool open = false;
if (m_autil.is_le(a)) {
lower = false;
}
else if (m_autil.is_ge(a)) {
lower = true;
}
else {
throw tactic_exception("unsupported atom");
}
if (neg) {
lower = !lower;
open = !open;
}
rational _k;
if (!m_autil.is_numeral(to_app(a)->get_arg(1), _k))
throw tactic_exception("use simplify tactic with option :arith-lhs true");
scoped_mpq k(m_qm);
k = _k.to_mpq();
scoped_mpz n(m_qm), d(m_qm);
subpaving::var x = m_e2s->internalize_term(to_app(a)->get_arg(0), n, d);
m_qm.mul(d, k, k);
m_qm.div(k, n, k);
if (is_neg(n))
lower = !lower;
TRACE("subpaving_tactic", tout << x << " " << k << " " << lower << " " << open << "\n";);
return m_ctx->mk_ineq(x, k, lower, open);
}
void process_clause(expr * c) {
expr * const * args = 0;
unsigned sz;
if (m().is_or(c)) {
args = to_app(c)->get_args();
sz = to_app(c)->get_num_args();
}
else {
args = &c;
sz = 1;
}
ref_buffer<subpaving::ineq, subpaving::context> ineq_buffer(*m_ctx);
for (unsigned i = 0; i < sz; i++) {
ineq_buffer.push_back(mk_ineq(args[i]));
}
m_ctx->add_clause(sz, ineq_buffer.c_ptr());
}
void internalize(goal const & g) {
try {
for (unsigned i = 0; i < g.size(); i++) {
process_clause(g.form(i));
}
}
catch (subpaving::exception) {
throw tactic_exception("failed to internalize goal into subpaving module");
}
}
void process(goal const & g) {
internalize(g);
m_proc = alloc(display_var_proc, m_e2v);
m_ctx->set_display_proc(m_proc.get());
try {
(*m_ctx)();
}
catch (subpaving::exception) {
throw tactic_exception("failed building subpaving tree...");
}
if (m_display) {
m_ctx->display_constraints(std::cout);
std::cout << "bounds at leaves: \n";
m_ctx->display_bounds(std::cout);
}
}
};
imp * m_imp;
params_ref m_params;
statistics m_stats;
public:
subpaving_tactic(ast_manager & m, params_ref const & p):
m_imp(alloc(imp, m, p)),
m_params(p) {
}
virtual ~subpaving_tactic() {
dealloc(m_imp);
}
virtual tactic * translate(ast_manager & m) {
return alloc(subpaving_tactic, m, m_params);
}
virtual void updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
virtual void collect_param_descrs(param_descrs & r) {
m_imp->collect_param_descrs(r);
}
virtual void collect_statistics(statistics & st) const {
st.copy(m_stats);
}
virtual void reset_statistics() {
m_stats.reset();
}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
try {
m_imp->process(*in);
m_imp->collect_statistics(m_stats);
result.reset();
result.push_back(in.get());
mc = 0;
pc = 0;
core = 0;
}
catch (z3_exception & ex) {
// convert all Z3 exceptions into tactic exceptions
throw tactic_exception(ex.msg());
}
}
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
d = m_imp;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
}
protected:
virtual void set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
};
tactic * mk_subpaving_tactic_core(ast_manager & m, params_ref const & p) {
return alloc(subpaving_tactic, m, p);
}
tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p) {
params_ref simp_p = p;
simp_p.set_bool(":arith-lhs", true);
simp_p.set_bool(":expand-power", true);
simp_p.set_uint(":max-power", UINT_MAX);
simp_p.set_bool(":som", true);
simp_p.set_bool(":eq2ineq", true);
simp_p.set_bool(":elim-and", true);
simp_p.set_bool(":blast-distinct", true);
params_ref simp2_p = p;
simp2_p.set_bool(":mul-to-power", true);
return and_then(using_params(mk_simplify_tactic(m, p),
simp_p),
using_params(mk_simplify_tactic(m, p),
simp2_p),
mk_subpaving_tactic_core(m, p));
}

31
src/tactic/subpaving/subpaving_tactic.h
View file

@ -1,31 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_tactic.h
Abstract:
"Fake" tactic used to test subpaving module.
Author:
Leonardo de Moura (leonardo) 2012-08-07.
Revision History:
--*/
#ifndef __SUBPAVING_TACTIC_H_
#define __SUBPAVING_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_subpaving_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("subpaving", "tactic for testing subpaving module.", "mk_subpaving_tactic(m, p)")
*/
#endif