From 890bacd7cb11c6e991722e8a7b7cd0ef9147ea3b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 28 Oct 2011 20:30:24 +0000 Subject: [PATCH] * ability to output NodeBuilders without first converting them to Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup --- src/expr/node.h | 2 +- src/expr/node_builder.h | 17 +++++++++- src/expr/node_value.cpp | 9 +++++- src/expr/node_value.h | 27 +++++++++++++++- src/main/Makefile.am | 1 - src/main/usage.h | 63 ------------------------------------ src/parser/smt2/Smt2.g | 9 ++++++ src/proof/cnf_proof.cpp | 19 +++++++++++ src/proof/cnf_proof.h | 3 +- src/proof/proof.h | 3 +- src/proof/proof_manager.cpp | 19 +++++++++++ src/proof/proof_manager.h | 1 + src/proof/sat_proof.cpp | 19 +++++++++++ src/proof/sat_proof.h | 3 +- src/theory/theory_engine.cpp | 42 ++++++++++++------------ src/util/options.cpp | 4 +++ 16 files changed, 148 insertions(+), 93 deletions(-) delete mode 100644 src/main/usage.h diff --git a/src/expr/node.h b/src/expr/node.h index 0f4b55d4a..2751c96a8 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -211,7 +211,7 @@ class NodeTemplate { /** * Assigns the expression value and does reference counting. No assumptions - * are made on the expression, and should only be used if we know what we + * are made on the expression, and should only be used if we know what we * are doing. * * @param ev the expression value to assign diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 2cb2527b2..1914bb736 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -157,6 +157,7 @@ #ifndef __CVC4__NODE_BUILDER_H #define __CVC4__NODE_BUILDER_H +#include #include #include #include @@ -184,6 +185,11 @@ class OrNodeBuilder; class PlusNodeBuilder; class MultNodeBuilder; +// Sometimes it's useful for debugging to output a NodeBuilder that +// isn't yet a Node.. +template +std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); + /** * The main template NodeBuilder. */ @@ -720,6 +726,10 @@ public: // private fields template friend class NodeBuilder; + + template + friend std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); + };/* class NodeBuilder<> */ }/* CVC4 namespace */ @@ -1151,7 +1161,7 @@ expr::NodeValue* NodeBuilder::constructNV() const { ** allocated "inline" in this NodeBuilder. **/ // Lookup the expression value in the pool we already have - expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); + expr::NodeValue* poolNv = d_nm->poolLookup(const_cast(&d_inlineNv)); // If something else is there, we reuse it if(poolNv != NULL) { /* Subcase (a): The Node under construction already exists in @@ -1301,6 +1311,11 @@ inline void NodeBuilder::maybeCheckType(const TNode n) const } #endif /* CVC4_DEBUG */ +template +std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb) { + return out << *nb.d_nv; +} + }/* CVC4 namespace */ #endif /* __CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 5fe48b01d..f1fade69d 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -39,16 +39,23 @@ NodeValue NodeValue::s_null(0); string NodeValue::toString() const { stringstream ss; - toStream(ss); + toStream(ss, -1, false, Options::current()->outputLanguage); return ss.str(); } void NodeValue::toStream(std::ostream& out, int toDepth, bool types, OutputLanguage language) const { + // Ensure that this node value is live for the length of this call. + // It really breaks things badly if we don't have a nonzero ref + // count, even just for printing. + RefCountGuard guard(this); + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types); } void NodeValue::printAst(std::ostream& out, int ind) const { + RefCountGuard guard(this); + indent(out, ind); out << '('; out << getKind(); diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 71aa37926..95af57719 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -297,6 +297,30 @@ public: private: + class RefCountGuard { + NodeValue* d_nv; + public: + RefCountGuard(const NodeValue* nv) : + d_nv(const_cast(nv)) { + // inc() + if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) { + ++d_nv->d_rc; + } + } + ~RefCountGuard() { + // dec() without marking for deletion: we don't want to garbage + // collect this NodeValue if ours is the last reference to it. + // E.g., this can happen when debugging code calls the print + // routines below. As RefCountGuards are scoped on the stack, + // this should be fine---but not in multithreaded contexts! + if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) { + --d_nv->d_rc; + } + } + };/* NodeValue::RefCountGuard */ + + friend class RefCountGuard; + /** * Indents the given stream a given amount of spaces. * @param out the stream to indent @@ -464,7 +488,8 @@ inline T NodeValue::iterator::operator*() const { inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { nv.toStream(out, Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out)); + Node::printtypes::getPrintTypes(out), + Node::setlanguage::getLanguage(out)); return out; } diff --git a/src/main/Makefile.am b/src/main/Makefile.am index da3b5896a..78d468000 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -11,7 +11,6 @@ libmain_a_SOURCES = \ interactive_shell.cpp \ main.h \ main.cpp \ - usage.h \ util.cpp cvc4_SOURCES = diff --git a/src/main/usage.h b/src/main/usage.h deleted file mode 100644 index f0c7c7f08..000000000 --- a/src/main/usage.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file usage.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): cconway - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief The "usage" string for the CVC4 driver binary. - ** - ** The "usage" string for the CVC4 driver binary. - **/ - -#ifndef __CVC4__MAIN__USAGE_H -#define __CVC4__MAIN__USAGE_H - -namespace CVC4 { -namespace main { - -// no more % chars in here without being escaped; it's used as a -// printf() format string -const char usage[] = "\ -usage: %s [options] [input-file]\n\ -\n\ -Without an input file, or with `-', CVC4 reads from standard input.\n\ -\n\ -CVC4 options:\n\ - --lang | -L force input language (default is `auto'; see --lang help)\n\ - --version | -V identify this CVC4 binary\n\ - --help | -h this command line reference\n\ - --parse-only exit after parsing input\n\ - --mmap memory map file input\n\ - --show-config show CVC4 static configuration\n\ - --segv-nospin don't spin on segfault waiting for gdb\n\ - --lazy-type-checking type check expressions only when necessary (default)\n\ - --eager-type-checking type check expressions immediately on creation\n\ - --no-type-checking never type check expressions\n\ - --no-checking disable ALL semantic checks, including type checks \n\ - --strict-parsing fail on non-conformant inputs (SMT2 only)\n\ - --verbose | -v increase verbosity (repeatable)\n\ - --quiet | -q decrease verbosity (repeatable)\n\ - --trace | -t tracing for something (e.g. --trace pushpop)\n\ - --debug | -d debugging for something (e.g. --debug arith), implies -t\n\ - --stats give statistics on exit\n\ - --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\ - --print-expr-types print types with variables when printing exprs\n\ - --uf=morgan|tim select uninterpreted function theory implementation\n\ - --interactive run interactively\n\ - --no-interactive do not run interactively\n\ - --produce-models support the get-value command\n\ - --produce-assignments support the get-assignment command\n\ - --lazy-definition-expansion expand define-fun lazily\n - --proof\n"; - -}/* CVC4::main namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MAIN__USAGE_H */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a1a98ac9b..7fb671bb0 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -127,6 +127,7 @@ using namespace CVC4::parser; #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst +#define UNSUPPORTED PARSER_STATE->unimplementedFeature }/* parser::postinclude */ @@ -294,6 +295,12 @@ command returns [CVC4::Command* cmd = NULL] | /* get-assertions */ GET_ASSERTIONS_TOK { cmd = new GetAssertionsCommand; } + | /* get-proof */ + GET_PROOF_TOK + { UNSUPPORTED("get-proof command not yet supported"); } + | /* get-unsat-core */ + GET_UNSAT_CORE_TOK + { UNSUPPORTED("unsat cores not yet supported"); } | /* push */ PUSH_TOK ( k=INTEGER_LITERAL @@ -855,6 +862,8 @@ DEFINE_SORT_TOK : 'define-sort'; GET_VALUE_TOK : 'get-value'; GET_ASSIGNMENT_TOK : 'get-assignment'; GET_ASSERTIONS_TOK : 'get-assertions'; +GET_PROOF_TOK : 'get-proof'; +GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; ITE_TOK : 'ite'; LET_TOK : 'let'; diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 2bf146661..a8dc39765 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file cnf_proof.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cnf_proof.h" using namespace CVC4::prop; diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index c43c9fc62..c35b0dfff 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -3,6 +3,7 @@ ** \verbatim ** Original author: lianah ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -31,5 +32,5 @@ public: CnfProof(CVC4::prop::CnfStream* cnfStream); }; -} /* CVC4 namespace*/ +} /* CVC4 namespace */ #endif /* __CVC4__CNF_PROOF_H */ diff --git a/src/proof/proof.h b/src/proof/proof.h index f163a4ffd..3e5b54cc7 100644 --- a/src/proof/proof.h +++ b/src/proof/proof.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file sat_proof.h +/*! \file proof.h ** \verbatim ** Original author: lianah ** Major contributors: none @@ -20,7 +20,6 @@ #define __CVC4__PROOF_H #include "util/options.h" -//#define CVC4_PROOFS #ifdef CVC4_PROOF # define PROOF(x) if(Options::current()->proof) { x; } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d6dd7b73d..2d7432cbc 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file proof_manager.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "proof/proof_manager.h" #include "proof/sat_proof.h" #include "proof/cnf_proof.h" diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 5d8b9d271..c79d26fed 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -3,6 +3,7 @@ ** \verbatim ** Original author: lianah ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 095251da8..57bb96513 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file sat_proof.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "proof/sat_proof.h" #include "prop/minisat/core/Solver.h" diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 4f9ba8e4a..4641ea4cc 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -190,7 +190,8 @@ public: * Constructs the empty clause resolution from the final conflict * * @param conflict - */void finalizeProof(::Minisat::CRef conflict); + */ + void finalizeProof(::Minisat::CRef conflict); /// clause registration methods ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c03b09be2..e09e9f47f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -90,7 +90,7 @@ void TheoryEngine::preRegister(TNode preprocessed) { // Pre-register the terms in the atom bool multipleTheories = NodeVisitor::run(d_preRegistrationVisitor, preprocessed); if (multipleTheories) { - // Collect the shared terms if there are multipe theories + // Collect the shared terms if there are multipe theories NodeVisitor::run(d_sharedTermsVisitor, preprocessed); // Mark the multiple theories flag d_sharedTermsExist = true; @@ -173,7 +173,7 @@ void TheoryEngine::check(Theory::Effort effort) { break; } } - + // Clear any leftover propagated equalities d_propagatedEqualities.clear(); @@ -214,10 +214,10 @@ void TheoryEngine::combineTheories() { CareGraph theoryGraph; \ reinterpret_cast::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \ careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \ - } + } CVC4_FOR_EACH_THEORY; - + // Now add splitters for the ones we are interested in for (unsigned i = 0; i < careGraph.size(); ++ i) { const CarePair& carePair = careGraph[i]; @@ -505,7 +505,7 @@ Node TheoryEngine::preprocess(TNode assertion) { return d_atomPreprocessingCache[assertion]; } -void TheoryEngine::assertFact(TNode node) +void TheoryEngine::assertFact(TNode node) { Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; @@ -516,7 +516,7 @@ void TheoryEngine::assertFact(TNode node) // Assert the fact to the apropriate theory theoryOf(atom)->assertFact(node, true); - + // If any shared terms, notify the theories if (d_sharedTerms.hasSharedTerms(atom)) { SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); @@ -536,11 +536,11 @@ void TheoryEngine::assertFact(TNode node) } void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { - + Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl; d_propEngine->checkTime(); - + if(Dump.isOn("t-propagations")) { Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl << QueryCommand(literal.toExpr()) << std::endl; @@ -550,7 +550,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - + if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) { // If not an equality it must be a SAT literal so we enlist it, and it can only // be propagated by the theory that owns it, as it is the only one that got @@ -563,7 +563,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { if (d_propEngine->isSatLiteral(normalizedEquality)) { // If there is a literal, just enqueue it, same as above d_propagatedLiterals.push_back(normalizedEquality); - } + } // Otherwise, we assert it to all interested theories Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]); Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]); @@ -586,7 +586,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { } } } - } + } } theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { @@ -594,33 +594,33 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } -Node TheoryEngine::getExplanation(TNode node) +Node TheoryEngine::getExplanation(TNode node) { - Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; + Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; TNode atom = node.getKind() == kind::NOT ? node[0] : node; - + Node explanation; // The theory that has explaining to do Theory* theory = theoryOf(atom); if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) { SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST)); - if (find == d_sharedAssertions.end()) { + if (find == d_sharedAssertions.end()) { theory = theoryOf(atom); - } - } + } + } // Get the explanation explanation = theory->explain(node); - + // Explain any shared equalities that might be in the explanation if (d_sharedTermsExist) { NodeBuilder<> nb(kind::AND); explainEqualities(theory->getId(), explanation, nb); explanation = nb; } - + Assert(!explanation.isNull()); if(Dump.isOn("t-explanations")) { Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl @@ -657,7 +657,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) { - Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl; + Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl; if (literals.getKind() == kind::AND) { for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) { TNode literal = literals[i]; @@ -695,6 +695,6 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild Node explanation = theoryOf(explainingTheory)->explain((*find).second.node); explainEqualities(explainingTheory, explanation, builder); } - } + } } diff --git a/src/util/options.cpp b/src/util/options.cpp index c69db62a3..3e877c541 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -856,6 +856,10 @@ throw(OptionException) { } } + if(incrementalSolving && proof) { + throw OptionException(string("The use of --incremental with --proof is not yet supported")); + } + return optind; } -- 2.30.2