diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-10 08:12:34 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-10 08:12:34 +0200 |
| commit | d5b0866bd2a2551143caf591d453993ab5a48840 (patch) | |
| tree | 71d9bf61a8134be3ca13596ab0d8f278a2021eb9 /src/theory/theory.h | |
| parent | 8a68cca2f9cf76b42187c39d09a4a40bd19622c1 (diff) | |
Ensure that expand definitions is called on all non-variable expressi… (#1070)
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.
* Add comments concerning expandDefinitions
* Expand comment, move to .h
Diffstat (limited to 'src/theory/theory.h')
| -rw-r--r-- | src/theory/theory.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 73102a6e2..1a72944ff 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -424,6 +424,12 @@ public: * used, definitions should only be used when rewrites are not * possible, for example in handling under-specified operations * using partially defined functions. + * + * TODO (github issue #1076): + * some theories like sets use expandDefinition as a "context + * independent preRegisterTerm". This is required for cases where + * a theory wants to be notified about a term before preprocessing + * and simplification but doesn't necessarily want to rewrite it. */ virtual Node expandDefinition(LogicRequest &logicRequest, Node node) { // by default, do nothing |