From: Andrew Reynolds Date: Tue, 22 Mar 2022 07:43:30 +0000 (-0500) Subject: Fixes for witness terms appearing in CEGQI instantiations (#8350) X-Git-Tag: cvc5-1.0.0~213 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=23c0a0b79688cf86f16029aa0ef19864c63d7c85;p=cvc5.git 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 8db3ba4ed..22261a9f6 100644 --- 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 index 000000000..6386888d4 --- /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 index 000000000..094a2dc84 --- /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 431bca649..6a86c315d 100644 --- 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; igetValue(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 a74c06c11..a0a453ba5 100644 --- 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 index 000000000..38b5abaaa --- /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)