Implement evaluation of semi-evaluated kinds in model (cvc5#11093)

This revises how APPLY_SELECTOR terms are evaluated in models.

Previously, APPLY_SELECTOR was marked "unevaluated" and hence a term `(s
x)` would only evaluate if `(s x)` could be rewritten or if `(s x)`
appeared syntactically in the model.

This updates `TheoryModel` so that APPLY_SELECTOR is marked
"semi-evaluated". It adds a further method to check whether the
evaluation of such a term is entailed by congruence, or else can be
assigned arbitrarily.

A similar change is made for `SEQ_NTH`, which had similar issues.

Fixes cvc5#10770.

src/theory/datatypes/theory_datatypes.cpp

@@ -123,7 +123,7 @@ void TheoryDatatypes::finishInit()
   d_valuation.setIrrelevantKind(Kind::APPLY_TESTER);
   d_valuation.setIrrelevantKind(Kind::DT_SYGUS_BOUND);
   // selectors don't always evaluate
-  d_valuation.setUnevaluatedKind(Kind::APPLY_SELECTOR);
+  d_valuation.setSemiEvaluatedKind(Kind::APPLY_SELECTOR);
 }
 
 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){

src/theory/strings/theory_strings.cpp

@@ -176,7 +176,7 @@ void TheoryStrings::finishInit()
   d_valuation.setIrrelevantKind(Kind::STRING_IN_REGEXP);
   d_valuation.setIrrelevantKind(Kind::STRING_LEQ);
   // seq nth doesn't always evaluate
-  d_valuation.setUnevaluatedKind(Kind::SEQ_NTH);
+  d_valuation.setSemiEvaluatedKind(Kind::SEQ_NTH);
 }
 
 std::string TheoryStrings::identify() const

src/theory/theory_model.cpp

@@ -77,6 +77,8 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
 
 void TheoryModel::reset(){
   d_modelCache.clear();
+  d_semiEvalCacheSet = false;
+  d_semiEvalCache.clear();
   d_sep_heap = Node::null();
   d_sep_nil_eq = Node::null();
   d_reps.clear();
@@ -245,7 +247,7 @@ Node TheoryModel::getModelValue(TNode n) const
           << "  " << n << "[" << i << "] is " << ret << std::endl;
       children.push_back(ret);
     }
-    ret = nm->mkNode(n.getKind(), children);
+    ret = nm->mkNode(nk, children);
     Trace("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
     ret = rewrite(ret);
     Trace("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
@@ -273,7 +275,7 @@ Node TheoryModel::getModelValue(TNode n) const
     // Note that we discard the evaluation of the arguments here
     Trace("model-getvalue-debug") << "Failed to evaluate " << ret << std::endl;
   }
-  // must rewrite the term at this point
+  // We revert to the original rewritten form of n here.
   ret = rewrite(n);
   Trace("model-getvalue-debug")
       << "Look up " << ret << " in equality engine" << std::endl;
@@ -304,10 +306,32 @@ Node TheoryModel::getModelValue(TNode n) const
     }
   }
 
-  // if we are a evaluated or semi-evaluated kind, return an arbitrary value
-  // if we are not in the d_unevaluated_kinds map, we are evaluated
-  if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end())
+  Kind rk = ret.getKind();
+  // If we are a ground term that is *not* unevaluated, we assign an arbitrary
+  // value.
+  if (d_unevaluated_kinds.find(rk) == d_unevaluated_kinds.end()
+      && !expr::hasBoundVar(ret))
   {
+    // If we are a semi-evaluated kind, then we need to check whether we are
+    // entailed equal to an existing term. For example, if we are a datatype
+    // selector S(x), x is equal to y, and S(y) is a term in the equality
+    // engine of this model, then the value of S(x) must be equal to the value
+    // of S(y).
+    if (d_semi_evaluated_kinds.find(rk) != d_semi_evaluated_kinds.end())
+    {
+      Node retSev = evaluateSemiEvalTerm(ret);
+      // if the result was entailed, return it
+      if (!retSev.isNull())
+      {
+        d_modelCache[n] = retSev;
+        Trace("model-getvalue-debug")
+            << "...semi-evaluated entailed is " << retSev << std::endl;
+        return retSev;
+      }
+      // otherwise we return an arbtirary value below.
+      Trace("model-getvalue-debug")
+          << "...not semi-evaluated entailed" << std::endl;
+    }
     if (t.isFunction() || t.isPredicate())
     {
       if (d_enableFuncModels)
@@ -849,6 +873,60 @@ bool TheoryModel::isAssignableUf(const Node& n) const
   return n.getKind() != Kind::LAMBDA;
 }
 
+Node TheoryModel::evaluateSemiEvalTerm(TNode n) const
+{
+  Assert(d_semi_evaluated_kinds.find(n.getKind())
+         != d_semi_evaluated_kinds.end());
+  if (!d_semiEvalCacheSet)
+  {
+    d_semiEvalCacheSet = true;
+    // traverse
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
+    for (; !eqcs_i.isFinished(); ++eqcs_i)
+    {
+      Node eqc = (*eqcs_i);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
+      for (; !eqc_i.isFinished(); ++eqc_i)
+      {
+        Node t = (*eqc_i);
+        Kind k = t.getKind();
+        if (d_semi_evaluated_kinds.find(k) == d_semi_evaluated_kinds.end())
+        {
+          continue;
+        }
+        Node eqcv = getModelValue(eqc);
+        Assert(t.hasOperator());
+        Node op = t.getOperator();
+        std::vector<Node> targs = getModelValueArgs(t);
+        NodeTrie& nt = d_semiEvalCache[op];
+        nt.addOrGetTerm(eqcv, targs);
+        Trace("semi-eval") << "Semi-eval: SET " << targs << " = " << eqcv
+                           << std::endl;
+      }
+    }
+  }
+  Trace("semi-eval") << "Semi-eval: EVALUATE " << n << "..." << std::endl;
+  Node op = n.getOperator();
+  std::unordered_map<Node, NodeTrie>::iterator it = d_semiEvalCache.find(op);
+  if (it != d_semiEvalCache.end())
+  {
+    std::vector<Node> nargs = getModelValueArgs(n);
+    Trace("semi-eval") << "Semi-eval: lookup " << nargs << std::endl;
+    return it->second.existsTerm(nargs);
+  }
+  return Node::null();
+}
+
+std::vector<Node> TheoryModel::getModelValueArgs(TNode n) const
+{
+  std::vector<Node> args;
+  for (const Node& nc : n)
+  {
+    args.emplace_back(getModelValue(nc));
+  }
+  return args;
+}
+
 bool TheoryModel::isValue(TNode n) const
 {
   IsModelValueAttr imva;

src/theory/theory_model.h

@@ -21,6 +21,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "expr/node_trie.h"
 #include "smt/env_obj.h"
 #include "theory/ee_setup_info.h"
 #include "theory/rep_set.h"
@@ -208,11 +209,11 @@ class TheoryModel : protected EnvObj
    * itself.
    *
    * [3] "Semi-evaluated"
-   * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
-   * those that correspond to abstractions. Like unevaluated kinds, these
-   * kinds do not have an evaluator. In contrast to unevaluated kinds, we
-   * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
-   * arbitrary value instead of the term itself.
+   * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV, APPLY_SELECTOR and.
+   * SEQ_NTH. Like unevaluated kinds, these kinds do not have an evaluator for
+   * (some) inputs. In contrast to unevaluated kinds, we interpret a term
+   * <k>( t1...tn ) not appearing in the equality engine as an arbitrary value
+   * instead of the term itself.
    *
    * [4] APPLY_UF, where getting the model value depends on an internally
    * constructed representation of a lambda model value (d_uf_models).
@@ -404,10 +405,27 @@ class TheoryModel : protected EnvObj
   bool isBaseModelValue(TNode n) const;
   /** Is assignable function. This returns true if n is not a lambda. */
   bool isAssignableUf(const Node& n) const;
+  /**
+   * Evaluate semi-evaluated term. This determines if there is a term n' that is
+   * in the equality engine of this model that is congruent to n, if so, it
+   * returns the model value of n', otherwise this returns the null term.
+   * @param n The term to evaluate. We assume it is in rewritten form and
+   * has a semi-evaluated kind (e.g. APPLY_SELECTOR).
+   * @return The entailed model value for n, if it exists.
+   */
+  Node evaluateSemiEvalTerm(TNode n) const;
+  /**
+   * @return The model values of the arguments of n.
+   */
+  std::vector<Node> getModelValueArgs(TNode n) const;
 
  private:
   /** cache for getModelValue */
   mutable std::unordered_map<Node, Node> d_modelCache;
+  /** whether we have computed d_semiEvalCache yet */
+  mutable bool d_semiEvalCacheSet;
+  /** cache used for evaluateSemiEvalTerm */
+  mutable std::unordered_map<Node, NodeTrie> d_semiEvalCache;
 
   //---------------------------- separation logic
   /** the value of the heap */

test/regress/cli/CMakeLists.txt

@@ -706,6 +706,7 @@ set(regress_0_tests
   regress0/datatypes/list-bool.smt2
   regress0/datatypes/list-update.smt2
   regress0/datatypes/list-update-sat.smt2
+  regress0/datatypes/model-semi-eval.smt2
   regress0/datatypes/model-subterms-min.smt2
   regress0/datatypes/mutual-rec-param-dt.smt2
   regress0/datatypes/mutually-recursive.cvc.smt2
@@ -1417,6 +1418,7 @@ set(regress_0_tests
   regress0/quantifiers/clock-10.smt2
   regress0/quantifiers/clock-3.smt2
   regress0/quantifiers/cond-var-elim-binary.smt2
+  regress0/quantifiers/dd_german169_semi_eval.smt2
   regress0/quantifiers/dd.german169-ieval.smt2
   regress0/quantifiers/dd.german169-lemma-inp.smt2
   regress0/quantifiers/dd.ho-matching-enum.smt2
@@ -1603,6 +1605,7 @@ set(regress_0_tests
   regress0/seq/issue9696-unit-type-cmi.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/mixed-types-seq-nth.smt2
+  regress0/seq/nth-model-semi-eval.smt2
   regress0/seq/nth-oob.smt2
   regress0/seq/nth-unit.smt2
   regress0/seq/nth-update.smt2

test/regress/cli/regress0/datatypes/model-semi-eval.smt2

@@ -0,0 +1,13 @@
+; COMMAND-LINE: --produce-models
+; EXPECT: sat
+; EXPECT: (((head (node (- x 1))) 4))
+(set-logic ALL)
+(declare-datatype list ((node (data Int)) (cons (head Int) (tail list))))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (> y 100))
+(assert (= (head (node y)) 4))
+(assert (<= y x (+ y 1)))
+(assert (not (= x y)))
+(check-sat)
+(get-value ((head (node (- x 1)))))

test/regress/cli/regress0/quantifiers/dd_german169_semi_eval.smt2

@@ -0,0 +1,10 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-datatypes ((B 0)) (((T) (F))))
+(declare-sort U 0)
+(declare-datatypes ((s 0)) (((i) (t))))
+(declare-datatypes ((m 0)) (((d (m s)))))
+(declare-fun c () (Array U m))
+(assert (not (= T (ite (or (forall ((n U)) (not (= t (m (select c n)))))) T F))))
+(check-sat)

test/regress/cli/regress0/seq/nth-model-semi-eval.smt2

@@ -0,0 +1,14 @@
+; COMMAND-LINE: --produce-models
+; EXPECT: sat
+; EXPECT: (((seq.nth (seq.unit (- x 1)) z) 4))
+(set-logic ALL)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (> y 100))
+(assert (= (seq.nth (seq.unit y) 10) 4))
+(assert (<= y x (+ y 1)))
+(assert (not (= x y)))
+(assert (< 9 z 11))
+(check-sat)
+(get-value ((seq.nth (seq.unit (- x 1)) z)))