diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 15:20:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 15:20:37 -0500 |
commit | 4b580ea3876055f701b13e67e0e4e78abbe47674 (patch) | |
tree | 35d1cd8f48077dfed5a5bae682f2efc90d80703f /src/theory/quantifiers/conjecture_generator.cpp | |
parent | 13e452be03bef09e2f54f42e2bc42383505ffcea (diff) |
(Refactor) Split term util (#1303)
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 35 |
1 files changed, 24 insertions, 11 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 508f58a07..e5a096c87 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -13,10 +13,12 @@ ** **/ -#include "options/quantifiers_options.h" #include "theory/quantifiers/conjecture_generator.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" @@ -398,7 +400,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { std::vector< TNode > args; Trace("sg-pat-debug") << "******* Get ground term for " << r << std::endl; Node n; - if( getTermUtil()->isInductionTerm( r ) ){ + if (Skolemize::isInductionTerm(r)) + { n = d_op_arg_index[r].getGroundTerm( this, args ); }else{ n = r; @@ -556,12 +559,13 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { if( std::find( provenConj.begin(), provenConj.end(), q )==provenConj.end() ){ //check each skolem variable bool disproven = true; - //std::vector< Node > sk; - //getTermUtil()->getSkolemConstants( q, sk, true ); + std::vector<Node> skolems; + d_quantEngine->getSkolemize()->getSkolemConstants(q, skolems); Trace("sg-conjecture") << " CONJECTURE : "; std::vector< Node > ce; - for( unsigned j=0; j<getTermUtil()->d_skolem_constants[q].size(); j++ ){ - TNode k = getTermUtil()->d_skolem_constants[q][j]; + for (unsigned j = 0; j < skolems.size(); j++) + { + TNode k = skolems[j]; TNode rk = getRepresentative( k ); std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk ); //check if it is a ground term @@ -569,7 +573,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { Trace("sg-conjecture") << "ACTIVE : " << q; if( Trace.isOn("sg-gen-eqc") ){ Trace("sg-conjecture") << " { "; - for( unsigned k=0; k<getTermUtil()->d_skolem_constants[q].size(); k++ ){ Trace("sg-conjecture") << getTermUtil()->d_skolem_constants[q][k] << ( j==k ? "*" : "" ) << " "; } + for (unsigned k = 0; k < skolems.size(); k++) + { + Trace("sg-conjecture") << skolems[k] << (j == k ? "*" : "") + << " "; + } Trace("sg-conjecture") << "}"; } Trace("sg-conjecture") << std::endl; @@ -1051,12 +1059,14 @@ Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ) { if( n.getNumChildren()>0 ){ + TermEnumeration* te = d_quantEngine->getTermEnumeration(); std::vector< int > vec; std::vector< TypeNode > types; for( unsigned i=0; i<n.getNumChildren(); i++ ){ vec.push_back( 0 ); TypeNode tn = n[i].getType(); - if( getTermUtil()->isClosedEnumerableType( tn ) ){ + if (te->isClosedEnumerableType(tn)) + { types.push_back( tn ); }else{ return; @@ -1074,7 +1084,9 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< vec.push_back( size_limit ); }else{ //see if we can iterate current - if( vec_sum<size_limit && !getTermUtil()->getEnumerateTerm( types[index], vec[index]+1 ).isNull() ){ + if (vec_sum < size_limit + && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull()) + { vec[index]++; vec_sum++; vec.push_back( size_limit - vec_sum ); @@ -1089,7 +1101,8 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } if( success ){ if( vec.size()==n.getNumChildren() ){ - Node lc = getTermUtil()->getEnumerateTerm( types[vec.size()-1], vec[vec.size()-1] ); + Node lc = + te->getEnumerateTerm(types[vec.size() - 1], vec[vec.size() - 1]); if( !lc.isNull() ){ for( unsigned i=0; i<vec.size(); i++ ){ Trace("sg-gt-enum-debug") << vec[i] << " "; @@ -1102,7 +1115,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< std::vector< Node > children; children.push_back( n.getOperator() ); for( unsigned i=0; i<(vec.size()-1); i++ ){ - Node nn = getTermUtil()->getEnumerateTerm( types[i], vec[i] ); + Node nn = te->getEnumerateTerm(types[i], vec[i]); Assert( !nn.isNull() ); Assert( nn.getType()==n[i].getType() ); children.push_back( nn ); |