diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-29 00:17:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-29 00:17:14 -0600 |
| commit | 43e02cedf0e2a2700a2ace23cf85cff9bb242f13 (patch) | |
| tree | 90ed1619e07e3a959dd5cf576e73a076a9523f20 /src/theory/quantifiers/sygus/sygus_unif.h | |
| parent | 8d3ea75e7895bbb169a2b7bd02c8fe3b626bdb5e (diff) | |
Combine sygus stream with PBE (#2726)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 67e798854..0784644f8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -181,6 +181,15 @@ class SygusUnif const std::map<Node, unsigned>& total_inc, const std::map<Node, std::vector<unsigned> >& incr); //------------------------------ end constructing solutions + /** map terms to their sygus size */ + std::map<Node, unsigned> d_termToSize; + /** + * Whether to ensure terms selected by the above methods lead to minimal + * solutions. + */ + bool d_enableMinimality; + /** returns the term whose sygus size is minimal among those in terms */ + Node getMinimalTerm(const std::vector<Node>& terms); }; } /* CVC4::theory::quantifiers namespace */ |