From e8021a81993fe5ed201e7fdaf7af007e4d9d012b Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 20 Mar 2014 19:27:21 -0400 Subject: [PATCH] cleanup --- src/smt/smt_engine.h | 3 -- src/theory/sets/kinds | 1 - src/theory/sets/theory_sets_private.cpp | 29 +++++++------------ src/theory/sets/theory_sets_private.h | 2 +- src/theory/theory_model.cpp | 12 -------- .../lemmabug-ListElts317minimized.smt2 | 2 +- 6 files changed, 12 insertions(+), 37 deletions(-) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8e400468c..c34d3ecba 100644 --- 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 a56601b98..e46f3a4f8 100644 --- 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 2675b73eb..70b757f0c 100644 --- 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& elements) { - out << "{ "; - std::copy(elements.begin(), - elements.end(), - std::ostream_iterator(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 daf0843e5..62274e1ce 100644 --- 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 Elements; typedef std::hash_map 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 6e0a71641..405fceb6f 100644 --- 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 a7be520e4..1ea3ea6b5 100644 --- 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) -- 2.30.2