Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.

6 files changed, 64 insertions, 100 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 80066d690..a00d6d8a1 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -30,17 +30,30 @@ struct sortTypeOrder {
 };
 
 Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+  std::map< Node, bool > visited;
   while( !tt.empty() ){
     if( tt.size()==arg_index.size()+1 ){
       Node t = tt.back();
-      Node op = t.hasOperator() ? t.getOperator() : t;
-      arg_index.push_back( 0 );
+      Node op;
+      if( t.hasOperator() ){
+        if( visited.find( t )==visited.end() ){
+          visited[t] = true;
+          op = t.getOperator();
+          arg_index.push_back( 0 );
+        }else{
+          op = t;
+          arg_index.push_back( -1 );
+        }
+      }else{
+        op = t;
+        arg_index.push_back( 0 );
+      }
       Trace("aeq-debug") << op << " ";
       aen = &(aen->d_children[op][t.getNumChildren()]);
     }else{
       Node t = tt.back();
       int i = arg_index.back();
-      if( i==(int)t.getNumChildren() ){
+      if( i==-1 || i==(int)t.getNumChildren() ){
         tt.pop_back();
         arg_index.pop_back();
       }else{
@@ -56,9 +69,9 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE
   }else{
     if( q.getNumChildren()==2 ){
       //lemma ( q <=> d_quant )
-      Trace("quant-ae") << "Alpha equivalent : " << std::endl;
-      Trace("quant-ae") << "  " << q << std::endl;
-      Trace("quant-ae") << "  " << aen->d_quant << std::endl;
+      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+      Trace("alpha-eq") << "  " << q << std::endl;
+      Trace("alpha-eq") << "  " << aen->d_quant << std::endl;
       lem = q.iffNode( aen->d_quant );
     }else{
       //do not reduce annotated quantified formulas based on alpha equivalence 
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 7489196b7..cd263e90c 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -22,6 +22,9 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
 
+#include "theory/bv/theory_bv_utils.h"
+#include "util/bitvector.h"
+
 //#define MBP_STRICT_ASSERTIONS
 
 using namespace std;
@@ -466,6 +469,36 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                 }
               }
             }
+            /*   TODO: algebraic reasoning for bitvector instantiation
+            else if( pvtn.isBitVector() ){
+              if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){
+                for( unsigned t=0; t<2; t++ ){
+                  if( atom[t]==pv ){
+                    computeProgVars( atom[1-t] );
+                    if( d_inelig.find( atom[1-t] )==d_inelig.end() ){
+                      //only ground terms  TODO: more
+                      if( d_prog_var[atom[1-t]].empty() ){
+                        Node veq_c;
+                        Node uval;
+                        if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){
+                          uval = atom[1-t];
+                        }else{
+                          uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], 
+                                                                   bv::utils::mkConst(pvtn.getConst<BitVectorSize>(), 1) );
+                        }
+                        if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
+                          subs_proc[uval][veq_c] = true;
+                          if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                            return true;
+                          }
+                        }
+                      }
+                    }
+                  }
+                }
+              }
+            }
+            */
           }
         }
       }
@@ -685,7 +718,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
 
     //[5] resort to using value in model
     // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype
-    if( ( effort>0 || pvtn.isBoolean() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
+    if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){
       Node mv = getModelValue( pv );
       Node pv_coeff_m;
       Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 5c28e4ab5..d1685bdd1 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -433,7 +433,7 @@ void TheoryUF::addSharedTerm(TNode t) {
   d_equalityEngine.addTriggerTerm(t, THEORY_UF);
 }
 
-/*
+//TODO: move quantifiers::TermArgTrie to src/theory/
 void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
   if( depth==arity ){
     if( t2!=NULL ){
@@ -498,13 +498,11 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
     }
   }
 }
-*/
 
 void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
-
-/*  TODO : this does (almost) the same as below, and is 1-2 order of magnitudes faster
+    //use term indexing 
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
     std::map< Node, quantifiers::TermArgTrie > index;
     std::map< Node, unsigned > arity;
@@ -530,92 +528,6 @@ void TheoryUF::computeCareGraph() {
       Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl;
       addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 );
     }
- */
-    vector< pair<TNode, TNode> > currentPairs;
-
-    // Go through the function terms and see if there are any to split on
-    unsigned functionTerms = d_functionsTerms.size();
-    for (unsigned i = 0; i < functionTerms; ++ i) {
-
-      TNode f1 = d_functionsTerms[i];
-      Node op = f1.getOperator();
-
-      for (unsigned j = i + 1; j < functionTerms; ++ j) {
-
-        TNode f2 = d_functionsTerms[j];
-
-        // If the operators are not the same, we can skip this pair
-        if (f2.getOperator() != op) {
-          continue;
-        }
-
-        Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
-
-        // If the terms are already known to be equal, we are also in good shape
-        if (d_equalityEngine.areEqual(f1, f2)) {
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal, skipping" << std::endl;
-          continue;
-        }
-
-        // We have two functions f(x1, ..., xn) and f(y1, ..., yn) no known to be equal
-        // We split on the argument pairs that are are not known, unless there is some
-        // argument pair that is already dis-equal.
-        bool somePairIsDisequal = false;
-        currentPairs.clear();
-        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
-
-          TNode x = f1[k];
-          TNode y = f2[k];
-
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking arguments " << x << " and " << y << std::endl;
-
-          if (d_equalityEngine.areDisequal(x, y, false)) {
-            // Mark that there is a dis-equal pair and break
-            somePairIsDisequal = true;
-            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): disequal, disregarding all" << std::endl;
-            break;
-          }
-
-          if (d_equalityEngine.areEqual(x, y)) {
-            // We don't need this one
-            Debug("uf::sharing") << "TheoryUf::computeCareGraph(): equal" << std::endl;
-            continue;
-          }
-
-          if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) {
-            // Not connected to shared terms, we don't care
-            continue;
-          }
-
-          // Get representative trigger terms
-          TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
-          TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
-
-          EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
-          switch (eqStatusDomain) {
-          case EQUALITY_FALSE_AND_PROPAGATED:
-          case EQUALITY_FALSE:
-          case EQUALITY_FALSE_IN_MODEL:
-            somePairIsDisequal = true;
-            continue;
-            break;
-          default:
-            break;
-            // nothing
-          }
-
-          // Otherwise, we need to figure it out
-          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
-          currentPairs.push_back(make_pair(x_shared, y_shared));
-        }
-
-        if (!somePairIsDisequal) {
-          for (unsigned i = 0; i < currentPairs.size(); ++ i) {
-            addCarePair(currentPairs[i].first, currentPairs[i].second);
-          }
-        }
-      }
-    }
   }
 }/* TheoryUF::computeCareGraph() */
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index ff7d7419a..3a83decec 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -209,8 +209,8 @@ public:
   StrongSolverTheoryUF* getStrongSolver() {
     return d_thss;
   }
-//private:
-  //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
+private:
+  void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 };/* class TheoryUF */
 
 }/* CVC4::theory::uf namespace */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index ed28cc2fc..cda94e1c4 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1670,6 +1670,12 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c,
   }
 }
 
+StrongSolverTheoryUF::~StrongSolverTheoryUF() { 
+  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+    delete it->second;
+  }
+}
+
 SortInference* StrongSolverTheoryUF::getSortInference() {
   return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 11f0664f3..4e4dbef83 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -414,7 +414,7 @@ private:
   SubsortSymmetryBreaker* d_sym_break;
 public:
   StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
-  ~StrongSolverTheoryUF() {}
+  ~StrongSolverTheoryUF();
   /** get theory */
   TheoryUF* getTheory() { return d_th; }
   /** disequality propagator */