diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 2 |
2 files changed, 1 insertions, 22 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index d0f156811..d1217d01d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -42,27 +42,6 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } -bool SygusUnif::constructSolution(std::vector<Node>& sols, - std::vector<Node>& lemmas) -{ - // initialize a call to construct solution - initializeConstructSol(); - for (const Node& f : d_candidates) - { - // initialize a call to construct solution for function f - initializeConstructSolFor(f); - // call the virtual construct solution method - Node e = d_strategy[f].getRootEnumerator(); - Node sol = constructSol(f, e, role_equal, 1, lemmas); - if (sol.isNull()) - { - return false; - } - sols.push_back(sol); - } - return true; -} - Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved) { Assert(!solved.empty()); diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index dd6922351..614a29d1c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -85,7 +85,7 @@ class SygusUnif * channel by the caller. */ virtual bool constructSolution(std::vector<Node>& sols, - std::vector<Node>& lemmas); + std::vector<Node>& lemmas) = 0; protected: /** reference to quantifier engine */ |