From 6a3ead1cca025ad4d07976b10fc3c3eda2bf8220 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Jan 2022 13:05:55 -0600 Subject: [PATCH] Refactor options related to rewriting and symmetry breaking in sygus (#7949) Note this also corrects a few inconsistencies in how the rewriter is invoked in fast / variable agnostic enumeration. Notably, fast enumeration now leverages the term datatype sygus for rewriting, meaning it can evaluate recursive functions for enumerated terms. --- src/options/datatypes_options.toml | 54 +++++++++++-------- src/options/quantifiers_options.toml | 8 --- src/smt/set_defaults.cpp | 4 +- src/theory/datatypes/sygus_extension.cpp | 9 ++-- .../sygus/enum_stream_substitution.cpp | 10 ++-- .../quantifiers/sygus/enum_value_manager.cpp | 5 +- .../quantifiers/sygus/sygus_enumerator.cpp | 7 +-- .../sygus/sygus_enumerator_callback.cpp | 9 ++-- .../sygus/sygus_enumerator_callback.h | 9 +++- .../quantifiers/sygus/term_database_sygus.cpp | 5 +- test/regress/regress1/rr-verify/bool-crci.sy | 2 +- test/regress/regress1/rr-verify/bv-term-32.sy | 2 +- test/regress/regress1/rr-verify/bv-term.sy | 2 +- test/regress/regress1/rr-verify/fp-arith.sy | 2 +- test/regress/regress1/rr-verify/fp-bool.sy | 2 +- .../regress/regress1/rr-verify/string-term.sy | 2 +- .../regress1/sygus/issue4025-no-rlv-cond.smt2 | 2 +- 17 files changed, 77 insertions(+), 57 deletions(-) diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 60cdcc335..0bb0edba6 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -86,28 +86,40 @@ name = "Datatypes Theory" help = "internally use shared selectors across multiple constructors" [[option]] - name = "sygusSymBreak" + name = "sygusSimpleSymBreak" category = "regular" - long = "sygus-sym-break" - type = "bool" - default = "true" - help = "simple sygus symmetry breaking lemmas" - -[[option]] - name = "sygusSymBreakAgg" - category = "regular" - long = "sygus-sym-break-agg" - type = "bool" - default = "true" - help = "use aggressive checks for simple sygus symmetry breaking lemmas" - -[[option]] - name = "sygusSymBreakDynamic" - category = "regular" - long = "sygus-sym-break-dynamic" - type = "bool" - default = "true" - help = "dynamic sygus symmetry breaking lemmas" + long = "sygus-simple-sym-break=MODE" + type = "SygusSimpleSymBreakMode" + default = "AGG" + help = "if and how to apply simple symmetry breaking based on the grammar for smart enumeration" + help_mode = "Modes for applying simple symmetry breaking based on the grammar for smart enumeration." +[[option.mode.NONE]] + name = "none" + help = "Do not apply simple symmetry breaking." +[[option.mode.BASIC]] + name = "basic" + help = "Apply basic simple symmetry breaking." +[[option.mode.AGG]] + name = "agg" + help = "Apply aggressive simple symmetry breaking." + +[[option]] + name = "sygusRewriter" + category = "regular" + long = "sygus-rewriter=MODE" + type = "SygusRewriterMode" + default = "EXTENDED" + help = "if and how to apply rewriting for sygus symmetry breaking" + help_mode = "Modes for applying rewriting for sygus symmetry breaking." +[[option.mode.NONE]] + name = "none" + help = "Do not use the rewriter." +[[option.mode.BASIC]] + name = "basic" + help = "Use the basic rewriter." +[[option.mode.EXTENDED]] + name = "extended" + help = "Use the extended rewriter." [[option]] name = "sygusSymBreakPbe" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c284518c7..312fc606b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1260,14 +1260,6 @@ name = "Quantifiers" default = "false" help = "enumerate a stream of solutions instead of terminating after the first one" -[[option]] - name = "sygusExtRew" - category = "regular" - long = "sygus-ext-rew" - type = "bool" - default = "true" - help = "use extended rewriter for sygus" - [[option]] name = "cegisSample" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index fea9d4398..1fd2c3dc5 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1580,9 +1580,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const opts.quantifiers.sygusRewSynth = true; // we should not use the extended rewriter, since we are interested // in rewrites that are not in the main rewriter - if (!opts.quantifiers.sygusExtRewWasSetByUser) + if (!opts.datatypes.sygusRewriterWasSetByUser) { - opts.quantifiers.sygusExtRew = false; + opts.datatypes.sygusRewriter = options::SygusRewriterMode::BASIC; } } // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 0318f7da9..1134c0a5a 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -691,7 +691,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, // if we are the "any constant" constructor, we do no symmetry breaking // only do simple symmetry breaking up to depth 2 - bool doSymBreak = options().datatypes.sygusSymBreak; + bool doSymBreak = options().datatypes.sygusSimpleSymBreak + != options::SygusSimpleSymBreakMode::NONE; if (isAnyConstant || depth > 2) { doSymBreak = false; @@ -1047,7 +1048,7 @@ Node SygusExtension::registerSearchValue(Node a, << ", type=" << tn << std::endl; Node bv = d_tds->sygusToBuiltin(cnv, tn); Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; - Node bvr = extendedRewrite(bv); + Node bvr = d_tds->rewriteNode(bv); Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl; Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl; unsigned sz = utils::getSygusTermSize(nv); @@ -1624,7 +1625,9 @@ void SygusExtension::check() // register the search value ( prog -> progv ), this may invoke symmetry // breaking - if (!isExc && options().datatypes.sygusSymBreakDynamic) + if (!isExc + && options().datatypes.sygusRewriter + != options::SygusRewriterMode::NONE) { bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog); // check that it is unique up to theory-specific rewriting and diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 233d7f17b..a4b65ab30 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -125,7 +125,7 @@ Node EnumStreamPermutation::getNext() { d_first = false; Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType()); - d_perm_values.insert(extendedRewrite(bultin_value)); + d_perm_values.insert(d_tds->rewriteNode(bultin_value)); return d_value; } unsigned n_classes = d_perm_state_class.size(); @@ -192,9 +192,9 @@ Node EnumStreamPermutation::getNext() bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType()); Trace("synth-stream-concrete-debug") << " ......perm builtin is " << bultin_perm_value; - if (options().datatypes.sygusSymBreakDynamic) + if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE) { - bultin_perm_value = extendedRewrite(bultin_perm_value); + bultin_perm_value = d_tds->rewriteNode(bultin_perm_value); Trace("synth-stream-concrete-debug") << " and rewrites to " << bultin_perm_value; } @@ -512,9 +512,9 @@ Node EnumStreamSubstitution::getNext() // construction (unless it's equiv to a constant, e.g. true / false) Node builtin_comb_value = d_tds->sygusToBuiltin(comb_value, comb_value.getType()); - if (options().datatypes.sygusSymBreakDynamic) + if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE) { - builtin_comb_value = extendedRewrite(builtin_comb_value); + builtin_comb_value = d_tds->rewriteNode(builtin_comb_value); } if (Trace.isOn("synth-stream-concrete")) { diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index fcbe3d42e..d9078bfaf 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -100,7 +100,8 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) || options().quantifiers.sygusEnumMode == options::SygusEnumMode::AUTO); // create the enumerator callback - if (options().datatypes.sygusSymBreakDynamic) + if (options().datatypes.sygusRewriter + != options::SygusRewriterMode::NONE) { std::ostream* out = nullptr; if (options().quantifiers.sygusRewVerify) @@ -112,7 +113,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) out = options().base.out; } d_secd = std::make_unique( - d_env, e, &d_stats, d_eec.get(), d_samplerRrV.get(), out); + d_env, e, d_tds, &d_stats, d_eec.get(), d_samplerRrV.get(), out); } // if sygus repair const is enabled, we enumerate terms with free // variables as arguments to any-constant constructors diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 52c1ef4a0..ba4496a7b 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -55,10 +55,11 @@ void SygusEnumerator::initialize(Node e) Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl; d_enum = e; // allocate the default callback - if (d_sec == nullptr && options().datatypes.sygusSymBreakDynamic) + if (d_sec == nullptr + && options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE) { - d_secd = - std::make_unique(d_env, e, d_stats); + d_secd = std::make_unique( + d_env, e, d_tds, d_stats); d_sec = d_secd.get(); } d_etype = d_enum.getType(); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp index bde1fdd67..d16b6d33e 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp @@ -18,6 +18,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/example_eval_cache.h" #include "theory/quantifiers/sygus/sygus_stats.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/rewriter.h" @@ -27,8 +28,9 @@ namespace quantifiers { SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env, Node e, + TermDbSygus* tds, SygusStatistics* s) - : EnvObj(env), d_enum(e), d_stats(s) + : EnvObj(env), d_enum(e), d_tds(tds), d_stats(s) { d_tn = e.getType(); } @@ -36,7 +38,7 @@ SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env, bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set& bterms) { Node bn = datatypes::utils::sygusToBuiltin(n); - Node bnr = extendedRewrite(bn); + Node bnr = d_tds == nullptr ? extendedRewrite(bn) : d_tds->rewriteNode(bn); if (d_stats != nullptr) { ++(d_stats->d_enumTermsRewrite); @@ -66,11 +68,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set& bterms) SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault( Env& env, Node e, + TermDbSygus* tds, SygusStatistics* s, ExampleEvalCache* eec, SygusSampler* ssrv, std::ostream* out) - : SygusEnumeratorCallback(env, e, s), + : SygusEnumeratorCallback(env, e, tds, s), d_eec(eec), d_samplerRrV(ssrv), d_out(out) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h index 9b7c3fd98..a83e1b071 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h @@ -31,6 +31,7 @@ namespace quantifiers { class ExampleEvalCache; class SygusStatistics; class SygusSampler; +class TermDbSygus; /** * Base class for callbacks in the fast enumerator. This allows a user to @@ -40,7 +41,10 @@ class SygusSampler; class SygusEnumeratorCallback : protected EnvObj { public: - SygusEnumeratorCallback(Env& env, Node e, SygusStatistics* s = nullptr); + SygusEnumeratorCallback(Env& env, + Node e, + TermDbSygus* tds = nullptr, + SygusStatistics* s = nullptr); virtual ~SygusEnumeratorCallback() {} /** * Add term, return true if the term should be considered in the enumeration. @@ -75,6 +79,8 @@ class SygusEnumeratorCallback : protected EnvObj Node d_enum; /** The type of enum */ TypeNode d_tn; + /** Term database sygus */ + TermDbSygus* d_tds; /** pointer to the statistics */ SygusStatistics* d_stats; }; @@ -84,6 +90,7 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback public: SygusEnumeratorCallbackDefault(Env& env, Node e, + TermDbSygus* tds = nullptr, SygusStatistics* s = nullptr, ExampleEvalCache* eec = nullptr, SygusSampler* ssrv = nullptr, diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 60170ceb4..622aa2a6a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -739,7 +739,7 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { Node res; - if (options().quantifiers.sygusExtRew) + if (options().datatypes.sygusRewriter == options::SygusRewriterMode::EXTENDED) { res = extendedRewrite(n); } @@ -855,7 +855,8 @@ bool TermDbSygus::canConstructKind(TypeNode tn, } return true; } - if (!options().datatypes.sygusSymBreakAgg) + if (options().datatypes.sygusSimpleSymBreak + != options::SygusSimpleSymBreakMode::AGG) { return false; } diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy index 75837695d..614a83f2b 100644 --- a/test/regress/regress1/rr-verify/bool-crci.sy +++ b/test/regress/regress1/rr-verify/bool-crci.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --sygus-simple-sym-break=none ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy index 9dfb19451..95296463b 100644 --- a/test/regress/regress1/rr-verify/bv-term-32.sy +++ b/test/regress/regress1/rr-verify/bv-term-32.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy index 9a11128d7..af954cbb1 100644 --- a/test/regress/regress1/rr-verify/bv-term.sy +++ b/test/regress/regress1/rr-verify/bv-term.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-simple-sym-break=none ; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)' diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index 2970fd0de..ad8635ca8 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index e4b3a0fac..33caed2e9 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)' ; EXIT: 1 diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy index 404719f6c..815cb70a5 100644 --- a/test/regress/regress1/rr-verify/string-term.sy +++ b/test/regress/regress1/rr-verify/string-term.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 index a7c864544..cc0c329cd 100644 --- a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 +++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 @@ -1,6 +1,6 @@ (set-logic ALL) (set-option :sygus-inference true) -(set-option :sygus-sym-break false) +(set-option :sygus-simple-sym-break none) (set-option :sygus-sym-break-lazy false) (set-option :sygus-sym-break-rlv false) (set-info :status sat) -- 2.30.2