New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index bdbc964c6..52afe05e2 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -63,7 +63,7 @@ EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheorySets::getModelValue(TNode node) {
-  return d_internal->getModelValue(node);
+  return Node::null();
 }
 
 void TheorySets::preRegisterTerm(TNode node) {
@@ -82,6 +82,10 @@ void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_internal->setMasterEqualityEngine(eq);
 }
 
+bool TheorySets::isEntailed( Node n, bool pol ) {
+  return d_internal->isEntailed( n, pol );
+}
+
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */