mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 02:45:51 +00:00
had to nuke mip_tactic, it was based on the smt_solver_exp (experimental), that depends on assertion_sets. This change will affect Z3's performance on QF_LIA and QF_LRA benchmarks. The new mcsat should fix that.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
361b55edfd
commit
96676efeb6
30 changed files with 18 additions and 1819 deletions
|
|
@ -58,8 +58,7 @@ add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_c
|
|||
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
|
||||
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core_tactics')
|
||||
add_lib('sat_tactic', ['tactic', 'sat'], 'tactic/sat_tactic')
|
||||
add_lib('sat_strategy', ['assertion_set', 'sat_tactic'], 'assertion_set/sat_strategy')
|
||||
add_lib('arith_tactics', ['core_tactics', 'assertion_set', 'sat', 'sat_strategy'], 'tactic/arith_tactics')
|
||||
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith_tactics')
|
||||
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'tactic/nlsat_tactic')
|
||||
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
|
||||
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv_tactics')
|
||||
|
|
@ -68,7 +67,7 @@ add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
|
|||
add_lib('smt_tactic', ['smt'], 'smt/tactic')
|
||||
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
||||
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls_tactic')
|
||||
add_lib('aig', ['cmd_context', 'assertion_set'], 'tactic/aig')
|
||||
add_lib('aig', ['cmd_context'], 'tactic/aig')
|
||||
# TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
|
||||
add_lib('muz_qe', ['smt', 'sat', 'smt2parser'])
|
||||
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogic_tactics')
|
||||
|
|
|
|||
|
|
@ -1,791 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
assertion_set2sat.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
"Compile" an assertion set 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 an assertion set.
|
||||
|
||||
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 an assertion set.
|
||||
3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into an assertion set.
|
||||
4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-05-22
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"assertion_set2sat.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"assertion_set_util.h"
|
||||
|
||||
struct assertion_set2sat::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 assertion_set2sat_exception("operator not supported, apply simplifier before invoking translator");
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l) {
|
||||
TRACE("assertion_set2sat", tout << "mk_clause: " << l << "\n";);
|
||||
m_solver.mk_clause(1, &l);
|
||||
}
|
||||
|
||||
void mk_clause(sat::literal l1, sat::literal l2) {
|
||||
TRACE("assertion_set2sat", 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("assertion_set2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
|
||||
m_solver.mk_clause(l1, l2, l3);
|
||||
}
|
||||
|
||||
void mk_clause(unsigned num, sat::literal * lits) {
|
||||
TRACE("assertion_set2sat", 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("assertion_set2sat", 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("assertion_set2sat_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("assertion_set2sat", 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("assertion_set2sat", 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("assertion_set2sat", 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("assertion_set2sat");
|
||||
if (m_cancel)
|
||||
throw assertion_set2sat_exception(STE_CANCELED_MSG);
|
||||
if (memory::get_allocation_size() > m_max_memory)
|
||||
throw assertion_set2sat_exception(STE_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("assertion_set2sat_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("assertion_set2sat_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()(assertion_set const & s) {
|
||||
m_interface_vars.reset();
|
||||
collect_boolean_interface(s, m_interface_vars);
|
||||
|
||||
unsigned size = s.size();
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
expr * f = s.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.
|
||||
assertion_set_rewriter (with the following configuration) can be used to
|
||||
eliminate unsupported operators.
|
||||
:elim-and true
|
||||
:blast-distinct true
|
||||
*/
|
||||
bool assertion_set2sat::has_unsupported_bool(assertion_set const & s) {
|
||||
return test<unsupported_bool_proc>(s);
|
||||
}
|
||||
|
||||
assertion_set2sat::assertion_set2sat():m_imp(0) {
|
||||
}
|
||||
|
||||
void assertion_set2sat::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 assertion_set2sat::scoped_set_imp {
|
||||
assertion_set2sat * m_owner;
|
||||
scoped_set_imp(assertion_set2sat * o, assertion_set2sat::imp * i):m_owner(o) {
|
||||
#pragma omp critical (assertion_set2sat)
|
||||
{
|
||||
m_owner->m_imp = i;
|
||||
}
|
||||
}
|
||||
~scoped_set_imp() {
|
||||
#pragma omp critical (assertion_set2sat)
|
||||
{
|
||||
m_owner->m_imp = 0;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void assertion_set2sat::operator()(assertion_set const & s, params_ref const & p, sat::solver & t, atom2bool_var & m) {
|
||||
imp proc(s.m(), p, t, m);
|
||||
scoped_set_imp set(this, &proc);
|
||||
proc(s);
|
||||
}
|
||||
|
||||
void assertion_set2sat::operator()(ast_manager & mng, unsigned num, expr * const * fs, params_ref const & p, sat::solver & t, atom2bool_var & m) {
|
||||
imp proc(mng, p, t, m);
|
||||
scoped_set_imp set(this, &proc);
|
||||
proc(num, fs);
|
||||
}
|
||||
|
||||
void assertion_set2sat::set_cancel(bool f) {
|
||||
#pragma omp critical (assertion_set2sat)
|
||||
{
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
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) {
|
||||
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";
|
||||
}
|
||||
};
|
||||
|
||||
struct sat2assertion_set::imp {
|
||||
ast_manager & m;
|
||||
expr_ref_vector m_lit2expr;
|
||||
unsigned long long m_max_memory;
|
||||
bool m_learned;
|
||||
bool m_produce_models;
|
||||
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_produce_models = p.get_bool(":produce-models", false);
|
||||
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 sat2assertion_set_exception(STE_CANCELED_MSG);
|
||||
if (memory::get_allocation_size() > m_max_memory)
|
||||
throw sat2assertion_set_exception(STE_MAX_MEMORY_MSG);
|
||||
}
|
||||
|
||||
void init_lit2expr(sat::solver const & s, atom2bool_var const & map, model_converter_ref & mc) {
|
||||
ref<sat_model_converter> _mc;
|
||||
if (m_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, assertion_set & 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, assertion_set & r, model_converter_ref & mc) {
|
||||
if (s.inconsistent()) {
|
||||
r.assert_expr(m.mk_false());
|
||||
return;
|
||||
}
|
||||
init_lit2expr(s, map, mc);
|
||||
// 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; }
|
||||
};
|
||||
|
||||
sat2assertion_set::sat2assertion_set():m_imp(0) {
|
||||
}
|
||||
|
||||
void sat2assertion_set::collect_param_descrs(param_descrs & r) {
|
||||
insert_max_memory(r);
|
||||
r.insert(":learned", CPK_BOOL, "(default: false) collect also learned clauses.");
|
||||
}
|
||||
|
||||
struct sat2assertion_set::scoped_set_imp {
|
||||
sat2assertion_set * m_owner;
|
||||
scoped_set_imp(sat2assertion_set * o, sat2assertion_set::imp * i):m_owner(o) {
|
||||
#pragma omp critical (sat2assertion_set)
|
||||
{
|
||||
m_owner->m_imp = i;
|
||||
}
|
||||
}
|
||||
~scoped_set_imp() {
|
||||
#pragma omp critical (sat2assertion_set)
|
||||
{
|
||||
m_owner->m_imp = 0;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void sat2assertion_set::operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p,
|
||||
assertion_set & s, model_converter_ref & mc) {
|
||||
imp proc(s.m(), p);
|
||||
scoped_set_imp set(this, &proc);
|
||||
proc(t, m, s, mc);
|
||||
}
|
||||
|
||||
void sat2assertion_set::set_cancel(bool f) {
|
||||
#pragma omp critical (sat2assertion_set)
|
||||
{
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
// HACK introduced during code reorg.
|
||||
// NOTE: the whole file will be deleted.
|
||||
struct collect_boolean_interface_proc2 {
|
||||
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_proc2(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_core2(T const & s, obj_hashtable<expr> & r) {
|
||||
collect_boolean_interface_proc2 proc(s.m(), r);
|
||||
proc(s);
|
||||
}
|
||||
|
||||
void collect_boolean_interface(assertion_set const & s, obj_hashtable<expr> & r) {
|
||||
collect_boolean_interface_core2(s, r);
|
||||
}
|
||||
|
|
@ -1,98 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
assertion_set2sat.h
|
||||
|
||||
Abstract:
|
||||
|
||||
"Compile" an assertion set 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 an assertion set.
|
||||
|
||||
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 an assertion set.
|
||||
3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into an assertion set.
|
||||
4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-05-22
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _ASSERTION_SET2SAT_H_
|
||||
#define _ASSERTION_SET2SAT_H_
|
||||
|
||||
#include"assertion_set.h"
|
||||
#include"sat_solver.h"
|
||||
#include"strategy_exception.h"
|
||||
#include"model_converter.h"
|
||||
#include"atom2bool_var.h"
|
||||
|
||||
class assertion_set; // TODO: delete
|
||||
void collect_boolean_interface(assertion_set const & s, obj_hashtable<expr> & r);
|
||||
|
||||
MK_ST_EXCEPTION(assertion_set2sat_exception);
|
||||
|
||||
class assertion_set2sat {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
struct scoped_set_imp;
|
||||
public:
|
||||
assertion_set2sat();
|
||||
|
||||
static void collect_param_descrs(param_descrs & r);
|
||||
|
||||
static bool has_unsupported_bool(assertion_set const & s);
|
||||
|
||||
/**
|
||||
\brief "Compile" the assertion set 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.
|
||||
*/
|
||||
void operator()(assertion_set const & s, params_ref const & p, sat::solver & t, atom2bool_var & m);
|
||||
|
||||
/**
|
||||
\brief "Compile" the formulas fs 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.
|
||||
*/
|
||||
void operator()(ast_manager & mng, unsigned num, expr * const * fs, params_ref const & p, sat::solver & t, atom2bool_var & m);
|
||||
|
||||
void operator()(ast_manager & mng, expr * f, params_ref const & p, sat::solver & t, atom2bool_var & m) { operator()(mng, 1, &f, p, t, m); }
|
||||
|
||||
void set_cancel(bool f);
|
||||
};
|
||||
|
||||
MK_ST_EXCEPTION(sat2assertion_set_exception);
|
||||
|
||||
class sat2assertion_set {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
struct scoped_set_imp;
|
||||
public:
|
||||
sat2assertion_set();
|
||||
|
||||
static void collect_param_descrs(param_descrs & r);
|
||||
|
||||
/**
|
||||
\brief Translate the state of the SAT engine back into an assertion set.
|
||||
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.
|
||||
*/
|
||||
void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, assertion_set & s, model_converter_ref & mc);
|
||||
|
||||
void set_cancel(bool f);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
@ -1,187 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_solver_strategy.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for using the SAT solver preprocessing capabilities.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-05-23
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"sat_solver_strategy.h"
|
||||
#include"assertion_set2sat.h"
|
||||
#include"sat_solver.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"model_v2_pp.h"
|
||||
|
||||
struct sat_solver_strategy::imp {
|
||||
ast_manager & m;
|
||||
assertion_set2sat m_as2sat;
|
||||
sat2assertion_set m_sat2as;
|
||||
sat::solver m_solver;
|
||||
params_ref m_params;
|
||||
bool m_produce_models;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_solver(p, 0),
|
||||
m_params(p) {
|
||||
SASSERT(!m.proofs_enabled());
|
||||
m_produce_models = p.get_bool(":produce-models", false);
|
||||
}
|
||||
|
||||
void operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
if (s.m().proofs_enabled())
|
||||
throw sat::solver_exception("sat solver does not support proofs");
|
||||
TRACE("before_sat_solver", s.display(tout););
|
||||
s.elim_redundancies();
|
||||
if (s.inconsistent()) {
|
||||
mc = 0;
|
||||
return;
|
||||
}
|
||||
|
||||
atom2bool_var map(m);
|
||||
m_as2sat(s, 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";
|
||||
});
|
||||
s.reset();
|
||||
s.m().compact_memory();
|
||||
CASSERT("sat_solver", m_solver.check_invariant());
|
||||
IF_VERBOSE(ST_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) {
|
||||
mc = 0;
|
||||
s.reset();
|
||||
s.assert_expr(m.mk_false(), 0);
|
||||
return;
|
||||
}
|
||||
else if (r == l_true && !map.interpreted_atoms()) {
|
||||
// register model
|
||||
model_ref md = alloc(model, m);
|
||||
sat::model const & ll_m = m_solver.get_model();
|
||||
TRACE("sat_solver_strategy", 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_solver_strategy", 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;
|
||||
}
|
||||
}
|
||||
s.reset();
|
||||
TRACE("sat_solver_strategy", model_v2_pp(tout, *md););
|
||||
mc = model2model_converter(md.get());
|
||||
}
|
||||
else {
|
||||
// get simplified problem.
|
||||
#if 0
|
||||
IF_VERBOSE(ST_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";);
|
||||
#endif
|
||||
m_solver.pop(m_solver.scope_lvl());
|
||||
m_sat2as(m_solver, map, m_params, s, mc);
|
||||
}
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_as2sat.set_cancel(f);
|
||||
m_sat2as.set_cancel(f);
|
||||
m_solver.set_cancel(f);
|
||||
}
|
||||
};
|
||||
|
||||
sat_solver_strategy::sat_solver_strategy(ast_manager & m, params_ref const & p):
|
||||
m_imp(0),
|
||||
m_params(p) {
|
||||
}
|
||||
|
||||
sat_solver_strategy::~sat_solver_strategy() {
|
||||
SASSERT(m_imp == 0);
|
||||
}
|
||||
|
||||
void sat_solver_strategy::updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
}
|
||||
|
||||
void sat_solver_strategy::get_param_descrs(param_descrs & r) {
|
||||
assertion_set2sat::collect_param_descrs(r);
|
||||
sat2assertion_set::collect_param_descrs(r);
|
||||
sat::solver::collect_param_descrs(r);
|
||||
insert_produce_models(r);
|
||||
}
|
||||
|
||||
|
||||
struct sat_solver_strategy::scoped_set_imp {
|
||||
sat_solver_strategy * m_owner;
|
||||
scoped_set_imp(sat_solver_strategy * o, sat_solver_strategy::imp * i):m_owner(o) {
|
||||
#pragma omp critical (sat_solver_strategy)
|
||||
{
|
||||
m_owner->m_imp = i;
|
||||
}
|
||||
}
|
||||
|
||||
~scoped_set_imp() {
|
||||
#pragma omp critical (sat_solver_strategy)
|
||||
{
|
||||
m_owner->m_imp = 0;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void sat_solver_strategy::operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
imp proc(s.m(), m_params);
|
||||
scoped_set_imp set(this, &proc);
|
||||
try {
|
||||
proc(s, mc);
|
||||
proc.m_solver.collect_statistics(m_stats);
|
||||
}
|
||||
catch (sat::solver_exception & ex) {
|
||||
proc.m_solver.collect_statistics(m_stats);
|
||||
throw ex;
|
||||
}
|
||||
TRACE("sat_stats", m_stats.display_smt2(tout););
|
||||
}
|
||||
|
||||
void sat_solver_strategy::cleanup() {
|
||||
SASSERT(m_imp == 0);
|
||||
}
|
||||
|
||||
void sat_solver_strategy::set_cancel(bool f) {
|
||||
#pragma omp critical (sat_solver_strategy)
|
||||
{
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
}
|
||||
|
||||
void sat_solver_strategy::reset_statistics() {
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void sat_solver_strategy::collect_statistics(statistics & st) const {
|
||||
st.copy(m_stats);
|
||||
}
|
||||
|
|
@ -1,65 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_solver_strategy.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for using the SAT solver.
|
||||
If the assertion set contains theory atoms, then the sat solver just
|
||||
checks whether the boolean abstraction is satisfiable or not.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-06-02
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _SAT_SOLVER_STRATEGY_H_
|
||||
#define _SAT_SOLVER_STRATEGY_H_
|
||||
|
||||
#include"assertion_set_strategy.h"
|
||||
|
||||
class assertion_set;
|
||||
|
||||
class sat_solver_strategy : public assertion_set_strategy {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
statistics m_stats;
|
||||
struct scoped_set_imp;
|
||||
public:
|
||||
sat_solver_strategy(ast_manager & m, params_ref const & p = params_ref());
|
||||
virtual ~sat_solver_strategy();
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
virtual void operator()(assertion_set & s, model_converter_ref & mc);
|
||||
|
||||
virtual void cleanup();
|
||||
|
||||
virtual void collect_statistics(statistics & st) const;
|
||||
virtual void reset_statistics();
|
||||
protected:
|
||||
virtual void set_cancel(bool f);
|
||||
};
|
||||
|
||||
inline as_st * mk_sat_solver(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
return clean(alloc(sat_solver_strategy, m, p));
|
||||
}
|
||||
|
||||
// Apply only simplification procedures
|
||||
inline as_st * mk_sat_preprocessor(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
params_ref p_aux;
|
||||
p_aux.set_uint(":max-conflicts", 0);
|
||||
as_st * st = clean(using_params(mk_sat_solver(m), p_aux));
|
||||
st->updt_params(p);
|
||||
return st;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -239,19 +239,9 @@ UNARY_CMD(sexpr_cmd, "dbg-sexpr", "<sexpr>", "display an s-expr", CPK_SEXPR, sex
|
|||
ctx.regular_stream() << std::endl;
|
||||
});
|
||||
|
||||
static void tst_bound_manager(cmd_context & ctx) {
|
||||
ast_manager & m = ctx.m();
|
||||
assertion_set s(m);
|
||||
assert_exprs_from(ctx, s);
|
||||
bound_manager bc(m);
|
||||
bc(s);
|
||||
bc.display(ctx.regular_stream());
|
||||
}
|
||||
|
||||
#define GUARDED_CODE(CODE) try { CODE } catch (z3_error & ex) { throw ex; } catch (z3_exception & ex) { ctx.regular_stream() << "(error \"" << escaped(ex.msg()) << "\")" << std::endl; }
|
||||
|
||||
ATOMIC_CMD(bounds_cmd, "dbg-bounds", "test bound manager", GUARDED_CODE(tst_bound_manager(ctx);));
|
||||
|
||||
UNARY_CMD(set_next_id, "dbg-set-next-id", "<unsigned>", "set the next expression id to be at least the given value", CPK_UINT, unsigned, {
|
||||
ctx.m().set_next_expr_id(arg);
|
||||
});
|
||||
|
|
@ -373,7 +363,6 @@ void install_dbg_cmds(cmd_context & ctx) {
|
|||
ctx.insert(alloc(params_cmd));
|
||||
ctx.insert(alloc(translator_cmd));
|
||||
ctx.insert(alloc(sexpr_cmd));
|
||||
ctx.insert(alloc(bounds_cmd));
|
||||
ctx.insert(alloc(used_vars_cmd));
|
||||
ctx.insert(alloc(elim_unused_vars_cmd));
|
||||
ctx.insert(alloc(instantiate_cmd));
|
||||
|
|
|
|||
|
|
@ -17,7 +17,6 @@ Notes:
|
|||
|
||||
--*/
|
||||
#include"aig.h"
|
||||
#include"assertion_set.h" // TODO delete
|
||||
#include"goal.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"cooperate.h"
|
||||
|
|
@ -1006,39 +1005,6 @@ struct aig_manager::imp {
|
|||
r = invert(r);
|
||||
}
|
||||
|
||||
|
||||
void operator()(aig_lit const & l, assertion_set & s) {
|
||||
#if 1
|
||||
s.reset();
|
||||
sbuffer<aig_lit> roots;
|
||||
roots.push_back(l);
|
||||
while (!roots.empty()) {
|
||||
aig_lit n = roots.back();
|
||||
roots.pop_back();
|
||||
if (n.is_inverted()) {
|
||||
s.assert_expr(invert(process_root(n.ptr())));
|
||||
continue;
|
||||
}
|
||||
aig * p = n.ptr();
|
||||
if (m.is_ite(p)) {
|
||||
s.assert_expr(process_root(p));
|
||||
continue;
|
||||
}
|
||||
if (is_var(p)) {
|
||||
s.assert_expr(m.var2expr(p));
|
||||
continue;
|
||||
}
|
||||
roots.push_back(left(p));
|
||||
roots.push_back(right(p));
|
||||
}
|
||||
#else
|
||||
s.reset();
|
||||
expr_ref r(ast_mng);
|
||||
naive(l, r);
|
||||
s.assert_expr(r);
|
||||
#endif
|
||||
}
|
||||
|
||||
void operator()(aig_lit const & l, expr_ref & r) {
|
||||
naive(l, r);
|
||||
}
|
||||
|
|
@ -1574,11 +1540,6 @@ public:
|
|||
return r;
|
||||
}
|
||||
|
||||
void to_formula(aig_lit const & r, assertion_set & s) {
|
||||
aig2expr proc(*this);
|
||||
proc(r, s);
|
||||
}
|
||||
|
||||
void to_formula(aig_lit const & r, goal & g) {
|
||||
aig2expr proc(*this);
|
||||
proc(r, g);
|
||||
|
|
@ -1745,10 +1706,6 @@ aig_ref aig_manager::mk_aig(expr * n) {
|
|||
return aig_ref(*this, m_imp->mk_aig(n));
|
||||
}
|
||||
|
||||
aig_ref aig_manager::mk_aig(assertion_set const & s) {
|
||||
return aig_ref(*this, m_imp->mk_aig(s));
|
||||
}
|
||||
|
||||
aig_ref aig_manager::mk_aig(goal const & s) {
|
||||
return aig_ref(*this, m_imp->mk_aig(s));
|
||||
}
|
||||
|
|
@ -1779,10 +1736,6 @@ void aig_manager::max_sharing(aig_ref & r) {
|
|||
r = aig_ref(*this, m_imp->max_sharing(aig_lit(r)));
|
||||
}
|
||||
|
||||
void aig_manager::to_formula(aig_ref const & r, assertion_set & s) {
|
||||
return m_imp->to_formula(aig_lit(r), s);
|
||||
}
|
||||
|
||||
void aig_manager::to_formula(aig_ref const & r, goal & g) {
|
||||
SASSERT(!g.proofs_enabled());
|
||||
SASSERT(!g.unsat_core_enabled());
|
||||
|
|
|
|||
|
|
@ -22,7 +22,6 @@ Notes:
|
|||
#include"ast.h"
|
||||
#include"tactic_exception.h"
|
||||
|
||||
class assertion_set;
|
||||
class goal;
|
||||
class aig_lit;
|
||||
class aig_manager;
|
||||
|
|
@ -62,7 +61,6 @@ public:
|
|||
~aig_manager();
|
||||
void set_max_memory(unsigned long long max);
|
||||
aig_ref mk_aig(expr * n);
|
||||
aig_ref mk_aig(assertion_set const & s); // TODO delete
|
||||
aig_ref mk_aig(goal const & g);
|
||||
aig_ref mk_not(aig_ref const & r);
|
||||
aig_ref mk_and(aig_ref const & r1, aig_ref const & r2);
|
||||
|
|
@ -70,7 +68,6 @@ public:
|
|||
aig_ref mk_iff(aig_ref const & r1, aig_ref const & r2);
|
||||
aig_ref mk_ite(aig_ref const & r1, aig_ref const & r2, aig_ref const & r3);
|
||||
void max_sharing(aig_ref & r);
|
||||
void to_formula(aig_ref const & r, assertion_set & s); // TODO delete
|
||||
void to_formula(aig_ref const & r, expr_ref & result);
|
||||
void to_formula(aig_ref const & r, goal & result);
|
||||
void to_cnf(aig_ref const & r, goal & result);
|
||||
|
|
|
|||
|
|
@ -1,164 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
add_bounds.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for bounding unbounded variables.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2011-06-30.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"add_bounds.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
#include"bound_manager.h"
|
||||
#include"for_each_expr.h"
|
||||
#include"assertion_set_util.h"
|
||||
|
||||
struct is_unbounded_proc {
|
||||
struct found {};
|
||||
arith_util m_util;
|
||||
bound_manager & m_bm;
|
||||
|
||||
is_unbounded_proc(bound_manager & bm):m_util(bm.m()), m_bm(bm) {}
|
||||
|
||||
void operator()(app * t) {
|
||||
if (is_uninterp_const(t) && (m_util.is_int(t) || m_util.is_real(t)) && (!m_bm.has_lower(t) || !m_bm.has_upper(t)))
|
||||
throw found();
|
||||
}
|
||||
|
||||
void operator()(var *) {}
|
||||
|
||||
void operator()(quantifier*) {}
|
||||
};
|
||||
|
||||
bool is_unbounded(assertion_set const & s) {
|
||||
ast_manager & m = s.m();
|
||||
bound_manager bm(m);
|
||||
bm(s);
|
||||
is_unbounded_proc proc(bm);
|
||||
return test(s, proc);
|
||||
}
|
||||
|
||||
struct add_bounds::imp {
|
||||
ast_manager & m;
|
||||
rational m_lower;
|
||||
rational m_upper;
|
||||
volatile bool m_cancel;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):
|
||||
m(_m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_lower = p.get_rat(":add-bound-lower", rational(-2));
|
||||
m_upper = p.get_rat(":add-bound-upper", rational(2));
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_cancel = f;
|
||||
}
|
||||
|
||||
struct add_bound_proc {
|
||||
arith_util m_util;
|
||||
bound_manager & m_bm;
|
||||
assertion_set & m_set;
|
||||
rational const & m_lower;
|
||||
rational const & m_upper;
|
||||
unsigned m_num_bounds;
|
||||
|
||||
add_bound_proc(bound_manager & bm, assertion_set & s, rational const & l, rational const & u):
|
||||
m_util(bm.m()),
|
||||
m_bm(bm),
|
||||
m_set(s),
|
||||
m_lower(l),
|
||||
m_upper(u) {
|
||||
m_num_bounds = 0;
|
||||
}
|
||||
|
||||
void operator()(app * t) {
|
||||
if (is_uninterp_const(t) && (m_util.is_int(t) || m_util.is_real(t))) {
|
||||
if (!m_bm.has_lower(t)) {
|
||||
m_set.assert_expr(m_util.mk_le(t, m_util.mk_numeral(m_upper, m_util.is_int(t))));
|
||||
m_num_bounds++;
|
||||
}
|
||||
if (!m_bm.has_upper(t)) {
|
||||
m_set.assert_expr(m_util.mk_ge(t, m_util.mk_numeral(m_lower, m_util.is_int(t))));
|
||||
m_num_bounds++;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void operator()(var *) {}
|
||||
|
||||
void operator()(quantifier*) {}
|
||||
};
|
||||
|
||||
void operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
mc = 0;
|
||||
if (s.inconsistent())
|
||||
return;
|
||||
as_st_report report("add-bounds", s);
|
||||
bound_manager bm(m);
|
||||
expr_fast_mark1 visited;
|
||||
add_bound_proc proc(bm, s, m_lower, m_upper);
|
||||
unsigned sz = s.size();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
quick_for_each_expr(proc, visited, s.form(i));
|
||||
visited.reset();
|
||||
report_st_progress(":added-bounds", proc.m_num_bounds);
|
||||
TRACE("add_bounds", s.display(tout););
|
||||
}
|
||||
};
|
||||
|
||||
add_bounds::add_bounds(ast_manager & m, params_ref const & p):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
add_bounds::~add_bounds() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
void add_bounds::updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
void add_bounds::get_param_descrs(param_descrs & r) {
|
||||
r.insert(":add-bound-lower", CPK_NUMERAL, "(default: -2) lower bound to be added to unbounded variables.");
|
||||
r.insert(":add-bound-upper", CPK_NUMERAL, "(default: 2) upper bound to be added to unbounded variables.");
|
||||
}
|
||||
|
||||
void add_bounds::operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
m_imp->operator()(s, mc);
|
||||
}
|
||||
|
||||
void add_bounds::set_cancel(bool f) {
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
|
||||
void add_bounds::cleanup() {
|
||||
ast_manager & m = m_imp->m;
|
||||
imp * d = m_imp;
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
d = m_imp;
|
||||
}
|
||||
dealloc(d);
|
||||
d = alloc(imp, m, m_params);
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
m_imp = d;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,50 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
add_bounds.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for bounding unbounded variables.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2011-06-30.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _ADD_BOUNDS_H_
|
||||
#define _ADD_BOUNDS_H_
|
||||
|
||||
#include"assertion_set_strategy.h"
|
||||
|
||||
bool is_unbounded(assertion_set const & s);
|
||||
|
||||
class add_bounds : public assertion_set_strategy {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
add_bounds(ast_manager & m, params_ref const & p = params_ref());
|
||||
virtual ~add_bounds();
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
virtual void operator()(assertion_set & s, model_converter_ref & mc);
|
||||
|
||||
virtual void cleanup();
|
||||
|
||||
protected:
|
||||
virtual void set_cancel(bool f);
|
||||
};
|
||||
|
||||
inline as_st * mk_add_bounds(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
return clean(alloc(add_bounds, m, p));
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -199,13 +199,6 @@ bool bound_manager::is_disjunctive_bound(expr * f, expr_dependency * d) {
|
|||
return true;
|
||||
}
|
||||
|
||||
void bound_manager::operator()(assertion_set const & s) {
|
||||
unsigned sz = s.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
operator()(s.form(i), 0);
|
||||
}
|
||||
}
|
||||
|
||||
void bound_manager::operator()(goal const & g) {
|
||||
unsigned sz = g.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
|
|
|
|||
|
|
@ -20,7 +20,6 @@ Notes:
|
|||
#define _BOUND_MANAGER_H_
|
||||
|
||||
#include"ast.h"
|
||||
#include"assertion_set.h"
|
||||
#include"arith_decl_plugin.h"
|
||||
|
||||
class goal;
|
||||
|
|
@ -48,7 +47,6 @@ public:
|
|||
|
||||
ast_manager & m() const { return m_util.get_manager(); }
|
||||
|
||||
void operator()(assertion_set const & s); // TODO: delete
|
||||
void operator()(goal const & g);
|
||||
void operator()(expr * n, expr_dependency * d = 0);
|
||||
|
||||
|
|
|
|||
|
|
@ -1,174 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
elim_term_ite_strategy.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Eliminate term if-then-else by adding
|
||||
new fresh auxiliary variables.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-06-15
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"elim_term_ite_strategy.h"
|
||||
#include"defined_names.h"
|
||||
#include"rewriter_def.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"cooperate.h"
|
||||
|
||||
struct elim_term_ite_strategy::imp {
|
||||
|
||||
struct rw_cfg : public default_rewriter_cfg {
|
||||
ast_manager & m;
|
||||
defined_names m_defined_names;
|
||||
ref<filter_model_converter> m_mc;
|
||||
assertion_set * m_set;
|
||||
unsigned long long m_max_memory; // in bytes
|
||||
bool m_produce_models;
|
||||
unsigned m_num_fresh;
|
||||
|
||||
bool max_steps_exceeded(unsigned num_steps) const {
|
||||
cooperate("elim term ite");
|
||||
if (memory::get_allocation_size() > m_max_memory)
|
||||
throw elim_term_ite_exception(STE_MAX_MEMORY_MSG);
|
||||
return false;
|
||||
}
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
if (!m.is_term_ite(f))
|
||||
return BR_FAILED;
|
||||
expr_ref new_ite(m);
|
||||
new_ite = m.mk_app(f, num, args);
|
||||
|
||||
expr_ref new_def(m);
|
||||
proof_ref new_def_pr(m);
|
||||
app_ref _result(m);
|
||||
if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) {
|
||||
m_set->assert_expr(new_def, new_def_pr);
|
||||
m_num_fresh++;
|
||||
if (m_produce_models) {
|
||||
if (!m_mc)
|
||||
m_mc = alloc(filter_model_converter, m);
|
||||
m_mc->insert(_result->get_decl());
|
||||
}
|
||||
}
|
||||
result = _result.get();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
rw_cfg(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_defined_names(m, 0 /* don't use prefix */) {
|
||||
updt_params(p);
|
||||
m_set = 0;
|
||||
m_num_fresh = 0;
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
|
||||
m_produce_models = p.get_bool(":produce-models", false);
|
||||
}
|
||||
};
|
||||
|
||||
struct rw : public rewriter_tpl<rw_cfg> {
|
||||
rw_cfg m_cfg;
|
||||
|
||||
rw(ast_manager & m, params_ref const & p):
|
||||
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
|
||||
m_cfg(m, p) {
|
||||
}
|
||||
};
|
||||
|
||||
ast_manager & m;
|
||||
rw m_rw;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_rw(m, p) {
|
||||
}
|
||||
|
||||
void set_cancel(bool f) {
|
||||
m_rw.set_cancel(f);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_rw.cfg().updt_params(p);
|
||||
}
|
||||
|
||||
void operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
mc = 0;
|
||||
if (s.inconsistent())
|
||||
return;
|
||||
{
|
||||
as_st_report report("elim-term-ite", s);
|
||||
m_rw.m_cfg.m_num_fresh = 0;
|
||||
m_rw.m_cfg.m_set = &s;
|
||||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned size = s.size();
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
expr * curr = s.form(idx);
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
if (m.proofs_enabled()) {
|
||||
proof * pr = s.pr(idx);
|
||||
new_pr = m.mk_modus_ponens(pr, new_pr);
|
||||
}
|
||||
s.update(idx, new_curr, new_pr);
|
||||
}
|
||||
mc = m_rw.m_cfg.m_mc.get();
|
||||
}
|
||||
report_st_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
elim_term_ite_strategy::elim_term_ite_strategy(ast_manager & m, params_ref const & p):
|
||||
m_params(p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
elim_term_ite_strategy::~elim_term_ite_strategy() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
void elim_term_ite_strategy::updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
m_imp->updt_params(p);
|
||||
}
|
||||
|
||||
void elim_term_ite_strategy::get_param_descrs(param_descrs & r) {
|
||||
insert_max_memory(r);
|
||||
insert_produce_models(r);
|
||||
}
|
||||
|
||||
void elim_term_ite_strategy::operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
m_imp->operator()(s, mc);
|
||||
}
|
||||
|
||||
void elim_term_ite_strategy::set_cancel(bool f) {
|
||||
if (m_imp)
|
||||
m_imp->set_cancel(f);
|
||||
}
|
||||
|
||||
void elim_term_ite_strategy::cleanup() {
|
||||
ast_manager & m = m_imp->m;
|
||||
imp * d = m_imp;
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
d = m_imp;
|
||||
}
|
||||
dealloc(d);
|
||||
d = alloc(imp, m, m_params);
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
m_imp = d;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
elim_term_ite_strategy.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Eliminate term if-then-else by adding
|
||||
new fresh auxiliary variables.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-06-15
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _ELIM_TERM_ITE_STRATEGY_H_
|
||||
#define _ELIM_TERM_ITE_STRATEGY_H_
|
||||
|
||||
#include"strategy_exception.h"
|
||||
#include"model_converter.h"
|
||||
#include"params.h"
|
||||
#include"assertion_set_strategy.h"
|
||||
|
||||
class assertion_set;
|
||||
MK_ST_EXCEPTION(elim_term_ite_exception);
|
||||
|
||||
class elim_term_ite_strategy : public assertion_set_strategy {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
params_ref m_params;
|
||||
public:
|
||||
elim_term_ite_strategy(ast_manager & m, params_ref const & p = params_ref());
|
||||
virtual ~elim_term_ite_strategy();
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
virtual void operator()(assertion_set & s, model_converter_ref & mc);
|
||||
|
||||
virtual void cleanup();
|
||||
virtual void set_cancel(bool f);
|
||||
};
|
||||
|
||||
inline as_st * mk_elim_term_ite(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
return clean(alloc(elim_term_ite_strategy, m, p));
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -1,96 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
sat_solver_strategy.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for using the SMT solver.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-06-25
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"smt_solver_strategy.h"
|
||||
#include"smt_solver_exp.h"
|
||||
|
||||
smt_solver_strategy::smt_solver_strategy(ast_manager & _m, params_ref const & p):
|
||||
m(_m),
|
||||
m_params(p) {
|
||||
}
|
||||
|
||||
smt_solver_strategy::~smt_solver_strategy() {
|
||||
}
|
||||
|
||||
void smt_solver_strategy::init_solver() {
|
||||
smt::solver_exp * new_solver = alloc(smt::solver_exp, m, m_params);
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
m_solver = new_solver;
|
||||
}
|
||||
}
|
||||
|
||||
void smt_solver_strategy::updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
}
|
||||
|
||||
void smt_solver_strategy::get_param_descrs(param_descrs & r) {
|
||||
// TODO
|
||||
}
|
||||
|
||||
void smt_solver_strategy::operator()(assertion_set & s, model_converter_ref & mc) {
|
||||
if (s.m().proofs_enabled())
|
||||
throw smt_solver_exception("smt quick solver does not support proof generation");
|
||||
mc = 0;
|
||||
s.elim_redundancies();
|
||||
if (s.inconsistent())
|
||||
return;
|
||||
|
||||
init_solver();
|
||||
m_solver->assert_set(s);
|
||||
s.reset();
|
||||
|
||||
lbool r = m_solver->check();
|
||||
m_solver->collect_statistics(m_stats);
|
||||
|
||||
if (r == l_false) {
|
||||
s.assert_expr(m.mk_false());
|
||||
}
|
||||
else if (r == l_true) {
|
||||
model_ref md;
|
||||
m_solver->get_model(md);
|
||||
mc = model2model_converter(md.get());
|
||||
}
|
||||
else {
|
||||
// recover simplified assertion set
|
||||
m_solver->get_assertions(s);
|
||||
m_solver->get_model_converter(mc);
|
||||
}
|
||||
}
|
||||
|
||||
void smt_solver_strategy::cleanup() {
|
||||
if (m_solver)
|
||||
m_solver->collect_statistics(m_stats);
|
||||
#pragma omp critical (as_st_cancel)
|
||||
{
|
||||
m_solver = 0;
|
||||
}
|
||||
}
|
||||
|
||||
void smt_solver_strategy::set_cancel(bool f) {
|
||||
if (m_solver)
|
||||
m_solver->set_cancel(f);
|
||||
}
|
||||
|
||||
void smt_solver_strategy::reset_statistics() {
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
void smt_solver_strategy::collect_statistics(statistics & st) const {
|
||||
st.copy(m_stats);
|
||||
}
|
||||
|
|
@ -1,55 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
smt_solver_strategy.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Strategy for using the SAT solver.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2011-06-25
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _SMT_SOLVER_STRATEGY_H_
|
||||
#define _SMT_SOLVER_STRATEGY_H_
|
||||
|
||||
#include"assertion_set_strategy.h"
|
||||
|
||||
namespace smt { class solver_exp; };
|
||||
|
||||
class smt_solver_strategy : public assertion_set_strategy {
|
||||
struct imp;
|
||||
ast_manager & m;
|
||||
params_ref m_params;
|
||||
statistics m_stats;
|
||||
scoped_ptr<smt::solver_exp> m_solver;
|
||||
void init_solver();
|
||||
public:
|
||||
smt_solver_strategy(ast_manager & m, params_ref const & p = params_ref());
|
||||
virtual ~smt_solver_strategy();
|
||||
|
||||
virtual void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
|
||||
|
||||
virtual void operator()(assertion_set & s, model_converter_ref & mc);
|
||||
|
||||
virtual void cleanup();
|
||||
|
||||
virtual void collect_statistics(statistics & st) const;
|
||||
virtual void reset_statistics();
|
||||
protected:
|
||||
virtual void set_cancel(bool f);
|
||||
};
|
||||
|
||||
inline as_st * mk_smt2_solver(ast_manager & m, params_ref const & p = params_ref()) {
|
||||
return clean(alloc(smt_solver_strategy, m, p));
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -59,7 +59,7 @@ Notes:
|
|||
#include"bv_size_reduction_tactic.h"
|
||||
#include"propagate_ineqs_tactic.h"
|
||||
#include"cofactor_term_ite_tactic.h"
|
||||
#include"mip_tactic.h"
|
||||
// include"mip_tactic.h"
|
||||
#include"vsubst_tactic.h"
|
||||
#include"sls_tactic.h"
|
||||
#include"probe_arith.h"
|
||||
|
|
@ -121,7 +121,6 @@ MK_SIMPLE_TACTIC_FACTORY(reduce_args_fct, mk_reduce_args_tactic(m, p));
|
|||
MK_SIMPLE_TACTIC_FACTORY(bv_size_reduction_fct, mk_bv_size_reduction_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(propagate_ineqs_fct, mk_propagate_ineqs_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(cofactor_term_ite_fct, mk_cofactor_term_ite_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(mip_fct, mk_mip_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(nla2bv_fct, mk_nla2bv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(vsubst_fct, mk_vsubst_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfbv_sls_fct, mk_qfbv_sls_tactic(m, p));
|
||||
|
|
@ -188,7 +187,6 @@ void install_tactics(tactic_manager & ctx) {
|
|||
ADD_TACTIC_CMD("reduce-bv-size", "try to reduce bit-vector sizes using inequalities.", bv_size_reduction_fct);
|
||||
ADD_TACTIC_CMD("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", propagate_ineqs_fct);
|
||||
ADD_TACTIC_CMD("cofactor-term-ite", "eliminate term if-the-else using cofactors.", cofactor_term_ite_fct);
|
||||
ADD_TACTIC_CMD("mip", "solver for mixed integer programming problems.", mip_fct);
|
||||
ADD_TACTIC_CMD("nla2bv", "convert a nonlinear arithmetic problem into a bit-vector problem, in most cases the resultant goal is an under approximation and is useul for finding models.", nla2bv_fct);
|
||||
ADD_TACTIC_CMD("vsubst", "checks satsifiability of quantifier-free non-linear constraints using virtual substitution.", vsubst_fct);
|
||||
ADD_TACTIC_CMD("qfbv-sls", "(try to) solve using stochastic local search for QF_BV.", qfbv_sls_fct);
|
||||
|
|
@ -223,7 +221,6 @@ void install_tactics(tactic_manager & ctx) {
|
|||
ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", mk_is_qflra_probe());
|
||||
ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", mk_is_qflira_probe());
|
||||
ADD_PROBE("is-ilp", "true if the goal is ILP.", mk_is_ilp_probe());
|
||||
ADD_PROBE("is-mip", "true if the goal is MIP.", mk_is_mip_probe());
|
||||
ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", mk_is_unbounded_probe());
|
||||
ADD_PROBE("is-pb", "true if the goal is a pseudo-boolean problem.", mk_is_pb_probe());
|
||||
ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", mk_arith_max_degree_probe());
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ Notes:
|
|||
#include"solve_eqs_tactic.h"
|
||||
#include"elim_uncnstr_tactic.h"
|
||||
#include"smt_tactic.h"
|
||||
#include"mip_tactic.h"
|
||||
// include"mip_tactic.h"
|
||||
#include"add_bounds_tactic.h"
|
||||
#include"pb2bv_tactic.h"
|
||||
#include"lia2pb_tactic.h"
|
||||
|
|
@ -109,7 +109,7 @@ static tactic * mk_pb_tactic(ast_manager & m) {
|
|||
fail_if(mk_produce_unsat_cores_probe()),
|
||||
or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))),
|
||||
fail_if_not(mk_is_ilp_probe()),
|
||||
try_for(mk_mip_tactic(m), 8000),
|
||||
// try_for(mk_mip_tactic(m), 8000),
|
||||
mk_fail_if_undecided_tactic()),
|
||||
and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
|
||||
fail_if_not(mk_is_qfbv_probe()),
|
||||
|
|
@ -147,14 +147,15 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
|
|||
fail_if(mk_produce_proofs_probe()),
|
||||
fail_if(mk_produce_unsat_cores_probe()),
|
||||
mk_propagate_ineqs_tactic(m),
|
||||
or_else(try_for(mk_mip_tactic(m), 5000),
|
||||
or_else(// try_for(mk_mip_tactic(m), 5000),
|
||||
try_for(mk_no_cut_smt_tactic(100), 2000),
|
||||
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
|
||||
try_for(mk_lia2sat_tactic(m), 5000)),
|
||||
try_for(mk_no_cut_smt_tactic(200), 5000),
|
||||
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
|
||||
try_for(mk_lia2sat_tactic(m), 10000)),
|
||||
mk_mip_tactic(m)),
|
||||
try_for(mk_lia2sat_tactic(m), 10000))
|
||||
// , mk_mip_tactic(m)
|
||||
),
|
||||
mk_fail_if_undecided_tactic());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ Notes:
|
|||
#include"solve_eqs_tactic.h"
|
||||
#include"elim_uncnstr_tactic.h"
|
||||
#include"smt_tactic.h"
|
||||
#include"mip_tactic.h"
|
||||
// include"mip_tactic.h"
|
||||
#include"recover_01_tactic.h"
|
||||
#include"ctx_simplify_tactic.h"
|
||||
#include"probe_arith.h"
|
||||
|
|
@ -47,6 +47,8 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
|
|||
params_ref elim_to_real_p;
|
||||
elim_to_real_p.set_bool(":elim-to-real", true);
|
||||
|
||||
|
||||
#if 0
|
||||
tactic * mip =
|
||||
and_then(fail_if(mk_produce_proofs_probe()),
|
||||
fail_if(mk_produce_unsat_cores_probe()),
|
||||
|
|
@ -64,8 +66,11 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
|
|||
fail_if(mk_not(mk_is_mip_probe())),
|
||||
try_for(mk_mip_tactic(m), 30000),
|
||||
mk_fail_if_undecided_tactic());
|
||||
#endif
|
||||
|
||||
return using_params(or_else(mip,
|
||||
using_params(mk_smt_tactic(), pivot_p)),
|
||||
p);
|
||||
// return using_params(or_else(mip,
|
||||
// using_params(mk_smt_tactic(), pivot_p)),
|
||||
// p);
|
||||
|
||||
return using_params(using_params(mk_smt_tactic(), pivot_p), p);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue