From e037509aa86cf68691d9ef9eac3cac771fb26d03 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 14 Jan 2022 17:59:58 -0600 Subject: [PATCH] Improve names for sygus enumeration option (#7945) Also deletes the unused (naive) basic enumerator. --- src/CMakeLists.txt | 2 - src/options/quantifiers_options.toml | 39 +++++----- .../quantifiers/sygus/enum_value_manager.cpp | 18 ++--- .../quantifiers/sygus/sygus_enumerator.cpp | 2 +- .../sygus/sygus_enumerator_basic.cpp | 62 ---------------- .../sygus/sygus_enumerator_basic.h | 71 ------------------- .../sygus/sygus_random_enumerator.cpp | 2 +- .../quantifiers/sygus/term_database_sygus.cpp | 10 ++- .../regress1/sygus/commutative-stream.sy | 2 +- test/regress/regress1/sygus/error1-dt.sy | 2 +- .../regress1/sygus/fast-enum-backtrack.sy | 2 +- .../regress1/sygus/interpol1-push-pop.smt2 | 2 +- test/regress/regress1/sygus/interpol1.smt2 | 2 +- .../regress/regress1/sygus/interpol_arr1.smt2 | 2 +- .../regress/regress1/sygus/interpol_arr2.smt2 | 2 +- .../regress1/sygus/interpol_cosa_1.smt2 | 4 +- .../regress1/sygus/interpol_from_pono_1.smt2 | 2 +- .../regress1/sygus/interpol_from_pono_2.smt2 | 2 +- test/regress/regress1/sygus/issue3580.sy | 2 +- test/regress/regress1/sygus/rand_const.sy | 2 +- test/regress/regress1/sygus/rand_p_0.sy | 4 +- test/regress/regress1/sygus/rand_p_1.sy | 4 +- test/regress/regress1/sygus/trivial-stream.sy | 2 +- test/regress/regress2/sygus/multi-udiv.sy | 2 +- test/regress/regress2/sygus/sets-fun-test.sy | 2 +- test/regress/regress2/sygus/three.sy | 2 +- test/regress/regress3/interpol2.smt2 | 2 +- test/regress/regress3/strings-any-term.sy | 2 +- 28 files changed, 52 insertions(+), 200 deletions(-) delete mode 100644 src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp delete mode 100644 src/theory/quantifiers/sygus/sygus_enumerator_basic.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b17f82ac6..49ea3a500 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -896,8 +896,6 @@ libcvc5_add_sources( theory/quantifiers/sygus/sygus_abduct.h theory/quantifiers/sygus/sygus_enumerator.cpp theory/quantifiers/sygus/sygus_enumerator.h - theory/quantifiers/sygus/sygus_enumerator_basic.cpp - theory/quantifiers/sygus/sygus_enumerator_basic.h theory/quantifiers/sygus/sygus_enumerator_callback.cpp theory/quantifiers/sygus/sygus_enumerator_callback.h theory/quantifiers/sygus/sygus_eval_unfold.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index f477d879c..c284518c7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1084,25 +1084,22 @@ name = "Quantifiers" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" [[option]] - name = "sygusActiveGenMode" + name = "sygusEnumMode" category = "regular" - long = "sygus-active-gen=MODE" - type = "SygusActiveGenMode" + long = "sygus-enum=MODE" + type = "SygusEnumMode" default = "AUTO" - help = "mode for actively-generated sygus enumerators" - help_mode = "Modes for actively-generated sygus enumerators." -[[option.mode.NONE]] - name = "none" - help = "Do not use actively-generated sygus enumerators." -[[option.mode.ENUM_BASIC]] - name = "basic" - help = "Use basic type enumerator for actively-generated sygus enumerators." -[[option.mode.ENUM]] - name = "enum" - help = "Use optimized enumerator for actively-generated sygus enumerators." + help = "mode for sygus enumeration" + help_mode = "Modes for sygus enumeration." +[[option.mode.SMART]] + name = "smart" + help = "Use smart enumeration based on datatype constraints." +[[option.mode.FAST]] + name = "fast" + help = "Use optimized enumerator for sygus enumeration." [[option.mode.RANDOM]] name = "random" - help = "Use basic random enumerator for actively-generated sygus enumerators." + help = "Use basic random enumerator for sygus enumeration." [[option.mode.VAR_AGNOSTIC]] name = "var-agnostic" help = "Use sygus solver to enumerate terms that are agnostic to variables." @@ -1111,22 +1108,22 @@ name = "Quantifiers" help = "Internally decide the best policy for each enumerator." [[option]] - name = "sygusActiveGenRandomP" + name = "sygusEnumRandomP" category = "regular" - long = "sygus-active-gen-random-p=P" + long = "sygus-enum-random-p=P" type = "double" default = "0.5" minimum = "0.0" maximum = "1.0" - help = "the parameter of the geometric distribution used to determine the size of terms generated by --sygus-active-gen=random" + help = "the parameter of the geometric distribution used to determine the size of terms generated by --sygus-enum=random" [[option]] - name = "sygusActiveGenEnumConsts" + name = "sygusEnumFastNumConsts" category = "regular" - long = "sygus-active-gen-cfactor=N" + long = "sygus-enum-fast-num-consts=N" type = "uint64_t" default = "5" - help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-active-gen=enum" + help = "the branching factor for the number of interpreted constants to consider for each size when using --sygus-enum=fast" [[option]] name = "sygusMinGrammar" diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp index b289e984e..fcbe3d42e 100644 --- a/src/theory/quantifiers/sygus/enum_value_manager.cpp +++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/sygus/enum_stream_substitution.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" -#include "theory/quantifiers/sygus/sygus_enumerator_basic.h" #include "theory/quantifiers/sygus/sygus_random_enumerator.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_registry.h" @@ -90,23 +89,16 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete) // or basic. The auto mode always prefers the optimized enumerator over // the basic one. Assert(d_tds->isBasicEnumerator(e)); - if (options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::ENUM_BASIC) - { - d_evg = - std::make_unique(d_env, d_tds, e.getType()); - } - else if (options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::RANDOM) + if (options().quantifiers.sygusEnumMode == options::SygusEnumMode::RANDOM) { d_evg = std::make_unique(d_env, d_tds); } else { - Assert(options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::ENUM - || options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::AUTO); + Assert(options().quantifiers.sygusEnumMode + == options::SygusEnumMode::FAST + || options().quantifiers.sygusEnumMode + == options::SygusEnumMode::AUTO); // create the enumerator callback if (options().datatypes.sygusSymBreakDynamic) { diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 8d22804b4..52c1ef4a0 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -1152,7 +1152,7 @@ bool SygusEnumerator::TermEnumMasterInterp::increment() { tc.pushEnumSizeIndex(); d_currSize++; - d_currNumConsts = d_currNumConsts * options::sygusActiveGenEnumConsts(); + d_currNumConsts = d_currNumConsts * options::sygusEnumFastNumConsts(); d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts; } ++d_te; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp deleted file mode 100644 index b9578a66a..000000000 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz - * - * 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 sygus basic enumerator. - */ -#include "theory/quantifiers/sygus/sygus_enumerator_basic.h" - -#include "options/datatypes_options.h" -#include "theory/rewriter.h" - -using namespace cvc5::kind; -using namespace std; - -namespace cvc5 { -namespace theory { -namespace quantifiers { - -EnumValGeneratorBasic::EnumValGeneratorBasic(Env& env, - TermDbSygus* tds, - TypeNode tn) - : EnumValGenerator(env), d_tds(tds), d_te(tn) -{ -} - -bool EnumValGeneratorBasic::increment() -{ - ++d_te; - if (d_te.isFinished()) - { - d_currTerm = Node::null(); - return false; - } - d_currTerm = *d_te; - if (options().datatypes.sygusSymBreakDynamic) - { - Node nextb = d_tds->sygusToBuiltin(d_currTerm); - nextb = extendedRewrite(nextb); - if (d_cache.find(nextb) == d_cache.end()) - { - d_cache.insert(nextb); - // only return the current term if not unique - } - else - { - d_currTerm = Node::null(); - } - } - return true; -} - -} // namespace quantifiers -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h deleted file mode 100644 index 543598a90..000000000 --- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h +++ /dev/null @@ -1,71 +0,0 @@ -/****************************************************************************** - * 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. - * **************************************************************************** - * - * Basic sygus enumerator class. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H -#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H - -#include -#include -#include "expr/node.h" -#include "expr/type_node.h" -#include "theory/quantifiers/sygus/enum_val_generator.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/type_enumerator.h" - -namespace cvc5 { -namespace theory { -namespace quantifiers { - -/** A basic sygus value generator - * - * This class is a "naive" term generator for sygus conjectures, which invokes - * the type enumerator to generate a stream of (all) sygus terms of a given - * type. - */ -class EnumValGeneratorBasic : public EnumValGenerator -{ - public: - EnumValGeneratorBasic(Env& env, TermDbSygus* tds, TypeNode tn); - ~EnumValGeneratorBasic() {} - /** initialize (do nothing) */ - void initialize(Node e) override {} - /** initialize (do nothing) */ - void addValue(Node v) override { d_currTerm = *d_te; } - /** - * Get next returns the next (T-rewriter-unique) value based on the type - * enumerator. - */ - bool increment() override; - /** get the current term */ - Node getCurrent() override { return d_currTerm; } - - private: - /** pointer to term database sygus */ - TermDbSygus* d_tds; - /** the type enumerator */ - TypeEnumerator d_te; - /** the current term */ - Node d_currTerm; - /** cache of (enumerated) builtin values we have enumerated so far */ - std::unordered_set d_cache; -}; - -} // namespace quantifiers -} // namespace theory -} // namespace cvc5 - -#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */ diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp index c679d3ea9..5bfde84c0 100644 --- a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp @@ -75,7 +75,7 @@ Node SygusRandomEnumerator::incrementH() NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); Random& rnd = Random::getRandom(); - double p = options().quantifiers.sygusActiveGenRandomP; + double p = options().quantifiers.sygusEnumRandomP; Node mainSkolem = sm->mkDummySkolem("sygus_rand", d_tn); // List of skolems with no corresponding constructor. diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index cf024c59f..60170ceb4 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -458,8 +458,7 @@ void TermDbSygus::registerEnumerator(Node e, // determine if we are actively-generated bool isActiveGen = false; - if (options().quantifiers.sygusActiveGenMode - != options::SygusActiveGenMode::NONE) + if (options().quantifiers.sygusEnumMode != options::SygusEnumMode::SMART) { if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED) { @@ -487,8 +486,7 @@ void TermDbSygus::registerEnumerator(Node e, { // If the enumerator is the single function-to-synthesize, if auto is // enabled, we infer whether it is better to enable active generation. - if (options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::AUTO) + if (options().quantifiers.sygusEnumMode == options::SygusEnumMode::AUTO) { // We use active generation if the grammar of the enumerator does not // have ITE and does not have Boolean connectives. Experimentally, it @@ -520,8 +518,8 @@ void TermDbSygus::registerEnumerator(Node e, // Currently, actively-generated enumerators are either basic or variable // agnostic. bool isVarAgnostic = isActiveGen - && options().quantifiers.sygusActiveGenMode - == options::SygusActiveGenMode::VAR_AGNOSTIC; + && options().quantifiers.sygusEnumMode + == options::SygusEnumMode::VAR_AGNOSTIC; d_enum_var_agnostic[e] = isVarAgnostic; if (isVarAgnostic) { diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy index 5febabc42..5a9d2a948 100644 --- a/test/regress/regress1/sygus/commutative-stream.sy +++ b/test/regress/regress1/sygus/commutative-stream.sy @@ -3,7 +3,7 @@ ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification +; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=2 --sygus-enum=smart --decision=justification (set-logic LIA) diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy index 9b57339db..31308d62a 100644 --- a/test/regress/regress1/sygus/error1-dt.sy +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-enum=fast (set-logic ALL) diff --git a/test/regress/regress1/sygus/fast-enum-backtrack.sy b/test/regress/regress1/sygus/fast-enum-backtrack.sy index 73a3dc2e2..1778f91c7 100644 --- a/test/regress/regress1/sygus/fast-enum-backtrack.sy +++ b/test/regress/regress1/sygus/fast-enum-backtrack.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-active-gen=enum +; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-enum=fast (set-logic ALL) diff --git a/test/regress/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/regress1/sygus/interpol1-push-pop.smt2 index 5ea6d8568..4e68b2517 100644 --- a/test/regress/regress1/sygus/interpol1-push-pop.smt2 +++ b/test/regress/regress1/sygus/interpol1-push-pop.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols -i +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols -i ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) diff --git a/test/regress/regress1/sygus/interpol1.smt2 b/test/regress/regress1/sygus/interpol1.smt2 index 58ef5420f..5962d1353 100644 --- a/test/regress/regress1/sygus/interpol1.smt2 +++ b/test/regress/regress1/sygus/interpol1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic NIA) diff --git a/test/regress/regress1/sygus/interpol_arr1.smt2 b/test/regress/regress1/sygus/interpol_arr1.smt2 index 16190f877..dde124bed 100644 --- a/test/regress/regress1/sygus/interpol_arr1.smt2 +++ b/test/regress/regress1/sygus/interpol_arr1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) diff --git a/test/regress/regress1/sygus/interpol_arr2.smt2 b/test/regress/regress1/sygus/interpol_arr2.smt2 index 18ce2b35f..fdd1a162d 100644 --- a/test/regress/regress1/sygus/interpol_arr2.smt2 +++ b/test/regress/regress1/sygus/interpol_arr2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2 index 7e349996d..0bee17ad9 100644 --- a/test/regress/regress1/sygus/interpol_cosa_1.smt2 +++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=conjecture --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) (set-option :produce-interpols conjecture) -(set-option :sygus-active-gen enum) +(set-option :sygus-enum fast) (declare-fun cfg@1 () (_ BitVec 1)) (declare-fun witness_0@1 () Bool) (declare-fun op@1 () (_ BitVec 4)) diff --git a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 index eff00e066..4970e2fd5 100644 --- a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 +++ b/test/regress/regress1/sygus/interpol_from_pono_1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) diff --git a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 index 894e8e781..ca8f14da6 100644 --- a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 +++ b/test/regress/regress1/sygus/interpol_from_pono_2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 (set-logic ALL) diff --git a/test/regress/regress1/sygus/issue3580.sy b/test/regress/regress1/sygus/issue3580.sy index 9da07407a..0366436b2 100644 --- a/test/regress/regress1/sygus/issue3580.sy +++ b/test/regress/regress1/sygus/issue3580.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2 +; COMMAND-LINE: --sygus-out=status --sygus-enum=smart --lang=sygus2 (set-logic ALL) (synth-fun f () Bool diff --git a/test/regress/regress1/sygus/rand_const.sy b/test/regress/regress1/sygus/rand_const.sy index e920a9cc0..cc87af3fe 100644 --- a/test/regress/regress1/sygus/rand_const.sy +++ b/test/regress/regress1/sygus/rand_const.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; COMMAND-LINE: --sygus-enum=random --sygus-out=status ; EXPECT: unsat (set-logic BV) diff --git a/test/regress/regress1/sygus/rand_p_0.sy b/test/regress/regress1/sygus/rand_p_0.sy index a7b3c9f41..03d6cbc67 100644 --- a/test/regress/regress1/sygus/rand_p_0.sy +++ b/test/regress/regress1/sygus/rand_p_0.sy @@ -1,8 +1,8 @@ -; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; COMMAND-LINE: --sygus-enum=random --sygus-out=status ; EXPECT: unsat (set-logic BV) -(set-option :sygus-active-gen-random-p 0) +(set-option :sygus-enum-random-p 0) ; Ensures random enumerator correctly handles cases where the coin flips to ; tails but there is no no-argument constructor to pick. diff --git a/test/regress/regress1/sygus/rand_p_1.sy b/test/regress/regress1/sygus/rand_p_1.sy index 412e55f73..a1eb85183 100644 --- a/test/regress/regress1/sygus/rand_p_1.sy +++ b/test/regress/regress1/sygus/rand_p_1.sy @@ -1,8 +1,8 @@ -; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status +; COMMAND-LINE: --sygus-enum=random --sygus-out=status ; EXPECT: unsat (set-logic BV) -(set-option :sygus-active-gen-random-p 1) +(set-option :sygus-enum-random-p 1) ; Ensures random enumerator correctly handles cases where the coin flips to ; heads but there is no constructor that takes arguments to pick. diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy index 8d3e91b06..32eb92fe3 100644 --- a/test/regress/regress1/sygus/trivial-stream.sy +++ b/test/regress/regress1/sygus/trivial-stream.sy @@ -3,7 +3,7 @@ ; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.") ; EXIT: 1 -; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic +; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=0 --sygus-enum=var-agnostic (set-logic LIA) diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy index 65e5d428f..3a81a4885 100644 --- a/test/regress/regress2/sygus/multi-udiv.sy +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic BV) (define-fun hd05 ((x (_ BitVec 32))) (_ BitVec 32) (bvor x (bvsub x #x00000001))) diff --git a/test/regress/regress2/sygus/sets-fun-test.sy b/test/regress/regress2/sygus/sets-fun-test.sy index 23abc5c7e..561014ed5 100644 --- a/test/regress/regress2/sygus/sets-fun-test.sy +++ b/test/regress/regress2/sygus/sets-fun-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic ALL) (synth-fun f ((x Int)) (Set Int)) diff --git a/test/regress/regress2/sygus/three.sy b/test/regress/regress2/sygus/three.sy index 9bed1e667..17af8c93b 100644 --- a/test/regress/regress2/sygus/three.sy +++ b/test/regress/regress2/sygus/three.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-active-gen=enum +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast (set-logic NIA) diff --git a/test/regress/regress3/interpol2.smt2 b/test/regress/regress3/interpol2.smt2 index c6876ee15..bfd034547 100644 --- a/test/regress/regress3/interpol2.smt2 +++ b/test/regress/regress3/interpol2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols +; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy index b84252d6c..d405d3b49 100644 --- a/test/regress/regress3/strings-any-term.sy +++ b/test/regress/regress3/strings-any-term.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-enum=smart (set-logic ALL) (synth-fun f ((x String) (y String)) Int) (declare-var x String) -- 2.30.2