diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index 51ea58836..e29c11772 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -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')
diff --git a/src/assertion_set/sat_strategy/assertion_set2sat.cpp b/src/assertion_set/sat_strategy/assertion_set2sat.cpp
deleted file mode 100644
index b81c32e51..000000000
--- a/src/assertion_set/sat_strategy/assertion_set2sat.cpp
+++ /dev/null
@@ -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 m_frame_stack;
- svector m_result_stack;
- obj_map m_cache;
- obj_hashtable 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(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 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(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 _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 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 bin_clauses;
- s.collect_bin_clauses(bin_clauses, m_learned);
- svector::iterator it = bin_clauses.begin();
- svector::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 & m_r;
- visitor(obj_hashtable & 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 todo;
- visitor proc;
-
- collect_boolean_interface_proc2(ast_manager & _m, obj_hashtable & 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
- 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
-void collect_boolean_interface_core2(T const & s, obj_hashtable & r) {
- collect_boolean_interface_proc2 proc(s.m(), r);
- proc(s);
-}
-
-void collect_boolean_interface(assertion_set const & s, obj_hashtable & r) {
- collect_boolean_interface_core2(s, r);
-}
diff --git a/src/assertion_set/sat_strategy/assertion_set2sat.h b/src/assertion_set/sat_strategy/assertion_set2sat.h
deleted file mode 100644
index 8f90b1367..000000000
--- a/src/assertion_set/sat_strategy/assertion_set2sat.h
+++ /dev/null
@@ -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 & 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
diff --git a/src/assertion_set/sat_strategy/sat_solver_strategy.cpp b/src/assertion_set/sat_strategy/sat_solver_strategy.cpp
deleted file mode 100644
index 94f66990b..000000000
--- a/src/assertion_set/sat_strategy/sat_solver_strategy.cpp
+++ /dev/null
@@ -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);
-}
diff --git a/src/assertion_set/sat_strategy/sat_solver_strategy.h b/src/assertion_set/sat_strategy/sat_solver_strategy.h
deleted file mode 100644
index b3cbd22b4..000000000
--- a/src/assertion_set/sat_strategy/sat_solver_strategy.h
+++ /dev/null
@@ -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
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index c473f6448..b7b4f058d 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -239,19 +239,9 @@ UNARY_CMD(sexpr_cmd, "dbg-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", "", "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));
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index d79f28903..d7c0b0f53 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -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 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());
diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h
index f8000b4d6..96aa59ee6 100644
--- a/src/tactic/aig/aig.h
+++ b/src/tactic/aig/aig.h
@@ -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);
diff --git a/src/tactic/arith_tactics/add_bounds.cpp b/src/tactic/arith_tactics/add_bounds.cpp
deleted file mode 100644
index 6702783f3..000000000
--- a/src/tactic/arith_tactics/add_bounds.cpp
+++ /dev/null
@@ -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;
- }
-}
diff --git a/src/tactic/arith_tactics/add_bounds.h b/src/tactic/arith_tactics/add_bounds.h
deleted file mode 100644
index 5cd1ac484..000000000
--- a/src/tactic/arith_tactics/add_bounds.h
+++ /dev/null
@@ -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
diff --git a/src/tactic/arith_tactics/bound_manager.cpp b/src/tactic/arith_tactics/bound_manager.cpp
index 2448521a3..ed77467c3 100644
--- a/src/tactic/arith_tactics/bound_manager.cpp
+++ b/src/tactic/arith_tactics/bound_manager.cpp
@@ -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++) {
diff --git a/src/tactic/arith_tactics/bound_manager.h b/src/tactic/arith_tactics/bound_manager.h
index 5904165f5..fbf02e59d 100644
--- a/src/tactic/arith_tactics/bound_manager.h
+++ b/src/tactic/arith_tactics/bound_manager.h
@@ -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);
diff --git a/src/tactic/arith_tactics/lu.cpp b/src/tactic/arith_tactics/dead/lu.cpp
similarity index 100%
rename from src/tactic/arith_tactics/lu.cpp
rename to src/tactic/arith_tactics/dead/lu.cpp
diff --git a/src/tactic/arith_tactics/lu.h b/src/tactic/arith_tactics/dead/lu.h
similarity index 100%
rename from src/tactic/arith_tactics/lu.h
rename to src/tactic/arith_tactics/dead/lu.h
diff --git a/src/tactic/arith_tactics/mip_tactic.cpp b/src/tactic/arith_tactics/dead/mip_tactic.cpp
similarity index 100%
rename from src/tactic/arith_tactics/mip_tactic.cpp
rename to src/tactic/arith_tactics/dead/mip_tactic.cpp
diff --git a/src/tactic/arith_tactics/mip_tactic.h b/src/tactic/arith_tactics/dead/mip_tactic.h
similarity index 100%
rename from src/tactic/arith_tactics/mip_tactic.h
rename to src/tactic/arith_tactics/dead/mip_tactic.h
diff --git a/src/tactic/arith_tactics/smt_arith.cpp b/src/tactic/arith_tactics/dead/smt_arith.cpp
similarity index 100%
rename from src/tactic/arith_tactics/smt_arith.cpp
rename to src/tactic/arith_tactics/dead/smt_arith.cpp
diff --git a/src/tactic/arith_tactics/smt_arith.h b/src/tactic/arith_tactics/dead/smt_arith.h
similarity index 100%
rename from src/tactic/arith_tactics/smt_arith.h
rename to src/tactic/arith_tactics/dead/smt_arith.h
diff --git a/src/tactic/arith_tactics/smt_formula_compiler.cpp b/src/tactic/arith_tactics/dead/smt_formula_compiler.cpp
similarity index 100%
rename from src/tactic/arith_tactics/smt_formula_compiler.cpp
rename to src/tactic/arith_tactics/dead/smt_formula_compiler.cpp
diff --git a/src/tactic/arith_tactics/smt_formula_compiler.h b/src/tactic/arith_tactics/dead/smt_formula_compiler.h
similarity index 100%
rename from src/tactic/arith_tactics/smt_formula_compiler.h
rename to src/tactic/arith_tactics/dead/smt_formula_compiler.h
diff --git a/src/tactic/arith_tactics/smt_solver_exp.cpp b/src/tactic/arith_tactics/dead/smt_solver_exp.cpp
similarity index 100%
rename from src/tactic/arith_tactics/smt_solver_exp.cpp
rename to src/tactic/arith_tactics/dead/smt_solver_exp.cpp
diff --git a/src/tactic/arith_tactics/smt_solver_exp.h b/src/tactic/arith_tactics/dead/smt_solver_exp.h
similarity index 100%
rename from src/tactic/arith_tactics/smt_solver_exp.h
rename to src/tactic/arith_tactics/dead/smt_solver_exp.h
diff --git a/src/tactic/arith_tactics/smt_solver_types.h b/src/tactic/arith_tactics/dead/smt_solver_types.h
similarity index 100%
rename from src/tactic/arith_tactics/smt_solver_types.h
rename to src/tactic/arith_tactics/dead/smt_solver_types.h
diff --git a/src/tactic/arith_tactics/elim_term_ite_strategy.cpp b/src/tactic/arith_tactics/elim_term_ite_strategy.cpp
deleted file mode 100644
index 85d79b37a..000000000
--- a/src/tactic/arith_tactics/elim_term_ite_strategy.cpp
+++ /dev/null
@@ -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 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 m_cfg;
-
- rw(ast_manager & m, params_ref const & p):
- rewriter_tpl(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;
- }
-}
-
diff --git a/src/tactic/arith_tactics/elim_term_ite_strategy.h b/src/tactic/arith_tactics/elim_term_ite_strategy.h
deleted file mode 100644
index 67eae2b29..000000000
--- a/src/tactic/arith_tactics/elim_term_ite_strategy.h
+++ /dev/null
@@ -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
diff --git a/src/tactic/arith_tactics/smt_solver_strategy.cpp b/src/tactic/arith_tactics/smt_solver_strategy.cpp
deleted file mode 100644
index 237cdcecf..000000000
--- a/src/tactic/arith_tactics/smt_solver_strategy.cpp
+++ /dev/null
@@ -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);
-}
diff --git a/src/tactic/arith_tactics/smt_solver_strategy.h b/src/tactic/arith_tactics/smt_solver_strategy.h
deleted file mode 100644
index 833d5326b..000000000
--- a/src/tactic/arith_tactics/smt_solver_strategy.h
+++ /dev/null
@@ -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 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
diff --git a/src/tactic/portfolio/install_tactics.cpp b/src/tactic/portfolio/install_tactics.cpp
index 9f99d6b77..6d5ebb13c 100644
--- a/src/tactic/portfolio/install_tactics.cpp
+++ b/src/tactic/portfolio/install_tactics.cpp
@@ -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());
diff --git a/src/tactic/smtlogic_tactics/qflia_tactic.cpp b/src/tactic/smtlogic_tactics/qflia_tactic.cpp
index a996015ce..1fb30faae 100644
--- a/src/tactic/smtlogic_tactics/qflia_tactic.cpp
+++ b/src/tactic/smtlogic_tactics/qflia_tactic.cpp
@@ -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());
}
diff --git a/src/tactic/smtlogic_tactics/qflra_tactic.cpp b/src/tactic/smtlogic_tactics/qflra_tactic.cpp
index 20182ba84..42aaa96b7 100644
--- a/src/tactic/smtlogic_tactics/qflra_tactic.cpp
+++ b/src/tactic/smtlogic_tactics/qflra_tactic.cpp
@@ -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);
}