merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

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 ))
+          );
+}