diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-27 19:43:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-27 19:43:05 -0500 |
| commit | 448a874adc9314d42a107b24654b155ba465e202 (patch) | |
| tree | 72a9ed78c241952f645376e07b782b3bf42aaee4 /src/theory/quantifiers/sygus/sygus_unif.h | |
| parent | 5b2c33bf0bd968b970d5f228f291477d20b751df (diff) | |
Make construct solution behavior specific to SygusIO (#1827)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 728d613b2..beb2023f9 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -99,18 +99,6 @@ class SygusUnif std::vector<Node>& vals, bool pol = true); //-----------------------end debug printing - - - /** - * Whether we will try to construct solution on the next call to - * constructSolution. This flag is set to true when we successfully - * register a new value for an enumerator. - */ - bool d_check_sol; - /** The number of values we have enumerated for all enumerators. */ - unsigned d_cond_count; - /** The solution for the function of this class, if one has been found */ - Node d_solution; /** the candidate for this class */ Node d_candidate; /** maps a function-to-synthesize to the above information */ |