src/theory/theory_model_builder.h

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