drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

5 files changed, 1 insertions, 185 deletions

diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 8b8a5bd48..be3f25ef5 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -17,8 +17,6 @@ libarrays_la_SOURCES = \
 	array_info.cpp \
 	static_fact_manager.h \
 	static_fact_manager.cpp \
-	theory_arrays_instantiator.h \
-	theory_arrays_instantiator.cpp \
 	theory_arrays_model.h \
 	theory_arrays_model.cpp
 
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 46cd5781a..a731d3677 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -6,7 +6,6 @@
 
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
-instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
 
 properties polite stable-infinite parametric
 properties check propagate presolve getNextDecisionRequest
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index b8c1ace4b..f4661c389 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,7 +21,6 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
 #include "theory/arrays/options.h"
@@ -721,7 +720,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
             }
           }
 
-          // Find all stores in which n[0] appears and get corresponding read terms        
+          // Find all stores in which n[0] appears and get corresponding read terms
           const CTNodeList* instores = d_infoMap.getInStores(array_eqc);
           size_t it = 0;
           for(; it < instores->size(); ++it) {
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
deleted file mode 100644
index 4c6c1a967..000000000
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ /dev/null
@@ -1,119 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_instantiator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of theory_arrays_instantiator class
- **/
-
-#include "theory/theory_engine.h"
-#include "theory/arrays/theory_arrays_instantiator.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/quantifiers/options.h"
-#include "theory/rewriterules/rr_candidate_generator.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
-
-InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) :
-Instantiator( c, ie, th ){
-
-}
-
-void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
-
-}
-
-void InstantiatorTheoryArrays::assertNode( Node assertion ){
-  Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
-  //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
-  if( options::cbqi() ){
-    if( assertion.hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
-    }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
-      setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) );
-    }
-  }
-}
-
-
-void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){
-
-}
-
-int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){
-  return InstStrategy::STATUS_SAT;
-}
-
-bool InstantiatorTheoryArrays::hasTerm( Node a ){
-  return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a );
-}
-
-bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
-  }else{
-    return false;
-  }
-}
-
-bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
-  if( a==b ){
-    return false;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
-  }else{
-    return false;
-  }
-}
-
-Node InstantiatorTheoryArrays::getRepresentative( Node a ){
-  if( hasTerm( a ) ){
-    return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a );
-  }else{
-    return a;
-  }
-}
-
-eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){
-  return ((TheoryArrays*)d_th)->getEqualityEngine();
-}
-
-void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
-  if( hasTerm( a ) ){
-    a = getEqualityEngine()->getRepresentative( a );
-    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
-    while( !eqc_iter.isFinished() ){
-      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
-        eqc.push_back( *eqc_iter );
-      }
-      eqc_iter++;
-    }
-  }
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
-  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
-  eq::EqualityEngine* ee =
-    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee);
-}
-
-rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){
-  arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
-  eq::EqualityEngine* ee =
-    static_cast<eq::EqualityEngine*>(ar->getEqualityEngine());
-  return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee);
-}
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
deleted file mode 100644
index accbff06b..000000000
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_instantiator.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): bobot
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Instantiator for theory of arrays
- **/
-
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/uf/equality_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arrays {
-
-class InstantiatorTheoryArrays : public Instantiator{
-  friend class QuantifiersEngine;
-protected:
-  /** reset instantiation round */
-  void processResetInstantiationRound( Theory::Effort effort );
-  /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
-  ~InstantiatorTheoryArrays() {}
-  /** Pre-register a term.  */
-  void preRegisterTerm( Node t );
-  /** assertNode function, assertion is asserted to theory */
-  void assertNode( Node assertion );
-  /** identify */
-  std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
-public:
-  /** general queries about equality */
-  bool hasTerm( Node a );
-  bool areEqual( Node a, Node b );
-  bool areDisequal( Node a, Node b );
-  Node getRepresentative( Node a );
-  eq::EqualityEngine* getEqualityEngine();
-  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
-  /** general creators of candidate generators */
-  rrinst::CandidateGenerator* getRRCanGenClasses();
-  rrinst::CandidateGenerator* getRRCanGenClass();
-};/* class Instantiatior */
-
-}
-}
-}
-
-#endif