From f809439274390d754c158bc105f769df3a55ee42 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 25 Apr 2021 15:05:15 -0500 Subject: [PATCH] Use fast enumeration by default for Boolean predicate synthesis (#6440) This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals. This significantly improves run time on a challenge benchmark from @makaimann. --- .../quantifiers/sygus/term_database_sygus.cpp | 9 ++++---- src/theory/quantifiers/sygus/type_info.cpp | 22 ++++++++++++++----- src/theory/quantifiers/sygus/type_info.h | 10 +++++++++ 3 files changed, 31 insertions(+), 10 deletions(-) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 41b4c27f4..b18a7c796 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -507,17 +507,16 @@ void TermDbSygus::registerEnumerator(Node e, if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO) { // We use active generation if the grammar of the enumerator does not - // have ITE and is not Boolean. Experimentally, it is better to - // use passive generation for these cases since it enables useful - // search space pruning techniques, e.g. evaluation unfolding, + // have ITE and does not have Boolean connectives. Experimentally, it + // is better to use passive generation for these cases since it enables + // useful search space pruning techniques, e.g. evaluation unfolding, // conjecture-specific symmetry breaking. Also, if sygus-stream is // enabled, we always use active generation, since the use cases of // sygus stream are to find many solutions to an easy problem, where // the bottleneck often becomes the large number of "exclude the current // solution" clauses. - const DType& dt = et.getDType(); if (options::sygusStream() - || (!eti.hasIte() && !dt.getSygusType().isBoolean())) + || (!eti.hasIte() && !eti.hasBoolConnective())) { isActiveGen = true; } diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index c8a86e32a..f9aa5bdc3 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -31,6 +31,7 @@ namespace quantifiers { SygusTypeInfo::SygusTypeInfo() : d_hasIte(false), + d_hasBoolConnective(false), d_min_term_size(0), d_sym_cons_any_constant(-1), d_has_subterm_sym_cons(false) @@ -150,11 +151,6 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) { d_kinds[builtinKind] = i; d_arg_kind[i] = builtinKind; - if (builtinKind == ITE) - { - // mark that this type has an ITE - d_hasIte = true; - } } // symbolic constructors if (sop.getAttribute(SygusAnyConstAttribute())) @@ -179,6 +175,21 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) << "Sygus datatype " << dt.getName() << " encodes terms that are not of type " << btn << std::endl; Trace("sygus-db") << "...done register Operator #" << i << std::endl; + Kind gk = g.getKind(); + if (gk == ITE) + { + // mark that this type has an ITE + d_hasIte = true; + if (g.getType().isBoolean()) + { + d_hasBoolConnective = true; + } + } + else if (gk == AND || gk == OR || gk == IMPLIES || gk == XOR + || (gk == EQUAL && g[0].getType().isBoolean())) + { + d_hasBoolConnective = true; + } } // compute minimum type depth information computeMinTypeDepthInternal(tn, 0); @@ -375,6 +386,7 @@ int SygusTypeInfo::getOpConsNum(Node n) const bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; } bool SygusTypeInfo::hasIte() const { return d_hasIte; } +bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; } bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; } bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; } diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h index 7b22f826c..3c0fbf30e 100644 --- a/src/theory/quantifiers/sygus/type_info.h +++ b/src/theory/quantifiers/sygus/type_info.h @@ -81,6 +81,11 @@ class SygusTypeInfo * ITE, or is a lambda whose body is ITE. */ bool hasIte() const; + /** + * Returns true if this sygus type has a constructor whose sygus operator is + * a Boolean connective. + */ + bool hasBoolConnective() const; /** * Get the builtin kind for the i^th constructor of this sygus type. If the * i^th constructor does not encode an application of a builtin kind, this @@ -196,6 +201,11 @@ class SygusTypeInfo * or is a lambda whose body is ITE. */ bool d_hasIte; + /** + * Whether this sygus type has a constructor whose sygus operator is a + * Boolean connective. + */ + bool d_hasBoolConnective; /** * Maps constructor indices to the constant that they encode, if any. */ -- 2.30.2