mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-11-06 17:29:53 -08:00
commit 3d993a4ee1
15 changed files with 246 additions and 180 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/cmd_context/cmd_context.cpp
View file

@ -507,6 +507,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "QF_ANIA" ||
s == "QF_LIRA" ||
s == "QF_UFLIA" ||
s == "QF_UFLRA" ||
s == "QF_UFIDL" ||
@ -518,6 +520,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_UFNIA" ||
s == "QF_UFNIRA" ||
s == "QF_BVRE" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
@ -526,9 +529,12 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "UFLRA" ||
s == "UFNRA" ||
s == "UFNIRA" ||
s == "NIA" ||
s == "NRA" ||
s == "UFNIA" ||
s == "LIA" ||
s == "LRA" ||
s == "UFIDL" ||
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
@ -583,10 +589,12 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
return
s == "QF_AX" ||
s == "QF_AUFLIA" ||
s == "QF_ANIA" ||
s == "QF_ALIA" ||
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||

6
src/smt/smt_conflict_resolution.cpp
View file

@ -288,11 +288,13 @@ namespace smt {
}
void conflict_resolution::process_antecedent(literal antecedent, unsigned & num_marks) {
TRACE("conflict", tout << "processing antecedent: "; m_ctx.display_literal(tout, antecedent); tout << "\n";);
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
m_ctx.set_mark(var);
m_ctx.inc_bvar_activity(var);

6
src/smt/smt_context.cpp
View file

@ -285,7 +285,9 @@ namespace smt {
}
void context::assign_core(literal l, b_justification j, bool decision) {
TRACE("assign_core", tout << "assigning: " << l << " "; display_literal(tout, l); tout << "\n";);
TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
display_literal(tout, l); tout << " level: " << m_scope_lvl << "\n";
display(tout, j););
SASSERT(l.var() < static_cast<int>(m_b_internalized_stack.size()));
m_assigned_literals.push_back(l);
m_assignment[l.index()] = l_true;
@ -1722,7 +1724,7 @@ namespace smt {
}
bool context::propagate() {
TRACE("propagate", tout << "propagating...\n";);
TRACE("propagate", tout << "propagating... " << m_qhead << ":" << m_assigned_literals.size() << "\n";);
while (true) {
if (inconsistent())
return false;

2
src/smt/smt_context.h
View file

@ -1237,6 +1237,8 @@ namespace smt {
void display_profile(std::ostream & out) const;
void display(std::ostream& out, b_justification j) const;
// -----------------------------------
//
// Debugging support

95
src/smt/smt_context_pp.cpp
View file

@ -27,19 +27,19 @@ namespace smt {
std::ostream& context::display_last_failure(std::ostream& out) const {
switch(m_last_search_failure) {
case OK:
case OK:
return out << "OK";
case UNKNOWN:
case UNKNOWN:
return out << "UNKNOWN";
case TIMEOUT:
return out << "TIMEOUT";
case MEMOUT:
case MEMOUT:
return out << "MEMOUT";
case CANCELED:
case CANCELED:
return out << "CANCELED";
case NUM_CONFLICTS:
case NUM_CONFLICTS:
return out << "NUM_CONFLICTS";
case THEORY:
case THEORY:
if (!m_incomplete_theories.empty()) {
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
@ -52,7 +52,7 @@ namespace smt {
out << "THEORY";
}
return out;
case QUANTIFIERS:
case QUANTIFIERS:
return out << "QUANTIFIERS";
}
UNREACHABLE();
@ -78,18 +78,18 @@ namespace smt {
r += "))";
break;
}
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
case UNKNOWN: r = "incomplete"; break;
}
return r;
}
void context::display_asserted_formulas(std::ostream & out) const {
m_asserted_formulas.display_ll(out, get_pp_visited());
}
void context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr());
l.display_compact(out, m_bool_var2expr.c_ptr());
}
void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
@ -97,7 +97,7 @@ namespace smt {
}
void context::display_literals_verbose(std::ostream & out, unsigned num_lits, literal const * lits) const {
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr());
display_verbose(out, m_manager, num_lits, lits, m_bool_var2expr.c_ptr(), "\n");
}
void context::display_literal_info(std::ostream & out, literal l) const {
@ -151,16 +151,16 @@ namespace smt {
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
display_literal(out, l);
out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
<< ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
<< ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
<< mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n";
}
}
void context::display_clause(std::ostream & out, clause const * cls) const {
cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
}
void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
ptr_vector<clause>::const_iterator it = v.begin();
ptr_vector<clause>::const_iterator end = v.end();
@ -201,12 +201,13 @@ namespace smt {
if (!m_assigned_literals.empty()) {
out << "current assignment:\n";
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
display_literal(out, *it);
out << " ";
out << ": ";
display_verbose(out, m_manager, 1, &*it, m_bool_var2expr.c_ptr());
out << "\n";
}
out << "\n";
}
}
@ -216,7 +217,7 @@ namespace smt {
pp.set_status("unknown");
pp.set_logic(logic);
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
expr_ref n(m_manager);
literal2expr(*it, n);
@ -301,7 +302,7 @@ namespace smt {
th->display(out);
}
}
void context::display(std::ostream & out) const {
get_pp_visited().reset();
out << "Logical context:\n";
@ -336,16 +337,16 @@ namespace smt {
void context::display_eq_detail(std::ostream & out, enode * n) const {
SASSERT(n->is_eq());
out << "#" << n->get_owner_id()
<< ", root: #" << n->get_root()->get_owner_id()
out << "#" << n->get_owner_id()
<< ", root: #" << n->get_root()->get_owner_id()
<< ", cg: #" << n->m_cg->get_owner_id()
<< ", val: " << get_assignment(enode2bool_var(n))
<< ", lhs: #" << n->get_arg(0)->get_owner_id()
<< ", rhs: #" << n->get_arg(1)->get_owner_id()
<< ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id()
<< ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id()
<< ", val: " << get_assignment(enode2bool_var(n))
<< ", lhs: #" << n->get_arg(0)->get_owner_id()
<< ", rhs: #" << n->get_arg(1)->get_owner_id()
<< ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id()
<< ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id()
<< ", is_marked: " << n->is_marked()
<< ", is_relevant: " << is_relevant(n)
<< ", is_relevant: " << is_relevant(n)
<< ", iscope_lvl: " << n->get_iscope_lvl() << "\n";
}
@ -354,7 +355,7 @@ namespace smt {
enode_vector::iterator end = n->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
if (parent->is_eq())
if (parent->is_eq())
display_eq_detail(out, parent);
}
}
@ -447,7 +448,7 @@ namespace smt {
g_lemma_id++;
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, const char * logic) const {
ast_smt_pp pp(m_manager);
@ -471,7 +472,7 @@ namespace smt {
pp.display_smt2(out, n);
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, const char * logic) const {
char buffer[BUFFER_SZ];
@ -533,7 +534,7 @@ namespace smt {
n->display_lbls(out);
}
}
void context::display_decl2enodes(std::ostream & out) const {
out << "decl2enodes:\n";
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
@ -544,7 +545,7 @@ namespace smt {
out << "id " << id << " ->";
enode_vector::const_iterator it2 = v.begin();
enode_vector::const_iterator end2 = v.end();
for (; it2 != end2; ++it2)
for (; it2 != end2; ++it2)
out << " #" << (*it2)->get_owner_id();
out << "\n";
}
@ -567,7 +568,7 @@ namespace smt {
out << std::right;
if (lit_internalized(n))
out << get_assignment(n);
else
else
out << "l_undef";
}
if (e_internalized(n)) {
@ -576,20 +577,13 @@ namespace smt {
}
out << "\n";
if (is_app(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
todo.push_back(to_app(n)->get_arg(i));
}
}
}
void context::trace_assign(literal l, b_justification j, bool decision) const {
SASSERT(m_manager.has_trace_stream());
std::ostream & out = m_manager.trace_stream();
out << "[assign] ";
display_literal(out, l);
if (decision)
out << " decision";
out << " ";
void context::display(std::ostream& out, b_justification j) const {
switch (j.get_kind()) {
case b_justification::AXIOM:
out << "axiom";
@ -597,8 +591,6 @@ namespace smt {
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal(out, l);
out << " ";
display_literal(out, l2);
break;
}
@ -618,5 +610,16 @@ namespace smt {
out << "\n";
}
void context::trace_assign(literal l, b_justification j, bool decision) const {
SASSERT(m_manager.has_trace_stream());
std::ostream & out = m_manager.trace_stream();
out << "[assign] ";
display_literal(out, l);
if (decision)
out << " decision";
out << " ";
display(out, j);
}
};

4
src/smt/smt_literal.cpp
View file

@ -69,10 +69,10 @@ namespace smt {
}
}
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) {
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) {
for (unsigned i = 0; i < num_lits; i++) {
if (i > 0)
out << " ";
out << sep;
lits[i].display(out, m, bool_var2expr_map);
}
}

2
src/smt/smt_literal.h
View file

@ -103,7 +103,7 @@ namespace smt {
void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " ");
template<typename T>
void neg_literals(unsigned num_lits, literal const * lits, T & result) {

47
src/smt/theory_arith.h
View file

@ -218,7 +218,7 @@ namespace smt {
typedef svector<enode_pair> eq_vector;
// keep track of coefficients used for bounds for proof generation.
class antecedents {
class antecedents_t {
literal_vector m_lits;
eq_vector m_eqs;
vector<numeral> m_lit_coeffs;
@ -233,16 +233,38 @@ namespace smt {
void init();
public:
antecedents(): m_init(false) {}
antecedents_t(): m_init(false) {}
void reset();
literal_vector& lits() { return m_lits; }
eq_vector& eqs() { return m_eqs; }
literal_vector const& lits() const { return m_lits; }
eq_vector const& eqs() const { return m_eqs; }
void push_lit(literal l, numeral const& r, bool proofs_enabled);
void push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled);
void append(unsigned sz, literal const* ls) { m_lits.append(sz, ls); }
void append(unsigned sz, enode_pair const* ps) { m_eqs.append(sz, ps); }
unsigned num_params() const { return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; }
numeral const* lit_coeffs() const { return m_lit_coeffs.c_ptr(); }
numeral const* eq_coeffs() const { return m_eq_coeffs.c_ptr(); }
parameter* params(char const* name);
std::ostream& display(theory_arith& th, std::ostream& out) const;
};
class antecedents {
theory_arith& th;
antecedents_t& a;
public:
antecedents(theory_arith& th);
~antecedents();
literal_vector const& lits() const { return a.lits(); }
eq_vector const& eqs() const { return a.eqs(); }
void push_lit(literal l, numeral const& r, bool e) { a.push_lit(l, r, e); }
void push_eq(enode_pair const& p, numeral const& r, bool e) { a.push_eq(p, r, e); }
void append(unsigned sz, literal const* ls) { a.append(sz, ls); }
void append(unsigned sz, enode_pair const* ps) { a.append(sz, ps); }
unsigned num_params() const { return a.num_params(); }
numeral const* lit_coeffs() const { return a.lit_coeffs(); }
numeral const* eq_coeffs() const { return a.eq_coeffs(); }
parameter* params(char const* name) { return a.params(name); }
std::ostream& display(std::ostream& out) const { return a.display(th, out); }
};
class gomory_cut_justification;
@ -324,11 +346,14 @@ namespace smt {
public:
derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
virtual ~derived_bound() {}
literal_vector const& lits() const { return m_lits; }
eq_vector const& eqs() const { return m_eqs; }
virtual bool has_justification() const { return true; }
virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled);
virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); }
virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); }
virtual void display(theory_arith const& th, std::ostream& out) const;
};
class justified_derived_bound : public derived_bound {
@ -460,8 +485,8 @@ namespace smt {
svector<scope> m_scopes;
literal_vector m_tmp_literal_vector2;
antecedents m_tmp_antecedents;
antecedents m_tmp_antecedents2;
antecedents_t m_antecedents[3];
unsigned m_antecedents_index;
struct var_value_hash;
friend struct var_value_hash;
@ -506,6 +531,8 @@ namespace smt {
bool relax_bounds() const { return m_params.m_arith_stronger_lemmas; }
bool skip_big_coeffs() const { return m_params.m_arith_skip_rows_with_big_coeffs; }
bool dump_lemmas() const { return m_params.m_arith_dump_lemmas; }
void dump_lemmas(literal l, antecedents const& ante);
void dump_lemmas(literal l, derived_bound const& ante);
bool process_atoms() const;
unsigned get_num_conflicts() const { return m_num_conflicts; }
var_kind get_var_kind(theory_var v) const { return m_data[v].kind(); }
@ -750,7 +777,7 @@ namespace smt {
void explain_bound(row const & r, int idx, bool lower, inf_numeral & delta,
antecedents & antecedents);
void mk_implied_bound(row const & r, unsigned idx, bool lower, theory_var v, bound_kind kind, inf_numeral const & k);
void assign_bound_literal(literal l, row const & r, unsigned idx, bool lower, inf_numeral & delta, antecedents& antecedents);
void assign_bound_literal(literal l, row const & r, unsigned idx, bool lower, inf_numeral & delta);
void propagate_bounds();
// -----------------------------------
@ -836,7 +863,9 @@ namespace smt {
// Justification
//
// -----------------------------------
void set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, antecedents& antecedents, bool is_lia, char const* proof_rule);
void set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs, antecedents& antecedents, char const* proof_rule);
void set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule);
void set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule);
void collect_fixed_var_justifications(row const & r, antecedents& antecedents) const;
// -----------------------------------
@ -989,7 +1018,7 @@ namespace smt {
gb_result compute_grobner(svector<theory_var> const & nl_cluster);
bool max_min_nl_vars();
final_check_status process_non_linear();
antecedents& get_antecedents();
// -----------------------------------
//

17
src/smt/theory_arith_aux.h
View file

@ -316,7 +316,7 @@ namespace smt {
// -----------------------------------
template<typename Ext>
void theory_arith<Ext>::antecedents::init() {
void theory_arith<Ext>::antecedents_t::init() {
if (!m_init && !empty()) {
m_params.push_back(parameter(symbol("unknown-arith")));
for (unsigned i = 0; i < m_lits.size(); i++) {
@ -330,7 +330,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::reset() {
void theory_arith<Ext>::antecedents_t::reset() {
m_init = false;
m_eq_coeffs.reset();
m_lit_coeffs.reset();
@ -340,7 +340,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::push_lit(literal l, numeral const& r, bool proofs_enabled) {
void theory_arith<Ext>::antecedents_t::push_lit(literal l, numeral const& r, bool proofs_enabled) {
m_lits.push_back(l);
if (proofs_enabled) {
m_lit_coeffs.push_back(r);
@ -348,7 +348,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) {
void theory_arith<Ext>::antecedents_t::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) {
m_eqs.push_back(p);
if (proofs_enabled) {
m_eq_coeffs.push_back(r);
@ -356,7 +356,7 @@ namespace smt {
}
template<typename Ext>
parameter * theory_arith<Ext>::antecedents::params(char const* name) {
parameter * theory_arith<Ext>::antecedents_t::params(char const* name) {
if (empty()) return 0;
init();
m_params[0] = parameter(symbol(name));
@ -740,8 +740,8 @@ namespace smt {
}
}
else {
a.lits().append(m_lits.size(), m_lits.c_ptr());
a.eqs().append(m_eqs.size(), m_eqs.c_ptr());
a.append(m_lits.size(), m_lits.c_ptr());
a.append(m_eqs.size(), m_eqs.c_ptr());
}
}
@ -804,8 +804,7 @@ namespace smt {
*/
template<typename Ext>
void theory_arith<Ext>::accumulate_justification(bound & b, derived_bound& new_bound, numeral const& coeff, literal_idx_set & lits, eq_set & eqs) {
antecedents& ante = m_tmp_antecedents;
ante.reset();
antecedents ante(*this);
b.push_justification(ante, coeff, proofs_enabled());
unsigned num_lits = ante.lits().size();
for (unsigned i = 0; i < num_lits; ++i) {

172
src/smt/theory_arith_core.h
View file

@ -349,7 +349,6 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_axiom(expr * ante, expr * conseq) {
ast_manager & m = get_manager();
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";);
context & ctx = get_context();
simplifier & s = ctx.get_simplifier();
expr_ref s_ante(m), s_conseq(m);
@ -371,6 +370,9 @@ namespace smt {
literal l_conseq = ctx.get_literal(s_conseq);
if (negated) l_conseq.neg();
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
tout << s_ante << "\n" << s_conseq << "\n";);
literal lits[2] = {l_ante, l_conseq};
ctx.mk_th_axiom(get_id(), 2, lits);
if (ctx.relevancy()) {
@ -394,12 +396,12 @@ namespace smt {
void theory_arith<Ext>::mk_div_axiom(expr * p, expr * q) {
if (!m_util.is_zero(q)) {
ast_manager & m = get_manager();
expr_ref div(m), zero(m), eqz(m), eq(m);
TRACE("div_axiom_bug", tout << "expanding div_axiom for: " << mk_pp(p, m) << " / " << mk_pp(q, m) << "\n";);
expr * div = m_util.mk_div(p, q);
expr * zero = m_util.mk_numeral(rational(0), false);
expr_ref eqz(m), eq(m);
eqz = m.mk_eq(q, zero);
eq = m.mk_eq(m_util.mk_mul(q, div), p);
div = m_util.mk_div(p, q);
zero = m_util.mk_numeral(rational(0), false);
eqz = m.mk_eq(q, zero);
eq = m.mk_eq(m_util.mk_mul(q, div), p);
TRACE("div_axiom_bug", tout << "eqz: " << mk_pp(eqz, m) << "\neq: " << mk_pp(eq, m) << "\n";);
mk_axiom(eqz, eq);
}
@ -410,15 +412,21 @@ namespace smt {
if (!m_util.is_zero(divisor)) {
// if divisor is zero, then idiv and mod are uninterpreted functions.
ast_manager & m = get_manager();
expr * div = m_util.mk_idiv(dividend, divisor);
expr * mod = m_util.mk_mod(dividend, divisor);
expr * zero = m_util.mk_numeral(rational(0), true);
expr * abs_divisor = m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor);
expr_ref div(m), mod(m), zero(m), abs_divisor(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);
eqz = m.mk_eq(divisor, zero);
eq = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
lower = m_util.mk_le(zero, mod);
upper = m_util.mk_lt(mod, abs_divisor);
div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_numeral(rational(0), true);
abs_divisor = m.mk_ite(m_util.mk_lt(divisor, zero), m_util.mk_sub(zero, divisor), divisor);
eqz = m.mk_eq(divisor, zero);
eq = m.mk_eq(m_util.mk_add(m_util.mk_mul(divisor, div), mod), dividend);
lower = m_util.mk_le(zero, mod);
upper = m_util.mk_lt(mod, abs_divisor);
TRACE("div_axiom_bug",
tout << "eqz: " << mk_pp(eqz, m) << "\neq: " << mk_pp(eq, m) << "\n";
tout << "lower: " << mk_pp(lower, m) << "\n";
tout << "upper: " << mk_pp(upper, m) << "\n";);
mk_axiom(eqz, eq);
mk_axiom(eqz, lower);
mk_axiom(eqz, upper);
@ -814,6 +822,7 @@ namespace smt {
void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
theory_var v = a1->get_var();
atoms & occs = m_var_occs[v];
//SASSERT(v != 15);
TRACE("mk_bound_axioms", tout << "add bound axioms for v" << v << " " << a1 << "\n";);
if (!get_context().is_searching()) {
//
@ -937,6 +946,8 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::flush_bound_axioms() {
CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
while (!m_new_atoms.empty()) {
ptr_vector<atom> atoms;
atoms.push_back(m_new_atoms.back());
@ -950,6 +961,10 @@ namespace smt {
--i;
}
}
TRACE("arith",
for (unsigned i = 0; i < atoms.size(); ++i) {
atoms[i]->display(*this, tout);
});
ptr_vector<atom> occs(m_var_occs[v]);
std::sort(atoms.begin(), atoms.end(), compare_atoms());
@ -1140,7 +1155,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
TRACE("arith", tout << "v" << v << " " << is_true << "\n";);
TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
atom * a = get_bv2a(v);
if (!a) return;
SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@ -1299,28 +1314,6 @@ namespace smt {
final_check_status theory_arith<Ext>::final_check_eh() {
TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
TRACE("arith_final_check", display(tout););
#if 0
if (true /*m_params.m_smtlib_dump_lemmas*/) {
literal_buffer tmp;
for (unsigned i = 0; i < m_asserted_qhead; i++) {
bound * b = m_asserted_bounds[i];
if (b->is_atom()) {
atom* a = static_cast<atom*>(b);
bool_var bv = a->get_bool_var();
lbool is_true = get_context().get_assignment(bv);
if (is_true == l_true) {
tmp.push_back(literal(bv));
}
else if (is_true == l_false) {
tmp.push_back(~literal(bv));
}
}
}
get_context().display_lemma_as_smt_problem(tmp.size(), tmp.c_ptr(), false_literal, "QF_LIA");
}
#endif
if (!propagate_core())
return FC_CONTINUE;
@ -1530,6 +1523,7 @@ namespace smt {
m_branch_cut_counter(0),
m_eager_gcd(m_params.m_arith_eager_gcd),
m_final_check_idx(0),
m_antecedents_index(0),
m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_liberal_final_check(true),
m_changed_assignment(false),
@ -2207,15 +2201,15 @@ namespace smt {
}
}
TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";);
antecedents& ante = get_antecedents();
antecedents ante(*this);
explain_bound(r, idx, !is_below, delta, ante);
b->push_justification(ante, numeral(1), coeffs_enabled());
TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i);
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";
ante.display(tout););
set_conflict(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(x_i), "farkas");
set_conflict(ante, ante, "farkas");
// display_bounds_in_smtlib();
}
@ -2353,11 +2347,11 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) {
SASSERT(b1->get_var() == b2->get_var());
antecedents& ante = get_antecedents();
antecedents ante(*this);
b1->push_justification(ante, numeral(1), coeffs_enabled());
b2->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
set_conflict(ante, ante, "farkas");
TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
tout << "bounds: " << b1 << " " << b2 << "\n";);
}
@ -2595,7 +2589,6 @@ namespace smt {
if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty()))
return;
context & ctx = get_context();
ante.reset(); // !!!!TBD: should equality ante also be reset here!!!!
row_entry const & entry = r[idx];
numeral coeff = entry.m_coeff;
if (relax_bounds()) {
@ -2700,7 +2693,6 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_implied_bound(row const & r, unsigned idx, bool is_lower, theory_var v, bound_kind kind, inf_numeral const & k) {
atoms const & as = m_var_occs[v];
antecedents& ante = get_antecedents();
inf_numeral const & epsilon = get_epsilon(v);
inf_numeral delta;
typename atoms::const_iterator it = as.begin();
@ -2721,7 +2713,7 @@ namespace smt {
}
TRACE("propagate_bounds", tout << "v" << v << " >= " << k << ", v" << v << " >= " << k2 << ", delta: " << delta << "\n";
display_row(tout, r););
assign_bound_literal(l, r, idx, is_lower, delta, ante);
assign_bound_literal(l, r, idx, is_lower, delta);
}
// v <= k k < k2 |- v < k2 |- not v >= k2
if (kind == B_UPPER && k < k2) {
@ -2737,7 +2729,7 @@ namespace smt {
if (delta.is_nonneg()) {
TRACE("propagate_bounds", tout << "v" << v << " <= " << k << ", not v" << v << " >= " << k2 << ", delta: " << delta << "\n";
display_row(tout, r););
assign_bound_literal(~l, r, idx, is_lower, delta, ante);
assign_bound_literal(~l, r, idx, is_lower, delta);
}
}
}
@ -2752,7 +2744,7 @@ namespace smt {
if (delta.is_nonneg()) {
TRACE("propagate_bounds", tout << "v" << v << " >= " << k << ", not v" << v << " <= " << k2 << ", delta: " << delta << "\n";
display_row(tout, r););
assign_bound_literal(~l, r, idx, is_lower, delta, ante);
assign_bound_literal(~l, r, idx, is_lower, delta);
}
}
// v <= k k <= k2 |- v <= k2
@ -2763,7 +2755,7 @@ namespace smt {
}
TRACE("propagate_bounds", tout << "v" << v << " <= " << k << ", v" << v << " <= " << k2 << ", delta: " << delta << "\n";
display_row(tout, r););
assign_bound_literal(l, r, idx, is_lower, delta, ante);
assign_bound_literal(l, r, idx, is_lower, delta);
}
}
}
@ -2771,28 +2763,34 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::assign_bound_literal(literal l, row const & r, unsigned idx, bool is_lower, inf_numeral & delta, antecedents& ante) {
void theory_arith<Ext>::dump_lemmas(literal l, antecedents const& ante) {
context & ctx = get_context();
if (dump_lemmas()) {
TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";);
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
}
}
template<typename Ext>
void theory_arith<Ext>::dump_lemmas(literal l, derived_bound const& ante) {
context & ctx = get_context();
if (dump_lemmas()) {
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l, 0);
}
}
template<typename Ext>
void theory_arith<Ext>::assign_bound_literal(literal l, row const & r, unsigned idx, bool is_lower, inf_numeral & delta) {
m_stats.m_bound_props++;
context & ctx = get_context();
antecedents ante(*this);
explain_bound(r, idx, is_lower, delta, ante);
if (dump_lemmas()) {
char const * logic = is_int(r.get_base_var()) ? "QF_LIA" : "QF_LRA";
ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(),
ante.eqs().size(), ante.eqs().c_ptr(), l, logic);
}
dump_lemmas(l, ante);
TRACE("propagate_bounds",
literal_vector::const_iterator it = ante.lits().begin();
literal_vector::const_iterator end = ante.lits().end();
for (; it != end; ++it) {
ctx.display_detailed_literal(tout, *it);
tout << " ";
}
eq_vector::const_iterator it2 = ante.eqs().begin();
eq_vector::const_iterator end2 = ante.eqs().end();
for (; it2 != end2; ++it2) {
tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " ";
}
tout << " --> ";
ante.display(tout) << " --> ";
ctx.display_detailed_literal(tout, l);
tout << "\n";);
if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
@ -2874,19 +2872,26 @@ namespace smt {
// Justification
//
// -----------------------------------
template<typename Ext>
void theory_arith<Ext>::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
}
template<typename Ext>
void theory_arith<Ext>::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) {
dump_lemmas(false_literal, ante);
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule);
}
template<typename Ext>
void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs,
antecedents& bounds, bool is_lia, char const* proof_rule) {
void theory_arith<Ext>::set_conflict(unsigned num_literals, literal const * lits, unsigned num_eqs, enode_pair const * eqs,
antecedents& bounds, char const* proof_rule) {
SASSERT(num_literals != 0 || num_eqs != 0);
context & ctx = get_context();
m_stats.m_conflicts++;
m_num_conflicts++;
if (dump_lemmas()) {
char const * logic = is_lia ? "QF_LIA" : "QF_LRA";
ctx.display_lemma_as_smt_problem(num_literals, lits, num_eqs, eqs, false_literal, logic);
}
region & r = ctx.get_region();
TRACE("arith_conflict",
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
@ -2908,7 +2913,7 @@ namespace smt {
record_conflict(num_literals, lits, num_eqs, eqs, bounds.num_params(), bounds.params(proof_rule));
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(get_id(), r, num_literals, lits, num_eqs, eqs,
ext_theory_conflict_justification(get_id(), ctx.get_region(), num_literals, lits, num_eqs, eqs,
bounds.num_params(), bounds.params(proof_rule))));
}
@ -3320,11 +3325,20 @@ namespace smt {
*/
template<typename Ext>
typename theory_arith<Ext>::antecedents& theory_arith<Ext>::get_antecedents() {
m_tmp_antecedents.reset();
return m_tmp_antecedents;
theory_arith<Ext>::antecedents::antecedents(theory_arith& th):
th(th),
a(th.m_antecedents[th.m_antecedents_index]) {
SASSERT(th.m_antecedents_index < 3);
a.reset();
++th.m_antecedents_index;
}
template<typename Ext>
theory_arith<Ext>::antecedents::~antecedents() {
--th.m_antecedents_index;
}
};
#endif /* THEORY_ARITH_CORE_H_ */

8
src/smt/theory_arith_eq.h
View file

@ -52,7 +52,7 @@ namespace smt {
// contain invalid (key -> value) pairs. So, we must check whether v2 is really equal to val (previous test) AND it has
// the same sort of v. The following test was missing in a previous version of Z3.
if (!is_equal(v, v2) && is_int(v) == is_int(v2)) {
antecedents& ante = get_antecedents();
antecedents ante(*this);
//
// v <= k <= v2 => v <= v2
@ -241,7 +241,7 @@ namespace smt {
is_int(x) == is_int(x2) &&
!is_equal(x, x2)) {
antecedents& ante = get_antecedents();
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
//
@ -256,7 +256,7 @@ namespace smt {
if (k.is_zero() && y != null_theory_var && !is_equal(x, y) && is_int(x) == is_int(y)) {
// found equality x = y
antecedents& ante = get_antecedents();
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
TRACE("propagate_cheap_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
m_stats.m_offset_eqs++;
@ -296,7 +296,7 @@ namespace smt {
if (new_eq) {
if (!is_equal(x, x2) && is_int(x) == is_int(x2)) {
SASSERT(y == y2 && k == k2);
antecedents& ante = get_antecedents();
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
collect_fixed_var_justifications(r2, ante);
TRACE("propagate_cheap_eq", tout << "propagate eq two rows:\n";

40
src/smt/theory_arith_int.h
View file

@ -201,12 +201,13 @@ namespace smt {
SASSERT(is_int(v));
SASSERT(!get_value(v).is_int());
m_stats.m_branches++;
TRACE("arith_branching", tout << "branching v" << v << " = " << get_value(v) << "\n";
TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
display_var(tout, v););
numeral k = ceil(get_value(v));
rational _k = k.to_rational();
expr * bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
TRACE("arith_branching", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
expr_ref bound(get_manager());
bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
context & ctx = get_context();
ctx.internalize(bound, true);
ctx.mark_as_relevant(bound);
@ -452,11 +453,11 @@ namespace smt {
expr_ref pol(m);
pol = m_util.mk_add(_args.size(), _args.c_ptr());
result = m_util.mk_ge(pol, m_util.mk_numeral(k, all_int));
TRACE("arith_mk_polynomial", tout << "before simplification:\n" << mk_pp(pol, m) << "\n";);
TRACE("arith_mk_polynomial", tout << "before simplification:\n" << result << "\n";);
simplifier & s = get_context().get_simplifier();
proof_ref pr(m);
s(result, result, pr);
TRACE("arith_mk_polynomial", tout << "after simplification:\n" << mk_pp(pol, m) << "\n";);
TRACE("arith_mk_polynomial", tout << "after simplification:\n" << result << "\n";);
SASSERT(is_well_sorted(get_manager(), result));
}
@ -498,7 +499,7 @@ namespace smt {
TRACE("gomory_cut", tout << "applying cut at:\n"; display_row_info(tout, r););
antecedents& ante = get_antecedents();
antecedents ante(*this);
m_stats.m_gomory_cuts++;
@ -508,6 +509,8 @@ namespace smt {
numeral f_0 = Ext::fractional_part(m_value[x_i]);
numeral one_minus_f_0 = numeral(1) - f_0;
SASSERT(!f_0.is_zero());
SASSERT(!one_minus_f_0.is_zero());
numeral lcm_den(1);
unsigned num_ints = 0;
@ -521,36 +524,30 @@ namespace smt {
a_ij.neg(); // make the used format compatible with the format used in: Integrating Simplex with DPLL(T)
if (is_real(x_j)) {
numeral new_a_ij;
TRACE("gomory_cut_detail", tout << a_ij << "*v" << x_j << "\n";);
if (at_lower(x_j)) {
if (a_ij.is_pos()) {
new_a_ij = a_ij / one_minus_f_0;
}
else {
TRUSTME(!f_0.is_zero());
new_a_ij = a_ij / f_0;
new_a_ij.neg();
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
else {
SASSERT(at_upper(x_j));
if (a_ij.is_pos()) {
TRUSTME(!f_0.is_zero());
new_a_ij = a_ij / f_0;
new_a_ij.neg(); // the upper terms are inverted.
}
else {
// new_a_ij = - a_ij / one_minus_f_0
// new_a_ij.neg() // the upper terms are inverted
new_a_ij = a_ij / one_minus_f_0;
new_a_ij = a_ij / one_minus_f_0;
}
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
TRACE("gomory_cut_detail", tout << a_ij << "*v" << x_j << " k: " << k << "\n";);
pol.push_back(row_entry(new_a_ij, x_j));
}
else {
@ -572,7 +569,6 @@ namespace smt {
else {
new_a_ij = (numeral(1) - f_j) / f_0;
}
// k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
@ -585,11 +581,10 @@ namespace smt {
new_a_ij = (numeral(1) - f_j) / one_minus_f_0;
}
new_a_ij.neg(); // the upper terms are inverted
// k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled());
}
TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << " k: " << k << "\n";);
pol.push_back(row_entry(new_a_ij, x_j));
lcm_den = lcm(lcm_den, denominator(new_a_ij));
}
@ -603,7 +598,7 @@ namespace smt {
if (pol.empty()) {
SASSERT(k.is_pos());
// conflict 0 >= k where k is positive
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, true, "gomory-cut");
set_conflict(ante, ante, "gomory-cut");
return true;
}
else if (pol.size() == 1) {
@ -639,18 +634,19 @@ namespace smt {
}
TRACE("gomory_cut_detail", tout << "after *lcm\n";
for (unsigned i = 0; i < pol.size(); i++) {
tout << pol[i].m_coeff << " " << pol[i].m_var << "\n";
tout << pol[i].m_coeff << " * v" << pol[i].m_var << "\n";
}
tout << "k: " << k << "\n";);
}
mk_polynomial_ge(pol.size(), pol.c_ptr(), k.to_rational(), bound);
}
TRACE("gomory_cut", tout << "new cut:\n" << mk_pp(bound, get_manager()) << "\n";);
TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
literal l = null_literal;
context & ctx = get_context();
ctx.internalize(bound, true);
l = ctx.get_literal(bound);
ctx.mark_as_relevant(l);
dump_lemmas(l, ante);
ctx.assign(l, ctx.mk_justification(
gomory_cut_justification(
get_id(), ctx.get_region(),
@ -721,7 +717,7 @@ namespace smt {
if (!(consts / gcds).is_int()) {
TRACE("gcd_test", tout << "row failed the GCD test:\n"; display_row_info(tout, r););
antecedents& ante = get_antecedents();
antecedents ante(*this);
collect_fixed_var_justifications(r, ante);
context & ctx = get_context();
ctx.set_conflict(
@ -754,7 +750,7 @@ namespace smt {
numeral l(consts);
numeral u(consts);
antecedents& ante = get_antecedents();
antecedents ante(*this);
typename vector<row_entry>::const_iterator it = r.begin_entries();

5
src/smt/theory_arith_nl.h
View file

@ -1910,11 +1910,10 @@ namespace smt {
*/
template<typename Ext>
void theory_arith<Ext>::set_conflict(v_dependency * d) {
bool is_lia = false; // TODO: fix it, but this is only used for debugging.
antecedents& ante = get_antecedents();
antecedents ante(*this);
derived_bound b(null_theory_var, inf_numeral(0), B_LOWER);
dependency2new_bound(d, b);
set_conflict(b.m_lits.size(), b.m_lits.c_ptr(), b.m_eqs.size(), b.m_eqs.c_ptr(), ante, is_lia, "arith_nl");
set_conflict(b, ante, "arith_nl");
TRACE("non_linear",
for (unsigned i = 0; i < b.m_lits.size(); ++i) {
tout << b.m_lits[i] << " ";

12
src/smt/theory_arith_pp.h
View file

@ -399,6 +399,18 @@ namespace smt {
out << "\n";
}
template<typename Ext>
std::ostream& theory_arith<Ext>::antecedents_t::display(theory_arith& th, std::ostream & out) const {
th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr());
if (!lits().empty()) out << "\n";
ast_manager& m = th.get_manager();
for (unsigned i = 0; i < m_eqs.size(); ++i) {
out << mk_pp(m_eqs[i].first->get_owner(), m) << " ";
out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
}
return out;
}
template<typename Ext>
void theory_arith<Ext>::display_deps(std::ostream & out, v_dependency* dep) {
ptr_vector<void> bounds;

2
src/util/scoped_timer.cpp
View file

@ -204,7 +204,7 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
timer_delete(m_timerid);
timer_delete(m_timerid);
#else
// Other Platforms
#endif