Make nonlinear extension account for relevant term set (#6147)

This fixes a subtle issue with non-linear and theory combination.

It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.

In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.

Fixes #5662.

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 671c3f44a59bff97ed6ac5df221eefdfc8d21553..25aebf6d4874fef72231de2742e51fa3e294b6c2 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -301,7 +301,7 @@ void NonlinearExtension::check(Theory::Effort e)
   }
 }
 
-bool NonlinearExtension::modelBasedRefinement()
+bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet)
 {
   ++(d_stats.d_mbrRuns);
   d_checkCounter++;
@@ -317,8 +317,18 @@ bool NonlinearExtension::modelBasedRefinement()
   Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl;
 
   // get the extended terms belonging to this theory
+  std::vector<Node> xtsAll;
+  d_extTheory.getTerms(xtsAll);
+  // only consider those that are currently relevant based on the current
+  // assertions, i.e. those contained in termSet
   std::vector<Node> xts;
-  d_extTheory.getTerms(xts);
+  for (const Node& x : xtsAll)
+  {
+    if (termSet.find(x) != termSet.end())
+    {
+      xts.push_back(x);
+    }
+  }
 
   if (Trace.isOn("nl-ext-debug"))
   {
@@ -496,7 +506,8 @@ bool NonlinearExtension::modelBasedRefinement()
   return false;
 }
 
-void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
+void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel,
+                                        const std::set<Node>& termSet)
 {
   if (!needsCheckLastEffort())
   {
@@ -509,7 +520,7 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
   if (!d_builtModel.get())
   {
     Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
-    modelBasedRefinement();
+    modelBasedRefinement(termSet);
   }
   if (d_builtModel.get())
   {

diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index baa0f886cd49d784921088a40a1ee0230ecc42e9..09e3a837012a7f0040796e6cc6c9be9d905aec71 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -128,7 +128,8 @@ class NonlinearExtension
    * arithModel so that it satisfies certain nonlinear constraints. This may
    * involve e.g. solving for variables in nonlinear equations.
    */
-  void interceptModel(std::map<Node, Node>& arithModel);
+  void interceptModel(std::map<Node, Node>& arithModel,
+                      const std::set<Node>& termSet);
   /** Does this class need a call to check(...) at last call effort? */
   bool needsCheckLastEffort() const { return d_needsLastCall; }
   /** presolve
@@ -158,7 +159,7 @@ class NonlinearExtension
    * may have information regarding how to construct a model, in the case that
    * we determined the problem is satisfiable.
    */
-  bool modelBasedRefinement();
+  bool modelBasedRefinement(const std::set<Node>& termSet);
 
   /** get assertions
    *

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 83337dd90a6356522d832cee6555396b4558f4bc..36b2d3eb8735d00b120b44763122d5d94d496ff6 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -248,7 +248,7 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
   {
     // Non-linear may repair values to satisfy non-linear constraints (see
     // documentation for NonlinearExtension::interceptModel).
-    d_nonlinearExtension->interceptModel(arithModel);
+    d_nonlinearExtension->interceptModel(arithModel, termSet);
   }
   // We are now ready to assert the model.
   for (const std::pair<const Node, Node>& p : arithModel)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 30cdf43d9c31b54b0473a9adf87f6a27e7d8e717..5c28a34cc9fb2bcf68ba068b4ac2983c0f9a983f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1596,6 +1596,8 @@ set(regress_1_tests
   regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
+  regress1/nl/issue5662-nl-tc.smt2
+  regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2

diff --git a/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2
new file mode 100644 (file)
index 0000000..0e7279e
--- /dev/null
+++ b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2
@@ -0,0 +1,16 @@
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun j () Real)
+(declare-fun k () Real)
+(declare-fun h () Real)
+(assert (< 0 k))
+(assert (= 1 (* k j)))
+(assert
+    (or
+        (= h 0)
+        (= 0.0 (* a k))
+    )
+)
+(assert (distinct a h))
+(check-sat)

diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2
new file mode 100644 (file)
index 0000000..d805b72
--- /dev/null
+++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2
@@ -0,0 +1,17 @@
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun j () Real)
+(declare-fun e () Real)
+(declare-fun f () Real)
+(declare-fun k () Real)
+(declare-fun g () Real)
+(declare-fun h () Real)
+(assert (forall ((i Real)) (xor (and (or (and (or (and (or (and (or
+  (and (> 0.0 (* a e) (* c e)) (>= 0 k)) (<= g 0)) (= (* b j)
+  2.0))))) (> f k)) (>= 0.0 k))) (>= 0 k))))
+(assert (distinct a (* d h)))
+(check-sat)