Fix for non-linear models (#3410)

* Towards fix for non-linear models

* Format

* Fix

* More

* Improve

* Format

* More

1 files changed, 63 insertions, 24 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index f067fda47..4dfda79b7 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -2288,32 +2288,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
 
 void NonlinearExtension::check(Theory::Effort e) {
   Trace("nl-ext") << std::endl;
-  Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl;
+  Trace("nl-ext") << "NonlinearExtension::check, effort = " << e
+                  << ", built model = " << d_builtModel.get() << std::endl;
   if (d_builtModel.get())
   {
-    if (e == Theory::EFFORT_FULL)
-    {
-      return;
-    }
-    // now, record the approximations we used
-    NodeManager* nm = NodeManager::currentNM();
-    for (const std::pair<const Node, std::pair<Node, Node> >& cb :
-         d_check_model_bounds)
-    {
-      Node l = cb.second.first;
-      Node u = cb.second.second;
-      if (l != u)
-      {
-        Node v = cb.first;
-        Node pred =
-            nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
-        pred = Rewriter::rewrite(pred);
-        d_containing.getValuation().getModel()->recordApproximation(v, pred);
-      }
-    }
-    return;
+    // already built model, nothing to do
   }
-  if (e == Theory::EFFORT_FULL) {
+  else if (e == Theory::EFFORT_FULL)
+  {
     d_containing.getExtTheory()->clearCache();
     d_needsLastCall = true;
     if (options::nlExtRewrites()) {
@@ -2328,7 +2310,9 @@ void NonlinearExtension::check(Theory::Effort e) {
         Trace("nl-ext") << "...sent lemmas." << std::endl;
       }
     }
-  } else {
+  }
+  else
+  {
     // get the assertions
     std::vector<Node> assertions;
     getAssertions(assertions);
@@ -2508,6 +2492,61 @@ void NonlinearExtension::check(Theory::Effort e) {
 
     } while (needsRecheck);
   }
+
+  // Did we internally determine a model exists? If so, we need to record some
+  // information in the theory engine's model class.
+  if (d_builtModel.get())
+  {
+    if (e < Theory::EFFORT_LAST_CALL)
+    {
+      // don't need to build the model yet
+      return;
+    }
+    // Record the approximations we used. This code calls the
+    // recordApproximation method of the model, which overrides the model
+    // values for variables that we solved for, using techniques specific to
+    // this class.
+    NodeManager* nm = NodeManager::currentNM();
+    TheoryModel* m = d_containing.getValuation().getModel();
+    for (const std::pair<const Node, std::pair<Node, Node> >& cb :
+         d_check_model_bounds)
+    {
+      Node l = cb.second.first;
+      Node u = cb.second.second;
+      Node pred;
+      Node v = cb.first;
+      if (l != u)
+      {
+        pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
+      }
+      else if (!m->areEqual(v, l))
+      {
+        // only record if value was not equal already
+        pred = v.eqNode(l);
+      }
+      if (!pred.isNull())
+      {
+        pred = Rewriter::rewrite(pred);
+        m->recordApproximation(v, pred);
+      }
+    }
+    // Also record the exact values we used. An exact value can be seen as a
+    // special kind approximation of the form (choice x. x = exact_value).
+    // Notice that the above term gets rewritten such that the choice function
+    // is eliminated.
+    for (size_t i = 0, num = d_check_model_vars.size(); i < num; i++)
+    {
+      Node v = d_check_model_vars[i];
+      Node s = d_check_model_subs[i];
+      if (!m->areEqual(v, s))
+      {
+        Node pred = v.eqNode(s);
+        pred = Rewriter::rewrite(pred);
+        m->recordApproximation(v, pred);
+      }
+    }
+    return;
+  }
 }
 
 void NonlinearExtension::presolve()