diff --git a/src/ast/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h
index 4e6ae9c15..ed6d506c5 100644
--- a/src/ast/simplifier/poly_simplifier_plugin.h
+++ b/src/ast/simplifier/poly_simplifier_plugin.h
@@ -37,7 +37,7 @@ protected:
expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); }
expr * mk_mul(unsigned num_args, expr * const * args);
expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); }
- expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
+ // expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); }
expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); }
void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer<expr> & result);
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index c75c12689..0faddce73 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -187,6 +187,7 @@ struct check_logic::imp {
m_bvs = true;
m_uf = true;
m_ints = true;
+ m_nonlinear = true; // non-linear 0-1 variables may get eliminated
}
else {
m_unknown_logic = true;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d6b39c394..22418ed28 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3180,7 +3180,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
sat::literal_vector lambda;
for (unsigned i = 0; i < vars.size(); i++) {
- lambda.push_back(sat::literal(i, m[vars[i]] == l_false));
+ lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false));
}
while (!lambda.empty()) {
IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";);
@@ -3259,9 +3259,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
}
}
- // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
+ is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
- is_sat = get_consequences(asms, lits, conseq);
+ // is_sat = get_consequences(asms, lits, conseq);
set_model(mdl);
return is_sat;
}
@@ -3371,13 +3371,14 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
propagate(false);
if (check_inconsistent()) return l_false;
- unsigned num_units = 0, num_iterations = 0;
- extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
+ unsigned num_iterations = 0;
+ extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
while (!unfixed_lits.empty()) {
if (scope_lvl() > 1) {
pop(scope_lvl() - 1);
}
+ propagate(false);
++num_iterations;
checkpoint();
literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
@@ -3389,8 +3390,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
literal lit = *it;
if (value(lit) != l_undef) {
++num_fixed;
- if (value(lit) == l_true && lvl(lit) == 1) {
- VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
+ if (lvl(lit) <= 1) {
+ SASSERT(value(lit) == l_true);
+ extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
}
continue;
}
@@ -3409,18 +3411,13 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
++num_resolves;
}
if (false && scope_lvl() == 1) {
+ is_sat = l_undef;
break;
}
}
- if (scope_lvl() == 1) {
- it = unfixed_lits.begin();
- for (; it != end; ++it) {
- literal lit = *it;
- if (value(lit) == l_true) {
- VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
- }
- }
- }
+
+ extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
+
if (is_sat == l_true) {
if (scope_lvl() == 1 && num_resolves > 0) {
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
@@ -3431,6 +3428,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
if (is_sat == l_undef) {
restart();
}
+ extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
}
}
if (is_sat == l_false) {
@@ -3440,7 +3438,6 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
if (is_sat == l_true) {
delete_unfixed(unfixed_lits, unfixed_vars);
}
- extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
<< " iterations: " << num_iterations
@@ -3492,19 +3489,27 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
SASSERT(!inconsistent());
unsigned sz = m_trail.size();
for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
- if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) {
- for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) {
- VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq));
- }
- break;
- }
+ extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq);
}
start = sz;
}
+ void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
+ literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
+ for (; it != end; ++it) {
+ literal lit = *it;
+ if (lvl(lit) <= 1) {
+ SASSERT(value(lit) == l_true);
+ extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
+ }
+ }
+ }
+
bool solver::check_domain(literal lit, literal lit2) {
if (!m_antecedents.contains(lit2.var())) {
+ SASSERT(value(lit2) == l_true);
m_todo_antecedents.push_back(lit2);
+ TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";);
return false;
}
else {
@@ -3514,16 +3519,17 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
bool solver::extract_assumptions(literal lit, index_set& s) {
justification js = m_justification[lit.var()];
+ TRACE("sat", tout << lit << " " << js << "\n";);
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
- if (!check_domain(lit, js.get_literal())) return false;
+ if (!check_domain(lit, ~js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
case justification::TERNARY:
- if (!check_domain(lit, js.get_literal1())) return false;
- if (!check_domain(lit, js.get_literal2())) return false;
+ if (!check_domain(lit, ~js.get_literal1()) ||
+ !check_domain(lit, ~js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
@@ -3531,7 +3537,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
if (c[i] != lit) {
- if (!check_domain(lit, c[i])) return false;
+ if (!check_domain(lit, ~c[i])) return false;
s |= m_antecedents.find(c[i].var());
}
}
@@ -3565,7 +3571,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
}
- bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
+ bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
index_set s;
if (m_antecedents.contains(lit.var())) {
return true;
@@ -3574,16 +3580,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
s.insert(lit.index());
}
else {
- SASSERT(m_todo_antecedents.empty());
if (!extract_assumptions(lit, s)) {
SASSERT(!m_todo_antecedents.empty());
- while (!m_todo_antecedents.empty()) {
- index_set s1;
- if (extract_assumptions(m_todo_antecedents.back(), s1)) {
- m_todo_antecedents.pop_back();
- }
- }
- VERIFY (extract_assumptions(lit, s));
+ return false;
}
add_assumption(lit);
}
@@ -3601,6 +3600,16 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
return true;
}
+ void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
+ SASSERT(m_todo_antecedents.empty());
+ m_todo_antecedents.push_back(lit);
+ while (!m_todo_antecedents.empty()) {
+ if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) {
+ m_todo_antecedents.pop_back();
+ }
+ }
+ }
+
void solver::asymmetric_branching() {
if (scope_lvl() > 0 || inconsistent())
return;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 091162f23..a26abe1e0 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -498,7 +498,11 @@ namespace sat {
void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
- bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+ void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+
+ void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+
+ bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index ae2aa95e2..255e2044f 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -762,6 +762,21 @@ namespace smt {
TRACE("bv", tout << mk_pp(cond, get_manager()) << "\n"; tout << l << "\n";); \
}
+ void theory_bv::internalize_sub(app *n) {
+ SASSERT(!get_context().e_internalized(n));
+ SASSERT(n->get_num_args() == 2);
+ process_args(n);
+ ast_manager & m = get_manager();
+ enode * e = mk_enode(n);
+ expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
+ get_arg_bits(e, 0, arg1_bits);
+ get_arg_bits(e, 1, arg2_bits);
+ SASSERT(arg1_bits.size() == arg2_bits.size());
+ expr_ref carry(m);
+ m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, carry);
+ init_bits(e, bits);
+ }
+
MK_UNARY(internalize_not, mk_not);
MK_UNARY(internalize_redand, mk_redand);
MK_UNARY(internalize_redor, mk_redor);
@@ -848,6 +863,7 @@ namespace smt {
switch (term->get_decl_kind()) {
case OP_BV_NUM: internalize_num(term); return true;
case OP_BADD: internalize_add(term); return true;
+ case OP_BSUB: internalize_sub(term); return true;
case OP_BMUL: internalize_mul(term); return true;
case OP_BSDIV_I: internalize_sdiv(term); return true;
case OP_BUDIV_I: internalize_udiv(term); return true;
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 17d03b412..50e4f9c30 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -172,6 +172,7 @@ namespace smt {
bool get_fixed_value(theory_var v, numeral & result) const;
void internalize_num(app * n);
void internalize_add(app * n);
+ void internalize_sub(app * n);
void internalize_mul(app * n);
void internalize_udiv(app * n);
void internalize_sdiv(app * n);
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 9afd97de5..35601f374 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -137,8 +137,10 @@ public:
SASSERT(num.is_unsigned());
expr_ref head(m);
ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
- head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
- consequences[i] = m.mk_implies(a, head);
+ if (enums.size() > num.get_unsigned()) {
+ head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
+ consequences[i] = m.mk_implies(a, head);
+ }
}
}
return r;
diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp
index c34e109d3..b95977a46 100644
--- a/src/test/cnf_backbones.cpp
+++ b/src/test/cnf_backbones.cpp
@@ -152,14 +152,13 @@ static void brute_force_consequences(sat::solver& s, sat::literal_vector const&
static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
lbool r = s.check(asms.size(), asms.c_ptr());
- display_status(r);
if (r != l_true) {
return r;
}
sat::model const & m = s.get_model();
sat::literal_vector lambda, backbones;
- for (unsigned i = 1; i < m.size(); i++) {
- lambda.push_back(sat::literal(i, m[i] == l_false));
+ for (unsigned i = 0; i < vars.size(); i++) {
+ lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false));
}
while (!lambda.empty()) {
IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << backbones.size() << ")\n";);
@@ -270,10 +269,15 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
}
void tst_cnf_backbones(char ** argv, int argc, int& i) {
+ bool use_chunk = i + 1 < argc && argv[i + 1] == std::string("chunk");
+ if (use_chunk) ++i;
+ char const* file = "";
if (i + 1 < argc) {
- bool use_chunk = (i + 2 < argc && argv[i + 1] == std::string("chunk"));
- if (use_chunk) ++i;
- cnf_backbones(use_chunk, argv[i + 1]);
- ++i;
+ file = argv[i + 1];
}
+ else {
+ file = argv[1];
+ }
+ cnf_backbones(use_chunk, file);
+ ++i;
}