diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-24 23:50:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-24 23:50:50 -0500 |
| commit | e9c115e82ea1341f1bbc37fb99c005aacec3d7ec (patch) | |
| tree | d274291c8b570e1ff383504e8eeccaafbffd7b15 /src/theory/quantifiers/sygus/sygus_module.h | |
| parent | b9cddd75ada97b4e1808b907125e366c3c03c412 (diff) | |
Allow partial models for multiple sygus enumerators (#2499)
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_module.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index c1b12dfd0..02cf1cdf2 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -71,6 +71,16 @@ class SygusModule */ virtual void getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) = 0; + /** allow partial model + * + * This method returns true if this module does not require that all + * terms returned by getTermList have "proper" model values when calling + * constructCandidates. A term may have a model value that is not proper + * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model + * values that are not proper are replaced by "null" when calling + * constructCandidates. + */ + virtual bool allowPartialModel() { return false; } /** construct candidate * * This function takes as input: |