src/theory/uf/proof_equality_engine.h

   1 /*********************                                                        */
   2 /*! \file proof_equality_engine.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Haniel Barbosa
   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 proof-producing equality engine
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
  18 #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
  19
  20 #include <map>
  21 #include <vector>
  22
  23 #include "context/cdhashmap.h"
  24 #include "context/cdhashset.h"
  25 #include "expr/buffered_proof_generator.h"
  26 #include "expr/lazy_proof.h"
  27 #include "expr/node.h"
  28 #include "expr/proof_node.h"
  29 #include "expr/proof_node_manager.h"
  30 #include "theory/eager_proof_generator.h"
  31 #include "theory/uf/equality_engine.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace eq {
  36
  37 /**
  38  * A layer on top of an EqualityEngine. The goal of this class is manage the
  39  * use of an EqualityEngine object in such a way that the proper proofs are
  40  * internally constructed, and can be retrieved from this class when
  41  * necessary.
  42  *
  43  * Notice that this class is intended to be a *partial layer* on top of
  44  * equality engine. A user of this class should still issue low-level calls
  45  * (getRepresentative, areEqual, areDisequal, etc.) on the underlying equality
  46  * engine directly. The methods that should *not* be called directly on the
  47  * underlying equality engine are:
  48  * - assertEquality/assertPredicate [*]
  49  * - explain
  50  * Instead, the user should use variants of the above methods provided by
  51  * the public interface of this class.
  52  *
  53  * [*] the exception is that assertions from the fact queue (who are their own
  54  * explanation) should be sent directly to the underlying equality engine. This
  55  * is for the sake of efficiency.
  56  *
  57  * This class tracks the reason for why all facts are added to an EqualityEngine
  58  * in a SAT-context dependent manner in a context-dependent (CDProof) object.
  59  * It furthermore maintains an internal FactProofGenerator class for managing
  60  * proofs of facts whose steps are explicitly provided (those that are given
  61  * concrete PfRule, children, and args). Call these "simple facts".
  62  *
  63  * Overall, this class is an eager proof generator (theory/proof_generator.h),
  64  * in that it stores (copies) of proofs for lemmas at the moment they are sent
  65  * out.
  66  *
  67  * A theory that is proof producing and uses the equality engine may use this
  68  * class to manage proofs that are justified by its underlying equality engine.
  69  * In particular, the following interfaces are available for constructing
  70  * a TrustNode:
  71  * - assertConflict, when the user of the equality engine has discovered that
  72  * false can be derived from the current state,
  73  * - assertLemma, for lemmas/conflicts that can be (partially) explained in the
  74  * current state,
  75  * - explain, for explaining why a literal is true in the current state.
  76  * Details on these methods can be found below.
  77  */
  78 class ProofEqEngine : public EagerProofGenerator
  79 {
  80   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
  81   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
  82       NodeProofMap;
  83
  84  public:
  85   ProofEqEngine(context::Context* c,
  86                 context::UserContext* u,
  87                 EqualityEngine& ee,
  88                 ProofNodeManager* pnm);
  89   ~ProofEqEngine() {}
  90   //-------------------------- assert fact
  91   /**
  92    * Assert the literal lit by proof step id, given explanation exp and
  93    * arguments args. This fact is
  94    *
  95    * @param lit The literal to assert to the equality engine
  96    * @param id The proof rule of the proof step concluding lit
  97    * @param exp The premises of the proof step concluding lit. These are also
  98    * the premises that are used when calling explain(lit).
  99    * @param args The arguments to the proof step concluding lit.
 100    * @return true if this fact was processed by this method. If lit already
 101    * holds in the equality engine, this method returns false.
 102    */
 103   bool assertFact(Node lit,
 104                   PfRule id,
 105                   const std::vector<Node>& exp,
 106                   const std::vector<Node>& args);
 107   /** Same as above but where exp is (conjunctive) node */
 108   bool assertFact(Node lit, PfRule id, Node exp, const std::vector<Node>& args);
 109   /**
 110    * Multi-step version of assert fact via a proof step buffer. This method
 111    * is similar to above, but the justification for lit may have multiple steps.
 112    * In particular, we assume that psb has a list of proof steps where the
 113    * proof step concluding lit has free assumptions exp.
 114    *
 115    * For example, a legal call to this method is such that:
 116    *   lit: A
 117    *   exp: B
 118    *   psb.d_steps: { A by (step id1 {B,C} {}), C by (step id2 {} {}) )
 119    * In other words, A holds by a proof step with rule id1 and premises
 120    * B and C, and C holds by proof step with rule id2 and no premises.
 121    *
 122    * @param lit The literal to assert to the equality engine.
 123    * @param exp The premises of the proof steps concluding lit. These are also
 124    * the premises that are used when calling explain(lit).
 125    * @param psb The proof step buffer containing the proof steps.
 126    * @return true if this fact was processed by this method. If lit already
 127    * holds in the equality engine, this method returns false.
 128    */
 129   bool assertFact(Node lit, Node exp, ProofStepBuffer& psb);
 130   /**
 131    * Assert fact via generator pg. This method asserts lit with explanation exp
 132    * to the equality engine of this class. It must be the case that pg can
 133    * provide a proof for lit in terms of exp. More precisely, pg should be
 134    * prepared in the remainder of the SAT context to respond to a call to
 135    * ProofGenerator::getProofFor(lit), and return a proof whose free
 136    * assumptions are a subset of the conjuncts of exp.
 137    *
 138    * @param lit The literal to assert to the equality engine.
 139    * @param exp The premises of the proof concluding lit. These are also
 140    * the premises that are used when calling explain(lit).
 141    * @param pg The proof generator that can provide a proof concluding lit
 142    * from free asumptions in exp.
 143    * @return true if this fact was processed by this method. If lit already
 144    * holds in the equality engine, this method returns false.
 145    */
 146   bool assertFact(Node lit, Node exp, ProofGenerator* pg);
 147   //-------------------------- assert conflicts
 148   /**
 149    * This method is called when the equality engine of this class is
 150    * inconsistent (false has been proven) by a contradictory literal lit. This
 151    * returns the trust node corresponding to the current conflict.
 152    *
 153    * @param lit The conflicting literal, which must rewrite to false.
 154    * @return The trust node capturing the fact that this class can provide a
 155    * proof for this conflict.
 156    */
 157   TrustNode assertConflict(Node lit);
 158   /**
 159    * Get proven conflict from contradictory facts. This method is called when
 160    * the proof rule with premises exp and arguments args implies a contradiction
 161    * by proof rule id.
 162    *
 163    * This method returns the TrustNode containing the corresponding conflict
 164    * resulting from adding this step, and ensures that a proof has been stored
 165    * internally so that this class may respond to a call to
 166    * ProofGenerator::getProof(...).
 167    */
 168   TrustNode assertConflict(PfRule id,
 169                            const std::vector<Node>& exp,
 170                            const std::vector<Node>& args);
 171   /** Generator version, where pg has a proof of false from assumptions exp */
 172   TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg);
 173   //-------------------------- assert lemma
 174   /**
 175    * Called when we have concluded conc, typically via theory specific
 176    * reasoning. The purpose of this method is to construct a TrustNode of
 177    * kind TrustNodeKind::LEMMA or TrustNodeKind::CONFLICT corresponding to the
 178    * lemma or conflict to be sent on the output channel of the Theory.
 179    *
 180    * The user provides the explanation of conc in two parts:
 181    * (1) (exp \ noExplain), which are literals that hold in the equality engine
 182    * of this class,
 183    * (2) noExplain, which do not necessarily hold in the equality engine of this
 184    * class.
 185    * Notice that noExplain is a subset of exp.
 186    *
 187    * The proof for conc follows from exp by proof rule with the given
 188    * id and arguments.
 189    *
 190    * This call corresponds to a conflict if conc is false and noExplain is
 191    * empty.
 192    *
 193    * This returns the TrustNode corresponding to the formula corresonding to
 194    * the call to this method [*], for which a proof can be provided by this
 195    * generator in the remainder of the user context.
 196    *
 197    * [*]
 198    * a. If this call does not correspond to a conflict, then this formula is:
 199    *   ( ^_{e in exp \ noExplain} <explain>(e) ^ noExplain ) => conc
 200    * where <explain>(e) is a conjunction of literals L1 ^ ... ^ Ln such that
 201    * L1 ^ ... ^ Ln entail e, and each Li was passed as an explanation to a
 202    * call to assertFact in the current SAT context. This explanation method
 203    * always succeeds, provided that e is a literal that currently holds in
 204    * the equality engine of this class. Notice that if the antecedant is empty,
 205    * the formula above is assumed to be conc itself. The above formula is
 206    * intended to be valid in Theory that owns this class.
 207    * b. If this call is a conflict, then this formula is:
 208    *   ^_{e in exp} <explain>(e)
 209    * The formula can be queried via TrustNode::getProven in the standard way.
 210    */
 211   TrustNode assertLemma(Node conc,
 212                         PfRule id,
 213                         const std::vector<Node>& exp,
 214                         const std::vector<Node>& noExplain,
 215                         const std::vector<Node>& args);
 216   /** Generator version, where pg has a proof of conc */
 217   TrustNode assertLemma(Node conc,
 218                         const std::vector<Node>& exp,
 219                         const std::vector<Node>& noExplain,
 220                         ProofGenerator* pg);
 221   //-------------------------- explain
 222   /**
 223    * Explain literal conc. This calls the appropriate methods in the underlying
 224    * equality engine of this class to construct the explanation of why conc
 225    * currently holds.
 226    *
 227    * It returns a trust node of kind TrustNodeKind::PROP_EXP whose node
 228    * is the explanation of conc (a conjunction of literals that implies it).
 229    * The proof that can be proven by this generator is then (=> exp conc), see
 230    * TrustNode::getPropExpProven(conc,exp);
 231    *
 232    * @param conc The conclusion to explain
 233    * @return The trust node indicating the explanation of conc and the generator
 234    * (this class) that can prove the implication.
 235    */
 236   TrustNode explain(Node conc);
 237
 238  private:
 239   /** Assert internal */
 240   bool assertFactInternal(TNode pred, bool polarity, TNode reason);
 241   /** holds */
 242   bool holds(TNode pred, bool polarity);
 243   /**
 244    * Ensure proof for fact. This is called by the above method after we have
 245    * determined the final set of assumptions used for showing conc. This
 246    * method is used for lemmas, conflicts, and explanations for propagations.
 247    * The argument tnk is the kind of trust node to return.
 248    */
 249   TrustNode ensureProofForFact(Node conc,
 250                                const std::vector<TNode>& assumps,
 251                                TrustNodeKind tnk,
 252                                ProofGenerator* curr);
 253   /**
 254    * This ensures the proof of the literals that are in exp but not in
 255    * noExplain have been added to curr. This additionally adds the
 256    * explanation of exp to assumps. It updates tnk to LEMMA if there
 257    * are any literals in exp that are not in noExplain.
 258    */
 259   void explainVecWithProof(TrustNodeKind& tnk,
 260                            std::vector<TNode>& assumps,
 261                            const std::vector<Node>& exp,
 262                            const std::vector<Node>& noExplain,
 263                            LazyCDProof* curr);
 264   /** Explain
 265    *
 266    * This adds to assumps the set of facts that were asserted to this
 267    * class in the current SAT context that are required for showing lit.
 268    *
 269    * This additionally registers the equality proof steps required to
 270    * regress the explanation of lit in curr.
 271    */
 272   void explainWithProof(Node lit,
 273                         std::vector<TNode>& assumps,
 274                         LazyCDProof* curr);
 275   /** Reference to the equality engine */
 276   eq::EqualityEngine& d_ee;
 277   /** The default proof generator (for simple facts) */
 278   BufferedProofGenerator d_factPg;
 279   /** common nodes */
 280   Node d_true;
 281   Node d_false;
 282   /** the proof node manager */
 283   ProofNodeManager* d_pnm;
 284   /** The SAT-context-dependent proof object */
 285   LazyCDProof d_proof;
 286   /**
 287    * The keep set of this class. This set is maintained to ensure that
 288    * facts and their explanations are reference counted. Since facts and their
 289    * explanations are SAT-context-dependent, this set is also
 290    * SAT-context-dependent.
 291    */
 292   NodeSet d_keep;
 293 };
 294
 295 }  // namespace eq
 296 }  // namespace theory
 297 }  // namespace CVC4
 298
 299 #endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */