From 628a13f0e5f95fb3372c0676e91a9e719fa05b8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 15:47:06 -0500 Subject: [PATCH] Make SyGuS solver robust to non-closed enumerable sorts (#7417) This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts. It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method. It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding. This addresses several of the issues raised in #6605. --- .../arrays/theory_arrays_type_rules.cpp | 20 ++++++++++++- src/theory/quantifiers/sygus/cegis.cpp | 28 +++++++++++++------ src/theory/quantifiers/sygus/cegis.h | 7 +++++ .../quantifiers/sygus/sygus_grammar_cons.cpp | 3 ++ test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/array-uc.sy | 14 ++++++++++ 6 files changed, 64 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress1/sygus/array-uc.sy diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index e1b4813ec..433768e5d 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -18,6 +18,7 @@ // for array-constant attributes #include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/builtin/theory_builtin_type_rules.h" #include "theory/type_enumerator.h" #include "util/cardinality.h" @@ -249,7 +250,24 @@ bool ArraysProperties::isWellFounded(TypeNode type) Node ArraysProperties::mkGroundTerm(TypeNode type) { - return *TypeEnumerator(type); + Assert(type.getKind() == kind::ARRAY_TYPE); + TypeNode elemType = type.getArrayConstituentType(); + Node elem = elemType.mkGroundTerm(); + if (elem.isConst()) + { + return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem)); + } + // Note the distinction between mkGroundTerm and mkGroundValue. While + // an arbitrary value can be obtained by calling the type enumerator here, + // that is wrong for types that are not closed enumerable since it may + // return a term containing values that should not appear in e.g. assertions. + // For example, arrays whose element type is an uninterpreted sort will + // incorrectly introduce uninterpreted sort values if this is done. + // It is currently infeasible to construct an ArrayStoreAll with the element + // type's mkGroundTerm as an argument when that term is not constant. + // Thus, we must simply return a fresh Skolem here, using the same utility + // as that of uninterpreted sorts. + return builtin::SortProperties::mkGroundTerm(type); } TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager, diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c8e14e4bd..fdc0b28e0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,6 +39,7 @@ Cegis::Cegis(Env& env, SynthConjecture* p) : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), + d_cexClosedEnum(false), d_cegis_sampler(env), d_usingSymCons(false) { @@ -47,11 +48,18 @@ Cegis::Cegis(Env& env, bool Cegis::initialize(Node conj, Node n, const std::vector& candidates) { d_base_body = n; + d_cexClosedEnum = true; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) { for (const Node& v : d_base_body[0][0]) { d_base_vars.push_back(v); + if (!v.getType().isClosedEnumerable()) + { + // not closed enumerable, refinement lemmas cannot be sent to the + // quantifier-free datatype solver + d_cexClosedEnum = false; + } } d_base_body = d_base_body[0][1]; } @@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, void Cegis::registerRefinementLemma(const std::vector& vars, Node lem) { addRefinementLemma(lem); - // Make the refinement lemma and add it to lems. - // This lemma is guarded by the parent's guard, which has the semantics - // "this conjecture has a solution", hence this lemma states: - // if the parent conjecture has a solution, it satisfies the specification - // for the given concrete point. - Node rlem = - NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); - d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + // must be closed enumerable + if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + { + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = NodeManager::currentNM()->mkNode( + OR, d_parent->getGuard().negate(), lem); + d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + } } bool Cegis::usingRepairConst() { return true; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 8e0fffdd1..8d1f0a1b2 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -119,6 +119,13 @@ class Cegis : public SygusModule std::vector d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set d_refinement_lemma_vars; + /** + * Are the counterexamples we are handling in this class of only closed + * enumerable types (see TypeNode::isClosedEnumerable). If this is false, + * then CEGIS refinement lemmas can contain terms that are unhandled by + * theory solvers, e.g. uninterpreted constants. + */ + bool d_cexClosedEnum; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43c958ff9..9b4cfb9e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "expr/ascription_type.h" #include "expr/dtype_cons.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); + // note that c should never contain an uninterpreted constant + Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); } else if (type.isRoundingMode()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6dafe6852..0f7b19e47 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2314,6 +2314,7 @@ set(regress_1_tests regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array-uc.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/cegar1.sy regress1/sygus/cegis-unif-inv-eq-fair.sy diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) -- 2.30.2