diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-22 16:04:39 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-22 16:04:39 -0500 |
| commit | 0b13f748c7a6f2cb5ee61404e0864667e9a931b9 (patch) | |
| tree | 707d8700eb75a702e91b119a3faa239fc58c43e5 /src/theory/quantifiers/theory_quantifiers.cpp | |
| parent | bdb5789713c03cf16f0ce6178b2fdc66f96ddc9e (diff) | |
Add option --cbqi-recurse.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
| -rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 52c9e34f3..066282c2c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( !TermDb::hasInstConstAttr(n) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); getQuantifiersEngine()->assertNode( n ); } @@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){ void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !TermDb::hasInstConstAttr(n[0]) ){ + if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ if( d_skolemized.find( n )==d_skolemized.end() ){ Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] ); NodeBuilder<> nb(kind::OR); |