diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-23 09:44:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-23 14:44:39 +0000 |
| commit | 6beb70fcedd18e965ad82949090365cb44a43692 (patch) | |
| tree | 0b66d7599fed75e39257a0d29e88483c59c6b03e /src/theory/quantifiers/candidate_rewrite_database.h | |
| parent | 61b9dadc88de3bf7d52538f9e914cfb61cbb7bb6 (diff) | |
Replace old sygus term reconstruction algorithm with a new one. (#5779)
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.h')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index a5fb33a1f..3313b507b 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -58,8 +58,7 @@ class CandidateRewriteDatabase : public ExprMiner bool filterPairs = true); ~CandidateRewriteDatabase() {} /** Initialize this class */ - void initialize(const std::vector<Node>& var, - SygusSampler* ss = nullptr) override; + void initialize(const std::vector<Node>& var, SygusSampler* ss) override; /** Initialize this class * * Serves the same purpose as the above function, but we will be using @@ -75,7 +74,7 @@ class CandidateRewriteDatabase : public ExprMiner void initializeSygus(const std::vector<Node>& vars, QuantifiersEngine* qe, Node f, - SygusSampler* ss = nullptr); + SygusSampler* ss); /** add term * * Notifies this class that the solution sol was enumerated. This may |