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/rep_set.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/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index cd1fac290..303e65eff 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -15,7 +15,7 @@ #include "theory/rep_set.h" #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers/first_order_model.h" using namespace std; @@ -183,7 +183,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ // terms in rep_set are now constants which mapped to terms through TheoryModel // thus, should introduce a constant and a term. for now, just a term. - //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + //Node c = d_qe->getTermUtil()->getEnumerateTerm( tn, 0 ); Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); @@ -208,7 +208,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ } if( !tn.isSort() ){ if( inc ){ - if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + if( d_qe->getTermUtil()->mayComplete( tn ) ){ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); //must have succeeded @@ -242,7 +242,7 @@ bool RepSetIterator::initialize( RepBoundExt* rext ){ for( unsigned i=0; i<d_qe->getBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){ Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i ); Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl; - varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) ); + varOrder.push_back( d_qe->getTermUtil()->getVariableNum( d_owner, v ) ); } for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) { if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { |