mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

temporarily patched in a get_eqc_allUnroll() implementation

Browse source
This commit is contained in:
Murphy Berzish 2015-11-06 14:13:38 -05:00
parent ac8b5e6eae
commit e9b31f2995
2 changed files with 29 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_str.cpp
View file

@ -3263,7 +3263,7 @@ final_check_status theory_str::final_check_eh() {
}
// -----------------------------------------------------------
// variables in freeVar are those not bouned by Concats
// variables in freeVar are those not bounded by Concats
// classify variables in freeVarMap:
// (1) freeVar = unroll(r1, t1)
// (2) vars are not bounded by either concat or unroll
@ -3424,6 +3424,30 @@ void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
NOT_IMPLEMENTED_YET();
}
/*
* Collect all unroll functions
* and constant string in eqc of node n
*/
void theory_str::get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet) {
constStr = NULL;
unrollFuncSet.clear();
context & ctx = get_context();
expr * curr = n;
do {
if (is_string(to_app(curr))) {
constStr = curr;
} else if (false) /*(td->Unroll == Z3_get_app_decl(ctx, Z3_to_app(ctx, curr)))*/ { // TODO
if (unrollFuncSet.find(curr) == unrollFuncSet.end()) {
unrollFuncSet.insert(curr);
}
}
enode * e_curr = ctx.get_enode(curr);
curr = e_curr->get_next()->get_owner();
// curr = get_eqc_next(t, curr);
} while (curr != n);
}
void theory_str::init_model(model_generator & mg) {
TRACE("t_str", tout << "initializing model" << std::endl; display(tout););
m_factory = alloc(str_value_factory, get_manager(), get_family_id());

4
src/smt/theory_str.h
View file

@ -160,6 +160,10 @@ namespace smt {
expr * getMostLeftNodeInConcat(expr * node);
expr * getMostRightNodeInConcat(expr * node);
// strRegex
void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
void dump_assignments();
public:
theory_str(ast_manager & m);