(Refactor) Split term util (#1303)

* Fix some documentation.

* Move model basis out of term db.

* Moving

* Finished moving.

* Document Skolemize and term enumeration.

* Minor

* Model basis to first order model.

* Change function name.

* Minor

* Clang format.

* Minor

* Format

* Minor

* Format

* Address review.

1 files changed, 31 insertions, 22 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2d5f48a5c..e742b8be9 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,8 +45,10 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_database_sygus.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers/trigger.h"
 #include "theory/sep/theory_sep.h"
@@ -67,11 +69,12 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      TheoryEngine* te)
     : d_te(te),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
+      d_skolemize(new quantifiers::Skolemize(this, u)),
+      d_term_enum(new quantifiers::TermEnumeration),
       d_conflict_c(c, false),
       // d_quants(u),
       d_quants_red(u),
       d_lemmas_produced_c(u),
-      d_skolemized(u),
       d_ierCounter_c(c),
       // d_ierCounter(c),
       // d_ierCounter_lc(c),
@@ -366,7 +369,9 @@ bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
     TypeNode tn = v.getType();
     if( tn.isSort() && options::finiteModelFind() ){
       return true;
-    }else if( getTermUtil()->mayComplete( tn ) ){
+    }
+    else if (d_term_enum->mayComplete(tn))
+    {
       return true;
     }
   }
@@ -792,17 +797,14 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
     //if not reduced
     if( !reduceQuantifier( f ) ){
       //do skolemization
-      if( d_skolemized.find( f )==d_skolemized.end() ){
-        Node body = d_term_util->getSkolemizedBody( f );
-        NodeBuilder<> nb(kind::OR);
-        nb << f << body.notNode();
-        Node lem = nb;
+      Node lem = d_skolemize->process(f);
+      if (!lem.isNull())
+      {
         if( Trace.isOn("quantifiers-sk-debug") ){
           Node slem = Rewriter::rewrite( lem );
           Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
         }
         getOutputChannel().lemma( lem, false, true );
-        d_skolemized[f] = true;
       }
     }
   }else{
@@ -848,8 +850,8 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
   //only wait if we are doing incremental solving
   if( !d_presolve || !options::incrementalSolving() ){
     std::set< Node > added;
-    getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
-    
+    d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
+
     //added contains also the Node that just have been asserted in this branch
     if( d_quant_rel ){
       for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
@@ -1125,15 +1127,16 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   for( unsigned i=0; i<terms.size(); i++ ){
     Trace("inst-add-debug") << "  " << q[0][i];
     Trace("inst-add-debug2") << " -> " << terms[i];
+    TypeNode tn = q[0][i].getType();
     if( terms[i].isNull() ){
-      terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
+      terms[i] = getTermForType(tn);
     }
     if( mkRep ){
       //pick the best possible representative for instantiation, based on past use and simplicity of term
       terms[i] = getInternalRepresentative( terms[i], q, i );
     }else{
       //ensure the type is correct
-      terms[i] = quantifiers::TermUtil::ensureType( terms[i], q[0][i].getType() );
+      terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
     }
     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
     if( terms[i].isNull() ){
@@ -1509,18 +1512,12 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   }
 
   bool printed = false;
-  for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
-    Node q = (*it).first;
+  // print the skolemizations
+  if (d_skolemize->printSkolemization(out))
+  {
     printed = true;
-    out << "(skolem " << q << std::endl;
-    out << "  ( ";
-    for( unsigned i=0; i<d_term_util->d_skolem_constants[q].size(); i++ ){
-      if( i>0 ){ out << " "; }
-      out << d_term_util->d_skolem_constants[q][i];
-    }
-    out << " )" << std::endl;
-    out << ")" << std::endl;
   }
+  // print the instantiations
   if( options::incrementalSolving() ){
     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
       bool firstTime = true;
@@ -1722,6 +1719,18 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
   return ret;
 }
 
+Node QuantifiersEngine::getTermForType(TypeNode tn)
+{
+  if (d_term_enum->isClosedEnumerableType(tn))
+  {
+    return d_term_enum->getEnumerateTerm(tn, 0);
+  }
+  else
+  {
+    return d_term_db->getOrMakeTypeGroundTerm(tn);
+  }
+}
+
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
   eq::EqualityEngine* ee = getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );