mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-24 20:47:02 -07:00
parent ceb4c985bf
commit e4bf1663b6
2 changed files with 46 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/diff_logic.h
View file

@ -1365,7 +1365,7 @@ public:
for (unsigned head = 0; head < bfs_todo.size(); ++head) { for (unsigned head = 0; head < bfs_todo.size(); ++head) {
bfs_elem & curr = bfs_todo[head]; bfs_elem & curr = bfs_todo[head];
int parent_idx = head; int parent_idx = head;
dl_var v = curr.m_var; dl_var v = curr.m_var;
TRACE("dl_bfs", tout << "processing: " << v << "\n";); TRACE("dl_bfs", tout << "processing: " << v << "\n";);
edge_id_vector & edges = m_out_edges[v]; edge_id_vector & edges = m_out_edges[v];
for (edge_id e_id : edges) { for (edge_id e_id : edges) {

110
src/smt/theory_special_relations.cpp
View file

@ -157,23 +157,20 @@ namespace smt {
final_check_status theory_special_relations::final_check_eh() { final_check_status theory_special_relations::final_check_eh() {
TRACE("special_relations", tout << "\n";); TRACE("special_relations", tout << "\n";);
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
lbool r = l_true; lbool r = final_check(*kv.m_value);
for (; it != end && r == l_true; ++it) { switch (r) {
r = final_check(*it->m_value); case l_undef:
return FC_GIVEUP;
case l_false:
return FC_CONTINUE;
default:
break;
}
} }
switch (r) {
case l_undef:
return FC_GIVEUP;
case l_false:
return FC_CONTINUE;
default:
break;
}
it = m_relations.begin();
bool new_equality = false; bool new_equality = false;
for (; it != end; ++it) { for (auto const& kv : m_relations) {
if (extract_equalities(*it->m_value)) { if (extract_equalities(*kv.m_value)) {
new_equality = true; new_equality = true;
} }
} }
@ -421,6 +418,7 @@ namespace smt {
u_map<ptr_vector<expr>> map; u_map<ptr_vector<expr>> map;
lbool res = l_true; lbool res = l_true;
// TBD: non-functional code?
for (atom * ap : r.m_asserted_atoms) { for (atom * ap : r.m_asserted_atoms) {
if (res != l_true) break; if (res != l_true) break;
atom a = *ap; atom a = *ap;
@ -449,7 +447,7 @@ namespace smt {
auto f = m.mk_implies( b, m.mk_not(literals.back()) ); auto f = m.mk_implies( b, m.mk_not(literals.back()) );
m_nested_solver->assert_expr(f); m_nested_solver->assert_expr(f);
atom_cache.insert(b->get_id(), &a); atom_cache.insert(b->get_id(), ap);
assumptions.push_back(b); assumptions.push_back(b);
r.m_explanation.reset(); r.m_explanation.reset();
if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) { if (m_nested_solver->check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
@ -496,9 +494,8 @@ namespace smt {
} }
void theory_special_relations::reset_eh() { void theory_special_relations::reset_eh() {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { dealloc(kv.m_value);
dealloc(it->m_value);
} }
m_relations.reset(); m_relations.reset();
del_atoms(0); del_atoms(0);
@ -510,21 +507,18 @@ namespace smt {
VERIFY(m_bool_var2atom.find(v, a)); VERIFY(m_bool_var2atom.find(v, a));
a->set_phase(is_true); a->set_phase(is_true);
a->get_relation().m_asserted_atoms.push_back(a); a->get_relation().m_asserted_atoms.push_back(a);
//std::cerr << "ASSIGN: " << a->v1() << ' ' << a->v2() << "\n";
} }
void theory_special_relations::push_scope_eh() { void theory_special_relations::push_scope_eh() {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { kv.m_value->push();
it->m_value->push();
} }
m_atoms_lim.push_back(m_atoms.size()); m_atoms_lim.push_back(m_atoms.size());
} }
void theory_special_relations::pop_scope_eh(unsigned num_scopes) { void theory_special_relations::pop_scope_eh(unsigned num_scopes) {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { kv.m_value->pop(num_scopes);
it->m_value->pop(num_scopes);
} }
unsigned new_lvl = m_atoms_lim.size() - num_scopes; unsigned new_lvl = m_atoms_lim.size() - num_scopes;
del_atoms(m_atoms_lim[new_lvl]); del_atoms(m_atoms_lim[new_lvl]);
@ -544,9 +538,8 @@ namespace smt {
void theory_special_relations::collect_statistics(::statistics & st) const { void theory_special_relations::collect_statistics(::statistics & st) const {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { kv.m_value->m_graph.collect_statistics(st);
it->m_value->m_graph.collect_statistics(st);
} }
} }
@ -613,9 +606,7 @@ namespace smt {
if (g.get_assignment(u) <= val_v) { if (g.get_assignment(u) <= val_v) {
continue; continue;
} }
int_vector const& edges = g.get_out_edges(u); for (edge_id e : g.get_out_edges(u)) {
for (unsigned i = 0; i < edges.size(); ++i) {
edge_id e = edges[i];
if (is_strict_neighbour_edge(g, e)) { if (is_strict_neighbour_edge(g, e)) {
todo.push_back(g.get_target(e)); todo.push_back(g.get_target(e));
} }
@ -773,9 +764,7 @@ namespace smt {
} }
unsigned nc = 1; unsigned nc = 1;
bool all_p = true; bool all_p = true;
int_vector const& edges = g.get_out_edges(v); for (edge_id e : g.get_out_edges(v)) {
for (unsigned i = 0; i < edges.size(); ++i) {
edge_id e = edges[i];
if (is_strict_neighbour_edge(g, e)) { if (is_strict_neighbour_edge(g, e)) {
dl_var dst = g.get_target(e); dl_var dst = g.get_target(e);
TRACE("special_relations", tout << v << " -> " << dst << "\n";); TRACE("special_relations", tout << v << " -> " << dst << "\n";);
@ -839,23 +828,22 @@ namespace smt {
} }
void theory_special_relations::init_model(model_generator & m) { void theory_special_relations::init_model(model_generator & m) {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { switch (kv.m_value->m_property) {
switch (it->m_value->m_property) {
case sr_lo: case sr_lo:
init_model_lo(*it->m_value, m); init_model_lo(*kv.m_value, m);
break; break;
case sr_plo: case sr_plo:
init_model_plo(*it->m_value, m); init_model_plo(*kv.m_value, m);
break; break;
case sr_to: case sr_to:
init_model_to(*it->m_value, m); init_model_to(*kv.m_value, m);
break; break;
case sr_po: case sr_po:
init_model_po(*it->m_value, m); init_model_po(*kv.m_value, m);
break; break;
default: default:
UNREACHABLE(); //ASHU: added to remove warning! Should be supported! UNREACHABLE(); //ASHU: added to remove warning! Should be supported!
} }
} }
} }
@ -864,38 +852,30 @@ namespace smt {
if (m_relations.empty()) return; if (m_relations.empty()) return;
out << "Theory Special Relations\n"; out << "Theory Special Relations\n";
display_var2enode(out); display_var2enode(out);
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { out << mk_pp(kv.m_value->decl(), get_manager()) << ":\n";
out << mk_pp(it->m_value->decl(), get_manager()) << ":\n"; kv.m_value->m_graph.display(out);
it->m_value->m_graph.display(out); kv.m_value->m_uf.display(out);
it->m_value->m_uf.display(out); for (atom* ap : kv.m_value->m_asserted_atoms) {
for (unsigned i = 0; i < it->m_value->m_asserted_atoms.size(); ++i){ display_atom(out, *ap);
atom& a = *it->m_value->m_asserted_atoms[i];
display_atom( out, a );
} }
} }
} }
void theory_special_relations::collect_asserted_po_atoms( vector< std::pair<bool_var,bool> >& atoms) const { void theory_special_relations::collect_asserted_po_atoms(vector<std::pair<bool_var, bool>>& atoms) const {
obj_map<func_decl, relation*>::iterator it = m_relations.begin(), end = m_relations.end(); for (auto const& kv : m_relations) {
for (; it != end; ++it) { relation& r = *kv.m_value;
relation& r = *(it->m_value ); if (r.m_property != sr_po) continue;
if( r.m_property != sr_po ) continue; for (atom* ap : r.m_asserted_atoms) {
// SASSERT( r.m_asserted_qhead == r.m_asserted_atoms.size() ); atoms.push_back(std::make_pair(ap->var(), ap->phase()));
for (unsigned i = 0; i < r.m_asserted_atoms.size(); ++i) {
atom& a = *r.m_asserted_atoms[i];
atoms.push_back( std::make_pair(a.var(),a.phase()) );
} }
} }
} }
void theory_special_relations::display_atom( std::ostream & out, atom& a ) const { void theory_special_relations::display_atom(std::ostream & out, atom& a) const {
context& ctx = get_context(); context& ctx = get_context();
expr* e = ctx.bool_var2expr( a.var() ); expr* e = ctx.bool_var2expr( a.var() );
if( !a.phase() ) out << "(not "; out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n";
out << mk_pp( e, get_manager());
if( !a.phase() ) out << ")";
out << "\n";
} }
} }