src/theory/theory_model_builder.h

   1 /*********************                                                        */
   2 /*! \file theory_model_builder.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mathias Preiner, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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
  27 class TheoryEngine;
  28
  29 namespace theory {
  30
  31 /** TheoryEngineModelBuilder class
  32  *
  33  * This is the class used by TheoryEngine
  34  * for constructing TheoryModel objects, which is the class
  35  * that represents models for a set of assertions.
  36  *
  37  * A call to TheoryEngineModelBuilder::buildModel(...) is made
  38  * after a full effort check passes with no theory solvers
  39  * adding lemmas or conflicts, and theory combination passes
  40  * with no splits on shared terms. If buildModel is successful,
  41  * this will set up the data structures in TheoryModel to represent
  42  * a model for the current set of assertions.
  43  */
  44 class TheoryEngineModelBuilder
  45 {
  46   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
  47   typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
  48
  49  public:
  50   TheoryEngineModelBuilder(TheoryEngine* te);
  51   virtual ~TheoryEngineModelBuilder() {}
  52   /**
  53    * Should be called only on models m after they have been prepared
  54    * (e.g. using ModelManager). In other words, the equality engine of model
  55    * m contains all relevant information from each theory that is needed
  56    * for building a model. This class is responsible simply for ensuring
  57    * that all equivalence classes of the equality engine of m are assigned
  58    * constants.
  59    *
  60    * This constructs the model m, via the following steps:
  61    * (1) builder-specified pre-processing,
  62    * (2) find the equivalence classes of m's
  63    *     equality engine that initially contain constants,
  64    * (3) assign constants to all equivalence classes
  65    *     of m's equality engine, through alternating
  66    *     iterations of evaluation and enumeration,
  67    * (4) builder-specific processing, which includes assigning total
  68    *     interpretations to uninterpreted functions.
  69    *
  70    * This function returns false if any of the above
  71    * steps results in a lemma sent on an output channel.
  72    * Lemmas may be sent on an output channel by this
  73    * builder in steps (2) or (5), for instance, if the model we
  74    * are building fails to satisfy a quantified formula.
  75    */
  76   bool buildModel(TheoryModel* m);
  77
  78   /** postprocess model
  79    *
  80    * This is called when m is a model that will be returned to the user. This
  81    * method checks the internal consistency of the model if we are in a debug
  82    * build.
  83    */
  84   void postProcessModel(bool incomplete, TheoryModel* m);
  85
  86  protected:
  87   /** pointer to theory engine */
  88   TheoryEngine* d_te;
  89
  90   //-----------------------------------virtual functions
  91   /** pre-process build model
  92    * Do pre-processing specific to this model builder.
  93    * Called in step (2) of the build construction,
  94    * described above.
  95    */
  96   virtual bool preProcessBuildModel(TheoryModel* m);
  97   /** process build model
  98    * Do processing specific to this model builder.
  99    * Called in step (5) of the build construction,
 100    * described above.
 101    * By default, this assigns values to each function
 102    * that appears in m's equality engine.
 103    */
 104   virtual bool processBuildModel(TheoryModel* m);
 105   /** debug the model
 106    * Check assertions and printing debug information for the model.
 107    * Calls after step (5) described above is complete.
 108    */
 109   virtual void debugModel(TheoryModel* m) {}
 110   //-----------------------------------end virtual functions
 111
 112   /** Debug check model.
 113    *
 114    * This throws an assertion failure if the model contains an equivalence
 115    * class with two terms t1 and t2 such that t1^M != t2^M.
 116    */
 117   void debugCheckModel(TheoryModel* m);
 118
 119   /** Evaluate equivalence class
 120    *
 121    * If this method returns a non-null node c, then c is a constant and some
 122    * term in the equivalence class of r evaluates to c based on the current
 123    * state of the model m.
 124    */
 125   Node evaluateEqc(TheoryModel* m, TNode r);
 126   /** is n an assignable expression?
 127    *
 128    * A term n is an assignable expression if its value is unconstrained by a
 129    * standard model. Examples of assignable terms are:
 130    * - variables,
 131    * - applications of array select,
 132    * - applications of datatype selectors,
 133    * - applications of uninterpreted functions.
 134    * Assignable terms must be first-order, that is, all instances of the above
 135    * terms are not assignable if they have a higher-order (function) type.
 136    */
 137   bool isAssignable(TNode n);
 138   /** add assignable subterms
 139    * Adds all assignable subterms of n to tm's equality engine.
 140    */
 141   void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
 142   /** normalize representative r
 143    *
 144    * This returns a term that is equivalent to r's
 145    * interpretation in the model m. It may do so
 146    * by rewriting the application of r's operator to the
 147    * result of normalizing each of r's children, if
 148    * each child is constant.
 149    */
 150   Node normalize(TheoryModel* m, TNode r, bool evalOnly);
 151   /** assign constant representative
 152    *
 153    * Called when equivalence class eqc is assigned a constant
 154    * representative const_rep.
 155    *
 156    * eqc should be a representative of tm's equality engine.
 157    */
 158   void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
 159   /** add to type list
 160    *
 161    * This adds to type_list the list of types that tn is built from.
 162    * For example, if tn is (Array Int Bool) and type_list is empty,
 163    * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
 164    */
 165   void addToTypeList(
 166       TypeNode tn,
 167       std::vector<TypeNode>& type_list,
 168       std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
 169   /** assign function f based on the model m.
 170   * This construction is based on "table form". For example:
 171   * (f 0 1) = 1
 172   * (f 0 2) = 2
 173   * (f 1 1) = 3
 174   * ...
 175   * becomes:
 176   * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
 177   *                 (ite (and (= x 0) (= y 2)) 2
 178   *                 (ite (and (= x 1) (= y 1)) 3 ...)))
 179   */
 180   void assignFunction(TheoryModel* m, Node f);
 181   /** assign function f based on the model m.
 182   * This construction is based on "dag form". For example:
 183   * (f 0 1) = 1
 184   * (f 0 2) = 2
 185   * (f 1 1) = 3
 186   * ...
 187   * becomes:
 188   * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
 189   *                              (ite (= y 2) 2 ...))
 190   *                 (ite (= x 1) (ite (= y 1) 3 ...)
 191   *                              ...))
 192   *
 193   * where the above is represented as a directed acyclic graph (dag).
 194   * This construction is accomplished by assigning values to (f c)
 195   * terms before f, e.g.
 196   * (f 0) = (lambda y. (ite (= y 1) 1
 197   *                    (ite (= y 2) 2 ...))
 198   * (f 1) = (lambda y. (ite (= y 1) 3 ...))
 199   * where
 200   * f = (lambda xy. (ite (= x 0) ((f 0) y)
 201   *                 (ite (= x 1) ((f 1) y) ...))
 202   */
 203   void assignHoFunction(TheoryModel* m, Node f);
 204   /** assign functions
 205    *
 206    * Assign all unassigned functions in the model m (those returned by
 207    * TheoryModel::getFunctionsToAssign),
 208    * using the two functions above. Currently:
 209    * If ufHo is disabled, we call assignFunction for all functions.
 210    * If ufHo is enabled, we call assignHoFunction.
 211    */
 212   void assignFunctions(TheoryModel* m);
 213
 214  private:
 215   /** normalized cache
 216    * A temporary cache mapping terms to their
 217    * normalized form, used during buildModel.
 218    */
 219   NodeMap d_normalizedCache;
 220   /** mapping from terms to the constant associated with their equivalence class
 221    */
 222   std::map<Node, Node> d_constantReps;
 223
 224   /** Theory engine model builder assigner class
 225    *
 226    * This manages the assignment of values to terms of a given type.
 227    * In particular, it is a wrapper around a type enumerator that is restricted
 228    * by a set of values that it cannot generate, called an "assignment exclusion
 229    * set".
 230    */
 231   class Assigner
 232   {
 233    public:
 234     Assigner() : d_te(nullptr), d_isActive(false) {}
 235     /**
 236      * Initialize this assigner to generate values of type tn, with properties
 237      * tep and assignment exclusion set aes.
 238      */
 239     void initialize(TypeNode tn,
 240                     TypeEnumeratorProperties* tep,
 241                     const std::vector<Node>& aes);
 242     /** get the next term in the enumeration
 243      *
 244      * This method returns the next legal term based on type enumeration, where
 245      * a term is legal it does not belong to the assignment exclusion set of
 246      * this assigner. If no more terms exist, this method returns null. This
 247      * should never be the case due to the conditions ensured by theory solvers
 248      * for finite types. If it is the case, we give an assertion failure.
 249      */
 250     Node getNextAssignment();
 251     /** The type enumerator */
 252     std::unique_ptr<TypeEnumerator> d_te;
 253     /** The assignment exclusion set of this Assigner */
 254     std::vector<Node> d_assignExcSet;
 255     /**
 256      * Is active, flag set to true when all values in d_assignExcSet are
 257      * constant.
 258      */
 259     bool d_isActive;
 260   };
 261   /** Is the given Assigner ready to assign values?
 262    *
 263    * This returns true if all values in the assignment exclusion set of a have
 264    * a known value according to the state of this model builder (via a lookup
 265    * in d_constantReps). It updates the assignment exclusion vector of a to
 266    * these values whenever possible.
 267    */
 268   bool isAssignerActive(TheoryModel* tm, Assigner& a);
 269   /** compute assignable information
 270    *
 271    * This computes necessary information pertaining to how values should be
 272    * assigned to equivalence classes in the equality engine of tm.
 273    *
 274    * The argument tep stores global information about how values should be
 275    * assigned, such as information on how many uninterpreted constant
 276    * values are available, which is restricted if finite model finding is
 277    * enabled.
 278    *
 279    * In particular this method constructs the following, passed as arguments:
 280    * (1) assignableEqc: the set of equivalence classes that are "assignable",
 281    * i.e. those that have an assignable expression in them (see isAssignable),
 282    * and have not already been assigned a constant,
 283    * (2) evaluableEqc: the set of equivalence classes that are "evaluable", i.e.
 284    * those that have an expression in them that is not assignable, and have not
 285    * already been assigned a constant,
 286    * (3) eqcToAssigner: assigner objects for relevant equivalence classes that
 287    * require special ways of assigning values, e.g. those that take into
 288    * account assignment exclusion sets,
 289    * (4) eqcToAssignerMaster: a map from equivalence classes to the equivalence
 290    * class that it shares an assigner object with (all elements in the range of
 291    * this map are in the domain of eqcToAssigner).
 292    */
 293   void computeAssignableInfo(
 294       TheoryModel* tm,
 295       TypeEnumeratorProperties& tep,
 296       std::unordered_set<Node, NodeHashFunction>& assignableEqc,
 297       std::unordered_set<Node, NodeHashFunction>& evaluableEqc,
 298       std::map<Node, Assigner>& eqcToAssigner,
 299       std::map<Node, Node>& eqcToAssignerMaster);
 300   //------------------------------------for codatatypes
 301   /** is v an excluded codatatype value?
 302    *
 303    * If this returns true, then v is a value
 304    * that cannot be used during enumeration in step (4)
 305    * of model construction.
 306    *
 307    * repSet is the set of representatives of the same type as v,
 308    * assertedReps is a map from representatives t,
 309    * eqc is the equivalence class that v reside.
 310    *
 311    * This function is used to avoid alpha-equivalent
 312    * assignments for codatatype terms, described in
 313    * Reynolds/Blanchette CADE 2015. In particular,
 314    * this function returns true if v is in
 315    * the set V^{x}_I from page 9, where x is eqc
 316    * and I is the model we are building.
 317    */
 318   bool isExcludedCdtValue(Node v,
 319                           std::set<Node>* repSet,
 320                           std::map<Node, Node>& assertedReps,
 321                           Node eqc);
 322   /** is codatatype value match
 323    *
 324    * This returns true if v is r{ eqc -> t } for some t.
 325    * If this function returns true, then t above is
 326    * stored in eqc_m.
 327    */
 328   bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
 329   //------------------------------------end for codatatypes
 330
 331   //---------------------------------for debugging finite model finding
 332   /** does type tn involve an uninterpreted sort? */
 333   bool involvesUSort(TypeNode tn);
 334   /** is v an excluded value based on uninterpreted sorts?
 335    * This gives an assertion failure in the case that v contains
 336    * an uninterpreted constant whose index is out of the bounds
 337    * specified by eqc_usort_count.
 338    */
 339   bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
 340                             Node v,
 341                             std::map<Node, bool>& visited);
 342   //---------------------------------end for debugging finite model finding
 343
 344 }; /* class TheoryEngineModelBuilder */
 345
 346 } /* CVC4::theory namespace */
 347 } /* CVC4 namespace */
 348
 349 #endif /* CVC4__THEORY__THEORY_MODEL_BUILDER_H */