src/theory/theory_model.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_H
  18 #define __CVC4__THEORY__THEORY_MODEL_H
  19
  20 #include <unordered_map>
  21 #include <unordered_set>
  22
  23 #include "smt/model.h"
  24 #include "theory/rep_set.h"
  25 #include "theory/substitutions.h"
  26 #include "theory/type_enumerator.h"
  27 #include "theory/type_set.h"
  28 #include "theory/uf/equality_engine.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32
  33 /** Theory Model class.
  34  *
  35  * This class represents a model produced by the TheoryEngine.
  36  * The data structures used to represent a model are:
  37  * (1) d_equalityEngine : an equality engine object, which stores
  38  *     an equivalence relation over all terms that exist in
  39  *     the current set of assertions.
  40  * (2) d_substitutions : a substitution map storing cases of
  41  *     explicitly solved terms, for instance during preprocessing.
  42  * (3) d_reps : a map from equivalence class representatives of
  43  *     the equality engine to the (constant) representatives
  44  *     assigned to that equivalence class.
  45  * (4) d_uf_models : a map from uninterpreted functions to their
  46  *     lambda representation.
  47  * (5) d_rep_set : a data structure that allows interpretations
  48  *     for types to be represented as terms. This is useful for
  49  *     finite model finding.
  50  *
  51  * These data structures are built after a full effort check with
  52  * no lemmas sent, within a call to:
  53  *    TheoryEngineModelBuilder::buildModel(...)
  54  * which includes subcalls to TheoryX::collectModelInfo(...) calls.
  55  *
  56  * These calls may modify the model object using the interface
  57  * functions below, including:
  58  * - assertEquality, assertPredicate, assertSkeleton,
  59  *   assertEqualityEngine.
  60  * - assignFunctionDefinition
  61  *
  62  * This class provides several interface functions:
  63  * - hasTerm, getRepresentative, areEqual, areDisequal
  64  * - getEqualityEngine
  65  * - getRepSet
  66  * - hasAssignedFunctionDefinition, getFunctionsToAssign
  67  * - getValue
  68  *
  69  * The above functions can be used for a model m after it has been
  70  * successfully built, i.e. when m->isBuiltSuccess() returns true.
  71  *
  72  * Additionally, all of the above functions, with the exception of getValue,
  73  * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as
  74  * documented in theory_model_builder.h. In particular, we make calls to the
  75  * above functions such as getRepresentative() when assigning total
  76  * interpretations for uninterpreted functions.
  77  */
  78 class TheoryModel : public Model
  79 {
  80   friend class TheoryEngineModelBuilder;
  81 public:
  82   TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
  83   ~TheoryModel() override;
  84
  85   /** reset the model */
  86   virtual void reset();
  87   /** is built
  88    *
  89    * Have we attempted to build this model since the last
  90    * call to reset? Notice for model building techniques
  91    * that are not guaranteed to succeed (such as
  92    * when quantified formulas are enabled), a true return
  93    * value does not imply that this is a model of the
  94    * current assertions.
  95    */
  96   bool isBuilt() { return d_modelBuilt; }
  97   /** is built success
  98    *
  99    * Was this model successfully built since the last call to reset?
 100    */
 101   bool isBuiltSuccess() { return d_modelBuiltSuccess; }
 102   //---------------------------- for building the model
 103   /** Adds a substitution from x to t. */
 104   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 105   /** assert equality holds in the model
 106    *
 107    * This method returns true if and only if the equality engine of this model
 108    * is consistent after asserting the equality to this model.
 109    */
 110   bool assertEquality(TNode a, TNode b, bool polarity);
 111   /** assert predicate holds in the model
 112    *
 113    * This method returns true if and only if the equality engine of this model
 114    * is consistent after asserting the predicate to this model.
 115    */
 116   bool assertPredicate(TNode a, bool polarity);
 117   /** assert all equalities/predicates in equality engine hold in the model
 118    *
 119    * This method returns true if and only if the equality engine of this model
 120    * is consistent after asserting the equality engine to this model.
 121    */
 122   bool assertEqualityEngine(const eq::EqualityEngine* ee,
 123                             std::set<Node>* termSet = NULL);
 124   /** assert skeleton
 125    *
 126    * This method gives a "skeleton" for the model value of the equivalence
 127    * class containing n. This should be an application of interpreted function
 128    * (e.g. datatype constructor, array store, set union chain). The subterms of
 129    * this term that are variables or terms that belong to other theories will
 130    * be filled in with model values.
 131    *
 132    * For example, if we call assertSkeleton on (C x y) where C is a datatype
 133    * constructor and x and y are variables, then the equivalence class of
 134    * (C x y) will be interpreted in m as (C x^m y^m) where
 135    * x^m = m->getValue( x ) and y^m = m->getValue( y ).
 136    *
 137    * It should be called during model generation, before final representatives
 138    * are chosen. In the case of TheoryEngineModelBuilder, it should be called
 139    * during Theory's collectModelInfo( ... ) functions.
 140    */
 141   void assertSkeleton(TNode n);
 142   /** record approximation
 143    *
 144    * This notifies this model that the value of n was approximated in this
 145    * model such that the predicate pred (involving n) holds. For example,
 146    * for transcendental functions, we may determine an error bound on the
 147    * value of a transcendental function, say c-e <= y <= c+e where
 148    * c and e are constants. We call this function with n set to sin( x ) and
 149    * pred set to c-e <= sin( x ) <= c+e.
 150    *
 151    * If recordApproximation is called at least once during the model
 152    * construction process, then check-model is not guaranteed to succeed.
 153    * However, there are cases where we can establish the input is satisfiable
 154    * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
 155    * say we have computed c=.7 and e=.01 as an approximation in the above
 156    * example, then we may reason that the set of assertions { sin(x)>.6 } is
 157    * satisfiable, albiet without establishing an exact (irrational) value for
 158    * sin(x).
 159    *
 160    * This function is simply for bookkeeping, it does not affect the model
 161    * construction process.
 162    */
 163   void recordApproximation(TNode n, TNode pred);
 164   /** set unevaluate/semi-evaluated kind
 165    *
 166    * This informs this model how it should interpret applications of terms with
 167    * kind k in getModelValue. We distinguish four categories of kinds:
 168    *
 169    * [1] "Evaluated"
 170    * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
 171    * These operators can be characterized by the invariant that they are
 172    * "evaluatable". That is, if they are applied to only constants, the rewriter
 173    * is guaranteed to rewrite the application to a constant. When getting
 174    * the model value of <k>( t1...tn ) where k is a kind of this category, we
 175    * compute the (constant) value of t1...tn, say this returns c1...cn, we
 176    * return the (constant) result of rewriting <k>( c1...cn ).
 177    *
 178    * [2] "Unevaluated"
 179    * This includes interpreted symbols like FORALL, EXISTS,
 180    * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
 181    * value for a term <k>( t1...tn ) where k is a kind of this category, we
 182    * check whether <k>( t1...tn ) exists in the equality engine of this model.
 183    * If it does, we return its representative, otherwise we return the term
 184    * itself.
 185    *
 186    * [3] "Semi-evaluated"
 187    * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
 188    * those that correspond to abstractions. Like unevaluated kinds, these
 189    * kinds do not have an evaluator. In contrast to unevaluated kinds, we
 190    * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
 191    * arbitrary value instead of the term itself.
 192    *
 193    * [4] APPLY_UF, where getting the model value depends on an internally
 194    * constructed representation of a lambda model value (d_uf_models).
 195    * It is optional whether this kind is "evaluated" or "semi-evaluated".
 196    * In the case that it is "evaluated", get model rewrites the application
 197    * of the lambda model value of its operator to its evaluated arguments.
 198    *
 199    * By default, all kinds are considered "evaluated". The following methods
 200    * change the interpretation of various (non-APPLY_UF) kinds to one of the
 201    * above categories and should be called by the theories that own the kind
 202    * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
 203    * this model does not enabled function values (this is the case for the model
 204    * of TheoryEngine when the option assignFunctionValues is set to false).
 205    */
 206   void setUnevaluatedKind(Kind k);
 207   void setSemiEvaluatedKind(Kind k);
 208   //---------------------------- end building the model
 209
 210   // ------------------- general equality queries
 211   /** does the equality engine of this model have term a? */
 212   bool hasTerm(TNode a);
 213   /** get the representative of a in the equality engine of this model */
 214   Node getRepresentative(TNode a);
 215   /** are a and b equal in the equality engine of this model? */
 216   bool areEqual(TNode a, TNode b);
 217   /** are a and b disequal in the equality engine of this model? */
 218   bool areDisequal(TNode a, TNode b);
 219   /** get the equality engine for this model */
 220   eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
 221   // ------------------- end general equality queries
 222
 223   /** Get value function.
 224    * This should be called only after a ModelBuilder
 225    * has called buildModel(...) on this model.
 226    *   useDontCares is whether to return Node::null() if
 227    *     n does not occur in the equality engine.
 228    */
 229   Node getValue(TNode n, bool useDontCares = false) const;
 230   /** get comments */
 231   void getComments(std::ostream& out) const override;
 232
 233   //---------------------------- separation logic
 234   /** set the heap and value sep.nil is equal to */
 235   void setHeapModel(Node h, Node neq);
 236   /** get the heap and value sep.nil is equal to */
 237   bool getHeapModel(Expr& h, Expr& neq) const override;
 238   //---------------------------- end separation logic
 239
 240   /** is the list of approximations non-empty? */
 241   bool hasApproximations() const override;
 242   /** get approximations */
 243   std::vector<std::pair<Expr, Expr> > getApproximations() const override;
 244   /** get the representative set object */
 245   const RepSet* getRepSet() const { return &d_rep_set; }
 246   /** get the representative set object (FIXME: remove this, see #1199) */
 247   RepSet* getRepSetPtr() { return &d_rep_set; }
 248   /** return whether this node is a don't-care */
 249   bool isDontCare(Expr expr) const override;
 250   /** get value function for Exprs. */
 251   Expr getValue(Expr expr) const override;
 252   /** get cardinality for sort */
 253   Cardinality getCardinality(Type t) const override;
 254   /** print representative debug function */
 255   void printRepresentativeDebug( const char* c, Node r );
 256   /** print representative function */
 257   void printRepresentative( std::ostream& out, Node r );
 258
 259   //---------------------------- function values
 260   /** a map from functions f to a list of all APPLY_UF terms with operator f */
 261   std::map< Node, std::vector< Node > > d_uf_terms;
 262   /** a map from functions f to a list of all HO_APPLY terms with first argument f */
 263   std::map< Node, std::vector< Node > > d_ho_uf_terms;
 264   /** are function values enabled? */
 265   bool areFunctionValuesEnabled() const;
 266   /** assign function value f to definition f_def */
 267   void assignFunctionDefinition( Node f, Node f_def );
 268   /** have we assigned function f? */
 269   bool hasAssignedFunctionDefinition( Node f ) const { return d_uf_models.find( f )!=d_uf_models.end(); }
 270   /** get the list of functions to assign.
 271   * This list will contain all terms of function type that are terms in d_equalityEngine.
 272   * If higher-order is enabled, we ensure that this list is sorted by type size.
 273   * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T,
 274   * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction).
 275   */
 276   std::vector< Node > getFunctionsToAssign();
 277   //---------------------------- end function values
 278  protected:
 279   /** substitution map for this model */
 280   SubstitutionMap d_substitutions;
 281   /** whether we have tried to build this model in the current context */
 282   bool d_modelBuilt;
 283   /** whether this model has been built successfully */
 284   bool d_modelBuiltSuccess;
 285   /** special local context for our equalityEngine so we can clear it
 286    * independently of search context */
 287   context::Context* d_eeContext;
 288   /** equality engine containing all known equalities/disequalities */
 289   eq::EqualityEngine* d_equalityEngine;
 290   /** approximations (see recordApproximation) */
 291   std::map<Node, Node> d_approximations;
 292   /** list of all approximations */
 293   std::vector<std::pair<Node, Node> > d_approx_list;
 294   /** a set of kinds that are not evaluated */
 295   std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
 296   /** a set of kinds that are semi-evaluated */
 297   std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
 298   /** map of representatives of equality engine to used representatives in
 299    * representative set */
 300   std::map<Node, Node> d_reps;
 301   /** stores set of representatives for each type */
 302   RepSet d_rep_set;
 303   /** true/false nodes */
 304   Node d_true;
 305   Node d_false;
 306   /** comment stream to include in printing */
 307   std::stringstream d_comment_str;
 308   /** Get model value function.
 309    *
 310    * This function is a helper function for getValue.
 311    *   hasBoundVars is whether n may contain bound variables
 312    *   useDontCares is whether to return Node::null() if
 313    *     n does not occur in the equality engine.
 314    */
 315   Node getModelValue(TNode n,
 316                      bool hasBoundVars = false,
 317                      bool useDontCares = false) const;
 318   /** add term internal
 319    *
 320    * This will do any model-specific processing necessary for n,
 321    * such as constraining the interpretation of uninterpreted functions.
 322    * This is called once for all terms in the equality engine, just before
 323    * a model builder constructs this model.
 324    */
 325   virtual void addTermInternal(TNode n);
 326
 327  private:
 328   /** cache for getModelValue */
 329   mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
 330
 331   //---------------------------- separation logic
 332   /** the value of the heap */
 333   Node d_sep_heap;
 334   /** the value of the nil element */
 335   Node d_sep_nil_eq;
 336   //---------------------------- end separation logic
 337
 338   //---------------------------- function values
 339   /** whether function models are enabled */
 340   bool d_enableFuncModels;
 341   /** map from function terms to the (lambda) definitions
 342   * After the model is built, the domain of this map is all terms of function
 343   * type that appear as terms in d_equalityEngine.
 344   */
 345   std::map<Node, Node> d_uf_models;
 346   //---------------------------- end function values
 347 };/* class TheoryModel */
 348
 349 }/* CVC4::theory namespace */
 350 }/* CVC4 namespace */
 351
 352 #endif /* __CVC4__THEORY__THEORY_MODEL_H */