mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

deal with subtraction that manages to sneak in. Issue #996

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-01 15:22:06 -07:00
parent aceee3fac8
commit d14f2af5ae
8 changed files with 84 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifier/poly_simplifier_plugin.h
View file

@ -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);

1
src/cmd_context/check_logic.cpp
View file

@ -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;

81
src/sat/sat_solver.cpp
View file

@ -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;

6
src/sat/sat_solver.h
View file

@ -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);

16
src/smt/theory_bv.cpp
View file

@ -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;

1
src/smt/theory_bv.h
View file

@ -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);

6
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -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;

18
src/test/cnf_backbones.cpp
View file

@ -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;
}