diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 13:32:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-10-10 13:32:49 +0200 |
| commit | 08077fa4c45c95b17eb557610a3950352f9d8a20 (patch) | |
| tree | 753d208c8635830b5e21b5ac73fe2d308998dd8a /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | ed5052c7672bd59f8a8ef28d980d56a4f036f97d (diff) | |
Add owner map to better manage QuantifiersModules. Initial infrastructure for cegqi.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ee4464f87..060994379 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1702,7 +1702,7 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) { //-------------------------------------------------- registration
void QuantConflictFind::registerQuantifier( Node q ) {
- if( !TermDb::isRewriteRule( q ) ){
+ if( d_quantEngine->hasOwnership( q, this ) ){
d_quants.push_back( q );
d_quant_id[q] = d_quants.size();
Trace("qcf-qregister") << "Register ";
@@ -1839,7 +1839,7 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { //-------------------------------------------------- handling assertions / eqc
void QuantConflictFind::assertNode( Node q ) {
- if( !TermDb::isRewriteRule( q ) ){
+ if( d_quantEngine->hasOwnership( q, this ) ){
Trace("qcf-proc") << "QCF : assertQuantifier : ";
debugPrintQuant("qcf-proc", q);
Trace("qcf-proc") << std::endl;
|