Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

1 files changed, 9 insertions, 9 deletions

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index b081e27ef..98ab3f10d 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -52,7 +52,7 @@ void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
 
 
 void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
-  Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; 
+  Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl;
 
   std::pair<TNode, TNode> search_pair(atom, term);
   SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
@@ -64,18 +64,18 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
     d_termsToTheories[search_pair] = theories;
   } else {
     Assert(theories != (*find).second);
-    d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); 
+    d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second);
   }
 }
 
 SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::begin(TNode atom) const {
   Assert(hasSharedTerms(atom));
-  return d_atomsToTerms.find(atom)->second.begin();  
+  return d_atomsToTerms.find(atom)->second.begin();
 }
 
 SharedTermsDatabase::shared_terms_iterator SharedTermsDatabase::end(TNode atom) const {
   Assert(hasSharedTerms(atom));
-  return d_atomsToTerms.find(atom)->second.end();  
+  return d_atomsToTerms.find(atom)->second.end();
 }
 
 bool SharedTermsDatabase::hasSharedTerms(TNode atom) const {
@@ -89,24 +89,24 @@ void SharedTermsDatabase::backtrack() {
     list.pop_back();
     if (list.empty()) {
       d_atomsToTerms.erase(atom);
-    } 
+    }
   }
   d_addedSharedTerms.resize(d_addedSharedTermsSize);
 }
 
 Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) const {
-  // Get the theories that share this term from this atom 
+  // Get the theories that share this term from this atom
   std::pair<TNode, TNode> search_pair(atom, term);
   SharedTermsTheoriesMap::iterator find = d_termsToTheories.find(search_pair);
-  Assert(find != d_termsToTheories.end());  
-  
+  Assert(find != d_termsToTheories.end());
+
   // Get the theories that were already notified
   Theory::Set alreadyNotified = 0;
   AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
   if (theoriesFind != d_alreadyNotifiedMap.end()) {
     alreadyNotified = (*theoriesFind).second;
   }
-  
+
   // Return the ones that haven't been notified yet
   return Theory::setDifference((*find).second, alreadyNotified);
 }