src/theory/theory_model_builder.h

   1 /*********************                                                        */
   2 /*! \file theory_model.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Clark Barrett, Morgan Deters, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Model class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H
  18 #define __CVC4__THEORY__THEORY_MODEL_BUILDER_H
  19
  20 #include <unordered_map>
  21 #include <unordered_set>
  22
  23 #include "theory/theory_model.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /** TheoryEngineModelBuilder class
  29  *
  30  * This is the class used by TheoryEngine
  31  * for constructing TheoryModel objects, which is the class
  32  * that represents models for a set of assertions.
  33  *
  34  * A call to TheoryEngineModelBuilder::buildModel(...) is made
  35  * after a full effort check passes with no theory solvers
  36  * adding lemmas or conflicts, and theory combination passes
  37  * with no splits on shared terms. If buildModel is successful,
  38  * this will set up the data structures in TheoryModel to represent
  39  * a model for the current set of assertions.
  40  */
  41 class TheoryEngineModelBuilder : public ModelBuilder
  42 {
  43   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
  44   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
  45
  46  public:
  47   TheoryEngineModelBuilder(TheoryEngine* te);
  48   virtual ~TheoryEngineModelBuilder() {}
  49   /** Build model function.
  50    *
  51    * Should be called only on TheoryModels m.
  52    *
  53    * This constructs the model m, via the following steps:
  54    * (1) call TheoryEngine::collectModelInfo,
  55    * (2) builder-specified pre-processing,
  56    * (3) find the equivalence classes of m's
  57    *     equality engine that initially contain constants,
  58    * (4) assign constants to all equivalence classes
  59    *     of m's equality engine, through alternating
  60    *     iterations of evaluation and enumeration,
  61    * (5) builder-specific processing, which includes assigning total
  62    *     interpretations to uninterpreted functions.
  63    *
  64    * This function returns false if any of the above
  65    * steps results in a lemma sent on an output channel.
  66    * Lemmas may be sent on an output channel by this
  67    * builder in steps (2) or (5), for instance, if the model we
  68    * are building fails to satisfy a quantified formula.
  69    */
  70   bool buildModel(Model* m) override;
  71   /** Debug check model.
  72    *
  73    * This throws an assertion failure if the model
  74    * contains an equivalence class with two terms t1 and t2
  75    * such that t1^M != t2^M.
  76    */
  77   void debugCheckModel(Model* m);
  78
  79  protected:
  80   /** pointer to theory engine */
  81   TheoryEngine* d_te;
  82
  83   //-----------------------------------virtual functions
  84   /** pre-process build model
  85    * Do pre-processing specific to this model builder.
  86    * Called in step (2) of the build construction,
  87    * described above.
  88    */
  89   virtual bool preProcessBuildModel(TheoryModel* m);
  90   /** process build model
  91    * Do processing specific to this model builder.
  92    * Called in step (5) of the build construction,
  93    * described above.
  94    * By default, this assigns values to each function
  95    * that appears in m's equality engine.
  96    */
  97   virtual bool processBuildModel(TheoryModel* m);
  98   /** debug the model
  99    * Check assertions and printing debug information for the model.
 100    * Calls after step (5) described above is complete.
 101    */
 102   virtual void debugModel(TheoryModel* m) {}
 103   //-----------------------------------end virtual functions
 104
 105   /** is n assignable?
 106    *
 107    * A term n is assignable if its value
 108    * is unconstrained by a standard model.
 109    * Examples of assignable terms are:
 110    * - variables,
 111    * - applications of array select,
 112    * - applications of datatype selectors,
 113    * - applications of uninterpreted functions.
 114    * Assignable terms must be first-order, that is,
 115    * all instances of the above terms are not
 116    * assignable if they have a higher-order (function) type.
 117    */
 118   bool isAssignable(TNode n);
 119   /** add assignable subterms
 120    * Adds all assignable subterms of n to tm's equality engine.
 121    */
 122   void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
 123   /** normalize representative r
 124    *
 125    * This returns a term that is equivalent to r's
 126    * interpretation in the model m. It may do so
 127    * by rewriting the application of r's operator to the
 128    * result of normalizing each of r's children, if
 129    * each child is constant.
 130    */
 131   Node normalize(TheoryModel* m, TNode r, bool evalOnly);
 132   /** assign constant representative
 133    *
 134    * Called when equivalence class eqc is assigned a constant
 135    * representative const_rep.
 136    *
 137    * eqc should be a representative of tm's equality engine.
 138    */
 139   void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
 140   /** add to type list
 141    *
 142    * This adds to type_list the list of types that tn is built from.
 143    * For example, if tn is (Array Int Bool) and type_list is empty,
 144    * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
 145    */
 146   void addToTypeList(
 147       TypeNode tn,
 148       std::vector<TypeNode>& type_list,
 149       std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
 150   /** assign function f based on the model m.
 151   * This construction is based on "table form". For example:
 152   * (f 0 1) = 1
 153   * (f 0 2) = 2
 154   * (f 1 1) = 3
 155   * ...
 156   * becomes:
 157   * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
 158   *                 (ite (and (= x 0) (= y 2)) 2
 159   *                 (ite (and (= x 1) (= y 1)) 3 ...)))
 160   */
 161   void assignFunction(TheoryModel* m, Node f);
 162   /** assign function f based on the model m.
 163   * This construction is based on "dag form". For example:
 164   * (f 0 1) = 1
 165   * (f 0 2) = 2
 166   * (f 1 1) = 3
 167   * ...
 168   * becomes:
 169   * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
 170   *                              (ite (= y 2) 2 ...))
 171   *                 (ite (= x 1) (ite (= y 1) 3 ...)
 172   *                              ...))
 173   *
 174   * where the above is represented as a directed acyclic graph (dag).
 175   * This construction is accomplished by assigning values to (f c)
 176   * terms before f, e.g.
 177   * (f 0) = (lambda y. (ite (= y 1) 1
 178   *                    (ite (= y 2) 2 ...))
 179   * (f 1) = (lambda y. (ite (= y 1) 3 ...))
 180   * where
 181   * f = (lambda xy. (ite (= x 0) ((f 0) y)
 182   *                 (ite (= x 1) ((f 1) y) ...))
 183   */
 184   void assignHoFunction(TheoryModel* m, Node f);
 185   /** assign functions
 186    *
 187    * Assign all unassigned functions in the model m (those returned by
 188    * TheoryModel::getFunctionsToAssign),
 189    * using the two functions above. Currently:
 190    * If ufHo is disabled, we call assignFunction for all functions.
 191    * If ufHo is enabled, we call assignHoFunction.
 192    */
 193   void assignFunctions(TheoryModel* m);
 194
 195  private:
 196   /** normalized cache
 197    * A temporary cache mapping terms to their
 198    * normalized form, used during buildModel.
 199    */
 200   NodeMap d_normalizedCache;
 201   /** mapping from terms to the constant associated with their equivalence class
 202    */
 203   std::map<Node, Node> d_constantReps;
 204
 205   //------------------------------------for codatatypes
 206   /** is v an excluded codatatype value?
 207    *
 208    * If this returns true, then v is a value
 209    * that cannot be used during enumeration in step (4)
 210    * of model construction.
 211    *
 212    * repSet is the set of representatives of the same type as v,
 213    * assertedReps is a map from representatives t,
 214    * eqc is the equivalence class that v reside.
 215    *
 216    * This function is used to avoid alpha-equivalent
 217    * assignments for codatatype terms, described in
 218    * Reynolds/Blanchette CADE 2015. In particular,
 219    * this function returns true if v is in
 220    * the set V^{x}_I from page 9, where x is eqc
 221    * and I is the model we are building.
 222    */
 223   bool isExcludedCdtValue(Node v,
 224                           std::set<Node>* repSet,
 225                           std::map<Node, Node>& assertedReps,
 226                           Node eqc);
 227   /** is codatatype value match
 228    *
 229    * This returns true if v is r{ eqc -> t } for some t.
 230    * If this function returns true, then t above is
 231    * stored in eqc_m.
 232    */
 233   bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
 234   //------------------------------------end for codatatypes
 235
 236   //---------------------------------for debugging finite model finding
 237   /** does type tn involve an uninterpreted sort? */
 238   bool involvesUSort(TypeNode tn);
 239   /** is v an excluded value based on uninterpreted sorts?
 240    * This gives an assertion failure in the case that v contains
 241    * an uninterpreted constant whose index is out of the bounds
 242    * specified by eqc_usort_count.
 243    */
 244   bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
 245                             Node v,
 246                             std::map<Node, bool>& visited);
 247   //---------------------------------end for debugging finite model finding
 248
 249 }; /* class TheoryEngineModelBuilder */
 250
 251 } /* CVC4::theory namespace */
 252 } /* CVC4 namespace */
 253
 254 #endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */