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

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-18 09:58:11 +01:00
commit 71a03dbeb3
46 changed files with 225 additions and 239 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/qi_queue.cpp
View file

@ -367,8 +367,7 @@ namespace smt {
unsigned sz = m_delayed_entries.size();
for (unsigned i = 0; i < sz; i++) {
entry & e = m_delayed_entries[i];
fingerprint * f = e.m_qb;
TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold && (!init || e.m_cost < min_cost)) {
init = true;
min_cost = e.m_cost;
@ -378,12 +377,10 @@ namespace smt {
bool result = true;
for (unsigned i = 0; i < sz; i++) {
entry & e = m_delayed_entries[i];
fingerprint * f = e.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());
TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= min_cost) {
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(qa, m_manager) << "\ncost: " << e.m_cost << "\n";);
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
m_stats.m_num_lazy_instances++;
@ -396,12 +393,10 @@ namespace smt {
bool result = true;
for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
entry & e = m_delayed_entries[i];
fingerprint * f = e.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());
TRACE("qi_queue", tout << f << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) {
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(qa, m_manager) << "\ncost: " << e.m_cost << "\n";);
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
m_stats.m_num_lazy_instances++;

5
src/smt/smt_conflict_resolution.cpp
View file

@ -99,9 +99,10 @@ namespace smt {
This method may update m_antecedents, m_todo_js and m_todo_eqs.
*/
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
ast_manager& m = get_manager();
SASSERT(m_antecedents);
TRACE("conflict_detail", tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
TRACE("conflict_detail",
ast_manager& m = get_manager();
tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
switch (js.get_kind()) {
case eq_justification::AXIOM: tout << " axiom\n"; break;
case eq_justification::EQUATION:

10
src/smt/smt_context.cpp
View file

@ -2259,6 +2259,7 @@ namespace smt {
}
unsigned ilvl = 0;
(void)ilvl;
for (unsigned j = 0; j < num; j++) {
expr * atom = cls->get_atom(j);
bool sign = cls->get_atom_sign(j);
@ -2855,8 +2856,7 @@ namespace smt {
propagate();
if (was_consistent && inconsistent()) {
// logical context became inconsistent during user PUSH
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
}
push_scope();
m_base_scopes.push_back(base_scope());
@ -3110,8 +3110,7 @@ namespace smt {
else {
TRACE("after_internalization", display(tout););
if (inconsistent()) {
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
r = l_false;
}
else {
@ -3197,8 +3196,7 @@ namespace smt {
init_assumptions(num_assumptions, assumptions);
TRACE("after_internalization", display(tout););
if (inconsistent()) {
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
mk_unsat_core();
r = l_false;
}

27
src/smt/smt_model_finder.cpp
View file

@ -2899,15 +2899,16 @@ namespace smt {
}
bool check_satisfied_residue_invariant() {
qsset::iterator it = m_satisfied.begin();
qsset::iterator end = m_satisfied.end();
for (; it != end; ++it) {
quantifier * q = *it;
SASSERT(!m_residue.contains(q));
quantifier_info * qi = get_qinfo(q);
SASSERT(qi != 0);
SASSERT(qi->get_the_one() != 0);
}
DEBUG_CODE(
qsset::iterator it = m_satisfied.begin();
qsset::iterator end = m_satisfied.end();
for (; it != end; ++it) {
quantifier * q = *it;
SASSERT(!m_residue.contains(q));
quantifier_info * qi = get_qinfo(q);
SASSERT(qi != 0);
SASSERT(qi->get_the_one() != 0);
});
return true;
}
@ -3544,14 +3545,10 @@ namespace smt {
//
// Since we only care about q (and its bindings), it only makes sense to restrict the variables of q.
bool asserted_something = false;
quantifier * flat_q = get_flat_quantifier(q);
unsigned num_decls = q->get_num_decls();
unsigned flat_num_decls = flat_q->get_num_decls();
unsigned num_sks = sks.size();
// Remark: sks were created for the flat version of q.
SASSERT(num_sks == flat_num_decls);
SASSERT(flat_num_decls >= num_decls);
SASSERT(num_sks >= num_decls);
SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size());
SASSERT(sks.size() >= num_decls);
for (unsigned i = 0; i < num_decls; i++) {
expr * sk = sks.get(num_decls - i - 1);
instantiation_set const * s = get_uvar_inst_set(q, i);

2
src/smt/theory_arith_aux.h
View file

@ -1784,7 +1784,7 @@ namespace smt {
template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) {
expr* e = get_enode(v)->get_owner();
(void)e;
SASSERT(!maintain_integrality || valid_assignment());
SASSERT(satisfy_bounds());
SASSERT(!is_quasi_base(v));

3
src/smt/theory_array.cpp
View file

@ -75,8 +75,7 @@ namespace smt {
ast_manager& m = get_manager();
context& ctx = get_context();
theory_var r = theory_array_base::mk_var(n);
theory_var r2 = m_find.mk_var();
SASSERT(r == r2);
VERIFY(r == m_find.mk_var());
SASSERT(r == static_cast<int>(m_var_data.size()));
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];

9
src/smt/theory_bv.cpp
View file

@ -457,8 +457,7 @@ namespace smt {
void theory_bv::fixed_var_eh(theory_var v) {
numeral val;
bool r = get_fixed_value(v, val);
SASSERT(r);
VERIFY(get_fixed_value(v, val));
unsigned sz = get_bv_size(v);
value_sort_pair key(val, sz);
theory_var v2;
@ -554,9 +553,8 @@ namespace smt {
void theory_bv::internalize_bv2int(app* n) {
SASSERT(!get_context().e_internalized(n));
ast_manager & m = get_manager();
context& ctx = get_context();
TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
TRACE("bv", tout << mk_bounded_pp(n, get_manager()) << "\n";);
process_args(n);
mk_enode(n);
if (!ctx.relevancy()) {
@ -1142,9 +1140,8 @@ namespace smt {
}
void theory_bv::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
atom * a = get_bv2a(v);
TRACE("bv", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
TRACE("bv", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
if (a->is_bit()) {
// The following optimization is not correct.
// Boolean variables created for performing bit-blasting are reused.

3
src/smt/theory_datatype.cpp
View file

@ -198,8 +198,7 @@ namespace smt {
theory_var theory_datatype::mk_var(enode * n) {
theory_var r = theory::mk_var(n);
theory_var r2 = m_find.mk_var();
SASSERT(r == r2);
VERIFY(r == m_find.mk_var());
SASSERT(r == static_cast<int>(m_var_data.size()));
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];

33
src/smt/theory_diff_logic_def.h
View file

@ -273,8 +273,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
template<typename Ext>
void theory_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
context & ctx = get_context();
ast_manager& m = get_manager();
TRACE("arith", tout << mk_pp(atom, m) << "\n";);
TRACE("arith", tout << mk_pp(atom, get_manager()) << "\n";);
app * lhs = to_app(atom->get_arg(0));
app * rhs = to_app(atom->get_arg(1));
app * s;
@ -606,7 +605,6 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
atom* a = 0;
m_bool_var2atom.find(bv, a);
SASSERT(a);
edge_id e_id = a->get_pos();
literal_vector lits;
for (unsigned i = 0; i < num_edges; ++i) {
@ -616,7 +614,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
TRACE("dl_activity",
tout << mk_pp(le, get_manager()) << "\n";
tout << "edge: " << e_id << "\n";
tout << "edge: " << a->get_pos() << "\n";
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
tout << "\n";
);
@ -927,18 +925,19 @@ void theory_diff_logic<Ext>::display(std::ostream & out) const {
template<typename Ext>
bool theory_diff_logic<Ext>::is_consistent() const {
context& ctx = get_context();
for (unsigned i = 0; i < m_atoms.size(); ++i) {
atom* a = m_atoms[i];
bool_var bv = a->get_bool_var();
lbool asgn = ctx.get_assignment(bv);
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
SASSERT((asgn == l_true) == a->is_true());
int edge_id = a->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
}
}
DEBUG_CODE(
context& ctx = get_context();
for (unsigned i = 0; i < m_atoms.size(); ++i) {
atom* a = m_atoms[i];
bool_var bv = a->get_bool_var();
lbool asgn = ctx.get_assignment(bv);
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
SASSERT((asgn == l_true) == a->is_true());
int edge_id = a->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
}
});
return m_graph.is_feasible();
}
@ -1194,9 +1193,9 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
ast_manager& m = get_manager();
update_simplex(S);
objective_term const& objective = m_objectives[v];
TRACE("arith",
objective_term const& objective = m_objectives[v];
for (unsigned i = 0; i < objective.size(); ++i) {
tout << "Coefficient " << objective[i].second
<< " of theory_var " << objective[i].first << "\n";

24
src/smt/theory_fpa.cpp
View file

@ -52,9 +52,8 @@ namespace smt {
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
unsigned ebits = m_th.m_fpa_util.get_ebits(s);
unsigned sbits = m_th.m_fpa_util.get_sbits(s);
SASSERT(bv_sz == ebits + sbits);
SASSERT(bv_sz == m_th.m_fpa_util.get_ebits(s) + sbits);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
@ -257,10 +256,11 @@ namespace smt {
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
TRACE("t_fpa_detail",
ast_manager & m = m_th.get_manager();
for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
mpf_manager & mpfm = m_fu.fm();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
@ -280,8 +280,7 @@ namespace smt {
rational all_r(0);
scoped_mpz all_z(mpzm);
bool r = m_bu.is_numeral(values[0], all_r, bv_sz);
SASSERT(r);
VERIFY(m_bu.is_numeral(values[0], all_r, bv_sz));
SASSERT(bv_sz == (m_ebits + m_sbits));
SASSERT(all_r.is_int());
mpzm.set(all_z, all_r.to_mpq().numerator());
@ -333,17 +332,17 @@ namespace smt {
app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
SASSERT(values.size() == 1);
ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
TRACE("t_fpa_detail",
ast_manager & m = m_th.get_manager();
for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
app * result = 0;
unsigned bv_sz;
rational val(0);
bool r = m_bu.is_numeral(values[0], val, bv_sz);
SASSERT(r);
VERIFY(m_bu.is_numeral(values[0], val, bv_sz));
SASSERT(bv_sz == 3);
switch (val.get_uint64())
@ -455,9 +454,8 @@ namespace smt {
expr_ref bv(m);
bv = wrap(e_conv);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv));
SASSERT(bv_sz == ebits + sbits);
SASSERT(bv_sz == m_fpa_util.get_ebits(m.get_sort(e_conv)) + sbits);
m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),

10
src/smt/theory_pb.cpp
View file

@ -787,8 +787,7 @@ namespace smt {
}
for (unsigned i = 0; i < ineqs->size(); ++i) {
ineq* c = (*ineqs)[i];
SASSERT(c->is_ge());
SASSERT((*ineqs)[i]->is_ge());
if (assign_watch_ge(v, is_true, *ineqs, i)) {
// i was removed from watch list.
--i;
@ -1834,13 +1833,12 @@ namespace smt {
void theory_pb::validate_assign(ineq const& c, literal_vector const& lits, literal l) const {
uint_set nlits;
context& ctx = get_context();
for (unsigned i = 0; i < lits.size(); ++i) {
SASSERT(ctx.get_assignment(lits[i]) == l_true);
SASSERT(get_context().get_assignment(lits[i]) == l_true);
nlits.insert((~lits[i]).index());
}
SASSERT(ctx.get_assignment(l) == l_undef);
SASSERT(ctx.get_assignment(c.lit()) == l_true);
SASSERT(get_context().get_assignment(l) == l_undef);
SASSERT(get_context().get_assignment(c.lit()) == l_true);
nlits.insert(l.index());
numeral sum = numeral::zero();
for (unsigned i = 0; i < c.size(); ++i) {

9
src/smt/theory_seq.cpp
View file

@ -3244,8 +3244,7 @@ void theory_seq::add_at_axiom(expr* e) {
step(s, idx, re, i, j, t) -> nth(s, idx) == t & len(s) > idx
*/
void theory_seq::propagate_step(literal lit, expr* step) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(lit) == l_true);
SASSERT(get_context().get_assignment(lit) == l_true);
expr* re, *acc, *s, *idx, *i, *j;
VERIFY(is_step(step, s, idx, re, i, j, acc));
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
@ -3265,9 +3264,8 @@ void theory_seq::propagate_step(literal lit, expr* step) {
lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
*/
void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
context& ctx = get_context();
rational r;
SASSERT(ctx.get_assignment(lit) == l_true);
SASSERT(get_context().get_assignment(lit) == l_true);
VERIFY(m_autil.is_numeral(idx, r) && r.is_unsigned());
unsigned _idx = r.get_unsigned();
expr_ref head(m), tail(m), conc(m), len1(m), len2(m);
@ -3743,7 +3741,6 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned
rej(s, idx, re, i) -> len(s) > idx if i is final
*/
void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
context& ctx = get_context();
expr *s, * idx, *re;
unsigned src;
eautomaton* aut = 0;
@ -3754,7 +3751,7 @@ void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
}
if (m_util.str.is_length(idx)) return;
SASSERT(m_autil.is_numeral(idx));
SASSERT(ctx.get_assignment(lit) == l_true);
SASSERT(get_context().get_assignment(lit) == l_true);
bool is_final = aut->is_final_state(src);
if (is_final == is_acc) {
propagate_lit(0, 1, &lit, mk_literal(m_autil.mk_ge(m_util.str.mk_length(s), idx)));

2
src/smt/theory_wmaxsat.cpp
View file

@ -260,7 +260,6 @@ void theory_wmaxsat::block() {
return;
}
++m_stats.m_num_blocks;
ast_manager& m = get_manager();
context& ctx = get_context();
literal_vector lits;
compare_cost compare_cost(*this);
@ -274,6 +273,7 @@ void theory_wmaxsat::block() {
lits.push_back(~literal(m_var2bool[costs[i]]));
}
TRACE("opt",
ast_manager& m = get_manager();
tout << "block: ";
for (unsigned i = 0; i < lits.size(); ++i) {
expr_ref tmp(m);