From c7c5e4a17b7c18804c0ebe82ef39bb34c60da92d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Feb 2022 15:03:30 -0600
Subject: [PATCH] Track names for witness terms in model (#8184)

This ensures that enough information is set to allow users to understand models with witness terms.

For example, for input:

(set-logic ALL)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (= (str.len x) 999999999999999999999999))
(assert (= (str.len y) 999999999999999999999999))
(assert (= z (str.++ x y)))
(check-sat)
we now get:

sat
(
(define-fun x () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ))
(define-fun y () String (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) ))
(define-fun z () String (str.++ (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w1) ) (witness ((s String)) (! (= (str.len s) 999999999999999999999999) :qid w0) )))
)
---
 src/parser/smt2/Smt2.g                        |  4 ++-
 src/printer/smt2/smt2_printer.cpp             | 25 +++++++++++++++++--
 src/theory/builtin/kinds                      |  2 +-
 .../builtin/theory_builtin_type_rules.h       | 10 ++++++++
 .../quantifiers/quantifiers_attributes.cpp    | 22 +++++++++++++---
 .../quantifiers/quantifiers_attributes.h      |  6 +++++
 src/theory/strings/theory_strings.cpp         |  7 ++++--
 src/theory/strings/theory_strings.h           |  5 ++++
 src/theory/strings/theory_strings_utils.cpp   |  8 ++++--
 src/theory/strings/theory_strings_utils.h     |  2 +-
 test/regress/CMakeLists.txt                   |  1 +
 .../regress0/strings/distinct-witness-id.smt2 | 11 ++++++++
 12 files changed, 90 insertions(+), 13 deletions(-)
 create mode 100644 test/regress/regress0/strings/distinct-witness-id.smt2

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fafda041a..e19a78c84 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1802,7 +1802,9 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
   | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
     {
       api::Term keyword = SOLVER->mkString("qid");
-      api::Term name = SOLVER->mkString(s);
+      // must create a variable whose name is the name of the quantified
+      // formula, not a string.
+      api::Term name = SOLVER->mkConst(SOLVER->getBooleanSort(), s);
       retExpr = MK_TERM(api::INST_ATTRIBUTE, keyword, name);
     }
   | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 05252b291..f3078a450 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -858,20 +858,41 @@ void Smt2Printer::toStream(std::ostream& out,
       annot << " ";
       for (const Node& nc : n[2])
       {
-        if (nc.getKind() == kind::INST_PATTERN)
+        Kind nck = nc.getKind();
+        if (nck == kind::INST_PATTERN)
         {
           out << "(! ";
           annot << ":pattern ";
           toStream(annot, nc, toDepth, nullptr);
           annot << ") ";
         }
-        else if (nc.getKind() == kind::INST_NO_PATTERN)
+        else if (nck == kind::INST_NO_PATTERN)
         {
           out << "(! ";
           annot << ":no-pattern ";
           toStream(annot, nc[0], toDepth, nullptr);
           annot << ") ";
         }
+        else if (nck == kind::INST_ATTRIBUTE)
+        {
+          // notice that INST_ATTRIBUTES either have an "internal" form,
+          // where the argument is a variable with an internal attribute set
+          // on it, or an "external" form where it is of the form
+          // (INST_ATTRIBUTE "keyword" [nodeValues]). We print the latter
+          // here only.
+          if (nc[0].getKind() == kind::CONST_STRING)
+          {
+            out << "(! ";
+            // print out as string to avoid quotes
+            annot << ":" << nc[0].getConst<String>().toString();
+            for (size_t j = 1, nchild = nc.getNumChildren(); j < nchild; j++)
+            {
+              annot << " ";
+              toStream(annot, nc[j], toDepth, nullptr);
+            }
+            annot << ") ";
+          }
+        }
       }
     }
     // Use a fresh let binder, since using existing let symbols may violate
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index eb184174e..9f1b4fb57 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -292,7 +292,7 @@ variable BOUND_VARIABLE "a bound variable (permitted in bindings and the associa
 variable SKOLEM "a Skolem variable (internal only)"
 operator SEXPR 0: "a symbolic expression (any arity)"
 
-operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
+operator WITNESS 2:3 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
 
 constant TYPE_CONSTANT \
     skip \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index d31733840..12e6b05a1 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -125,6 +125,16 @@ class WitnessTypeRule
         ss << "expected a body of a WITNESS expression to have Boolean type";
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
+      if (n.getNumChildren() == 3)
+      {
+        if (n[2].getType(check) != nodeManager->instPatternListType())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n,
+              "third argument of witness is not instantiation "
+              "pattern list");
+        }
+      }
     }
     // The type of a witness function is the type of its bound variable.
     return n[0][0].getType();
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index bb9568c88..e6b4d49b1 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/quantifiers_attributes.h"
 
+#include "expr/node_manager_attributes.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
@@ -269,13 +271,13 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           // only set the name if there is a value
           if (q[2][i].getNumChildren() > 1)
           {
-            Trace("quant-attr") << "Attribute : quantifier name : "
-                                << q[2][i][1].getConst<String>().toString()
+            std::string name;
+            q[2][i][1].getAttribute(expr::VarNameAttr(), name);
+            Trace("quant-attr") << "Attribute : quantifier name : " << name
                                 << " for " << q << std::endl;
             // assign the name to a variable with the given name (to avoid
             // enclosing the name in quotes)
-            qa.d_name = nm->mkBoundVar(q[2][i][1].getConst<String>().toString(),
-                                       nm->booleanType());
+            qa.d_name = nm->mkBoundVar(name, nm->booleanType());
           }
           else
           {
@@ -443,6 +445,18 @@ void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
   }
 }
 
+Node mkNamedQuant(Kind k, Node bvl, Node body, const std::string& name)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  Node v = sm->mkDummySkolem(
+      name, nm->booleanType(), "", SkolemManager::SKOLEM_EXACT_NAME);
+  Node attr = nm->mkConst(String("qid"));
+  Node ip = nm->mkNode(INST_ATTRIBUTE, attr, v);
+  Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
+  return nm->mkNode(k, bvl, body, ipl);
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 53f59b0e5..24d02e960 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -227,6 +227,12 @@ class QuantAttributes
   std::map< Node, bool > d_fun_defs;
 };
 
+/**
+ * Make a named quantified formula. This is a quantified formula that will
+ * print like:
+ *   (<k> <bvl> (! <body> :qid name))
+ */
+Node mkNamedQuant(Kind k, Node bvl, Node body, const std::string& name);
 }
 }
 }  // namespace cvc5
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b14621f07..1f9d8caa5 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -84,7 +84,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
           env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
       d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
       d_stringsFmf(env, valuation, d_termReg),
-      d_strat(d_env)
+      d_strat(d_env),
+      d_absModelCounter(0)
 {
   d_termReg.finishInit(&d_im);
 
@@ -408,7 +409,9 @@ bool TheoryStrings::collectModelInfoType(
         Assert(!lenValue.isNull() && lenValue.isConst());
         // make the abstract value (witness ((x String)) (= (str.len x)
         // lenValue))
-        Node w = utils::mkAbstractStringValueForLength(eqc, lenValue);
+        Node w = utils::mkAbstractStringValueForLength(
+            eqc, lenValue, d_absModelCounter);
+        d_absModelCounter++;
         Trace("strings-model")
             << "-> length out of bounds, assign abstract " << w << std::endl;
         if (!m->assertEquality(eqc, w, true))
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6337e164b..9d15af896 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -317,6 +317,11 @@ class TheoryStrings : public Theory {
   StringsFmf d_stringsFmf;
   /** The representation of the strategy */
   Strategy d_strat;
+  /**
+   * For model building, a counter on the number of abstract witness terms
+   * we have built, so that unique debug names can be assigned.
+   */
+  size_t d_absModelCounter;
 };/* class TheoryStrings */
 
 }  // namespace strings
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 9404298c4..3c6562aae 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -22,6 +22,7 @@
 #include "expr/skolem_manager.h"
 #include "options/strings_options.h"
 #include "theory/quantifiers/fmf/bounded_integers.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/strings_entail.h"
@@ -419,7 +420,7 @@ struct StringValueForLengthVarAttributeId
 typedef expr::Attribute<StringValueForLengthVarAttributeId, Node>
     StringValueForLengthVarAttribute;
 
-Node mkAbstractStringValueForLength(Node n, Node len)
+Node mkAbstractStringValueForLength(Node n, Node len, size_t id)
 {
   NodeManager* nm = NodeManager::currentNM();
   BoundVarManager* bvm = nm->getBoundVarManager();
@@ -428,7 +429,10 @@ Node mkAbstractStringValueForLength(Node n, Node len)
       cacheVal, "s", n.getType());
   Node pred = nm->mkNode(STRING_LENGTH, v).eqNode(len);
   // return (witness ((v String)) (= (str.len v) len))
-  return nm->mkNode(WITNESS, nm->mkNode(BOUND_VAR_LIST, v), pred);
+  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+  std::stringstream ss;
+  ss << "w" << id;
+  return quantifiers::mkNamedQuant(WITNESS, bvl, pred, ss.str());
 }
 
 }  // namespace utils
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 6aff3742a..59b58709a 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -209,7 +209,7 @@ Node mkForallInternal(Node bvl, Node body);
  * This is used for constructing models for strings whose lengths are too large
  * to represent in memory.
  */
-Node mkAbstractStringValueForLength(Node n, Node len);
+Node mkAbstractStringValueForLength(Node n, Node len, size_t id);
 
 }  // namespace utils
 }  // namespace strings
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 083edd4ec..393e191da 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1278,6 +1278,7 @@ set(regress_0_tests
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/complement-simple.smt2
   regress0/strings/delta-trust-subs.smt2
+  regress0/strings/distinct-witness-id.smt2
   regress0/strings/escchar_25.smt2
   regress0/strings/escchar.smt2
   regress0/strings/from_code.smt2
diff --git a/test/regress/regress0/strings/distinct-witness-id.smt2 b/test/regress/regress0/strings/distinct-witness-id.smt2
new file mode 100644
index 000000000..d306aface
--- /dev/null
+++ b/test/regress/regress0/strings/distinct-witness-id.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(assert (= (str.len x) 999999999999999999999999))
+(assert (= (str.len y) 999999999999999999999999))
+(assert (= z (str.++ x y)))
+(check-sat)
-- 
2.30.2