(Move-only) Refactor and document theory model part 2 (#1305)

* Move type set to its own file and document.

* Move theory engine model builder to its own class.

* Working on documentation.

* Document Theory Model.

* Minor

* Document theory model builder.

* Clang format

* Address review.

1 files changed, 84 insertions, 255 deletions

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 0d73cd72a..a8726f490 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -21,51 +21,80 @@
 #include <unordered_set>
 
 #include "smt/model.h"
-#include "theory/uf/equality_engine.h"
 #include "theory/rep_set.h"
 #include "theory/substitutions.h"
 #include "theory/type_enumerator.h"
+#include "theory/type_set.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-/**
- * Theory Model class.
- *    For Model m, should call m.initialize() before using.
+/** Theory Model class.
+ *
+ * This class represents a model produced by the TheoryEngine.
+ * The data structures used to represent a model are:
+ * (1) d_equalityEngine : an equality engine object, which stores
+ *     an equivalence relation over all terms that exist in
+ *     the current set of assertions.
+ * (2) d_substitutions : a substitution map storing cases of
+ *     explicitly solved terms, for instance during preprocessing.
+ * (3) d_reps : a map from equivalence class representatives of
+ *     the equality engine to the (constant) representatives
+ *     assigned to that equivalence class.
+ * (4) d_uf_models : a map from uninterpreted functions to their
+ *     lambda representation.
+ * (5) d_rep_set : a data structure that allows interpretations
+ *     for types to be represented as terms. This is useful for
+ *     finite model finding.
+ *
+ * These data structures are built after a full effort check with
+ * no lemmas sent, within a call to:
+ *    TheoryEngineModelBuilder::buildModel(...)
+ * which includes subcalls to TheoryX::collectModelInfo(...) calls.
+ *
+ * These calls may modify the model object using the interface
+ * functions below, including:
+ * - assertEquality, assertPredicate, assertRepresentative,
+ *   assertEqualityEngine.
+ * - assignFunctionDefinition
+ *
+ * During and after this building process, these calls may use
+ * interface functions below to guide the model construction:
+ * - hasTerm, getRepresentative, areEqual, areDisequal
+ * - getEqualityEngine
+ * - getRepSet
+ * - hasAssignedFunctionDefinition, getFunctionsToAssign
+ *
+ * After this building process, the function getValue can be
+ * used to query the value of nodes.
  */
 class TheoryModel : public Model
 {
   friend class TheoryEngineModelBuilder;
-
 public:
   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
   virtual ~TheoryModel() throw();
 
-  /** get comments */
-  void getComments(std::ostream& out) const;
-  /** is built */
-  bool isBuilt() { return d_modelBuilt; }
-  /** set need build */
-  void setNeedsBuild() { d_modelBuilt = false; }
-  /**
-   * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
-   * on this model.
+  /** reset the model */
+  virtual void reset();
+  /** is built
+   *
+   * Have we (attempted to) build this model since the last
+   * call to reset? Notice for model building techniques
+   * that are not guaranteed to succeed (such as
+   * when quantified formulas are enabled), a true return
+   * value does not imply that this is a model of the
+   * current assertions.
    */
-  Node getValue( TNode n, bool useDontCares = false ) const;
-
-  //---------------------------- separation logic
-  /** set the heap and value sep.nil is equal to */
-  void setHeapModel(Node h, Node neq);
-  /** get the heap and value sep.nil is equal to */
-  bool getHeapModel(Expr& h, Expr& neq) const;
-  //---------------------------- end separation logic
-
+  bool isBuilt() { return d_modelBuilt; }
+  //---------------------------- for building the model
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
-  /** add term function
-    *   addTerm( n ) will do any model-specific processing necessary for n,
-    *   such as constraining the interpretation of uninterpreted functions,
-    *   and adding n to the equality engine of this model
+  /** add term
+    *  This will do any model-specific processing necessary for n,
+    *  such as constraining the interpretation of uninterpreted functions,
+    *  and adding n to the equality engine of this model.
     */
   virtual void addTerm(TNode n);
   /** assert equality holds in the model */
@@ -81,6 +110,7 @@ public:
     *  functions.
     */
   void assertRepresentative(TNode n);
+  //---------------------------- end building the model
 
   // ------------------- general equality queries
   /** does the equality engine of this model have term a? */
@@ -95,6 +125,23 @@ public:
   eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
   // ------------------- end general equality queries
 
+  /** Get value function.
+   * This should be called only after a ModelBuilder
+   * has called buildModel(...) on this model.
+   *   useDontCares is whether to return Node::null() if
+   *     n does not occur in the equality engine.
+   */
+  Node getValue(TNode n, bool useDontCares = false) const;
+  /** get comments */
+  void getComments(std::ostream& out) const;
+
+  //---------------------------- separation logic
+  /** set the heap and value sep.nil is equal to */
+  void setHeapModel(Node h, Node neq);
+  /** get the heap and value sep.nil is equal to */
+  bool getHeapModel(Expr& h, Expr& neq) const;
+  //---------------------------- end separation logic
+
   /** get the representative set object */
   const RepSet* getRepSet() const { return &d_rep_set; }
   /** get the representative set object (FIXME: remove this, see #1199) */
@@ -145,19 +192,23 @@ public:
   /** true/false nodes */
   Node d_true;
   Node d_false;
-  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
   /** comment stream to include in printing */
   std::stringstream d_comment_str;
-  /** reset the model */
-  virtual void reset();
-  /**
-   * Get model value function.  This function is called by getValue
+  /** Get model value function.
+   *
+   * This function is a helper function for getValue.
+   *   hasBoundVars is whether n may contain bound variables
+   *   useDontCares is whether to return Node::null() if
+   *     n does not occur in the equality engine.
    */
   Node getModelValue(TNode n,
                      bool hasBoundVars = false,
                      bool useDontCares = false) const;
 
  private:
+  /** cache for getModelValue */
+  mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+
   //---------------------------- separation logic
   /** the value of the heap */
   Node d_sep_heap;
@@ -170,234 +221,12 @@ public:
   bool d_enableFuncModels;
   /** map from function terms to the (lambda) definitions
   * After the model is built, the domain of this map is all terms of function
-  * type
-  * that appear as terms in d_equalityEngine.
+  * type that appear as terms in d_equalityEngine.
   */
   std::map<Node, Node> d_uf_models;
   //---------------------------- end function values
 };/* class TheoryModel */
 
-/*
- * Class that encapsulates a map from types to sets of nodes
- */
-class TypeSet {
-public:
-  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
-  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
-  typedef TypeSetMap::iterator iterator;
-  typedef TypeSetMap::const_iterator const_iterator;
-private:
-  TypeSetMap d_typeSet;
-  TypeToTypeEnumMap d_teMap;
-  TypeEnumeratorProperties * d_tep;
-
-  /* Note that recursive traversal here is over enumerated expressions
-   * (very low expression depth). */
-  void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){
-    if( visited.find( n )==visited.end() ){
-      visited[n] = true;
-      if( !topLevel ){
-        add(n.getType(), n);
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        addSubTerms( n[i], visited, false );
-      }
-    }
-  }
-public:
-  TypeSet() : d_tep(NULL) {}
-  ~TypeSet() {
-    iterator it;
-    for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
-      if ((*it).second != NULL) {
-        delete (*it).second;
-      }
-    }
-    TypeToTypeEnumMap::iterator it2;
-    for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
-      if ((*it2).second != NULL) {
-        delete (*it2).second;
-      }
-    }
-  }
-  void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
-  void add(TypeNode t, TNode n)
-  {
-    iterator it = d_typeSet.find(t);
-    std::set<Node>* s;
-    if (it == d_typeSet.end()) {
-      s = new std::set<Node>;
-      d_typeSet[t] = s;
-    }
-    else {
-      s = (*it).second;
-    }
-    s->insert(n);
-  }
-
-  std::set<Node>* getSet(TypeNode t) const
-  {
-    const_iterator it = d_typeSet.find(t);
-    if (it == d_typeSet.end()) {
-      return NULL;
-    }
-    return (*it).second;
-  }
-
-  Node nextTypeEnum(TypeNode t, bool useBaseType = false)
-  {
-    TypeEnumerator* te;
-    TypeToTypeEnumMap::iterator it = d_teMap.find(t);
-    if (it == d_teMap.end()) {
-      te = new TypeEnumerator(t, d_tep);
-      d_teMap[t] = te;
-    }
-    else {
-      te = (*it).second;
-    }
-    if (te->isFinished()) {
-      return Node();
-    }
-
-    if (useBaseType) {
-      t = t.getBaseType();
-    }
-    iterator itSet = d_typeSet.find(t);
-    std::set<Node>* s;
-    if (itSet == d_typeSet.end()) {
-      s = new std::set<Node>;
-      d_typeSet[t] = s;
-    }
-    else {
-      s = (*itSet).second;
-    }
-    Node n = **te;
-    while (s->find(n) != s->end()) {
-      ++(*te);
-      if (te->isFinished()) {
-        return Node();
-      }
-      n = **te;
-    }
-    s->insert(n);
-    // add all subterms of n to this set as well
-    // this is necessary for parametric types whose values are constructed from other types 
-    // to ensure that we do not enumerate subterms of other previous enumerated values
-    std::map< TNode, bool > visited;
-    addSubTerms(n, visited);
-    ++(*te);
-    return n;
-  }
-
-  bool empty()
-  {
-    return d_typeSet.empty();
-  }
-
-  iterator begin()
-  {
-    return d_typeSet.begin();
-  }
-
-  iterator end()
-  {
-    return d_typeSet.end();
-  }
-
-  static TypeNode getType(iterator it)
-  {
-    return (*it).first;
-  }
-
-  static std::set<Node>& getSet(iterator it)
-  {
-    return *(*it).second;
-  }
-
-};/* class TypeSet */
-
-/** TheoryEngineModelBuilder class
-  *    This model builder will consult all theories in a theory engine for
-  *    collectModelInfo( ... ) when building a model.
-  */
-class TheoryEngineModelBuilder : public ModelBuilder
-{
-protected:
-  /** pointer to theory engine */
-  TheoryEngine* d_te;
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_normalizedCache;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-  std::map< Node, Node > d_constantReps;
-
-  /** process build model */
-  virtual bool preProcessBuildModel(TheoryModel* m);
-  virtual bool processBuildModel(TheoryModel* m);
-  virtual void debugModel( TheoryModel* m ) {}
-  /** normalize representative */
-  Node normalize(TheoryModel* m, TNode r, bool evalOnly);
-  bool isAssignable(TNode n);
-  void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
-  void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
-  void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting );
-  /** is v an excluded codatatype value */
-  bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
-  bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
-  /** involves usort */
-  bool involvesUSort( TypeNode tn );
-  bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
-protected:
-  /** assign function f based on the model m. 
-  * This construction is based on "table form". For example:
-  * (f 0 1) = 1
-  * (f 0 2) = 2
-  * (f 1 1) = 3
-  * ...
-  * becomes:
-  * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 
-  *                 (ite (and (= x 0) (= y 2)) 2
-  *                 (ite (and (= x 1) (= y 1)) 3 ...)))
-  */
-  void assignFunction(TheoryModel* m, Node f);
-  /** assign function f based on the model m. 
-  * This construction is based on "dag form". For example:
-  * (f 0 1) = 1
-  * (f 0 2) = 2
-  * (f 1 1) = 3
-  * ...
-  * becomes:
-  * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
-  *                              (ite (= y 2) 2 ...))
-  *                 (ite (= x 1) (ite (= y 1) 3 ...)
-  *                              ...))
-  * 
-  * where the above is represented as a directed acyclic graph (dag).
-  * This construction is accomplished by assigning values to (f c) 
-  * terms before f, e.g. 
-  * (f 0) = (lambda y. (ite (= y 1) 1
-  *                    (ite (= y 2) 2 ...))
-  * (f 1) = (lambda y. (ite (= y 1) 3 ...))
-  * where
-  * f = (lambda xy. (ite (= x 0) ((f 0) y)
-  *                 (ite (= x 1) ((f 1) y) ...))
-  */
-  void assignHoFunction(TheoryModel* m, Node f);
-  /** Assign all unassigned functions in the model m (those returned by TheoryModel::getFunctionsToAssign), 
-  * using the two functions above. Currently:
-  * If ufHo is disabled, we call assignFunction for all functions. 
-  * If ufHo is enabled, we call assignHoFunction.
-  */
-  void assignFunctions(TheoryModel* m);
-public:
-  TheoryEngineModelBuilder(TheoryEngine* te);
-  virtual ~TheoryEngineModelBuilder(){}
-  /** Build model function.
-   *    Should be called only on TheoryModels m
-   */
-  bool buildModel(Model* m);
-  void debugCheckModel(Model* m);
-};/* class TheoryEngineModelBuilder */
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */