Fixes for witness terms appearing in CEGQI instantiations (#8350)

Fixes #8344.

We now have cases where witness terms e.g. `(witness x : String. len(x) = N)` appear in model values.  These terms require special care in CEGQI.

There are 2 fixes in this PR:
(1) we update our policy on what a legal term is,
(2) we erase annotations from witness terms appearing in instantiations, which is required for ensuring that proofs are consistent.  Otherwise, the skolemization lemma for a witness term does not introduce the same skolem.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 8db3ba4ed8c51a6cb4f754b17a9d31a42444ee93..22261a9f64eda7e4c2fc4bbc805ecfc2660169cd 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -15,6 +15,8 @@
 
 libcvc5_add_sources(
   algorithm/flatten.h
+  annotation_elim_node_converter.cpp
+  annotation_elim_node_converter.h
   array_store_all.cpp
   array_store_all.h
   ascription_type.cpp

diff --git a/src/expr/annotation_elim_node_converter.cpp b/src/expr/annotation_elim_node_converter.cpp
new file mode 100644 (file)
index 0000000..6386888
--- /dev/null
+++ b/src/expr/annotation_elim_node_converter.cpp
@@ -0,0 +1,33 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of annotation elimination node conversion
+ */
+
+#include "expr/annotation_elim_node_converter.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+
+AnnotationElimNodeConverter::AnnotationElimNodeConverter() {}
+
+Node AnnotationElimNodeConverter::postConvert(Node n)
+{
+  if (n.isClosure() && n.getNumChildren() == 3)
+  {
+    return NodeManager::currentNM()->mkNode(n.getKind(), n[0], n[1]);
+  }
+  return n;
+}
+
+}  // namespace cvc5

diff --git a/src/expr/annotation_elim_node_converter.h b/src/expr/annotation_elim_node_converter.h
new file mode 100644 (file)
index 0000000..094a2dc
--- /dev/null
+++ b/src/expr/annotation_elim_node_converter.h
@@ -0,0 +1,41 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of annotation elimination node conversion
+ */
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__EXPR__ANNOTATION_ELIM_NODE_CONVERTER_H
+#define CVC4__PROOF__EXPR__ANNOTATION_ELIM_NODE_CONVERTER_H
+
+#include "expr/node.h"
+#include "expr/node_converter.h"
+
+namespace cvc5 {
+
+/**
+ * This converts a node into one that does not involve annotations for
+ * quantified formulas. In other words, the third child is dropped for all
+ * closure terms with 3 children.
+ */
+class AnnotationElimNodeConverter : public NodeConverter
+{
+ public:
+  AnnotationElimNodeConverter();
+  ~AnnotationElimNodeConverter() {}
+  /** convert node n as described above during post-order traversal */
+  Node postConvert(Node n) override;
+};
+
+}  // namespace cvc5
+
+#endif

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 431bca6493d3aaf04f0e9252cb6dcbdf7bd2c616..6a86c315df0168208b93f7b31d81ec89e3b7315e 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 
+#include "expr/annotation_elim_node_converter.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
@@ -209,9 +210,11 @@ CegInstantiator::~CegInstantiator() {
 void CegInstantiator::computeProgVars( Node n ){
   if( d_prog_var.find( n )==d_prog_var.end() ){
     d_prog_var[n].clear();
-    if (n.getKind() == kind::WITNESS)
+    Kind k = n.getKind();
+    if (k == kind::WITNESS)
     {
       Assert(d_prog_var.find(n[0][0]) == d_prog_var.end());
+      // ignore the bound variable
       d_prog_var[n[0][0]].clear();
     }
     if (d_vars_set.find(n) != d_vars_set.end())
@@ -223,7 +226,14 @@ void CegInstantiator::computeProgVars( Node n ){
       d_inelig.insert(n);
       return;
     }
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    bool isClosure = n.isClosure();
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      if (isClosure && i != 1)
+      {
+        // ignore the bound variable list and annotation
+        continue;
+      }
       computeProgVars( n[i] );
       if( d_inelig.find( n[i] )!=d_inelig.end() ){
         d_inelig.insert(n);
@@ -232,12 +242,11 @@ void CegInstantiator::computeProgVars( Node n ){
       d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
     }
     // selectors applied to program variables are also variables
-    if (n.getKind() == APPLY_SELECTOR
-        && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
+    if (k == APPLY_SELECTOR && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
     {
       d_prog_var[n].insert(n);
     }
-    if (n.getKind() == kind::WITNESS)
+    if (k == kind::WITNESS)
     {
       d_prog_var.erase(n[0][0]);
     }
@@ -1455,7 +1464,12 @@ void CegInstantiator::processAssertions() {
 }
 
 Node CegInstantiator::getModelValue( Node n ) {
-  return d_treg.getModel()->getValue(n);
+  Node mv = d_treg.getModel()->getValue(n);
+  // Witness terms with identifiers may appear in the model. We require
+  // dropping their annotations here.
+  AnnotationElimNodeConverter aenc;
+  mv = aenc.convert(mv);
+  return mv;
 }
 
 Node CegInstantiator::getBoundVariable(TypeNode tn)

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index a74c06c11aa1f6cfb0cd4a95c11c68eeb37a9cc3..a0a453ba50c3b0763c7cfe1bb2d82bb818858814 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2204,6 +2204,7 @@ set(regress_1_tests
   regress1/quantifiers/issue7385-sygus-inst-i.smt2
   regress1/quantifiers/issue7537-cegqi-comp-types.smt2
   regress1/quantifiers/issue8157-duplicate-conflicts.smt2
+  regress1/quantifiers/issue8344-cegqi-string-witness.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2

diff --git a/test/regress/cli/regress1/quantifiers/issue8344-cegqi-string-witness.smt2 b/test/regress/cli/regress1/quantifiers/issue8344-cegqi-string-witness.smt2
new file mode 100644 (file)
index 0000000..38b5aba
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8344-cegqi-string-witness.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun a () String)
+(assert (forall ((b Int)) (or (> (str.len a) b) (= 0 (mod b 74998)))))
+(check-sat)