src/theory/quantifiers/entailment_check.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   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  * Entailment check class
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
  19 #define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
  20
  21 #include <map>
  22 #include <vector>
  23
  24 #include "expr/node.h"
  25 #include "smt/env_obj.h"
  26
  27 namespace cvc5 {
  28 namespace theory {
  29 namespace quantifiers {
  30
  31 class QuantifiersState;
  32 class TermDb;
  33
  34 /**
  35  * Entailment check utility, which determines whether formulas are entailed
  36  * in the current context. The main focus of this class is on UF formulas.
  37  * It works by looking at the term argument trie data structures in term
  38  * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018.
  39  */
  40 class EntailmentCheck : protected EnvObj
  41 {
  42  public:
  43   EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb);
  44   ~EntailmentCheck();
  45   /** evaluate term
  46    *
  47    * Returns a term n' such that n = n' is entailed based on the equality
  48    * information ee.  This function may generate new terms. In particular,
  49    * we typically rewrite subterms of n of maximal size to terms that exist in
  50    * the equality engine specified by ee.
  51    *
  52    * useEntailmentTests is whether to call the theory engine's entailmentTest
  53    * on literals n for which this call fails to find a term n' that is
  54    * equivalent to n, for increased precision. This is not frequently used.
  55    *
  56    * The vector exp stores the explanation for why n evaluates to that term,
  57    * that is, if this call returns a non-null node n', then:
  58    *   exp => n = n'
  59    *
  60    * If reqHasTerm, then we require that the returned term is a Boolean
  61    * combination of terms that exist in the equality engine used by this call.
  62    * If no such term is constructable, this call returns null. The motivation
  63    * for setting this to true is to "fail fast" if we require the return value
  64    * of this function to only involve existing terms. This is used e.g. in
  65    * the "propagating instances" portion of conflict-based instantiation
  66    * (quant_conflict_find.h).
  67    */
  68   Node evaluateTerm(TNode n,
  69                     std::vector<Node>& exp,
  70                     bool useEntailmentTests = false,
  71                     bool reqHasTerm = false);
  72   /** same as above, without exp */
  73   Node evaluateTerm(TNode n,
  74                     bool useEntailmentTests = false,
  75                     bool reqHasTerm = false);
  76   /** get entailed term
  77    *
  78    * If possible, returns a term n' such that:
  79    * (1) n' exists in the current equality engine (as specified by the state),
  80    * (2) n = n' is entailed in the current context.
  81    * It returns null if no such term can be found.
  82    * Wrt evaluateTerm, this version does not construct new terms, and
  83    * thus is less aggressive.
  84    */
  85   TNode getEntailedTerm(TNode n);
  86   /** get entailed term
  87    *
  88    * If possible, returns a term n' such that:
  89    * (1) n' exists in the current equality engine (as specified by the state),
  90    * (2) n * subs = n' is entailed in the current context, where * denotes
  91    * substitution application.
  92    * It returns null if no such term can be found.
  93    * subsRep is whether the substitution maps to terms that are representatives
  94    * according to the quantifiers state.
  95    * Wrt evaluateTerm, this version does not construct new terms, and
  96    * thus is less aggressive.
  97    */
  98   TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
  99   /** is entailed
 100    * Checks whether the current context entails n with polarity pol, based on
 101    * the equality information in the quantifiers state. Returns true if the
 102    * entailment can be successfully shown.
 103    */
 104   bool isEntailed(TNode n, bool pol);
 105   /** is entailed
 106    *
 107    * Checks whether the current context entails ( n * subs ) with polarity pol,
 108    * based on the equality information in the quantifiers state,
 109    * where * denotes substitution application.
 110    * subsRep is whether the substitution maps to terms that are representatives
 111    * according to in the quantifiers state.
 112    */
 113   bool isEntailed(TNode n,
 114                   std::map<TNode, TNode>& subs,
 115                   bool subsRep,
 116                   bool pol);
 117
 118  protected:
 119   /** helper for evaluate term */
 120   Node evaluateTerm2(TNode n,
 121                      std::map<TNode, Node>& visited,
 122                      std::vector<Node>& exp,
 123                      bool useEntailmentTests,
 124                      bool computeExp,
 125                      bool reqHasTerm);
 126   /** helper for get entailed term */
 127   TNode getEntailedTerm2(TNode n,
 128                          std::map<TNode, TNode>& subs,
 129                          bool subsRep,
 130                          bool hasSubs);
 131   /** helper for is entailed */
 132   bool isEntailed2(TNode n,
 133                    std::map<TNode, TNode>& subs,
 134                    bool subsRep,
 135                    bool hasSubs,
 136                    bool pol);
 137   /** The quantifiers state object */
 138   QuantifiersState& d_qstate;
 139   /** Reference to the term database */
 140   TermDb& d_tdb;
 141   /** boolean terms */
 142   Node d_true;
 143   Node d_false;
 144 }; /* class EntailmentCheck */
 145
 146 }  // namespace quantifiers
 147 }  // namespace theory
 148 }  // namespace cvc5
 149
 150 #endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */