Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930)

This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this.

This addresses CVC4/cvc4-projects#113.

Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB:

QF_NIA: +484-53 unsat +792-440 sat
QF_NRA: +32-19 unsat +57-23 sat
However, this PR does not (yet) enable this method by default.

Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions.

1 files changed, 11 insertions, 1 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 91984daca..549f4078e 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -35,7 +35,6 @@
 #include "prop/prop_engine.h"
 #include "smt/command.h"
 #include "theory/atom_requests.h"
-#include "theory/decision_manager.h"
 #include "theory/engine_output_channel.h"
 #include "theory/interrupted.h"
 #include "theory/rewriter.h"
@@ -92,6 +91,9 @@ namespace theory {
   class TheoryEngineModelBuilder;
   class EqEngineManagerDistributed;
 
+  class DecisionManager;
+  class RelevanceManager;
+
   namespace eq {
     class EqualityEngine;
   }/* CVC4::theory::eq namespace */
@@ -165,6 +167,8 @@ class TheoryEngine {
    * The decision manager
    */
   std::unique_ptr<theory::DecisionManager> d_decManager;
+  /** The relevance manager */
+  std::unique_ptr<theory::RelevanceManager> d_relManager;
 
   /**
    * Default model object
@@ -498,6 +502,12 @@ public:
   inline bool needCheck() const {
     return d_outputChannelUsed || d_lemmasAdded;
   }
+  /**
+   * Is the literal lit (possibly) critical for satisfying the input formula in
+   * the current context? This call is applicable only during collectModelInfo
+   * or during LAST_CALL effort.
+   */
+  bool isRelevant(Node lit) const;
 
   /**
    * This is called at shutdown time by the SmtEngine, just before