Initial infrastructure for ExtTheory, generalize extended term handling in TheoryStrings to use this.

3 files changed, 34 insertions, 0 deletions

diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 643093327..93a938cc0 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -117,6 +117,7 @@ public:
   bool hasTerm(TNode node) const { return d_equalityEngine.hasTerm(node); }
   void addTermToEqualityEngine(TNode node) { d_equalityEngine.addTerm(node); }
   void enableSlicer();
+  eq::EqualityEngine * getEqualityEngine() { return &d_equalityEngine; }
 };
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fec93e033..f0981044b 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -495,7 +495,36 @@ void TheoryBV::propagate(Effort e) {
   }
 }
 
+eq::EqualityEngine * TheoryBV::getEqualityEngine() {
+  return NULL;
+}
 
+bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
+#if 0
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if( core ){
+    //get the constant equivalence classes
+    bool retVal = false;
+    for( unsigned i=0; i<vars.size(); i++ ){
+      Node n = vars[i];
+      if( core->getEqualityEngine()->hasTerm( n ) ){
+        Node nr = core->getEqualityEngine()->getRepresenative( n );
+        if( nr.isConst() ){
+          subs.push_back( nr );
+          exp[n].push_back( n.eqNode( nr ) );
+          retVal = true;
+        }else{
+          subs.push_back( n );
+        }
+      }
+    }
+    //return true if the substitution is non-trivial
+    return retVal;
+  }
+#endif
+  return false;
+}
+  
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
   case kind::EQUAL:
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ba2a4fc2a..0709ca427 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -79,6 +79,10 @@ public:
 
   std::string identify() const { return std::string("TheoryBV"); }
 
+  /** equality engine */
+  eq::EqualityEngine * getEqualityEngine();
+  bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+  
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
   void enableCoreTheorySlicer();