summaryrefslogtreecommitdiff
path: root/src/theory/candidate_generator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/candidate_generator.cpp')
-rw-r--r--src/theory/candidate_generator.cpp510
1 files changed, 255 insertions, 255 deletions
diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp
index ffecaa8da..a0f303c21 100644
--- a/src/theory/candidate_generator.cpp
+++ b/src/theory/candidate_generator.cpp
@@ -1,255 +1,255 @@
-/********************* */
-/*! \file theory_uf_candidate_generator.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 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/candidate_generator.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/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::current()->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();
-}
+/********************* */
+/*! \file theory_uf_candidate_generator.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 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/candidate_generator.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/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::current()->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();
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback