diff options
| -rw-r--r-- | src/theory/term_registration_visitor.cpp | 76 | ||||
| -rw-r--r-- | test/regress/README | 2 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bug593.smt2 | 20 |
4 files changed, 94 insertions, 5 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 0e573ce62..7ece4594d 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -50,13 +50,36 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { d_theories = Theory::setInsert(parentTheoryId, d_theories); // Should we use the theory of the type - bool useType = current != parent && currentTheoryId != parentTheoryId; + bool useType = false; + TheoryId typeTheoryId = THEORY_LAST; + if (current != parent) { + if (currentTheoryId != parentTheoryId) { + // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers + TypeNode type = current.getType(); + useType = true; + typeTheoryId = Theory::theoryOf(type); + } else { + TypeNode type = current.getType(); + typeTheoryId = Theory::theoryOf(type); + if (typeTheoryId != currentTheoryId) { + if (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + useType = true; + } + } + } + } + } + // Get the theories that have already visited this node TNodeToTheorySetMap::iterator find = d_visited.find(current); if (find == d_visited.end()) { if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); d_theories = Theory::setInsert(typeTheoryId, d_theories); } return false; @@ -93,8 +116,32 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TheoryId parentTheoryId = Theory::theoryOf(parent); // Should we use the theory of the type - bool useType = current != parent && currentTheoryId != parentTheoryId; + bool useType = false; + TheoryId typeTheoryId = THEORY_LAST; + if (current != parent) { + if (currentTheoryId != parentTheoryId) { + // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers + TypeNode type = current.getType(); + useType = true; + typeTheoryId = Theory::theoryOf(type); + } else { + TypeNode type = current.getType(); + typeTheoryId = Theory::theoryOf(type); + if (typeTheoryId != currentTheoryId) { + if (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + useType = true; + } + } + } + } + } + Theory::Set visitedTheories = d_visited[current]; Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; if (!Theory::setContains(currentTheoryId, visitedTheories)) { @@ -112,7 +159,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); if (!Theory::setContains(typeTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); d_visited[current] = visitedTheories; @@ -187,6 +233,28 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } } + if (current != parent) { + if (currentTheoryId != parentTheoryId) { + // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers + TypeNode type = current.getType(); + useType = true; + typeTheoryId = Theory::theoryOf(type); + } else { + TypeNode type = current.getType(); + typeTheoryId = Theory::theoryOf(type); + if (typeTheoryId != currentTheoryId) { + if (options::finiteModelFind() && type.isSort()) { + // We're looking for finite models + useType = true; + } else { + Cardinality card = type.getCardinality(); + if (card.isFinite()) { + useType = true; + } + } + } + } + } if (Theory::setContains(currentTheoryId, theories)) { if (Theory::setContains(parentTheoryId, theories)) { diff --git a/test/regress/README b/test/regress/README index 58cd2f2e7..6fcdf16a3 100644 --- a/test/regress/README +++ b/test/regress/README @@ -3,7 +3,7 @@ Regressions To insert a new regression, add the file to Subversion, for example: - svn add regress/regress0/testMyFunctionality.cvc + git add regress/regress0/testMyFunctionality.cvc Also add it to the relevant Makefile.am, here, in regress/regress0/Makefile.am. diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index ad4e8a602..68d002367 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -167,6 +167,7 @@ BUG_TESTS = \ bug585.cvc \ bug586.cvc \ bug590.smt2 \ + bug593.smt2 \ bug595.cvc \ bug596.cvc \ bug596b.cvc diff --git a/test/regress/regress0/bug593.smt2 b/test/regress/regress0/bug593.smt2 new file mode 100644 index 000000000..2c28bb47c --- /dev/null +++ b/test/regress/regress0/bug593.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_UFBV) +(set-info :status unsat) + +(declare-sort A 0) + +(declare-fun f ((_ BitVec 1)) A) +(declare-fun g (A) (_ BitVec 1)) + +(declare-fun x () A) +(declare-fun y () A) +(declare-fun z () A) + +(assert (and + +(not (= (f (g x)) (f (g y)))) +(not (= (f (g x)) (f (g z)))) +(not (= (f (g y)) (f (g z)))))) + +(check-sat) + |