From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Oct 2019 17:50:08 +0000 (-0500)
Subject: Fix for non-linear models (#3410)
X-Git-Tag: cvc5-1.0.0~3870
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6a8803054c0c5731a6c4111d8d00c18e2953032;p=cvc5.git

Fix for non-linear models (#3410)

* Towards fix for non-linear models

* Format

* Fix

* More

* Improve

* Format

* More
---

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()
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index f65d3a203..0d82d3f02 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -530,6 +530,8 @@ void TheoryModel::recordApproximation(TNode n, TNode pred)
   Assert(pred.getType().isBoolean());
   d_approximations[n] = pred;
   d_approx_list.push_back(std::pair<Node, Node>(n, pred));
+  // model cache is invalid
+  d_modelCache.clear();
 }
 void TheoryModel::setUsingModelCore()
 {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c1264a122..134f42610 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -536,6 +536,7 @@ set(regress_0_tests
   regress0/model-core.smt2
   regress0/nl/coeff-sat.smt2
   regress0/nl/ext-rew-aggr-test.smt2
+  regress0/nl/issue3407.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2
diff --git a/test/regress/regress0/nl/issue3407.smt2 b/test/regress/regress0/nl/issue3407.smt2
new file mode 100644
index 000000000..e4be74c8a
--- /dev/null
+++ b/test/regress/regress0/nl/issue3407.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert (= (* a b) 1))
+(check-sat)