diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:15 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 12:43:31 -0600 |
| commit | e8c09abb9165278b13491c83bdcbe17ae535126e (patch) | |
| tree | 1101d3e878bcfd9e12cd64aaad3017aa320c896b /src/theory/quantifiers_engine.h | |
| parent | 0e956da9b32ce8a8fcf20ec65e5a2820b4e31324 (diff) | |
Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 43beec6e3..83076c51a 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -271,6 +271,8 @@ public: void setOwner( Node q, QuantifiersModule * m, int priority = 0 ); /** considers */ bool hasOwnership( Node q, QuantifiersModule * m = NULL ); + /** is finite bound */ + bool isFiniteBound( Node q, Node v ); public: /** initialize */ void finishInit(); |