diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-28 09:13:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-28 09:13:13 -0500 |
commit | 34e84a25a044e3af192bb69089467c2125911900 (patch) | |
tree | 924a3ae0894bfec136f91949a1bf55e19c4125da /src/theory/quantifiers/quantifiers_attributes.cpp | |
parent | 675e82e32a34911163f9de0e6389eb107be5b0f1 (diff) |
Document term db (#1220)
* Document TermDb and related classes. Minor changes to quantifiers utils and their interface. Address some comments left over from PR 1206.
* Minor
* Minor
* Change namespace style.
* Address review
* Fix incorrectly merged portion that led to regression failures.
* New clang format, fully document relevant domain.
* Clang format again.
* Minor
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index c9a7f07ab..d02ad667e 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -22,11 +22,12 @@ #include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : d_quantEngine(qe) { @@ -94,7 +95,10 @@ bool QuantAttributes::checkRewriteRule( Node q ) { } Node QuantAttributes::getRewriteRule( Node q ) { - if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){ + if (q.getKind() == FORALL && q.getNumChildren() == 3 + && q[2][0].getNumChildren() > 0 + && q[2][0][0].getKind() == REWRITE_RULE) + { return q[2][0][0]; }else{ return Node::null(); @@ -121,12 +125,13 @@ bool QuantAttributes::checkFunDefAnnotation( Node ipl ) { Node QuantAttributes::getFunDefHead( Node q ) { //&& q[1].getKind()==EQUAL && 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()) ){ - return q[2][i][0]; - } + Node ipl = q[2]; + for (unsigned i = 0; i < ipl.getNumChildren(); i++) + { + if (ipl[i].getKind() == INST_ATTRIBUTE + && ipl[i][0].getAttribute(FunDefAttribute())) + { + return ipl[i][0]; } } } @@ -197,7 +202,7 @@ void QuantAttributes::computeAttributes( Node q ) { Node f = d_qattr[q].d_fundef_f; if( d_fun_defs.find( f )!=d_fun_defs.end() ){ Message() << "Cannot define function " << f << " more than once." << std::endl; - exit( 1 ); + AlwaysAssert(false); } d_fun_defs[f] = true; d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 ); @@ -383,3 +388,6 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) { } } +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ |