mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-08 16:37:08 -08:00
parent 6c2e7e7675
commit 24de0a9b90
2 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_seq.cpp
View file

@ -44,14 +44,13 @@ void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d
expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
std::pair<expr*, enode_pair_dependency*> value; std::pair<expr*, enode_pair_dependency*> value;
if (m_map.find(e, value)) { d = 0;
d = value.second; // TBD add path compression?
return value.first; while (m_map.find(e, value)) {
} d = d ? m_dm.mk_join(d, value.second) : value.second;;
else { e = value.first;
d = 0;
return e;
} }
return e;
} }
void theory_seq::solution_map::pop_scope(unsigned num_scopes) { void theory_seq::solution_map::pop_scope(unsigned num_scopes) {
@ -77,7 +76,7 @@ theory_seq::theory_seq(ast_manager& m):
theory(m.mk_family_id("seq")), theory(m.mk_family_id("seq")),
m(m), m(m),
m_dam(m_dep_array_value_manager, m_alloc), m_dam(m_dep_array_value_manager, m_alloc),
m_rep(m), m_rep(m, m_dm),
m_ineqs(m), m_ineqs(m),
m_axioms(m), m_axioms(m),
m_axioms_head(0), m_axioms_head(0),

5
src/smt/theory_seq.h
View file

@ -46,17 +46,18 @@ namespace smt {
typedef union_find<theory_seq> th_union_find; typedef union_find<theory_seq> th_union_find;
typedef trail_stack<theory_seq> th_trail_stack; typedef trail_stack<theory_seq> th_trail_stack;
class solution_map { class solution_map {
enum map_update { INS, DEL }; enum map_update { INS, DEL };
ast_manager& m; ast_manager& m;
enode_pair_dependency_manager& m_dm;
obj_map<expr, std::pair<expr*, enode_pair_dependency*> > m_map; obj_map<expr, std::pair<expr*, enode_pair_dependency*> > m_map;
expr_ref_vector m_lhs, m_rhs; expr_ref_vector m_lhs, m_rhs;
ptr_vector<enode_pair_dependency> m_deps; ptr_vector<enode_pair_dependency> m_deps;
svector<map_update> m_updates; svector<map_update> m_updates;
unsigned_vector m_limit; unsigned_vector m_limit;
public: public:
solution_map(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
void update(expr* e, expr* r, enode_pair_dependency* d); void update(expr* e, expr* r, enode_pair_dependency* d);
expr* find(expr* e, enode_pair_dependency*& d); expr* find(expr* e, enode_pair_dependency*& d);
void push_scope() { m_limit.push_back(m_updates.size()); } void push_scope() { m_limit.push_back(m_updates.size()); }