Make nonlinear extension (more) deterministic (#4996)

This PR tries to make the nonlinear extension more deterministic by keeping the order of input assertion (instead of taking them from a hash set). This makes the ordering somewhat more robust against varying node ids, which proved to be a problem for debugging...
Also adds a few logging messages at interesting places.

1 files changed, 27 insertions, 2 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 733912969..09806cbbd 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -198,6 +198,8 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
   {
     nassertions++;
     const Assertion& assertion = *it;
+    Trace("nl-ext") << "Loaded " << assertion.d_assertion << " from theory"
+                    << std::endl;
     Node lit = assertion.d_assertion;
     if (useRelevance && !v.isRelevant(lit))
     {
@@ -298,6 +300,21 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
     }
   }
 
+  // Try to be "more deterministic" by adding assertions in the order they were
+  // given
+  for (auto it = d_containing.facts_begin(); it != d_containing.facts_end();
+       ++it)
+  {
+    Node lit = (*it).d_assertion;
+    auto iait = init_assertions.find(lit);
+    if (iait != init_assertions.end())
+    {
+      assertions.push_back(lit);
+      init_assertions.erase(iait);
+    }
+  }
+  // Now add left over assertions that have been newly created within this
+  // function by the code above.
   for (const Node& a : init_assertions)
   {
     assertions.push_back(a);
@@ -372,6 +389,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
 
   ++(d_stats.d_checkRuns);
 
+  if (Trace.isOn("nl-ext"))
+  {
+    for (const auto& a : assertions)
+    {
+      Trace("nl-ext") << "Input assertion: " << a << std::endl;
+    }
+  }
+
   if (options::nlExt())
   {
     // initialize the non-linear solver
@@ -388,7 +413,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
 
   // init last call with IAND
   d_iandSlv.initLastCall(assertions, false_asserts, xts);
-  
+
   if (!lems.empty())
   {
     Trace("nl-ext") << "  ...finished with " << lems.size()
@@ -432,7 +457,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                     << std::endl;
     return lems.size();
   }
-  
+
   // main calls to nlExt
   if (options::nlExt())
   {