mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

merge duality changes with unstable

Browse source
This commit is contained in:
Ken McMillan 2014-10-22 10:14:05 -07:00
commit d815af9f0f
194 changed files with 3554 additions and 1887 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/arith_eq_solver.cpp
View file

@ -604,7 +604,9 @@ bool arith_eq_solver::solve_integer_equations_gcd(
}
SASSERT(g == r0[i]);
}
SASSERT(abs(r0[i]).is_one());
if (!abs(r0[i]).is_one()) {
return false;
}
live.erase(live.begin()+live_pos);
for (j = 0; j < live.size(); ++j) {
row& r = rows[live[j]];

3
src/smt/params/smt_params.cpp
View file

@ -19,10 +19,11 @@ Revision History:
#include"smt_params.h"
#include"smt_params_helper.hpp"
#include"model_params.hpp"
#include"gparams.h"
void smt_params::updt_local_params(params_ref const & _p) {
smt_params_helper p(_p);
m_auto_config = p.auto_config();
m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
m_random_seed = p.random_seed();
m_relevancy_lvl = p.relevancy();
m_ematching = p.ematching();

4
src/smt/smt_context.cpp
View file

@ -1615,6 +1615,8 @@ namespace smt {
unsigned qhead = m_qhead;
if (!bcp())
return false;
if (m_cancel_flag)
return true;
SASSERT(!inconsistent());
propagate_relevancy(qhead);
if (inconsistent())
@ -3945,7 +3947,7 @@ namespace smt {
m_fingerprints.display(tout);
);
failure fl = get_last_search_failure();
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
// don't generate model.
return;
}

2
src/smt/smt_context.h
View file

@ -76,7 +76,7 @@ namespace smt {
protected:
ast_manager & m_manager;
smt_params & m_fparams;
smt_params & m_fparams;
params_ref m_params;
setup m_setup;
volatile bool m_cancel_flag;

3
src/smt/smt_model_checker.cpp
View file

@ -136,9 +136,8 @@ namespace smt {
if (cex == 0)
return false; // no model available.
unsigned num_decls = q->get_num_decls();
unsigned num_sks = sks.size();
// Remark: sks were created for the flat version of q.
SASSERT(num_sks >= num_decls);
SASSERT(sks.size() >= num_decls);
expr_ref_buffer bindings(m_manager);
bindings.resize(num_decls);
unsigned max_generation = 0;

6
src/smt/smt_quantifier.cpp
View file

@ -453,9 +453,9 @@ namespace smt {
instantiated.
*/
virtual void add(quantifier * q) {
if (m_fparams->m_mbqi && mbqi_enabled(q)) {
m_model_finder->register_quantifier(q);
}
if (m_fparams->m_mbqi && mbqi_enabled(q)) {
m_model_finder->register_quantifier(q);
}
}
virtual void del(quantifier * q) {

17
src/smt/theory_arith.h
View file

@ -410,6 +410,7 @@ namespace smt {
atoms m_atoms; // set of theory atoms
ptr_vector<bound> m_asserted_bounds; // set of asserted bounds
unsigned m_asserted_qhead;
ptr_vector<atom> m_new_atoms; // new bound atoms that have yet to be internalized.
svector<theory_var> m_nl_monomials; // non linear monomials
svector<theory_var> m_nl_propagated; // non linear monomials that became linear
v_dependency_manager m_dep_manager; // for tracking bounds during non-linear reasoning
@ -570,6 +571,22 @@ namespace smt {
void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params);
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params);
void mk_bound_axioms(atom * a);
void mk_bound_axiom(atom* a1, atom* a2);
void flush_bound_axioms();
typename atoms::iterator next_sup(atom* a1, atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end,
bool& found_compatible);
typename atoms::iterator next_inf(atom* a1, atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end,
bool& found_compatible);
typename atoms::iterator first(atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end);
struct compare_atoms {
bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); }
};
virtual bool default_internalizer() const { return false; }
virtual bool internalize_atom(app * n, bool gate_ctx);
virtual bool internalize_term(app * term);

262
src/smt/theory_arith_core.h
View file

@ -348,13 +348,24 @@ namespace smt {
context & ctx = get_context();
simplifier & s = ctx.get_simplifier();
expr_ref s_ante(m), s_conseq(m);
expr* s_conseq_n, * s_ante_n;
bool negated;
proof_ref pr(m);
s(ante, s_ante, pr);
negated = m.is_not(s_ante, s_ante_n);
if (negated) s_ante = s_ante_n;
ctx.internalize(s_ante, false);
literal l_ante = ctx.get_literal(s_ante);
if (negated) l_ante.neg();
s(conseq, s_conseq, pr);
negated = m.is_not(s_conseq, s_conseq_n);
if (negated) s_conseq = s_conseq_n;
ctx.internalize(s_conseq, false);
literal l_conseq = ctx.get_literal(s_conseq);
if (negated) l_conseq.neg();
literal lits[2] = {l_ante, l_conseq};
ctx.mk_th_axiom(get_id(), 2, lits);
if (ctx.relevancy()) {
@ -800,48 +811,238 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
theory_var v = a1->get_var();
literal l1(a1->get_bool_var());
atoms & occs = m_var_occs[v];
if (!get_context().is_searching()) {
//
// NB. We make an assumption that user push calls propagation
// before internal scopes are pushed. This flushes all newly
// asserted atoms into the right context.
//
m_new_atoms.push_back(a1);
return;
}
numeral const & k1(a1->get_k());
atom_kind kind1 = a1->get_atom_kind();
TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";);
atoms & occs = m_var_occs[v];
typename atoms::iterator it = occs.begin();
typename atoms::iterator end = occs.end();
typename atoms::iterator lo_inf = end, lo_sup = end;
typename atoms::iterator hi_inf = end, hi_sup = end;
for (; it != end; ++it) {
atom * a2 = *it;
literal l2(a2->get_bool_var());
numeral const & k2 = a2->get_k();
atom_kind kind2 = a2->get_atom_kind();
atom * a2 = *it;
numeral const & k2(a2->get_k());
atom_kind kind2 = a2->get_atom_kind();
SASSERT(k1 != k2 || kind1 != kind2);
SASSERT(a2->get_var() == v);
parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) };
if (kind1 == A_LOWER) {
if (kind2 == A_LOWER) {
// x >= k1, x >= k2
if (k1 >= k2) mk_clause(~l1, l2, 3, coeffs);
else mk_clause(~l2, l1, 3, coeffs);
if (kind2 == A_LOWER) {
if (k2 < k1) {
if (lo_inf == end || k2 > (*lo_inf)->get_k()) {
lo_inf = it;
}
}
else {
// x >= k1, x <= k2
if (k1 > k2) mk_clause(~l1, ~l2, 3, coeffs);
else mk_clause(l1, l2, 3, coeffs);
else if (lo_sup == end || k2 < (*lo_sup)->get_k()) {
lo_sup = it;
}
}
else {
if (kind2 == A_LOWER) {
// x <= k1, x >= k2
if (k1 < k2) mk_clause(~l1, ~l2, 3, coeffs);
else mk_clause(l1, l2, 3, coeffs);
else if (k2 < k1) {
if (hi_inf == end || k2 > (*hi_inf)->get_k()) {
hi_inf = it;
}
}
else if (hi_sup == end || k2 < (*hi_sup)->get_k()) {
hi_sup = it;
}
}
if (lo_inf != end) mk_bound_axiom(a1, *lo_inf);
if (lo_sup != end) mk_bound_axiom(a1, *lo_sup);
if (hi_inf != end) mk_bound_axiom(a1, *hi_inf);
if (hi_sup != end) mk_bound_axiom(a1, *hi_sup);
}
template<typename Ext>
void theory_arith<Ext>::mk_bound_axiom(atom* a1, atom* a2) {
theory_var v = a1->get_var();
literal l1(a1->get_bool_var());
literal l2(a2->get_bool_var());
numeral const & k1(a1->get_k());
numeral const & k2(a2->get_k());
atom_kind kind1 = a1->get_atom_kind();
atom_kind kind2 = a2->get_atom_kind();
bool v_is_int = is_int(v);
SASSERT(v == a2->get_var());
SASSERT(k1 != k2 || kind1 != kind2);
parameter coeffs[3] = { parameter(symbol("farkas")),
parameter(rational(1)), parameter(rational(1)) };
if (kind1 == A_LOWER) {
if (kind2 == A_LOWER) {
if (k2 <= k1) {
mk_clause(~l1, l2, 3, coeffs);
}
else {
// x <= k1, x <= k2
if (k1 < k2) mk_clause(~l1, l2, 3, coeffs);
else mk_clause(~l2, l1, 3, coeffs);
mk_clause(l1, ~l2, 3, coeffs);
}
}
else if (k1 <= k2) {
// k1 <= k2, k1 <= x or x <= k2
mk_clause(l1, l2, 3, coeffs);
}
else {
// k1 > hi_inf, k1 <= x => ~(x <= hi_inf)
mk_clause(~l1, ~l2, 3, coeffs);
if (v_is_int && k1 == k2 + numeral(1)) {
// k1 <= x or x <= k1-1
mk_clause(l1, l2, 3, coeffs);
}
}
}
else if (kind2 == A_LOWER) {
if (k1 >= k2) {
// k1 >= lo_inf, k1 >= x or lo_inf <= x
mk_clause(l1, l2, 3, coeffs);
}
else {
// k1 < k2, k2 <= x => ~(x <= k1)
mk_clause(~l1, ~l2, 3, coeffs);
if (v_is_int && k1 == k2 - numeral(1)) {
// x <= k1 or k1+l <= x
mk_clause(l1, l2, 3, coeffs);
}
}
}
else {
// kind1 == A_UPPER, kind2 == A_UPPER
if (k1 >= k2) {
// k1 >= k2, x <= k2 => x <= k1
mk_clause(l1, ~l2, 3, coeffs);
}
else {
// k1 <= hi_sup , x <= k1 => x <= hi_sup
mk_clause(~l1, l2, 3, coeffs);
}
}
}
template<typename Ext>
void theory_arith<Ext>::flush_bound_axioms() {
while (!m_new_atoms.empty()) {
ptr_vector<atom> atoms;
atoms.push_back(m_new_atoms.back());
m_new_atoms.pop_back();
theory_var v = atoms.back()->get_var();
for (unsigned i = 0; i < m_new_atoms.size(); ++i) {
if (m_new_atoms[i]->get_var() == v) {
atoms.push_back(m_new_atoms[i]);
m_new_atoms[i] = m_new_atoms.back();
m_new_atoms.pop_back();
--i;
}
}
ptr_vector<atom> occs(m_var_occs[v]);
std::sort(atoms.begin(), atoms.end(), compare_atoms());
std::sort(occs.begin(), occs.end(), compare_atoms());
typename atoms::iterator begin1 = occs.begin();
typename atoms::iterator begin2 = occs.begin();
typename atoms::iterator end = occs.end();
begin1 = first(A_LOWER, begin1, end);
begin2 = first(A_UPPER, begin2, end);
typename atoms::iterator lo_inf = begin1, lo_sup = begin1;
typename atoms::iterator hi_inf = begin2, hi_sup = begin2;
typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1;
typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
ptr_addr_hashtable<atom> visited;
for (unsigned i = 0; i < atoms.size(); ++i) {
atom* a1 = atoms[i];
lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup);
if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1;
if (hi_sup1 != end) hi_sup = hi_sup1;
if (!flo_inf) lo_inf = end;
if (!fhi_inf) hi_inf = end;
if (!flo_sup) lo_sup = end;
if (!fhi_sup) hi_sup = end;
visited.insert(a1);
if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(a1, *lo_inf);
if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(a1, *lo_sup);
if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(a1, *hi_inf);
if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(a1, *hi_sup);
}
}
}
template<typename Ext>
typename theory_arith<Ext>::atoms::iterator
theory_arith<Ext>::first(
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end) {
for (; it != end; ++it) {
atom* a = *it;
if (a->get_atom_kind() == kind) return it;
}
return end;
}
template<typename Ext>
typename theory_arith<Ext>::atoms::iterator
theory_arith<Ext>::next_inf(
atom* a1,
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end,
bool& found_compatible) {
numeral const & k1(a1->get_k());
typename atoms::iterator result = end;
found_compatible = false;
for (; it != end; ++it) {
atom * a2 = *it;
if (a1 == a2) continue;
if (a2->get_atom_kind() != kind) continue;
numeral const & k2(a2->get_k());
found_compatible = true;
if (k2 <= k1) {
result = it;
}
else {
break;
}
}
return result;
}
template<typename Ext>
typename theory_arith<Ext>::atoms::iterator
theory_arith<Ext>::next_sup(
atom* a1,
atom_kind kind,
typename atoms::iterator it,
typename atoms::iterator end,
bool& found_compatible) {
numeral const & k1(a1->get_k());
found_compatible = false;
for (; it != end; ++it) {
atom * a2 = *it;
if (a1 == a2) continue;
if (a2->get_atom_kind() != kind) continue;
numeral const & k2(a2->get_k());
found_compatible = true;
if (k1 < k2) {
return it;
}
}
return end;
}
template<typename Ext>
bool theory_arith<Ext>::internalize_atom(app * n, bool gate_ctx) {
TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
@ -879,7 +1080,7 @@ namespace smt {
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
rational _k;
m_util.is_numeral(rhs, _k);
VERIFY(m_util.is_numeral(rhs, _k));
numeral k(_k);
atom * a = alloc(atom, bv, v, k, kind);
mk_bound_axioms(a);
@ -927,6 +1128,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";);
atom * a = get_bv2a(v);
if (!a) return;
SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@ -1072,8 +1274,10 @@ namespace smt {
}
}
while (m_final_check_idx != old_idx);
if (result == FC_DONE && m_found_unsupported_op)
if (result == FC_DONE && m_found_unsupported_op) {
TRACE("arith", tout << "Found unsupported operation\n";);
result = FC_GIVEUP;
}
return result;
}
@ -1142,6 +1346,7 @@ namespace smt {
CASSERT("arith", wf_columns());
CASSERT("arith", valid_row_assignment());
flush_bound_axioms();
propagate_linear_monomials();
while (m_asserted_qhead < m_asserted_bounds.size()) {
bound * b = m_asserted_bounds[m_asserted_qhead];
@ -2421,6 +2626,8 @@ namespace smt {
if (val == l_undef)
continue;
// TODO: check if the following line is a bottleneck
TRACE("arith", tout << "v" << a->get_bool_var() << " " << (val == l_true) << "\n";);
a->assign_eh(val == l_true, get_epsilon(a->get_var()));
if (val != l_undef && a->get_bound_kind() == b->get_bound_kind()) {
SASSERT((ctx.get_assignment(bv) == l_true) == a->is_true());
@ -2916,6 +3123,7 @@ namespace smt {
SASSERT(m_to_patch.empty());
m_to_check.reset();
m_in_to_check.reset();
m_new_atoms.reset();
CASSERT("arith", wf_rows());
CASSERT("arith", wf_columns());
CASSERT("arith", valid_row_assignment());

4
src/smt/theory_arith_int.h
View file

@ -1294,8 +1294,10 @@ namespace smt {
}
tout << "max: " << max << ", min: " << min << "\n";);
if (m_params.m_arith_ignore_int)
if (m_params.m_arith_ignore_int) {
TRACE("arith", tout << "Ignore int: give up\n";);
return FC_GIVEUP;
}
if (!gcd_test())
return FC_CONTINUE;

6
src/smt/theory_arith_nl.h
View file

@ -2314,13 +2314,15 @@ namespace smt {
return FC_DONE;
}
if (!m_params.m_nl_arith)
if (!m_params.m_nl_arith) {
TRACE("non_linear", tout << "Non-linear is not enabled\n";);
return FC_GIVEUP;
}
TRACE("process_non_linear", display(tout););
if (m_nl_rounds > m_params.m_nl_arith_rounds) {
TRACE("non_linear", tout << "GIVE UP non linear problem...\n";);
TRACE("non_linear", tout << "GIVEUP non linear problem...\n";);
IF_VERBOSE(3, verbose_stream() << "Max. non linear arithmetic rounds. Increase threshold using NL_ARITH_ROUNDS=<limit>\n";);
return FC_GIVEUP;
}

32
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
ctx.internalize(bit, true);
@ -75,12 +76,14 @@ namespace smt {
void theory_bv::mk_bit2bool(app * n) {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
if (!ctx.e_internalized(n->get_arg(0))) {
expr* first_arg = n->get_arg(0);
if (!ctx.e_internalized(first_arg)) {
// This may happen if bit2bool(x) is in a conflict
// clause that is being reinitialized, and x was not reinitialized
// yet.
// So, we internalize x (i.e., n->get_arg(0))
expr * first_arg = n->get_arg(0);
// So, we internalize x (i.e., arg)
ctx.internalize(first_arg, false);
SASSERT(ctx.e_internalized(first_arg));
// In most cases, when x is internalized, its bits are created.
@ -91,10 +94,27 @@ namespace smt {
// This will also force the creation of all bits for x.
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
SASSERT(ctx.b_internalized(n));
// numerals are not blasted into bit2bool, so we do this directly.
if (!ctx.b_internalized(n)) {
rational val;
unsigned sz;
VERIFY(m_util.is_numeral(first_arg, val, sz));
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
}
else {
enode * arg = ctx.get_enode(n->get_arg(0));
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
@ -1041,6 +1061,7 @@ namespace smt {
void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) {
if (is_bv(v1)) {
SASSERT(m_bits[v1].size() == m_bits[v2].size());
expand_diseq(v1, v2);
}
}
@ -1381,6 +1402,7 @@ namespace smt {
if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, it->m_idx);
RESET_MERGET_AUX();
return false;

7
src/smt/theory_diff_logic_def.h
View file

@ -983,11 +983,8 @@ template<typename Ext>
void theory_diff_logic<Ext>::get_eq_antecedents(
theory_var v1, theory_var v2, unsigned timestamp, conflict_resolution & cr) {
imp_functor functor(cr);
bool r;
r = m_graph.find_shortest_zero_edge_path(v1, v2, timestamp, functor);
SASSERT(r);
r = m_graph.find_shortest_zero_edge_path(v2, v1, timestamp, functor);
SASSERT(r);
VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, timestamp, functor));
VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, timestamp, functor));
}
template<typename Ext>