mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 10:50:24 +00:00
Code Activity

added TODO markers in theory_str.h for moving to obj_map, remove include of stdbool for now

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-16 07:46:27 -07:00
parent 46048d5150
commit 86d3bbe6cb
5 changed files with 48 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_str.h
View file

@ -77,25 +77,8 @@ public:
void register_value(expr * n) override { /* Ignore */ }
};
// rather than modify obj_pair_map I inherit from it and add my own helper methods
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
public:
expr * operator[](std::pair<expr*, expr*> key) const {
expr * value;
bool found = this->find(key.first, key.second, value);
if (found) {
return value;
} else {
TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
return nullptr;
}
}
bool contains(std::pair<expr*, expr*> key) const {
expr * unused;
return this->find(key.first, key.second, unused);
}
};
// NSB: added operator[] and contains to obj_pair_hashtable
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail<Ctx> {
@ -169,7 +152,7 @@ class theory_str : public theory {
struct T_cut
{
int level;
std::map<expr*, int> vars;
obj_map<expr, int> vars;
T_cut() {
level = -100;
@ -292,8 +275,8 @@ protected:
int tmpXorVarCount;
int tmpLenTestVarCount;
int tmpValTestVarCount;
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
@ -312,9 +295,11 @@ protected:
obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map;
// TBD: need to replace by obj_map for determinism
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map;
// TBD: need to replace by obj_map for determinism
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
std::map<expr*, expr*> valueTester_fvar_map;
@ -322,8 +307,10 @@ protected:
// This can't be an expr_ref_vector because the constructor is wrong,
// we would need to modify the allocator so we pass in ast_manager
// TBD: need to replace by obj_map for determinism
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
std::map<expr*, expr*> unroll_var_map;
// TBD: need to replace by obj_pair_map for determinism
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
expr_ref_vector contains_map;
@ -332,9 +319,10 @@ protected:
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
// TBD: do a curried map for determinism.
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
// TBD: need to replace by obj_map for determinism
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
svector<char> char_set;