diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-21 09:54:12 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-21 09:54:12 -0600 |
commit | 0e5655c7d1fddde55bfeba9f59bf9af79e8b5f0a (patch) | |
tree | f25f05c008810cd71586faf010906347a20eb911 /src/theory/quantifiers/sygus/cegis.h | |
parent | 596fe8c79106dd9b7764df2ddce6b2d3344fea34 (diff) |
Evaluation unfolding for symbolic SyGuS constructors (#3483)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.h')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 08cf98c99..adaecc7f6 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -204,15 +204,15 @@ class Cegis : public SygusModule */ std::unordered_set<unsigned> d_cegis_sample_refine; - //---------------------------------for sygus repair - /** are we using grammar-based repair? + //---------------------------------for symbolic constructors + /** are we using symbolic constants? * * This flag is set ot true if at least one of the enumerators allocated * by this class has been configured to allow model values with symbolic * constructors, such as the "any constant" constructor. */ - bool d_using_gr_repair; - //---------------------------------end for sygus repair + bool d_usingSymCons; + //---------------------------------end for symbolic constructors }; } /* CVC4::theory::quantifiers namespace */ |