Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)

This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.

This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.

In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.

This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index b5411aaba..544be84d6 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -33,6 +33,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
+class QuantifiersMacros;
+
 class TheoryQuantifiers : public Theory {
  public:
   TheoryQuantifiers(context::Context* c,
@@ -56,6 +58,11 @@ class TheoryQuantifiers : public Theory {
 
   void preRegisterTerm(TNode n) override;
   void presolve() override;
+  /**
+   * Preprocess assert, which solves for quantifier macros when enabled.
+   */
+  PPAssertStatus ppAssert(TrustNode tin,
+                          TrustSubstitutionMap& outSubstitutions) override;
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   //--------------------------------- standard check
   /** Post-check, called after the fact queue of the theory is processed. */
@@ -95,6 +102,8 @@ class TheoryQuantifiers : public Theory {
   QuantifiersInferenceManager d_qim;
   /** The quantifiers engine, which lives here */
   std::unique_ptr<QuantifiersEngine> d_qengine;
+  /** The quantifiers macro module, used for ppAssert. */
+  std::unique_ptr<QuantifiersMacros> d_qmacros;
 };/* class TheoryQuantifiers */
 
 }  // namespace quantifiers