diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-31 21:24:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-31 21:24:31 +0000 |
commit | b88133bc679c541798c2063fec2bc441e744328a (patch) | |
tree | 42097c3b9dabc5f4195e489158ea122e73155813 /src/theory/quantifiers/candidate_generator.cpp | |
parent | f73e17d5649f636eb88aafe05aaf32565a806bab (diff) |
Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat.
The namespaces weren't changed, only the file locations.
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 255 |
1 files changed, 255 insertions, 0 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp new file mode 100644 index 000000000..6a7c4c504 --- /dev/null +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -0,0 +1,255 @@ +/********************* */ +/*! \file candidate_generator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of theory uf candidate generator class + **/ + +#include "theory/quantifiers/candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::inst; + +bool CandidateGenerator::isLegalCandidate( Node n ){ + return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) ); +} + +void CandidateGeneratorQueue::addCandidate( Node n ) { + if( isLegalCandidate( n ) ){ + d_candidates.push_back( n ); + } +} + +void CandidateGeneratorQueue::reset( Node eqc ){ + if( d_candidate_index>0 ){ + d_candidates.erase( d_candidates.begin(), d_candidates.begin() + d_candidate_index ); + d_candidate_index = 0; + } + if( !eqc.isNull() ){ + d_candidates.push_back( eqc ); + } +} +Node CandidateGeneratorQueue::getNextCandidate(){ + if( d_candidate_index<(int)d_candidates.size() ){ + Node n = d_candidates[d_candidate_index]; + d_candidate_index++; + return n; + }else{ + d_candidate_index = 0; + d_candidates.clear(); + return Node::null(); + } +} + +#if 0 + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : + d_op( op ), d_qe( qe ), d_term_iter( -2 ){ + Assert( !d_op.isNull() ); +} +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + if( eqc.isNull() ){ + d_term_iter = 0; + }else{ + //create an equivalence class iterator in eq class eqc + if( d_qe->getEqualityQuery()->getEngine()->hasTerm( eqc ) ){ + eqc = d_qe->getEqualityQuery()->getEngine()->getRepresentative( eqc ); + d_eqc = eq::EqClassIterator( eqc, d_qe->getEqualityQuery()->getEngine() ); + d_retNode = Node::null(); + }else{ + d_retNode = eqc; + } + d_term_iter = -1; + } +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_term_iter>=0 ){ + //get next candidate term in the uf term database + while( d_term_iter<d_term_iter_limit ){ + Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter]; + d_term_iter++; + if( isLegalCandidate( n ) ){ + return n; + } + } + }else if( d_term_iter==-1 ){ + if( d_retNode.isNull() ){ + //get next candidate term in equivalence class + while( !d_eqc.isFinished() ){ + Node n = (*d_eqc); + ++d_eqc; + if( n.hasOperator() && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return n; + } + } + } + }else{ + Node ret; + if( d_retNode.hasOperator() && d_retNode.getOperator()==d_op ){ + ret = d_retNode; + } + d_term_iter = -2; //done returning matches + return ret; + } + } + return Node::null(); +} + +#else + + +CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : + d_op( op ), d_qe( qe ), d_term_iter( -1 ){ + Assert( !d_op.isNull() ); +} +void CandidateGeneratorQE::resetInstantiationRound(){ + d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); +} + +void CandidateGeneratorQE::reset( Node eqc ){ + d_term_iter = 0; + if( eqc.isNull() ){ + d_using_term_db = true; + }else{ + //create an equivalence class iterator in eq class eqc + d_eqc.clear(); + d_qe->getEqualityQuery()->getEquivalenceClass( eqc, d_eqc ); + d_using_term_db = false; + } +} + +Node CandidateGeneratorQE::getNextCandidate(){ + if( d_term_iter>=0 ){ + if( d_using_term_db ){ + //get next candidate term in the uf term database + while( d_term_iter<d_term_iter_limit ){ + Node n = d_qe->getTermDatabase()->d_op_map[d_op][d_term_iter]; + d_term_iter++; + if( isLegalCandidate( n ) ){ + return n; + } + } + }else{ + while( d_term_iter<(int)d_eqc.size() ){ + Node n = d_eqc[d_term_iter]; + d_term_iter++; + if( n.hasOperator() && n.getOperator()==d_op ){ + if( isLegalCandidate( n ) ){ + return n; + } + } + } + } + } + return Node::null(); +} + +#endif + +//CandidateGeneratorQEDisequal::CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ) : +// d_qe( qe ), d_eq_class( eqc ){ +// d_eci = NULL; +//} +//void CandidateGeneratorQEDisequal::resetInstantiationRound(){ +// +//} +////we will iterate over all terms that are disequal from eqc +//void CandidateGeneratorQEDisequal::reset( Node eqc ){ +// //Assert( !eqc.isNull() ); +// ////begin iterating over equivalence classes that are disequal from eqc +// //d_eci = d_ith->getEquivalenceClassInfo( eqc ); +// //if( d_eci ){ +// // d_eqci_iter = d_eci->d_disequal.begin(); +// //} +//} +//Node CandidateGeneratorQEDisequal::getNextCandidate(){ +// //if( d_eci ){ +// // while( d_eqci_iter != d_eci->d_disequal.end() ){ +// // if( (*d_eqci_iter).second ){ +// // //we have an equivalence class that is disequal from eqc +// // d_cg->reset( (*d_eqci_iter).first ); +// // Node n = d_cg->getNextCandidate(); +// // //if there is a candidate in this equivalence class, return it +// // if( !n.isNull() ){ +// // return n; +// // } +// // } +// // ++d_eqci_iter; +// // } +// //} +// return Node::null(); +//} + + +CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} +void CandidateGeneratorQELitEq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitEq::reset( Node eqc ){ + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); +} +Node CandidateGeneratorQELitEq::getNextCandidate(){ + while( d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern[0].getType() ){ + //an equivalence class with the same type as the pattern, return reflexive equality + return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); + } + } + return Node::null(); +} + + +CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} +void CandidateGeneratorQELitDeq::resetInstantiationRound(){ + +} +void CandidateGeneratorQELitDeq::reset( Node eqc ){ + Node false_term = d_qe->getEqualityQuery()->getEngine()->getRepresentative( NodeManager::currentNM()->mkConst<bool>(false) ); + d_eqc_false = eq::EqClassIterator( false_term, d_qe->getEqualityQuery()->getEngine() ); +} +Node CandidateGeneratorQELitDeq::getNextCandidate(){ + //get next candidate term in equivalence class + while( !d_eqc_false.isFinished() ){ + Node n = (*d_eqc_false); + ++d_eqc_false; + if( n.getKind()==d_match_pattern.getKind() ){ + //found an iff or equality, try to match it + //DO_THIS: cache to avoid redundancies? + //DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? + return n; + } + } + return Node::null(); +} |