diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-03 11:30:09 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-03 11:30:09 -0500 |
| commit | 4251c330cc2e9e87ffaaf4dd2c1bc9db6f1046a5 (patch) | |
| tree | 3ef2a3e16fb023f1edb7d004d0d2f52d096e8cb2 /src/theory/quantifiers/sygus/sygus_module.h | |
| parent | 53e1523de04c8643186244d9fc3c329ff158a057 (diff) | |
Link cegis unif with the enumeration manager (#1859)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_module.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 0a3fa9995..07f5aec9d 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -114,6 +114,14 @@ class SygusModule std::vector<Node>& lems) { } + /** get next decision request + * + * This has the same contract as Theory::getNextDecisionRequest. + */ + virtual Node getNextDecisionRequest(unsigned& priority) + { + return Node::null(); + } protected: /** reference to quantifier engine */ |