From ac8b5e6eae5cf97146fafd4f1cc450cda7dc4a27 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 6 Nov 2015 14:10:18 -0500 Subject: [PATCH] free variable WIP --- src/smt/theory_str.cpp | 160 ++++++++++++++++++++++++++++++++++++++++- src/smt/theory_str.h | 3 + 2 files changed, 161 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7d9aaad7d..cb31aedde 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -3262,10 +3262,166 @@ final_check_status theory_str::final_check_eh() { return FC_DONE; } + // ----------------------------------------------------------- + // variables in freeVar are those not bouned by Concats + // classify variables in freeVarMap: + // (1) freeVar = unroll(r1, t1) + // (2) vars are not bounded by either concat or unroll + // ----------------------------------------------------------- + std::map > fv_unrolls_map; + std::set tmpSet; + expr * constValue = NULL; + for (std::map::iterator fvIt2 = freeVar_map.begin(); fvIt2 != freeVar_map.end(); fvIt2++) { + expr * var = fvIt2->first; + tmpSet.clear(); + get_eqc_allUnroll(var, constValue, tmpSet); + if (tmpSet.size() > 0) { + fv_unrolls_map[var] = tmpSet; + } + } + // erase var bounded by an unroll function from freeVar_map + for (std::map >::iterator fvIt3 = fv_unrolls_map.begin(); + fvIt3 != fv_unrolls_map.end(); fvIt3++) { + expr * var = fvIt3->first; + freeVar_map.erase(var); + } + // collect the case: + // * Concat(X, Y) = unroll(r1, t1) /\ Concat(X, Y) = unroll(r2, t2) + // concatEqUnrollsMap[Concat(X, Y)] = {unroll(r1, t1), unroll(r2, t2)} - // TODO the rest... - NOT_IMPLEMENTED_YET(); + std::map > concatEqUnrollsMap; + for (std::map >::iterator urItor = unrollGroup_map.begin(); + urItor != unrollGroup_map.end(); urItor++) { + expr * unroll = urItor->first; + expr * curr = unroll; + do { + if (is_concat(to_app(curr))) { + concatEqUnrollsMap[curr].insert(unroll); + concatEqUnrollsMap[curr].insert(unrollGroup_map[unroll].begin(), unrollGroup_map[unroll].end()); + } + enode * e_curr = ctx.get_enode(curr); + curr = e_curr->get_next()->get_owner(); + // curr = get_eqc_next(curr); + } while (curr != unroll); + } + + std::map > concatFreeArgsEqUnrollsMap; + std::set fvUnrollSet; + for (std::map >::iterator concatItor = concatEqUnrollsMap.begin(); + concatItor != concatEqUnrollsMap.end(); concatItor++) { + expr * concat = concatItor->first; + expr * concatArg1 = to_app(concat)->get_arg(0); + expr * concatArg2 = to_app(concat)->get_arg(1); + bool arg1Bounded = false; + bool arg2Bounded = false; + // arg1 + if (variable_set.find(concatArg1) != variable_set.end()) { + if (freeVar_map.find(concatArg1) == freeVar_map.end()) { + arg1Bounded = true; + } else { + fvUnrollSet.insert(concatArg1); + } + } else if (is_concat(to_app(concatArg1))) { + if (concatEqUnrollsMap.find(concatArg1) == concatEqUnrollsMap.end()) { + arg1Bounded = true; + } + } + // arg2 + if (variable_set.find(concatArg2) != variable_set.end()) { + if (freeVar_map.find(concatArg2) == freeVar_map.end()) { + arg2Bounded = true; + } else { + fvUnrollSet.insert(concatArg2); + } + } else if (is_concat(to_app(concatArg2))) { + if (concatEqUnrollsMap.find(concatArg2) == concatEqUnrollsMap.end()) { + arg2Bounded = true; + } + } + if (!arg1Bounded && !arg2Bounded) { + concatFreeArgsEqUnrollsMap[concat].insert( + concatEqUnrollsMap[concat].begin(), + concatEqUnrollsMap[concat].end()); + } + } + for (std::set::iterator vItor = fvUnrollSet.begin(); vItor != fvUnrollSet.end(); vItor++) { + freeVar_map.erase(*vItor); + } + + // Assign free variables + std::set fSimpUnroll; + + constValue = NULL; + + // TODO this would be a great place to print debugging information + + // TODO process_concat_eq_unroll() + /* + for (std::map >::iterator fvIt2 = concatFreeArgsEqUnrollsMap.begin(); + fvIt2 != concatFreeArgsEqUnrollsMap.end(); fvIt2++) { + expr * concat = fvIt2->first; + for (std::set::iterator urItor = fvIt2->second.begin(); urItor != fvIt2->second.end(); urItor++) { + Z3_ast unroll = *urItor; + processConcatEqUnroll(concat, unroll); + } + } + */ + + // -------- + // experimental free variable assignment - begin + // * special handling for variables that are not used in concat + // -------- + bool testAssign = true; + if (!testAssign) { + for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { + expr * freeVar = fvIt->first; + /* + std::string vName = std::string(Z3_ast_to_string(ctx, freeVar)); + if (vName.length() >= 9 && vName.substr(0, 9) == "$$_regVar") { + continue; + } + */ + // TODO if this variable represents a regular expression, continue + expr * toAssert = gen_len_val_options_for_free_var(freeVar, NULL, ""); + if (toAssert != NULL) { + assert_axiom(toAssert); + } + } + } else { + process_free_var(freeVar_map); + } + // experimental free variable assignment - end + + // TODO more unroll stuff + /* + for (std::map >::iterator fvIt1 = fv_unrolls_map.begin(); + fvIt1 != fv_unrolls_map.end(); fvIt1++) { + Z3_ast var = fvIt1->first; + fSimpUnroll.clear(); + get_eqc_simpleUnroll(t, var, constValue, fSimpUnroll); + if (fSimpUnroll.size() == 0) { + genAssignUnrollReg(t, fv_unrolls_map[var]); + } else { + Z3_ast toAssert = genAssignUnrollStr2Reg(t, var, fSimpUnroll); + if (toAssert != NULL) { + addAxiom(t, toAssert, __LINE__); + } + } + } + */ + + return FC_CONTINUE; // since by this point we've added axioms +} + +expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, std::string lenTesterValue) { + // TODO + NOT_IMPLEMENTED_YET(); +} + +void theory_str::process_free_var(std::map & freeVar_map) { + // TODO this one first + NOT_IMPLEMENTED_YET(); } void theory_str::init_model(model_generator & mg) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 3d0f14ca7..60c2c3a8e 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -153,6 +153,9 @@ namespace smt { void classify_ast_by_type_in_positive_context(std::map & varMap, std::map & concatMap, std::map & unrollMap); + expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, std::string lenTesterValue); + void process_free_var(std::map & freeVar_map); + expr * get_alias_index_ast(std::map & aliasIndexMap, expr * node); expr * getMostLeftNodeInConcat(expr * node); expr * getMostRightNodeInConcat(expr * node);