diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:07 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-24 12:52:21 -0500 |
commit | 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 (patch) | |
tree | 409009a6ab55986308cc73d030db53489beef26d /src/theory/quantifiers/candidate_generator.cpp | |
parent | 3eaf02c01e74a2a43b2eff7638d6c16171a11a13 (diff) |
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 6c6a80b90..e20f8c8e8 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -149,7 +149,7 @@ void CandidateGeneratorQELitEq::reset( Node eqc ){ d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); } Node CandidateGeneratorQELitEq::getNextCandidate(){ - while( d_eq.isFinished() ){ + while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; if( n.getType()==d_match_pattern[0].getType() ){ @@ -186,3 +186,29 @@ Node CandidateGeneratorQELitDeq::getNextCandidate(){ } return Node::null(); } + + +CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) : + d_match_pattern( mpat ), d_qe( qe ){ + +} + +void CandidateGeneratorQEAll::resetInstantiationRound() { + +} + +void CandidateGeneratorQEAll::reset( Node eqc ) { + d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() ); +} + +Node CandidateGeneratorQEAll::getNextCandidate() { + while( !d_eq.isFinished() ){ + Node n = (*d_eq); + ++d_eq; + if( n.getType()==d_match_pattern.getType() ){ + //an equivalence class with the same type as the pattern, return it + return n; + } + } + return Node::null(); +}
\ No newline at end of file |