summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.h3
-rw-r--r--src/theory/sets/kinds1
-rw-r--r--src/theory/sets/theory_sets_private.cpp29
-rw-r--r--src/theory/sets/theory_sets_private.h2
-rw-r--r--src/theory/theory_model.cpp12
-rw-r--r--test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt22
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<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 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<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 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback