diff options
Diffstat (limited to 'src/theory/rr_candidate_generator.cpp')
-rw-r--r-- | src/theory/rr_candidate_generator.cpp | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/src/theory/rr_candidate_generator.cpp b/src/theory/rr_candidate_generator.cpp new file mode 100644 index 000000000..a2e895c7f --- /dev/null +++ b/src/theory/rr_candidate_generator.cpp @@ -0,0 +1,125 @@ +/********************* */ +/*! \file rr_candidate_generator.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot + ** 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 rr candidate generator class + **/ + +#include "theory/rr_candidate_generator.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::rrinst; + +GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(qe->getInstantiator(i) != NULL) + d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); + else d_can_gen[i] = NULL; + } +} + +GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + } +} + +void GenericCandidateGeneratorClasses::resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + } + d_can_gen_id=THEORY_FIRST; +} + +void GenericCandidateGeneratorClasses::reset(TNode eqc){ + Assert(eqc.isNull()); + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + } + d_can_gen_id=THEORY_FIRST; + lookForNextTheory(); +} + +TNode GenericCandidateGeneratorClasses::getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); +} + +void GenericCandidateGeneratorClasses::lookForNextTheory(){ + do{ /* look for the next available generator */ + ++d_can_gen_id; + } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); +} + +GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_qe->getInstantiator(i) != NULL) + d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); + else d_can_gen[i] = NULL; + } +} + +GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + delete(d_can_gen[i]); + } +} + +void GenericCandidateGeneratorClass::resetInstantiationRound(){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); + } + d_can_gen_id=THEORY_FIRST; +} + +void GenericCandidateGeneratorClass::reset(TNode eqc){ + for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ + if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); + } + d_can_gen_id=THEORY_FIRST; + d_node = eqc; + lookForNextTheory(); +} + +TNode GenericCandidateGeneratorClass::getNextCandidate(){ + Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); + /** No more */ + if(d_can_gen_id == THEORY_LAST) return TNode::null(); + /** Try with this theory */ + TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); + if( !cand.isNull() ) return cand; + lookForNextTheory(); + return getNextCandidate(); +} + +void GenericCandidateGeneratorClass::lookForNextTheory(){ + do{ /* look for the next available generator, where the element is */ + ++d_can_gen_id; + } while( + d_can_gen_id < THEORY_LAST && + (d_can_gen[d_can_gen_id] == NULL || + !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) + ); +} |