mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 18:06:15 +00:00
Code Activity

fix zstring

Browse source
This commit is contained in:
Murphy Berzish 2017-02-27 21:16:15 -05:00
parent c62b55f9b1
commit 11000efbfe
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -9723,7 +9723,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin
return final_term; return final_term;
} }
expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue) { expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
@ -9889,7 +9889,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT
// lenTesterInCbEq != NULL, and its value will be passed by lenTesterValue // lenTesterInCbEq != NULL, and its value will be passed by lenTesterValue
// The difference is that in new_eq_eh(), lenTesterInCbEq and its value have NOT been put into a same eqc // The difference is that in new_eq_eh(), lenTesterInCbEq and its value have NOT been put into a same eqc
// ----------------------------------------------------------------------------------------------------- // -----------------------------------------------------------------------------------------------------
expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, std::string lenTesterValue) { expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();

4
src/smt/theory_str.h
View file

@ -492,7 +492,7 @@ namespace smt {
std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap); std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
expr * mk_internal_lenTest_var(expr * node, int lTries); expr * mk_internal_lenTest_var(expr * node, int lTries);
expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, std::string lenTesterValue); expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue);
void process_free_var(std::map<expr*, int> & freeVar_map); void process_free_var(std::map<expr*, int> & freeVar_map);
expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries);
expr * gen_free_var_options(expr * freeVar, expr * len_indicator, expr * gen_free_var_options(expr * freeVar, expr * len_indicator,
@ -504,7 +504,7 @@ namespace smt {
zstring gen_val_string(int len, int_vector & encoding); zstring gen_val_string(int len, int_vector & encoding);
// binary search heuristic // binary search heuristic
expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, std::string previousLenTesterValue); expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue);
expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits); expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits);
bool free_var_attempt(expr * nn1, expr * nn2); bool free_var_attempt(expr * nn1, expr * nn2);