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, 8 insertions, 0 deletions

diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
index 9fe973569..c918438ee 100644
--- a/src/theory/output_channel.cpp
+++ b/src/theory/output_channel.cpp
@@ -49,6 +49,10 @@ bool isLemmaPropertySendAtoms(LemmaProperty p)
 {
   return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
 }
+bool isLemmaPropertyNeedsJustify(LemmaProperty p)
+{
+  return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE;
+}
 
 std::ostream& operator<<(std::ostream& out, LemmaProperty p)
 {
@@ -71,6 +75,10 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p)
     {
       out << " SEND_ATOMS";
     }
+    if (isLemmaPropertyNeedsJustify(p))
+    {
+      out << " NEEDS_JUSTIFY";
+    }
     out << " }";
   }
   return out;