Fix corner case of wrongly applied selector as trigger (#5786)

[cvc5.git] / src / theory / theory_preprocessor.h

diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index e34b10b1dbd01bc6fb018cc6d3c820e019ca5a46..d7c22270dfbdf266420330b9dd8f2d4c062dce98 100644 (file)
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/tconv_seq_proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"
+#include "smt/term_formula_removal.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
@@ -45,7 +46,6 @@ class TheoryPreprocessor
  public:
   /** Constructs a theory preprocessor */
   TheoryPreprocessor(TheoryEngine& engine,
-                     RemoveTermFormulas& tfr,
                      context::UserContext* userContext,
                      ProofNodeManager* pnm = nullptr);
   /** Destroys a theory preprocessor */
@@ -63,20 +63,50 @@ class TheoryPreprocessor
    * @param newLemmas The lemmas to add to the set of assertions,
    * @param newSkolems The skolems that newLemmas correspond to,
    * @param doTheoryPreprocess whether to run theory-specific preprocessing.
-   * @return The trust node corresponding to rewriting node via preprocessing.
+   * @return The (REWRITE) trust node corresponding to rewritten node via
+   * preprocessing.
    */
   TrustNode preprocess(TNode node,
                        std::vector<TrustNode>& newLemmas,
                        std::vector<Node>& newSkolems,
-                       bool doTheoryPreprocess);
+                       bool doTheoryPreprocess,
+                       bool fixedPoint);
   /**
-   * Runs theory specific preprocessing on the non-Boolean parts of
-   * the formula.  This is only called on input assertions, after ITEs
-   * have been removed.
+   * Same as above, without lemma tracking or fixed point. Lemmas for skolems
+   * can be extracted from the RemoveTermFormulas utility.
    */
-  TrustNode theoryPreprocess(TNode node);
+  TrustNode preprocess(TNode node, bool doTheoryPreprocess);
+  /**
+   * Same as above, but transforms the proof of node into a proof of the
+   * preprocessed node and returns the LEMMA trust node.
+   *
+   * @param node The assertion to preprocess,
+   * @param newLemmas The lemmas to add to the set of assertions,
+   * @param newSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The (LEMMA) trust node corresponding to the proof of the rewritten
+   * form of the proven field of node.
+   */
+  TrustNode preprocessLemma(TrustNode node,
+                            std::vector<TrustNode>& newLemmas,
+                            std::vector<Node>& newSkolems,
+                            bool doTheoryPreprocess,
+                            bool fixedPoint);
+  /**
+   * Same as above, without lemma tracking or fixed point. Lemmas for skolems
+   * can be extracted from the RemoveTermFormulas utility.
+   */
+  TrustNode preprocessLemma(TrustNode node, bool doTheoryPreprocess);
+
+  /** Get the term formula removal utility */
+  RemoveTermFormulas& getRemoveTermFormulas();
 
  private:
+  /**
+   * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean
+   * parts of the node.
+   */
+  TrustNode theoryPreprocess(TNode node);
   /** Reference to owning theory engine */
   TheoryEngine& d_engine;
   /** Logic info of theory engine */
@@ -84,7 +114,7 @@ class TheoryPreprocessor
   /** Cache for theory-preprocessing of assertions */
   NodeMap d_ppCache;
   /** The term formula remover */
-  RemoveTermFormulas& d_tfr;
+  RemoveTermFormulas d_tfr;
   /** The term context, which computes hash values for term contexts. */
   InQuantTermContext d_iqtc;
   /**