cleanup

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8e400468c94a637511cb77eddfa13935378917d3..c34d3ecba14f9acdd177aa27e278ae4fc2ea3bda 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -277,9 +277,6 @@ class CVC4_PUBLIC SmtEngine {
    * as often as you like.  Should be called whenever the final options
    * and logic for the problem are set (at least, those options that are
    * not permitted to change after assertions and queries are made).
-   *
-   * FIXME: Above comment not true. Please don't call this more than
-   * once. (6/14/2012 -- K)
    */
   void finalOptionsAreSet();
 

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index a56601b98c7d22f64f4b8237ba6dd8e93a0f8673..e46f3a4f81be3b2aa9956ca0f037ea849f8e5718 100644 (file)
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -41,7 +41,6 @@ operator SUBSET 2 "subset"
 operator MEMBER 2 "set membership"
 
 operator SET_SINGLETON 1 "singleton set"
-operator FINITE_SET 1: "finite set"
 
 typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
 typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 2675b73ebdb108d2d07e825dba4fa896af389857..70b757f0cc82d2ad46d8e543a91b656486a46403 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -378,7 +378,7 @@ void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 /******************** Model generation ********************/
 
 const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
-(TNode setterm, SettermElementsMap& settermElementsMap) {
+(TNode setterm, SettermElementsMap& settermElementsMap) const {
   SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
   bool alreadyCalculated = (it != settermElementsMap.end());
   if( !alreadyCalculated ) {
@@ -419,15 +419,6 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 }
 
 
-void printSet(std::ostream& out, const std::set<TNode>& elements) {
-  out << "{ ";
-  std::copy(elements.begin(),
-            elements.end(),
-            std::ostream_iterator<TNode>(out, ", ")
-            );
-  out << " }";
-}
-
 
 void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 
@@ -437,13 +428,13 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
   Assert(S.getType().isSet());
 
   Elements emptySetOfElements;
-  const Elements& saved = 
+  const Elements& saved =
     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ?
     emptySetOfElements :
     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
-  Debug("sets-model") << "[sets-model] saved :  ";
-  printSet(Debug("sets-model"), saved);
-  Debug("sets-model") << std::endl;
+  Debug("sets-model") << "[sets-model] saved :  { ";
+  BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
+  Debug("sets-model") << " }" << std::endl;
 
   if(S.getNumChildren() == 2) {
 
@@ -470,9 +461,9 @@ void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
       Unhandled();
     }
 
-    Debug("sets-model") << "[sets-model] cur   :  ";
-    printSet(Debug("sets-model"), cur);
-    Debug("sets-model") << std::endl;
+    Debug("sets-model") << "[sets-model] cur :  { ";
+    BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; }
+    Debug("sets-model") << " }" << std::endl;
 
     if(saved != cur) {
       Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved "
@@ -880,7 +871,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
 
 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality 
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
                    << " value = " << value << std::endl;
   if (value) {
     return d_theory.propagate(equality);
@@ -903,7 +894,7 @@ bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, b
 
 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag 
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
   if(value) {
     d_theory.d_termInfoManager->mergeTerms(t1, t2);

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index daf0843e5a5984f79b45656d88420183978cbba5..62274e1ce74c422d744ed184cf424f1cf9fcabdc 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -163,7 +163,7 @@ private:
   /** model generation and helper function */
   typedef std::set<TNode> Elements;
   typedef std::hash_map<TNode, Elements, TNodeHashFunction> SettermElementsMap;
-  const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap);
+  const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const;
   Node elementsToShape(Elements elements, TypeNode setType) const;
   void checkModel(const SettermElementsMap& settermElementsMap, TNode S) const;
 };/* class TheorySetsPrivate */

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6e0a71641ee36b2e5d0a1770e1c5c8bd7fabeace..405fceb6f1d77a454add470e0ae8f74f9a40279c 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -56,24 +56,14 @@ void TheoryModel::reset(){
 }
 
 Node TheoryModel::getValue(TNode n) const {
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) "
-                          << std::endl;
-
   //apply substitutions
   Node nn = d_substitutions.apply(n);
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) post-sub:"
-                          << nn << std::endl;
-
   //get value in model
   nn = getModelValue(nn);
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ) getmodelvalue: "
-                          << nn << std::endl;
-
   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
-
   Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
                           << nn << std::endl;
   return nn;
@@ -240,8 +230,6 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){
 
 /** add substitution */
 void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){
-  Debug("model-builder") << "TheoryModel::addSubstitution("<< x << ", " << t
-                         << ", invalidateCache = " << invalidateCache << ")\n";
   if( !d_substitutions.hasSubstitution( x ) ){
     d_substitutions.addSubstitution( x, t, invalidateCache );
   } else {

diff --git a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
index a7be520e414338ed71ef9ffae9d1cf5c7e3b633e..1ea3ea6b5b836b47e6528dec056769eb6a78bdf9 100644 (file)
--- a/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
+++ b/test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
@@ -17,7 +17,7 @@
 ;
 ; Resolution:
 ;   adding terms to d_pendingEverInserted was moved from addToPending()
-; to getLemma(). 
+; to getLemma().
 
 (set-logic QF_ALL_SUPPORTED)
 (set-info :status sat)