diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-29 15:17:03 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-29 15:17:03 +0200 |
| commit | 4182943e7accc8a0e05f6dfdf9db7db06e94c6cd (patch) | |
| tree | d4f3bad70e464321a4e7fe977f1528f783dcd1b1 /src/theory/quantifiers/term_database.cpp | |
| parent | ef7b7bba7bc9b207d5a2198518f21b13490caa32 (diff) | |
Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 366c7ce07..2c9430876 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1549,6 +1549,10 @@ bool TermDb::isComm( Kind k ) { k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; } +bool TermDb::isBoolConnective( Kind k ) { + return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT; +} + void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); |