Support for witnessing choice in models (#3781)

Fixes #3300.

This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.

9 files changed, 65 insertions, 10 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 024530224..88842faf7 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -420,6 +420,15 @@ header = "options/smt_options.h"
   help       = "in models, output uninterpreted sorts as datatype enumerations"
 
 [[option]]
+  name       = "modelWitnessChoice"
+  category   = "regular"
+  long       = "model-witness-choice"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "in models, use a witness constant for choice functions"
+
+[[option]]
   name       = "regularChannelName"
   smt_name   = "regular-output-channel"
   category   = "regular"
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 8a4145552..929eb4acc 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -1247,8 +1247,9 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const
   }
 }
 
-void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel,
-                                  std::map<Node, Node>& approximations)
+void NlModel::getModelValueRepair(
+    std::map<Node, Node>& arithModel,
+    std::map<Node, std::pair<Node, Node>>& approximations)
 {
   // Record the approximations we used. This code calls the
   // recordApproximation method of the model, which overrides the model
@@ -1266,8 +1267,17 @@ void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel,
     if (l != u)
     {
       Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v));
-      approximations[v] = pred;
       Trace("nl-model") << v << " approximated as " << pred << std::endl;
+      Node witness;
+      if (options::modelWitnessChoice())
+      {
+        // witness is the midpoint
+        witness = nm->mkNode(
+            MULT, nm->mkConst(Rational(1, 2)), nm->mkNode(PLUS, l, u));
+        witness = Rewriter::rewrite(witness);
+        Trace("nl-model") << v << " witness is " << witness << std::endl;
+      }
+      approximations[v] = std::pair<Node, Node>(pred, witness);
     }
     else
     {
diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h
index 66c5d89c1..354f6f71c 100644
--- a/src/theory/arith/nl_model.h
+++ b/src/theory/arith/nl_model.h
@@ -180,10 +180,12 @@ class NlModel
    * The mapping arithModel is updated by this method to map arithmetic terms v
    * to their (exact) value that was computed during checkModel; the mapping
    * approximations is updated to store approximate values in the form of a
-   * predicate over v.
+   * pair (P, w), where P is a predicate that describes the possible values of
+   * v and w is a witness point that satisfies this predicate.
    */
-  void getModelValueRepair(std::map<Node, Node>& arithModel,
-                           std::map<Node, Node>& approximations);
+  void getModelValueRepair(
+      std::map<Node, Node>& arithModel,
+      std::map<Node, std::pair<Node, Node>>& approximations);
 
  private:
   /** The current model */
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 6c04268db..acae404ba 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1304,9 +1304,16 @@ void NonlinearExtension::check(Theory::Effort e) {
     // Otherwise, we will answer SAT. The values that we approximated are
     // recorded as approximations here.
     TheoryModel* tm = d_containing.getValuation().getModel();
-    for (std::pair<const Node, Node>& a : d_approximations)
+    for (std::pair<const Node, std::pair<Node, Node>>& a : d_approximations)
     {
-      tm->recordApproximation(a.first, a.second);
+      if (a.second.second.isNull())
+      {
+        tm->recordApproximation(a.first, a.second.first);
+      }
+      else
+      {
+        tm->recordApproximation(a.first, a.second.first, a.second.second);
+      }
     }
   }
 }
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index ddca284a4..338ae6611 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -480,8 +480,11 @@ class NonlinearExtension {
    */
   std::vector<Node> d_cmiLemmas;
   std::vector<Node> d_cmiLemmasPp;
-  /** The approximations computed during collectModelInfo. */
-  std::map<Node, Node> d_approximations;
+  /**
+   * The approximations computed during collectModelInfo. For details, see
+   * NlModel::getModelValueRepair.
+   */
+  std::map<Node, std::pair<Node, Node>> d_approximations;
   /** have we successfully built the model in this SAT context? */
   context::CDO<bool> d_builtModel;
 
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index c6055ede9..399695131 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -598,6 +598,11 @@ void TheoryModel::recordApproximation(TNode n, TNode pred)
   // model cache is invalid
   d_modelCache.clear();
 }
+void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness)
+{
+  Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
+  recordApproximation(n, predDisj);
+}
 void TheoryModel::setUsingModelCore()
 {
   d_using_model_core = true;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 0914987cc..d2ce63ac5 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -215,6 +215,13 @@ public:
    * construction process.
    */
   void recordApproximation(TNode n, TNode pred);
+  /**
+   * Same as above, but with a witness constant. This ensures that the
+   * approximation predicate is of the form (or (= n witness) pred). This
+   * is useful if the user wants to know a possible concrete value in
+   * the range of the predicate.
+   */
+  void recordApproximation(TNode n, TNode pred, Node witness);
   /** set unevaluate/semi-evaluated kind
    *
    * This informs this model how it should interpret applications of terms with
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b909817df..6acc6f7c8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1306,6 +1306,7 @@ set(regress_1_tests
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
+  regress1/nl/issue3300-approx-sqrt-witness.smt2
   regress1/nl/issue3441.smt2
   regress1/nl/issue3617.smt2
   regress1/nl/issue3656.smt2
diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
new file mode 100644
index 000000000..9bc47f925
--- /dev/null
+++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -0,0 +1,11 @@
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (choice ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/'
+; COMMAND-LINE: --produce-models --model-witness-choice --no-check-models
+; EXPECT: sat
+; EXPECT: SUCCESS
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (= (* x x) 2))
+(check-sat)
+(get-value (x))
+