Also deletes the unused (naive) basic enumerator.
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
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."
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"
#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"
// 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<EnumValGeneratorBasic>(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<SygusRandomEnumerator>(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)
{
{
tc.pushEnumSizeIndex();
d_currSize++;
- d_currNumConsts = d_currNumConsts * options::sygusActiveGenEnumConsts();
+ d_currNumConsts = d_currNumConsts * options::sygusEnumFastNumConsts();
d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts;
}
++d_te;
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 <map>
-#include <unordered_set>
-#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<Node> d_cache;
-};
-
-} // namespace quantifiers
-} // namespace theory
-} // namespace cvc5
-
-#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
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.
// 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)
{
{
// 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
// 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)
{
; 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)
; 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)
; 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)
-; 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)
-; 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)
-; 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)
-; 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)
-; 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))
-; 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)
-; 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)
; 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
-; COMMAND-LINE: --sygus-active-gen=random --sygus-out=status
+; COMMAND-LINE: --sygus-enum=random --sygus-out=status
; EXPECT: unsat
(set-logic BV)
-; 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.
-; 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.
; 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)
; 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)))
; 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))
; 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)
-; 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
; 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)
projects / cvc5.git / commitdiff