mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

add #2298 to regression/example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-29 07:24:42 -07:00
parent 857dc0fcec
commit 25c93410b1
2 changed files with 35 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
examples/c++/example.cpp
View file

@ -1221,6 +1221,37 @@ static void string_values() {
std::cout << s1 << "\n";
}
expr MakeStringConstant(context* context, std::string value) {
return context->string_val(value.c_str());
}
expr MakeStringFunction(context* c, std::string s) {
sort sort = c->string_sort();
symbol name = c->str_symbol(s.c_str());
return c->constant(name, sort);
}
static void string_issue_2298() {
context c;
solver s(c);
s.push();
expr func1 = MakeStringFunction(&c, "func1");
expr func2 = MakeStringFunction(&c, "func2");
expr abc = MakeStringConstant(&c, "abc");
expr cde = MakeStringConstant(&c, "cde");
expr length = func1.length();
expr five = c.int_val(5);
s.add(func2 == abc || func1 == cde);
s.add(func2 == abc || func2 == cde);
s.add(length <= five);
s.check();
s.pop();
}
int main() {
try {
@ -1272,6 +1303,7 @@ int main() {
mk_model_example(); std::cout << "\n";
recfun_example(); std::cout << "\n";
string_values(); std::cout << "\n";
string_issue_2298(); std::cout << "\n";
std::cout << "done\n";
}
catch (exception & ex) {

15
src/smt/smt_enode.cpp
View file

@ -274,10 +274,7 @@ namespace smt {
// Parent use-list
if (this == m_root) {
enode_vector::const_iterator it2 = m_parents.begin();
enode_vector::const_iterator end2 = m_parents.end();
for (; it2 != end2; ++it2) {
enode const * parent = *it2;
for (enode* parent : m_parents) {
unsigned i = 0;
unsigned num_args = parent->get_num_args();
SASSERT(num_args > 0);
@ -318,10 +315,7 @@ namespace smt {
enode const * curr = m_root;
do {
if (curr != m_root) {
enode_vector::const_iterator it = curr->m_parents.begin();
enode_vector::const_iterator end = curr->m_parents.end();
for (; it != end; ++it) {
enode * p = *it;
for (enode * p : curr->m_parents) {
if (!p->is_true_eq() && !m_root->contains_parent_congruent_to(p)) {
UNREACHABLE();
}
@ -334,10 +328,7 @@ namespace smt {
}
bool enode::contains_parent_congruent_to(enode * p) const {
enode_vector::const_iterator it = m_parents.begin();
enode_vector::const_iterator end = m_parents.end();
for (; it != end; ++it) {
enode * curr = *it;
for (enode* curr : m_parents) {
if (congruent(curr, p))
return true;
}