(cad-solver) Fixed excluding lemma generation. (#4958)

The lemma generation for partial cad checks had a number of issues that have been fixed in this PR.
The previous version had both soundness issues and a very naive approach to handling algebraic numbers.
This new version is sound (fingers crossed) and allows to construct more precise, but also more complex lemmas.
To avoid constructing very large lemmas, a (somewhat arbitrary) limit based on the size of coefficients was added.

1 files changed, 6 insertions, 4 deletions

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index bb1ef9911..b1f0894fb 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -134,10 +134,12 @@ std::vector<NlLemma> CadSolver::checkPartial()
         premise = nm->mkNode(Kind::AND, interval.d_origins);
       }
       Node conclusion =
-          excluding_interval_to_lemma(first_var, interval.d_interval);
-      Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
-      Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl;
-      lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL);
+          excluding_interval_to_lemma(first_var, interval.d_interval, false);
+      if (!conclusion.isNull()) {
+        Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
+        Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl;
+        lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL);
+       }
     }
   }
   return lems;