src/smt/term_formula_removal.h

   1 /*********************                                                        */
   2 /*! \file term_formula_removal.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** \brief Removal of term formulas
  13  **
  14  ** Removal of term formulas.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #pragma once
  20
  21 #include <unordered_set>
  22 #include <vector>
  23
  24 #include "context/cdinsert_hashmap.h"
  25 #include "context/context.h"
  26 #include "expr/node.h"
  27 #include "expr/term_context.h"
  28 #include "theory/trust_node.h"
  29 #include "util/hash.h"
  30
  31 namespace CVC4 {
  32
  33 class LazyCDProof;
  34 class ProofNodeManager;
  35 class TConvProofGenerator;
  36
  37 class RemoveTermFormulas {
  38  public:
  39   RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);
  40   ~RemoveTermFormulas();
  41
  42   /**
  43    * By introducing skolem variables, this function removes all occurrences of:
  44    * (1) term ITEs,
  45    * (2) terms of type Boolean that are not Boolean term variables,
  46    * (3) lambdas, and
  47    * (4) Hilbert choice expressions.
  48    * from assertions.
  49    * All additional assertions are pushed into assertions. iteSkolemMap
  50    * contains a map from introduced skolem variables to the index in
  51    * assertions containing the new definition created in conjunction
  52    * with that skolem variable.
  53    *
  54    * As an example of (1):
  55    *   f( (ite C 0 1)) = 2
  56    * becomes
  57    *   f( k ) = 2 ^ ite( C, k=0, k=1 )
  58    *
  59    * As an example of (2):
  60    *   g( (and C1 C2) ) = 3
  61    * becomes
  62    *   g( k ) = 3 ^ ( k <=> (and C1 C2) )
  63    *
  64    * As an example of (3):
  65    *   (lambda x. t[x]) = f
  66    * becomes
  67    *   (forall x. k(x) = t[x]) ^ k = f
  68    * where k is a fresh skolem function.
  69    * This is sometimes called "lambda lifting"
  70    *
  71    * As an example of (4):
  72    *   (witness x. P( x ) ) = t
  73    * becomes
  74    *   P( k ) ^ k = t
  75    * where k is a fresh skolem constant.
  76    *
  77    * With reportDeps true, report reasoning dependences to the proof
  78    * manager (for unsat cores).
  79    *
  80    * @param assertion The assertion to remove term formulas from
  81    * @param newAsserts The new assertions corresponding to axioms for newly
  82    * introduced skolems.
  83    * @param newSkolems The skolems corresponding to each of the newAsserts.
  84    * @param fixedPoint Whether to run term formula removal on the lemmas in
  85    * newAsserts. This adds new assertions to this vector until a fixed
  86    * point is reached. When this option is true, all lemmas in newAsserts
  87    * have all term formulas removed.
  88    * @return a trust node of kind TrustNodeKind::REWRITE whose
  89    * right hand side is assertion after removing term formulas, and the proof
  90    * generator (if provided) that can prove the equivalence.
  91    */
  92   theory::TrustNode run(TNode assertion,
  93                         std::vector<theory::TrustNode>& newAsserts,
  94                         std::vector<Node>& newSkolems,
  95                         bool fixedPoint = false);
  96   /**
  97    * Same as above, but does not track lemmas, and does not run to fixed point.
  98    * The relevant lemmas can be extracted by the caller later using getSkolems
  99    * and getLemmaForSkolem.
 100    */
 101   theory::TrustNode run(TNode assertion);
 102   /**
 103    * Same as above, but transforms a lemma, returning a LEMMA trust node that
 104    * proves the same formula as lem with term formulas removed.
 105    */
 106   theory::TrustNode runLemma(theory::TrustNode lem,
 107                              std::vector<theory::TrustNode>& newAsserts,
 108                              std::vector<Node>& newSkolems,
 109                              bool fixedPoint = false);
 110
 111   /**
 112    * Get proof generator that is responsible for all proofs for removing term
 113    * formulas from nodes. When proofs are enabled, the returned trust node
 114    * of the run method use this proof generator (the trust nodes in newAsserts
 115    * do not use this generator).
 116    */
 117   ProofGenerator* getTConvProofGenerator();
 118
 119   /**
 120    * Get axiom for term n. This returns the axiom that this class uses to
 121    * eliminate the term n, which is determined by its top-most symbol. For
 122    * example, if n is (ite n1 n2 n3), this returns the formula:
 123    *   (ite n1 (= (ite n1 n2 n3) n2) (= (ite n1 n2 n3) n3))
 124    */
 125   static Node getAxiomFor(Node n);
 126
 127  private:
 128   typedef context::CDInsertHashMap<
 129       std::pair<Node, uint32_t>,
 130       Node,
 131       PairHashFunction<Node, uint32_t, NodeHashFunction> >
 132       TermFormulaCache;
 133   /** term formula removal cache
 134    *
 135    * This stores the results of term formula removal for inputs to the run(...)
 136    * function below, where the integer in the pair we hash on is the
 137    * result of cacheVal below.
 138    */
 139   TermFormulaCache d_tfCache;
 140
 141   /** skolem cache
 142    *
 143    * This is a cache that maps terms to the skolem we use to replace them.
 144    *
 145    * Notice that this cache is necessary in addition to d_tfCache, since
 146    * we should use the same skolem to replace terms, regardless of the input
 147    * arguments to run(...). For example:
 148    *
 149    * ite( G, a, b ) = c ^ forall x. P( ite( G, a, b ), x )
 150    *
 151    * should be processed to:
 152    *
 153    * k = c ^ forall x. P( k, x ) ^ ite( G, k=a, k=b )
 154    *
 155    * where notice
 156    *   d_skolem_cache[ite( G, a, b )] = k, and
 157    *   d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
 158    */
 159   context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache;
 160
 161   /** gets the skolem for node
 162    *
 163    * This returns the d_skolem_cache value for node, if it exists as a key
 164    * in the above map, or the null node otherwise.
 165    */
 166   inline Node getSkolemForNode(Node node) const;
 167
 168   /** Pointer to a proof node manager */
 169   ProofNodeManager* d_pnm;
 170   /**
 171    * A proof generator for the term conversion.
 172    */
 173   std::unique_ptr<TConvProofGenerator> d_tpg;
 174   /**
 175    * A proof generator for skolems we introduce that are based on axioms that
 176    * this class is responsible for.
 177    */
 178   std::unique_ptr<LazyCDProof> d_lp;
 179   /**
 180    * The remove term formula context, which computes hash values for term
 181    * contexts.
 182    */
 183   RtfTermContext d_rtfc;
 184
 185   /**
 186    * Removes terms of the forms described above from formula assertion.
 187    * All additional assertions and skolems are pushed into newAsserts and
 188    * newSkolems, which are always of the same length.
 189    *
 190    * This uses a term-context-sensitive stack to process assertion. It returns
 191    * the version of assertion with all term formulas removed.
 192    */
 193   Node runInternal(TNode assertion,
 194                    std::vector<theory::TrustNode>& newAsserts,
 195                    std::vector<Node>& newSkolems);
 196   /**
 197    * This is called on curr of the form (t, val) where t is a term and val is
 198    * a term context identifier computed by RtfTermContext. If curr should be
 199    * replaced by a skolem, this method returns this skolem k. If this was the
 200    * first time that t was encountered, we set newLem to the lemma for the
 201    * skolem that axiomatizes k.
 202    *
 203    * Otherwise, if t should not be replaced in the term context, this method
 204    * returns the null node.
 205    */
 206   Node runCurrent(std::pair<Node, uint32_t>& curr, theory::TrustNode& newLem);
 207
 208   /** Whether proofs are enabled */
 209   bool isProofEnabled() const;
 210 };/* class RemoveTTE */
 211
 212 }/* CVC4 namespace */