#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 {
public:
/** Constructs a theory preprocessor */
TheoryPreprocessor(TheoryEngine& engine,
- RemoveTermFormulas& tfr,
context::UserContext* userContext,
ProofNodeManager* pnm = nullptr);
/** Destroys a theory preprocessor */
* @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 */
/** 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;
/**