cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation

5 files changed, 14 insertions, 70 deletions

diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index eef2dac79..4fe5772de 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -48,48 +48,6 @@ struct sortQuantifiersForSymbol {
   }
 };
 
-
-void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort effort ){
-  for( std::map< Node, bool >::iterator it = d_solved.begin(); it != d_solved.end(); ++it ){
-    calcSolved( it->first );
-  }
-}
-
-int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    //calc solved if not done so already
-    if( d_solved.find( f )==d_solved.end() ){
-      calcSolved( f );
-    }
-    //check if f is counterexample-solved
-    Debug("quant-uf-strategy") << "Try CE-solved.." << std::endl;
-    if( d_solved[ f ] ){
-      if( d_quantEngine->addInstantiation( f, d_th->d_baseMatch[f] ) ){
-        ++(d_th->d_statistics.d_instantiations_ce_solved);
-        //d_quantEngine->d_hasInstantiated[f] = true;
-      }
-      d_solved[f] = false;
-    }
-    Debug("quant-uf-strategy") << "done." << std::endl;
-  }
-  return STATUS_UNKNOWN;
-}
-
-void InstStrategyCheckCESolved::calcSolved( Node f ){
-  d_th->d_baseMatch[f].clear();
-  d_solved[ f ]= true;
-  //check if instantiation constants are solved for
-  for( int j = 0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-    Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-    Node rep = d_th->getInternalRepresentative( i );
-    if( !rep.hasAttribute(InstConstantAttribute()) ){
-      d_th->d_baseMatch[f].set(i,rep);
-    }else{
-      d_solved[ f ] = false;
-    }
-  }
-}
-
 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
   //reset triggers
   for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index 6baa5b147..5a3b9cc3d 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -34,25 +34,6 @@ class InstantiatorTheoryUf;
 
 //instantiation strategies
 
-class InstStrategyCheckCESolved : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** is solved? */
-  std::map< Node, bool > d_solved;
-  /** calc if f is solved */
-  void calcSolved( Node f );
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyCheckCESolved(){}
-  /** identify */
-  std::string identify() const { return std::string("CheckCESolved"); }
-};/* class InstStrategyCheckCESolved */
-
 class InstStrategyUserPatterns : public InstStrategy{
 private:
   /** InstantiatorTheoryUf class */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 0cc32d420..099eb5b5e 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -38,9 +38,9 @@ InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::Qu
 Instantiator( c, qe, th )
 {
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    if( options::cbqi() ){
-      addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
-    }
+    //if( options::cbqi() ){
+    //  addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
+    //}
     if( options::userPatternsQuant() ){
       d_isup = new InstStrategyUserPatterns( this, qe );
       addInstStrategy( d_isup );
@@ -88,7 +88,7 @@ void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
 
 
 void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
-  d_ground_reps.clear();
+  //d_ground_reps.clear();
 }
 
 int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){
@@ -132,7 +132,7 @@ Node InstantiatorTheoryUf::getRepresentative( Node a ){
     return a;
   }
 }
-
+/*
 Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
   if( d_ground_reps.find( a )==d_ground_reps.end() ){
     if( !hasTerm( a ) ){
@@ -160,7 +160,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
   }
   return d_ground_reps[a];
 }
-
+*/
 eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
   return &((TheoryUF*)d_th)->d_equalityEngine;
 }
diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h
index 324fa6386..3cb4f97cc 100644
--- a/src/theory/uf/theory_uf_instantiator.h
+++ b/src/theory/uf/theory_uf_instantiator.h
@@ -48,7 +48,7 @@ protected:
   typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
   /** map to representatives used */
-  std::map< Node, Node > d_ground_reps;
+  //std::map< Node, Node > d_ground_reps;
 protected:
   /** instantiation strategies */
   InstStrategyUserPatterns* d_isup;
@@ -132,7 +132,6 @@ public:
   Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); }
   bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
   bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
-  Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
   eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
   void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
 }; /* EqualityQueryInstantiatorTheoryUf */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index d037c374d..548d6f2f0 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -919,7 +919,13 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
       //must generate new cardinality lemma term
       std::stringstream ss;
       ss << "_c_" << d_aloc_cardinality;
-      Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+      Node var;
+      if( d_totality_terms[0].empty() ){
+        //get arbitrary ground term
+        var = d_cardinality_term;
+      }else{
+        var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+      }
       d_totality_terms[0].push_back( var );
       Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
       //must be distinct from all other cardinality terms