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.

4 files changed, 32 insertions, 10 deletions

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;