remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

11 files changed, 0 insertions, 495 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 1f0108581..1362b1f5c 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -45,7 +45,6 @@ libtheory_la_SOURCES = \
 
 nodist_libtheory_la_SOURCES = \
 	rewriter_tables.h \
-	instantiator_tables.cpp \
 	theory_traits.h \
 	type_enumerator.cpp
 
@@ -64,23 +63,19 @@ EXTRA_DIST = \
 	logic_info.i \
 	options_handlers.h \
 	rewriter_tables_template.h \
-	instantiator_tables_template.cpp \
 	theory_traits_template.h \
 	type_enumerator_template.cpp \
 	mktheorytraits \
 	mkrewriter \
-	mkinstantiator \
 	Makefile.subdirs
 
 BUILT_SOURCES = \
 	rewriter_tables.h \
-	instantiator_tables.cpp \
 	theory_traits.h \
 	type_enumerator.cpp
 
 CLEANFILES = \
 	rewriter_tables.h \
-	instantiator_tables.cpp \
 	theory_traits.h \
 	type_enumerator.cpp
 
@@ -94,14 +89,6 @@ rewriter_tables.h: rewriter_tables_template.h mkrewriter @top_builddir@/src/theo
 		`cat @top_builddir@/src/theory/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-instantiator_tables.cpp: instantiator_tables_template.cpp mkinstantiator @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
-	$(AM_V_at)chmod +x @srcdir@/mkinstantiator
-	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
-	$(AM_V_GEN)(@srcdir@/mkinstantiator \
-		$< \
-		`cat @top_builddir@/src/theory/.subdirs` \
-	> $@) || (rm -f $@ && exit 1)
-
 theory_traits.h: theory_traits_template.h mktheorytraits @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mktheorytraits
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 4380eca58..90d82e255 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -34,11 +34,9 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-class InstantiatorTheoryDatatypes;
 class EqualityQueryTheory;
 
 class TheoryDatatypes : public Theory {
-  friend class InstantiatorTheoryDatatypes;
   friend class EqualityQueryTheory;
 private:
   typedef context::CDChunkList<Node> NodeList;
diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp
deleted file mode 100644
index bc038df63..000000000
--- a/src/theory/instantiator_tables_template.cpp
+++ /dev/null
@@ -1,38 +0,0 @@
-/*********************                                                        */
-/*! \file instantiator_tables_template.cpp
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** 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 tables for quantifier-friendly theories
- **
- ** This file contains template code for the instantiator tables that are
- ** generated from the Theory kinds files.
- **/
-
-#include "context/context.h"
-#include "theory/quantifiers_engine.h"
-
-${instantiator_includes}
-
-#line 24 "${template}"
-
-namespace CVC4 {
-namespace theory {
-
-Instantiator* Theory::makeInstantiator(context::Context* c, theory::QuantifiersEngine* qe) {
-  switch(d_id) {
-${make_instantiator_cases}
-#line 32 "${template}"
-  default:
-    Unhandled(d_id);
-  }
-}
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
deleted file mode 100755
index 73fc6706d..000000000
--- a/src/theory/mkinstantiator
+++ /dev/null
@@ -1,254 +0,0 @@
-#!/bin/bash
-#
-# mkinstantiator
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
-#
-# The purpose of this script is to create rewriter_tables.h from a template
-# and a list of theory kinds.
-#
-# Invocation:
-#
-#   mkinstantiator template-file theory-kind-files...
-#
-# Output is to standard out.
-#
-
-copyright=2010-2012
-
-cat <<EOF
-/*********************                                                        */
-/** instantiator_tables.h
- **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
- **
- ** This header file automatically generated by:
- **
- **     $0 $@
- **
- ** for the CVC4 project.
- **/
-
-EOF
-
-me=$(basename "$0")
-
-template=$1; shift
-
-instantiator_includes=
-instantiator_class=
-theory_id=
-theory_class=
-theory_header=
-
-make_instantiator_cases=
-instantiator=
-
-seen_theory=false
-seen_theory_builtin=false
-
-function theory {
-  # theory id T header
-
-  lineno=${BASH_LINENO[0]}
-
-  if $seen_theory; then
-    echo "$kf:$lineno: theory declaration can only appear once" >&2
-    exit 1;
-  fi
-
-  seen_theory=true
-  if [ "$1" = THEORY_BUILTIN ]; then
-    if $seen_theory_builtin; then
-      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
-      exit 1
-    fi
-    seen_theory_builtin=true
-  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
-    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
-    exit 1
-  elif ! expr "$2" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
-  fi
-
-  theory_id="$1"
-  theory_class="$2"
-  theory_header="$3"
-
-  instantiator_class=
-  instantiator=NULL
-}
-
-function instantiator {
-  # instantiator class header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-
-  if [ -n "$instantiator_class" ]; then
-    echo "$kf:$lineno: error: cannot have two \"instantiator\" directives" >&2
-    exit 1
-  fi
-
-  instantiator_class="$1"
-  instantiator_header="$2"
-
-  if [ -z "$instantiator_class" -o -z "$instantiator_header" ]; then
-    echo "$kf:$lineno: error: \"instantiator\" directive missing class or header argument" >&2
-    exit 1
-  fi
-
-  instantiator_includes="${instantiator_includes}#include \"$theory_header\"
-#line $lineno \"$kf\"
-#include \"$instantiator_header\"
-"
-  instantiator="new $instantiator_class(c, qe, static_cast< $theory_class* >(this))";
-}
-
-function properties {
-  # properties prop*
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function endtheory {
-  # endtheory
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-  seen_endtheory=true
-
-  make_instantiator_cases="${make_instantiator_cases}
-#line $lineno \"$kf\"
-  case $theory_id:
-    return $instantiator;
-"
-}
-
-function enumerator {
-  # enumerator KIND enumerator-class header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function typechecker {
-  # typechecker header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function typerule {
-  # typerule OPERATOR typechecking-class
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function construle {
-  # construle OPERATOR isconst-checking-class
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function rewriter {
-  # rewriter class header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function sort {
-  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function cardinality {
-  # cardinality TYPE cardinality-computer [header]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function well-founded {
-  # well-founded TYPE wellfoundedness-computer [header]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function variable {
-  # variable K ["comment"]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function operator {
-  # operator K #children ["comment"]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function parameterized {
-  # parameterized K1 K2 #children ["comment"]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function constant {
-  # constant K T Hasher header ["comment"]
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
-function check_theory_seen {
-  if $seen_endtheory; then
-    echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2
-    exit 1
-  fi
-  if ! $seen_theory; then
-    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
-    exit 1
-  fi
-}
-
-function check_builtin_theory_seen {
-  if ! $seen_theory_builtin; then
-    echo "$me: warning: no declaration for the builtin theory found" >&2
-  fi
-}
-
-while [ $# -gt 0 ]; do
-  kf=$1
-  seen_theory=false
-  seen_endtheory=false
-  b=$(basename $(dirname "$kf"))
-  source "$kf"
-  if ! $seen_theory; then
-    echo "$kf: error: no theory content found in file!" >&2
-    exit 1
-  fi
-  if ! $seen_endtheory; then
-    echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2
-    exit 1
-  fi
-  shift
-done
-check_builtin_theory_seen
-
-## output
-
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
-text=$(cat "$template")
-for var in \
-    instantiator_includes \
-    make_instantiator_cases \
-    template \
-    ; do
-  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
-done
-error=`expr "$text" : '.*\${\([^}]*\)}.*'`
-if [ -n "$error" ]; then
-  echo "$template:0: error: undefined replacement \${$error}" >&2
-  exit 1
-fi
-echo "$text"
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 0d00b616c..88ac5b9fb 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -81,12 +81,6 @@ function theory {
   theory_id="$1"
 }
 
-function instantiator {
-  # instantiator class header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-}
-
 function properties {
   # properties prop*
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index c8ef23a78..a44d8e9c3 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -61,9 +61,6 @@ theory_parametric="false"
 rewriter_class=
 rewriter_header=
 
-instantiator_class=void
-instantiator_header=
-
 theory_id=
 theory_class=
 
@@ -135,7 +132,6 @@ template<>
 struct TheoryTraits<${theory_id}> {
     typedef ${theory_class} theory_class;
     typedef ${rewriter_class} rewriter_class;
-    typedef ${instantiator_class} instantiator_class;
 
     static const bool isStableInfinite = ${theory_stable_infinite};
     static const bool isFinite = ${theory_finite};
@@ -240,18 +236,6 @@ function construle {
   check_theory_seen
 }
 
-function instantiator {
-  # instantiator class header
-  lineno=${BASH_LINENO[0]}
-  check_theory_seen
-
-  instantiator_class="$1"
-  instantiator_header="$2"
-
-  theory_includes="${theory_includes}#include \"$2\"
-"
-}
-
 function properties {
   # properties property*
   lineno=${BASH_LINENO[0]}
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index c32d6ff75..b41089b80 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -102,9 +102,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(currentTheoryId);
     th->preRegisterTerm(current);
-    if(th->getInstantiator() != NULL) {
-      th->getInstantiator()->preRegisterTerm(current);
-    }
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
   }
   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
@@ -112,9 +109,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     d_visited[current] = visitedTheories;
     Theory* th = d_engine->theoryOf(parentTheoryId);
     th->preRegisterTerm(current);
-    if(th->getInstantiator() != NULL) {
-      th->getInstantiator()->preRegisterTerm(current);
-    }
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
@@ -124,9 +118,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
       d_visited[current] = visitedTheories;
       Theory* th = d_engine->theoryOf(typeTheoryId);
       th->preRegisterTerm(current);
-      if(th->getInstantiator() != NULL) {
-        th->getInstantiator()->preRegisterTerm(current);
-      }
       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
     }
   }
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index ea3902d59..f513b0d78 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -48,11 +48,6 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
 }/* ostream& operator<<(ostream&, Theory::Effort) */
 
 Theory::~Theory() {
-  if(d_inst != NULL) {
-    delete d_inst;
-    d_inst = NULL;
-  }
-
   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
 }
 
@@ -174,73 +169,6 @@ void Theory::debugPrintFacts() const{
   printFacts(DebugChannel.getStream());
 }
 
-Instantiator::Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th) :
-  d_quantEngine(qe),
-  d_th(th) {
-}
-
-Instantiator::~Instantiator() {
-}
-
-void Instantiator::resetInstantiationRound(Theory::Effort effort) {
-  /*
-  for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
-    if(isActiveStrategy(d_instStrategies[i])) {
-      d_instStrategies[i]->processResetInstantiationRound(effort);
-    }
-  }
-  processResetInstantiationRound(effort);
-  */
-}
-
-int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
-  /*
-  if( getQuantifierActive(f) ) {
-    int status = process(f, effort, e );
-    if(d_instStrategies.empty()) {
-      Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl;
-    } else {
-      for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
-        if(isActiveStrategy(d_instStrategies[i])) {
-          Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl;
-          //call the instantiation strategy's process method
-          int s_status = d_instStrategies[i]->process( f, effort, e );
-          Debug("inst-engine-inst") << "  -> status is " << s_status << endl;
-          InstStrategy::updateStatus(status, s_status);
-        } else {
-          Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " is not active." << endl;
-        }
-      }
-    }
-    return status;
-  } else {
-    Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl;
-    return InstStrategy::STATUS_SAT;
-  }
-  */
-  return 0;
-}
-
-//void Instantiator::doInstantiation(int effort) {
-//  d_status = InstStrategy::STATUS_SAT;
-//  for( int q = 0; q < d_quantEngine->getNumQuantifiers(); ++q ) {
-//    Node f = d_quantEngine->getQuantifier(q);
-//    if( d_quantEngine->getActive(f) && hasConstraintsFrom(f) ) {
-//      int d_quantStatus = process( f, effort );
-//      InstStrategy::updateStatus( d_status, d_quantStatus );
-//      for( int i = 0; i < (int)d_instStrategies.size(); ++i ) {
-//        if( isActiveStrategy( d_instStrategies[i] ) ) {
-//          Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl;
-//          //call the instantiation strategy's process method
-//          d_quantStatus = d_instStrategies[i]->process( f, effort );
-//          Debug("inst-engine-inst") << "  -> status is " << d_quantStatus << endl;
-//          InstStrategy::updateStatus( d_status, d_quantStatus );
-//        }
-//      }
-//    }
-//  }
-//}
-
 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
   for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 1f55a4b90..f317d4b92 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -46,7 +46,6 @@ class TheoryEngine;
 
 namespace theory {
 
-class Instantiator;
 class QuantifiersEngine;
 class TheoryModel;
 
@@ -192,12 +191,6 @@ private:
    */
   QuantifiersEngine* d_quantEngine;
 
-  /**
-   * The instantiator for this theory, or NULL if quantifiers are not
-   * supported or not enabled.
-   */
-  Instantiator* d_inst;
-
   // === STATISTICS ===
   /** time spent in theory combination */
   TimerStat d_computeCareGraphTime;
@@ -208,12 +201,6 @@ private:
     return ss.str();
   }
 
-  /**
-   * Construct and return the instantiator for the given theory.
-   * If there is no instantiator class, NULL is returned.
-   */
-  theory::Instantiator* makeInstantiator(context::Context* c, theory::QuantifiersEngine* qe);
-
 protected:
 
   /**
@@ -261,7 +248,6 @@ protected:
   , d_sharedTermsIndex(satContext, 0)
   , d_careGraph(0)
   , d_quantEngine(qe)
-  , d_inst(makeInstantiator(satContext, qe))
   , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
   , d_sharedTerms(satContext)
   , d_out(&out)
@@ -487,20 +473,6 @@ public:
   }
 
   /**
-   * Get the theory instantiator.
-   */
-  Instantiator* getInstantiator() {
-    return d_inst;
-  }
-
-  /**
-   * Get the theory instantiator (const version).
-   */
-  const Instantiator* getInstantiator() const {
-    return d_inst;
-  }
-
-  /**
    * Pre-register a term.  Done one time for a Node, ever.
    */
   virtual void preRegisterTerm(TNode) { }
@@ -821,55 +793,6 @@ namespace eq{
 }
 
 
-/** instantiator class */
-class Instantiator {
-  friend class QuantifiersEngine;
-protected:
-  /** reference to the quantifiers engine */
-  QuantifiersEngine* d_quantEngine;
-  /** reference to the theory that it looks at */
-  Theory* d_th;
-  /** reset instantiation round */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process quantifier */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-public:
-  Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th);
-  virtual ~Instantiator();
-
-  /** get quantifiers engine */
-  QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
-  /** get corresponding theory for this instantiator */
-  Theory* getTheory() { return d_th; }
-  /** Pre-register a term.  */
-  virtual void preRegisterTerm( Node t ) { }
-  /** assertNode function, assertion was asserted to theory */
-  virtual void assertNode( Node assertion ){}
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-  /** print debug information */
-  virtual void debugPrint( const char* c ) {}
-public:
-  /** reset instantiation round */
-  void resetInstantiationRound( Theory::Effort effort );
-  /** do instantiation method*/
-  int doInstantiation( Node f, Theory::Effort effort, int e );
-public:
-  /** general queries about equality */
-  virtual bool hasTerm( Node a ) { return false; }
-  virtual bool areEqual( Node a, Node b ) { return false; }
-  virtual bool areDisequal( Node a, Node b ) { return false; }
-  virtual Node getRepresentative( Node a ) { return a; }
-  virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
-  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {}
-public:
-  /** A Creator of CandidateGenerator for classes (one element in each
-      equivalence class) and class (every element of one equivalence
-      class) */
-  virtual rrinst::CandidateGenerator* getRRCanGenClasses(){ return NULL; };
-  virtual rrinst::CandidateGenerator* getRRCanGenClass(){ return NULL; };
-};/* class Instantiator */
-
 inline Assertion Theory::get() {
   Assert( !done(), "Theory::get() called with assertion queue empty!" );
 
@@ -883,11 +806,6 @@ inline Assertion Theory::get() {
     Dump("state") << AssertCommand(fact.assertion.toExpr());
   }
 
-  // if quantifiers are turned on and we have an instantiator, notify it
-  if(getLogicInfo().isQuantified() && getInstantiator() != NULL) {
-    getInstantiator()->assertNode(fact);
-  }
-
   return fact;
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4a1ab4ca0..063943056 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -74,7 +74,6 @@ struct NodeTheoryPairHashFunction {
 };/* struct NodeTheoryPairHashFunction */
 
 namespace theory {
-  class Instantiator;
   class TheoryModel;
   class TheoryEngineModelBuilder;
 
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 46a17a5e0..fe1fc5137 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -35,12 +35,10 @@ namespace theory {
 namespace uf {
 
 class UfTermDb;
-class InstantiatorTheoryUf;
 class StrongSolverTheoryUf;
 
 class TheoryUF : public Theory {
 
-  friend class InstantiatorTheoryUf;
   friend class StrongSolverTheoryUf;
 
 public: