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

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