From 36cfaab5caa86773e47a8cca8f4d8c0d5edec99f Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 16 Aug 2016 12:24:58 -0500
Subject: Initial infrastructure for ExtTheory, generalize extended term
 handling in TheoryStrings to use this.

---
 src/theory/bv/theory_bv.cpp | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

(limited to 'src/theory/bv/theory_bv.cpp')

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:
-- 
cgit v1.2.3