From: Kshitij Bansal Date: Tue, 8 Apr 2014 14:29:02 +0000 (-0400) Subject: some debugging changes X-Git-Tag: cvc5-1.0.0~6977^2~7 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b6d9f0bd9058db1358897834ac987f5d34de8734;p=cvc5.git some debugging changes --- diff --git a/src/Makefile.am b/src/Makefile.am index d75535e15..2d306d464 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -223,6 +223,7 @@ libcvc4_la_SOURCES = \ theory/datatypes/theory_datatypes.cpp \ theory/sets/expr_patterns.h \ theory/sets/options_handlers.h \ + theory/sets/scrutinize.h \ theory/sets/term_info.h \ theory/sets/theory_sets.cpp \ theory/sets/theory_sets.h \ diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h new file mode 100644 index 000000000..a0e2a1d5b --- /dev/null +++ b/src/theory/sets/scrutinize.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file scrutinize.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2013-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Check consistency of internal data structures. + ** + ** Some checks are very low-level with respect to TheorySetsPrivate + ** implementation, and hence might become outdated pretty quickly. + **/ + +#pragma once + +#include "theory/sets/theory_sets_private.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +class TheorySetsScrutinize { + TheorySetsPrivate* d_theory; +public: + TheorySetsScrutinize(TheorySetsPrivate* theory): d_theory(theory) { + Debug("sets") << "[sets] scrunitize enabled" << std::endl; + } + void postCheckInvariants() const { + Debug("sets-scrutinize") << "[sets-scrutinize] postCheckInvariants()" << std::endl; + + // assume not in conflict, and complete: + // - try building model + // - check it + } +}; + +}/* CVC4::theory::sets namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f487e1566..b29e2d4c6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -17,6 +17,7 @@ #include #include "theory/theory_model.h" +#include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" @@ -88,7 +89,10 @@ void TheorySetsPrivate::check(Theory::Effort level) { Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; Assert( d_conflict ^ d_equalityEngine.consistent() ); - if(d_conflict) return; + if(d_conflict) { + if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } + return; + } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } @@ -96,6 +100,8 @@ void TheorySetsPrivate::check(Theory::Effort level) { d_external.d_out->lemma(getLemma()); } + if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } + return; }/* TheorySetsPrivate::check() */ @@ -526,14 +532,28 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) TNode x = d_equalityEngine.getRepresentative(n[0]); TNode S = d_equalityEngine.getRepresentative(n[1]); settermElementsMap[S].insert(x); - if(Debug.isOn("sets-model-details")) { - vector explanation; - d_equalityEngine.explainPredicate(n, true, explanation); - Debug("sets-model-details") - << "[sets-model-details] > node: " << n << ", explanation:" << std::endl; - BOOST_FOREACH(TNode m, explanation) { - Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; - } + } + if(Debug.isOn("sets-model-details")) { + vector explanation; + d_equalityEngine.explainPredicate(n, true, explanation); + Debug("sets-model-details") + << "[sets-model-details] > node: " << n << ", explanation:" << std::endl; + BOOST_FOREACH(TNode m, explanation) { + Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; + } + } + } + + if(Debug.isOn("sets-model-details")) { + for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine); + ! it_eqclasses.isFinished() ; ++it_eqclasses) { + TNode n = (*it_eqclasses); + vector explanation; + d_equalityEngine.explainPredicate(n, false, explanation); + Debug("sets-model-details") + << "[sets-model-details] > node: not: " << n << ", explanation:" << std::endl; + BOOST_FOREACH(TNode m, explanation) { + Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; } } } @@ -585,8 +605,12 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) checkPassed &= checkModel(settermElementsMap, term); } } - Assert( checkPassed, - "THEORY_SETS check-model failed. Run with -d sets-model for details." ); + if(Debug.isOn("sets-checkmodel-ignore")) { + Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; + } else { + Assert( checkPassed, + "THEORY_SETS check-model failed. Run with -d sets-model for details." ); + } #endif } @@ -735,10 +759,10 @@ bool TheorySetsPrivate::isComplete() { Node TheorySetsPrivate::getLemma() { Assert(!d_pending.empty() || !d_pendingDisequal.empty()); - Node lemma; + Node n, lemma; if(!d_pending.empty()) { - Node n = d_pending.front(); + n = d_pending.front(); d_pending.pop(); d_pendingEverInserted.insert(n); @@ -747,7 +771,7 @@ Node TheorySetsPrivate::getLemma() { lemma = OR(n, NOT(n)); } else { - Node n = d_pendingDisequal.front(); + n = d_pendingDisequal.front(); d_pendingDisequal.pop(); d_pendingEverInserted.insert(n); @@ -758,7 +782,7 @@ Node TheorySetsPrivate::getLemma() { lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); } - Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl; + Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl; return lemma; } @@ -777,7 +801,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_nodeSaver(c), d_pending(u), d_pendingDisequal(u), - d_pendingEverInserted(u) + d_pendingEverInserted(u), + d_scrutinize(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); @@ -787,12 +812,20 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); + + if( Debug.isOn("sets-scrutinize") ) { + d_scrutinize = new TheorySetsScrutinize(this); + } }/* TheorySetsPrivate::TheorySetsPrivate() */ TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; + if( Debug.isOn("sets-scrutinize") ) { + Assert(d_scrutinize != NULL); + delete d_scrutinize; + } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 9576384bb..a4c9fb726 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -33,6 +33,7 @@ namespace sets { /** Internal classes, forward declared here */ class TheorySetsTermInfoManager; class TheorySets; +class TheorySetsScrutinize; class TheorySetsPrivate { public: @@ -166,6 +167,10 @@ private: const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const; Node elementsToShape(Elements elements, TypeNode setType) const; bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; + + // more debugging stuff + friend class TheorySetsScrutinize; + TheorySetsScrutinize* d_scrutinize; };/* class TheorySetsPrivate */