From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 3 Sep 2020 13:39:58 +0000 (+0200)
Subject: Make nonlinear extension (more) deterministic (#4996)
X-Git-Tag: cvc5-1.0.0~2904
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=337f8b791943e9b6b9a234f4f5422cf173342dd9;p=cvc5.git

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.
---

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())
   {
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index b6d9a19db..2334d3817 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -162,8 +162,8 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
 {
   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
   Trace("theory::conflict")
-      << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode()
-      << ")" << std::endl;
+      << "EngineOutputChannel<" << d_theory << ">::trustedConflict("
+      << pconf.getNode() << ")" << std::endl;
   if (pconf.getGenerator() != nullptr)
   {
     ++d_statistics.trustedConflicts;
@@ -175,6 +175,8 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
 
 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 {
+  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
+                         << ">::trustedLemma(" << plem << ")" << std::endl;
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
   if (plem.getGenerator() != nullptr)
   {