diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-09 21:56:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-09 21:56:40 -0500 |
commit | 96a0bc3b022b67b5ab79bf2ab087573c65a8d248 (patch) | |
tree | 427223e34ce9bd100ef4443c80b95a9526169363 /src/theory/quantifiers/quant_util.cpp | |
parent | 3b0ce95e7b7d1cbc351df9a7d2acbf3b6e13f9e7 (diff) |
Split term database (#1206)
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b34abba13..1e30914ef 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -48,6 +49,10 @@ quantifiers::TermDb * QuantifiersModule::getTermDatabase() { return d_quantEngine->getTermDatabase(); } +quantifiers::TermUtil * QuantifiersModule::getTermUtil() { + return d_quantEngine->getTermUtil(); +} + bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ c = n[0]; @@ -218,7 +223,7 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) { } } if( tn.isReal() ){ - if( quantifiers::TermDb::containsTerm( lit, v ) ){ + if( quantifiers::TermUtil::containsTerm( lit, v ) ){ std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( lit, msum ) ){ Node val, veqc; @@ -338,13 +343,13 @@ void QuantPhaseReq::initialize( Node n, bool computeEq ){ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; if( it->first.getKind()==EQUAL ){ - if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){ - if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ + if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ + if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; d_phase_reqs_equality[ it->first[0] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; } - }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ + }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; d_phase_reqs_equality[ it->first[1] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; |