src/theory/uf/ho_extension.h

   1 /*********************                                                        */
   2 /*! \file ho_extension.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 The higher-order extension of TheoryUF.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__UF__HO_EXTENSION_H
  18 #define __CVC4__THEORY__UF__HO_EXTENSION_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "context/cdhashset.h"
  22 #include "context/cdo.h"
  23 #include "expr/node.h"
  24 #include "theory/theory_model.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace uf {
  29
  30 class TheoryUF;
  31
  32 /** The higher-order extension of the theory of uninterpreted functions
  33  *
  34  * This extension is capable of handling UF constraints involving partial
  35  * applications via the applicative encoding (kind HO_APPLY), and
  36  * (dis)equalities involving function sorts. It uses a lazy applicative
  37  * encoding and implements two axiom schemes, at a high level:
  38  *
  39  * (1) Extensionality, where disequalities between functions witnessed by
  40  * arguments where the two functions differ,
  41  *
  42  * (2) App-Encode, where full applications of UF (kind APPLY_UF) are equated
  43  * with curried applications (kind HO_APPLY).
  44  *
  45  * For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al.
  46  */
  47 class HoExtension
  48 {
  49   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  50   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
  51
  52  public:
  53   HoExtension(TheoryUF& p, context::Context* c, context::UserContext* u);
  54
  55   /** expand definition
  56    *
  57    * This returns the expanded form of node.
  58    *
  59    * In particular, this function will convert applications of HO_APPLY
  60    * to applications of APPLY_UF if they are fully applied, and introduce
  61    * function variables for function heads that are not variables via the
  62    * getApplyUfForHoApply method below.
  63    */
  64   Node expandDefinition(Node node);
  65
  66   /** check higher order
  67    *
  68    * This is called at full effort and infers facts and sends lemmas
  69    * based on higher-order reasoning (specifically, extentionality and
  70    * app completion). It returns the number of lemmas plus facts
  71    * added to the equality engine.
  72    */
  73   unsigned check();
  74
  75   /** applyExtensionality
  76    *
  77    * Given disequality deq f != g, if not already cached, this sends a lemma of
  78    * the form:
  79    *   f = g V (f k) != (g k) for fresh constant k on the output channel of the
  80    * parent TheoryUF object. This is an "extensionality lemma".
  81    * Return value is the number of lemmas of this form sent on the output
  82    * channel.
  83    */
  84   unsigned applyExtensionality(TNode deq);
  85
  86   /** collect model info
  87    *
  88    * This method adds the necessary equalities to the model m such that
  89    * model construction is possible if this method returns true. These
  90    * equalities may include HO_APPLY versions of all APPLY_UF terms.
  91    *
  92    * The argument termSet is the set of relevant terms that the parent TheoryUF
  93    * object has added to m that belong to TheoryUF.
  94    *
  95    * This method ensures that the function variables in termSet
  96    * respect extensionality. If some pair does not, then this method adds an
  97    * extensionality equality directly to the equality engine of m.
  98    *
  99    * In more detail, functions f and g do not respect extensionality if f and g
 100    * are not equal in the model, and there is not a pair of unequal witness
 101    * terms f(k), g(k). In this case, we add the disequality
 102    *    f(k') != g(k')
 103    * for fresh (tuple) of variables k' to the equality engine of m. Notice
 104    * this is done only for functions whose type has infinite cardinality,
 105    * since all functions with finite cardinality are ensured to respect
 106    * extensionality by this point due to our extentionality inference schema.
 107    *
 108    * If this method returns true, then all pairs of functions that are in
 109    * distinct equivalence classes will be guaranteed to be assigned different
 110    * values in m. It returns false if any (dis)equality added to m led to
 111    * an inconsistency in m.
 112    */
 113   bool collectModelInfoHo(std::set<Node>& termSet, TheoryModel* m);
 114
 115  protected:
 116   /** get apply uf for ho apply
 117    *
 118    * This returns the APPLY_UF equivalent for the HO_APPLY term node, where
 119    * node has non-functional return type (that is, it corresponds to a fully
 120    * applied function term).
 121    * This call may introduce a skolem for the head operator and send out a lemma
 122    * specifying the definition.
 123    */
 124   Node getApplyUfForHoApply(Node node);
 125
 126   /** get extensionality disequality
 127    *
 128    * Given disequality deq f != g, this returns the disequality:
 129    *   (f k) != (g k) for fresh constant(s) k.
 130    *
 131    * If isCached is true, then this returns the same k for all calls to this
 132    * method with the same deq. If it is false, it creates fresh k and does not
 133    * cache the result.
 134    */
 135   Node getExtensionalityDeq(TNode deq, bool isCached = true);
 136
 137   /**
 138    * Check whether extensionality should be applied for any pair of terms in the
 139    * equality engine.
 140    *
 141    * If we pass a null model m to this function, then we add extensionality
 142    * lemmas to the output channel and return the total number of lemmas added.
 143    * We only add lemmas for functions whose type is finite, since pairs of
 144    * functions whose types are infinite can be made disequal in a model by
 145    * witnessing a point they are disequal.
 146    *
 147    * If we pass a non-null model m to this function, then we add disequalities
 148    * that correspond to the conclusion of extensionality lemmas to the model's
 149    * equality engine. We return 0 if the equality engine of m is consistent
 150    * after this call, and 1 otherwise. We only add disequalities for functions
 151    * whose type is infinite, since our decision procedure guarantees that
 152    * extensionality lemmas are added for all pairs of functions whose types are
 153    * finite.
 154    */
 155   unsigned checkExtensionality(TheoryModel* m = nullptr);
 156
 157   /** applyAppCompletion
 158    * This infers a correspondence between APPLY_UF and HO_APPLY
 159    * versions of terms for higher-order.
 160    * Given APPLY_UF node e.g. (f a b c), this adds the equality to its
 161    * HO_APPLY equivalent:
 162    *   (f a b c) == (@ (@ (@ f a) b) c)
 163    * to equality engine, if not already equal.
 164    * Return value is the number of equalities added.
 165    */
 166   unsigned applyAppCompletion(TNode n);
 167
 168   /** check whether app-completion should be applied for any
 169    * pair of terms in the equality engine.
 170    */
 171   unsigned checkAppCompletion();
 172   /** collect model info for higher-order term
 173    *
 174    * This adds required constraints to m for term n. In particular, if n is
 175    * an APPLY_UF term, we add its HO_APPLY equivalent in this call. We return
 176    * true if the model m is consistent after this call.
 177    */
 178   bool collectModelInfoHoTerm(Node n, TheoryModel* m);
 179
 180  private:
 181   /** common constants */
 182   Node d_true;
 183   /** the parent of this extension */
 184   TheoryUF& d_parent;
 185   /** extensionality has been applied to these disequalities */
 186   NodeSet d_extensionality;
 187
 188   /** cache of getExtensionalityDeq below */
 189   std::map<Node, Node> d_extensionality_deq;
 190
 191   /** map from non-standard operators to their skolems */
 192   NodeNodeMap d_uf_std_skolem;
 193 }; /* class TheoryUF */
 194
 195 }  // namespace uf
 196 }  // namespace theory
 197 }  // namespace CVC4
 198
 199 #endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */