From b34fc06fe95645db09b8b3eb1778c9607e0c1e94 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 20 Nov 2015 12:24:23 -0500 Subject: [PATCH] fix all compilation errors, now to test it --- src/smt/theory_str.cpp | 71 +++++++++++++++++++++--------------------- src/smt/theory_str.h | 13 ++++---- 2 files changed, 42 insertions(+), 42 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1961a3e36..068745d94 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -32,7 +32,9 @@ theory_str::theory_str(ast_manager & m): tmpStringVarCount(0), tmpXorVarCount(0), avoidLoopCut(true), - loopDetected(false) + loopDetected(false), + char_set(NULL), + charSetSize(0) { } @@ -222,7 +224,6 @@ app * theory_str::mk_int(int n) { } expr * theory_str::mk_internal_lenTest_var(expr * node, int lTries) { - context & ctx = get_context(); ast_manager & m = get_manager(); std::stringstream ss; @@ -240,7 +241,6 @@ expr * theory_str::mk_internal_lenTest_var(expr * node, int lTries) { } expr * theory_str::mk_internal_valTest_var(expr * node, int len, int vTries) { - context & ctx = get_context(); ast_manager & m = get_manager(); std::stringstream ss; ss << "$$_val_" << mk_ismt2_pp(node, m) << "_" << len << "_" << vTries; @@ -257,7 +257,6 @@ expr * theory_str::mk_internal_valTest_var(expr * node, int len, int vTries) { } app * theory_str::mk_internal_xor_var() { - context & ctx = get_context(); ast_manager & m = get_manager(); std::stringstream ss; ss << tmpXorVarCount; @@ -296,7 +295,6 @@ app * theory_str::mk_str_var(std::string name) { } app * theory_str::mk_nonempty_str_var() { - context & ctx = get_context(); ast_manager & m = get_manager(); std::stringstream ss; ss << tmpStringVarCount; @@ -435,12 +433,10 @@ void theory_str::instantiate_concat_axiom(enode * cat) { SASSERT(is_concat(cat)); app * a_cat = cat->get_owner(); - context & ctx = get_context(); ast_manager & m = get_manager(); // build LHS expr_ref len_xy(m); - // TODO re-use ASTs for length subexpressions, like in old Z3-str? // TODO should we use str_util for these and other expressions? len_xy = mk_strlen(a_cat); SASSERT(len_xy); @@ -2580,9 +2576,6 @@ void theory_str::dump_assignments() { void theory_str::classify_ast_by_type(expr * node, std::map & varMap, std::map & concatMap, std::map & unrollMap) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - // check whether the node is a non-internal string variable; // testing set membership here bypasses several expensive checks if (variable_set.find(node) != variable_set.end() @@ -2620,7 +2613,6 @@ void theory_str::classify_ast_by_type(expr * node, std::map & varMap } } // recursively visit all arguments - app * aNode = to_app(node); for (unsigned i = 0; i < aNode->get_num_args(); ++i) { expr * arg = aNode->get_arg(i); classify_ast_by_type(arg, varMap, concatMap, unrollMap); @@ -2964,7 +2956,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map & strVarMap, std::map > & testerList) { +void theory_str::print_value_tester_list(svector > & testerList) { ast_manager & m = get_manager(); STRACE("t_str_detail", int ss = testerList.size(); @@ -3495,13 +3486,14 @@ void theory_str::print_value_tester_list(std::vector > & t ); } -std::string theory_str::gen_val_string(int len, std::vector & encoding) { +std::string theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); + SASSERT(char_set != NULL); - std::string re = std::string(len, charSet[0]); + std::string re = std::string(len, char_set[0]); for (int i = 0; i < (int) encoding.size() - 1; i++) { int idx = encoding[i]; - re[len - 1 - i] = charSet[idx]; + re[len - 1 - i] = char_set[idx]; } return re; } @@ -3511,10 +3503,10 @@ std::string theory_str::gen_val_string(int len, std::vector & encoding) { * - If the next encoding is valid, return false * - Otherwise, return true */ -bool theory_str::get_next_val_encode(std::vector & base, std::vector & next) { +bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { int s = 0; int carry = 0; - next.clear(); + next.reset(); for (int i = 0; i < (int) base.size(); i++) { if (i == 0) { @@ -3530,7 +3522,7 @@ bool theory_str::get_next_val_encode(std::vector & base, std::vector & } } if (next[next.size() - 1] > 0) { - next.clear(); + next.reset(); return true; } else { return false; @@ -3539,7 +3531,6 @@ bool theory_str::get_next_val_encode(std::vector & base, std::vector & expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, std::string lenStr, int tries) { - context & ctx = get_context(); ast_manager & m = get_manager(); int distance = 32; @@ -3558,11 +3549,11 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * // ---------------------------------------------------------------------------------------- int len = atoi(lenStr.c_str()); bool coverAll = false; - std::vector > options; - std::vector base; + svector options; + int_vector base; if (tries == 0) { - base = std::vector(len + 1, 0); + base = int_vector(len + 1, 0); coverAll = false; } else { expr * lastestValIndi = fvar_valueTester_map[freeVar][len][tries - 1].second; @@ -3581,12 +3572,20 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * } val_range_map[val_indicator] = options[options.size() - 1]; - STRACE("t_str_detail", tout << "value tester encoding " << printVectorInt(valRangeMap[val_indicator]) << std::endl;); + STRACE("t_str_detail", + tout << "value tester encoding " << "{" << std::endl; + int_vector vec = val_range_map[val_indicator]; + + for (int_vector::iterator it = vec.begin(); it != vec.end(); ++it) { + tout << *it << std::endl; + } + tout << "}" << std::endl; + ); // ---------------------------------------------------------------------------------------- - std::vector orList; - std::vector andList; + ptr_vector orList; + ptr_vector andList; for (long long i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()) )); @@ -3618,7 +3617,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * // If the new value tester is $$_val_x_16_i // Should add ($$_len_x_j = 16) /\ ($$_val_x_16_i = "more") // --------------------------------------- - andList.clear(); + andList.reset(); andList.push_back(m.mk_eq(len_indicator, m_strutil.mk_string(lenStr.c_str()))); for (int i = 0; i < tries; i++) { expr * vTester = fvar_valueTester_map[freeVar][len][i].second; @@ -3646,6 +3645,8 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, context & ctx = get_context(); ast_manager & m = get_manager(); + int sLevel = ctx.get_scope_level(); + int len = atoi(len_valueStr.c_str()); if (fvar_valueTester_map[freeVar].find(len) == fvar_valueTester_map[freeVar].end()) { @@ -3671,12 +3672,12 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, // Z3_ast anEqc = get_eqc_value(t, aTester, anEqcHasValue); get_eqc_value(aTester, anEqcHasValue); if (!anEqcHasValue) { - STRACE("t_str_detail", "value tester " << mk_ismt2_pp(aTester, m) + STRACE("t_str_detail", tout << "value tester " << mk_ismt2_pp(aTester, m) << "doesn't have an equivalence class value." << std::endl;); expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); - STRACE("t_str_detail", "var: " << mk_ismt2_pp(freeVar, m) << std::endl + STRACE("t_str_detail", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl << mk_ismt2_pp(makeupAssert, m) << std::endl;); assert_axiom(makeupAssert); } @@ -3701,7 +3702,6 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, } expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tries) { - context & ctx = get_context(); ast_manager & m = get_manager(); expr * freeVarLen = mk_strlen(freeVar); @@ -3724,12 +3724,12 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr expr ** or_items = alloc_svect(expr*, orList.size()); expr ** and_items = alloc_svect(expr*, andList.size() + 1); - for (int i = 0; i < orList.size(); ++i) { + for (unsigned i = 0; i < orList.size(); ++i) { or_items[i] = orList[i]; } and_items[0] = m.mk_or(orList.size(), or_items); - for(int i = 0; i < andList.size(); ++i) { + for(unsigned i = 0; i < andList.size(); ++i) { and_items[i+1] = andList[i]; } expr * lenTestAssert = m.mk_and(andList.size() + 1, and_items); @@ -3772,7 +3772,6 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr // ----------------------------------------------------------------------------------------------------- expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, std::string lenTesterValue) { - context & ctx = get_context(); ast_manager & m = get_manager(); STRACE("t_str_detail", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); @@ -3814,7 +3813,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe << " does not have an equivalence class value." << " i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); if (i > 0) { - effectiveLenInd = fvarLenTesterMap[freeVar][i - 1]; + effectiveLenInd = fvar_lenTester_map[freeVar][i - 1]; if (effectiveLenInd == lenTesterInCbEq) { effectiveLenIndiStr = lenTesterValue; } else { @@ -3850,7 +3849,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe fvar_lenTester_map[freeVar].push_back(indicator); lenTester_fvar_map[indicator] = freeVar; } else { - indicator = fvarLenTesterMap[freeVar][i]; + indicator = fvar_lenTester_map[freeVar][i]; testNum = i + 1; } expr_ref lenTestAssert(gen_len_test_options(freeVar, indicator, testNum), m); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index b7a63edb3..2f23ce43e 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -89,12 +89,13 @@ namespace smt { std::map > fvar_lenTester_map; std::map lenTester_fvar_map; - std::map > > > fvar_valueTester_map; + std::map > > > fvar_valueTester_map; std::map valueTester_fvar_map; - std::map > val_range_map; + std::map val_range_map; - int charSetSize = 0; + char * char_set; + int charSetSize; protected: void assert_axiom(expr * e); @@ -177,9 +178,9 @@ namespace smt { std::string len_valueStr, expr * valTesterInCbEq, std::string valTesterValueStr); expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, std::string lenStr, int tries); - void print_value_tester_list(std::vector > & testerList); - bool get_next_val_encode(std::vector & base, std::vector & next); - std::string gen_val_string(int len, std::vector & encoding); + void print_value_tester_list(svector > & testerList); + bool get_next_val_encode(int_vector & base, int_vector & next); + std::string gen_val_string(int len, int_vector & encoding); expr * get_alias_index_ast(std::map & aliasIndexMap, expr * node); expr * getMostLeftNodeInConcat(expr * node);