mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

use z3str2 eqc semantics for get_eqc_value

Browse source
This commit is contained in:
Murphy Berzish 2016-09-14 15:37:48 -04:00
parent 50353168ef
commit 804009a757
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_str.cpp
View file

@ -3967,6 +3967,7 @@ void theory_str::unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr) {
* Return that constant if it is found, and set hasEqcValue to true. * Return that constant if it is found, and set hasEqcValue to true.
* Otherwise, return n, and set hasEqcValue to false. * Otherwise, return n, and set hasEqcValue to false.
*/ */
/*
expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) { expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
context & ctx = get_context(); context & ctx = get_context();
// I hope this works // I hope this works
@ -3985,6 +3986,12 @@ expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
hasEqcValue = false; hasEqcValue = false;
return n; return n;
} }
*/
expr * theory_str::get_eqc_value(expr * n, bool & hasEqcValue) {
return z3str2_get_eqc_value(n, hasEqcValue);
}
// Simulate the behaviour of get_eqc_value() from Z3str2. // Simulate the behaviour of get_eqc_value() from Z3str2.
// We only check m_find for a string constant. // We only check m_find for a string constant.