diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:41:49 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:42:01 +0100 |
commit | f9e109b0ac12ffbfd167a19dcd60f16241a0542c (patch) | |
tree | 07547a834d60cbbbd75c91e1695c5518774c813e /src/theory/quantifiers/term_database.cpp | |
parent | 5fae5ff49bfc9c96c03c52f5e2a5caa52ac40d03 (diff) |
Better combination of UF with cbqi, refactor quantifiers intialization.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index bfeacf044..e513666a4 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1599,9 +1599,23 @@ bool TermDb::isFunDef( Node q ) { return !getFunDefHead( q ).isNull(); } +bool TermDb::isFunDefAnnotation( Node ipl ) { + if( !ipl.isNull() ){ + for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ + if( ipl[i].getKind()==INST_ATTRIBUTE ){ + if( ipl[i][0].getAttribute(FunDefAttribute()) ){ + return true; + } + } + } + } + return false; +} + Node TermDb::getFunDefHead( Node q ) { //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && if( q.getKind()==FORALL && q.getNumChildren()==3 ){ + for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ if( q[2][i].getKind()==INST_ATTRIBUTE ){ if( q[2][i][0].getAttribute(FunDefAttribute()) ){ |