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.h | |
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.h')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.h | 187 |
1 files changed, 187 insertions, 0 deletions
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h new file mode 100644 index 000000000..a6aa34a62 --- /dev/null +++ b/src/theory/quantifiers/candidate_generator.h @@ -0,0 +1,187 @@ +/********************* */ +/*! \file candidate_generator.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** 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 Theory uf candidate generator + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H + +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace inst { + +/** base class for generating candidates for matching */ +class CandidateGenerator { +public: + CandidateGenerator(){} + ~CandidateGenerator(){} + + /** Get candidates functions. These set up a context to get all match candidates. + cg->reset( eqc ); + do{ + Node cand = cg->getNextCandidate(); + //....... + }while( !cand.isNull() ); + + eqc is the equivalence class you are searching in + */ + virtual void reset( Node eqc ) = 0; + virtual Node getNextCandidate() = 0; + /** add candidate to list of nodes returned by this generator */ + virtual void addCandidate( Node n ) {} + /** call this at the beginning of each instantiation round */ + virtual void resetInstantiationRound() = 0; +public: + /** legal candidate */ + static bool isLegalCandidate( Node n ); +};/* class CandidateGenerator */ + +/** candidate generator queue (for manual candidate generation) */ +class CandidateGeneratorQueue : public CandidateGenerator { +private: + std::vector< Node > d_candidates; + int d_candidate_index; +public: + CandidateGeneratorQueue() : d_candidate_index( 0 ){} + ~CandidateGeneratorQueue(){} + + void addCandidate( Node n ); + + void resetInstantiationRound(){} + void reset( Node eqc ); + Node getNextCandidate(); +};/* class CandidateGeneratorQueue */ + +class CandidateGeneratorQEDisequal; + +#if 0 + +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + QuantifiersEngine* d_qe; + //the equality class iterator + eq::EqClassIterator d_eqc; + int d_term_iter; + int d_term_iter_limit; +private: + Node d_retNode; +public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); + ~CandidateGeneratorQE(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +#else + +class CandidateGeneratorQE : public CandidateGenerator +{ + friend class CandidateGeneratorQEDisequal; +private: + //operator you are looking for + Node d_op; + //instantiator pointer + QuantifiersEngine* d_qe; + //the equality class iterator + std::vector< Node > d_eqc; + int d_term_iter; + int d_term_iter_limit; + bool d_using_term_db; +public: + CandidateGeneratorQE( QuantifiersEngine* qe, Node op ); + ~CandidateGeneratorQE(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +#endif + +//class CandidateGeneratorQEDisequal : public CandidateGenerator +//{ +//private: +// //equivalence class +// Node d_eq_class; +// //equivalence class info +// EqClassInfo* d_eci; +// //equivalence class iterator +// EqClassInfo::BoolMap::const_iterator d_eqci_iter; +// //instantiator pointer +// QuantifiersEngine* d_qe; +//public: +// CandidateGeneratorQEDisequal( QuantifiersEngine* qe, Node eqc ); +// ~CandidateGeneratorQEDisequal(){} +// +// void resetInstantiationRound(); +// void reset( Node eqc ); //should be what you want to be disequal from +// Node getNextCandidate(); +//}; + +class CandidateGeneratorQELitEq : public CandidateGenerator +{ +private: + //the equality classes iterator + eq::EqClassesIterator d_eq; + //equality you are trying to match equalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitEq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +class CandidateGeneratorQELitDeq : public CandidateGenerator +{ +private: + //the equality class iterator for false + eq::EqClassIterator d_eqc_false; + //equality you are trying to match disequalities for + Node d_match_pattern; + //einstantiator pointer + QuantifiersEngine* d_qe; +public: + CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ); + ~CandidateGeneratorQELitDeq(){} + + void resetInstantiationRound(); + void reset( Node eqc ); + Node getNextCandidate(); +}; + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ |