mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

add tracing, fix #2214, remove unused variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-02 12:20:55 -07:00
parent 5fdf5b67a4
commit ff6d703c05
3 changed files with 14 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/opt_parse.cpp
View file

@ -417,7 +417,7 @@ private:
if (is_num(c)) { if (is_num(c)) {
rational n(0); rational n(0);
unsigned div = 1; rational div(1);
while (is_num(c) && !in.eof()) { while (is_num(c) && !in.eof()) {
n = n*rational(10) + rational(c - '0'); n = n*rational(10) + rational(c - '0');
in.next(); in.next();
@ -429,11 +429,11 @@ private:
while (is_num(c) && !in.eof()) { while (is_num(c) && !in.eof()) {
n = n*rational(10) + rational(c - '0'); n = n*rational(10) + rational(c - '0');
in.next(); in.next();
div *= 10; div *= rational(10);
c = in.ch(); c = in.ch();
} }
} }
if (div > 1) n = n / rational(div); if (div > rational(1)) n = n / div;
if (neg) n.neg(); if (neg) n.neg();
m_tokens.push_back(asymbol(n, in.line())); m_tokens.push_back(asymbol(n, in.line()));
IF_VERBOSE(10, verbose_stream() << "num: " << m_tokens.back() << "\n"); IF_VERBOSE(10, verbose_stream() << "num: " << m_tokens.back() << "\n");

1
src/smt/diff_logic.h
View file

@ -1752,7 +1752,6 @@ public:
find_subsumed1(id, subsumed); find_subsumed1(id, subsumed);
typename edge_id_vector::const_iterator it, end, it3, end3;
for (edge_id e_id : m_in_edges[src]) { for (edge_id e_id : m_in_edges[src]) {
edge const& e2 = m_edges[e_id]; edge const& e2 = m_edges[e_id];
if (!e2.is_enabled() || e2.get_source() == dst) { if (!e2.is_enabled() || e2.get_source() == dst) {

19
src/smt/theory_special_relations.cpp
View file

@ -133,7 +133,6 @@ namespace smt {
} }
void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) {
context& ctx = get_context();
app* t1 = get_enode(v1)->get_owner(); app* t1 = get_enode(v1)->get_owner();
app* t2 = get_enode(v2)->get_owner(); app* t2 = get_enode(v2)->get_owner();
literal eq = mk_eq(t1, t2, false); literal eq = mk_eq(t1, t2, false);
@ -282,6 +281,7 @@ namespace smt {
void theory_special_relations::set_conflict(relation& r) { void theory_special_relations::set_conflict(relation& r) {
literal_vector const& lits = r.m_explanation; literal_vector const& lits = r.m_explanation;
context & ctx = get_context(); context & ctx = get_context();
TRACE("special_relations", ctx.display_literals_verbose(tout, lits) << "\n";);
vector<parameter> params; vector<parameter> params;
ctx.set_conflict( ctx.set_conflict(
ctx.mk_justification( ctx.mk_justification(
@ -319,22 +319,26 @@ namespace smt {
int_vector scc_id; int_vector scc_id;
u_map<unsigned> roots; u_map<unsigned> roots;
context& ctx = get_context(); context& ctx = get_context();
ast_manager& m = get_manager();
(void)m;
r.m_graph.compute_zero_edge_scc(scc_id); r.m_graph.compute_zero_edge_scc(scc_id);
for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) { for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) {
if (scc_id[i] == -1) { if (scc_id[i] == -1) {
continue; continue;
} }
enode* n = get_enode(i); enode* x = get_enode(i);
if (roots.find(scc_id[i], j)) { if (roots.find(scc_id[i], j)) {
enode* m = get_enode(j); enode* y = get_enode(j);
if (n->get_root() != m->get_root()) { if (x->get_root() != y->get_root()) {
new_eq = true; new_eq = true;
unsigned timestamp = r.m_graph.get_timestamp(); unsigned timestamp = r.m_graph.get_timestamp();
r.m_explanation.reset(); r.m_explanation.reset();
r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r); r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r);
r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r); r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r);
eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), r.m_explanation.size(), r.m_explanation.c_ptr()))); literal_vector const& lits = r.m_explanation;
ctx.assign_eq(n, m, js); TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << " ", lits) << "\n";);
eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr())));
ctx.assign_eq(x, y, js);
} }
} }
else { else {
@ -646,7 +650,6 @@ namespace smt {
void theory_special_relations::init_model_po(relation& r, model_generator& mg) { void theory_special_relations::init_model_po(relation& r, model_generator& mg) {
ast_manager& m = get_manager(); ast_manager& m = get_manager();
sort* s = r.m_decl->get_domain(0); sort* s = r.m_decl->get_domain(0);
context& ctx = get_context();
datatype_util dt(m); datatype_util dt(m);
recfun::util rf(m); recfun::util rf(m);
recfun::decl::plugin& p = rf.get_plugin(); recfun::decl::plugin& p = rf.get_plugin();
@ -715,7 +718,7 @@ namespace smt {
for (atom* ap : r.m_asserted_atoms) { for (atom* ap : r.m_asserted_atoms) {
atom& a = *ap; atom& a = *ap;
if (!a.phase()) continue; if (!a.phase()) continue;
SASSERT(ctx.get_assignment(a.var()) == l_true); SASSERT(get_context().get_assignment(a.var()) == l_true);
expr* n1 = get_enode(a.v1())->get_root()->get_owner(); expr* n1 = get_enode(a.v1())->get_root()->get_owner();
expr* n2 = get_enode(a.v2())->get_root()->get_owner(); expr* n2 = get_enode(a.v2())->get_root()->get_owner();
expr* Sr = connected_rec_body; expr* Sr = connected_rec_body;