summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_builder.h17
-rw-r--r--src/expr/node_value.cpp9
-rw-r--r--src/expr/node_value.h27
-rw-r--r--src/main/Makefile.am1
-rw-r--r--src/main/usage.h63
-rw-r--r--src/parser/smt2/Smt2.g9
-rw-r--r--src/proof/cnf_proof.cpp19
-rw-r--r--src/proof/cnf_proof.h3
-rw-r--r--src/proof/proof.h3
-rw-r--r--src/proof/proof_manager.cpp19
-rw-r--r--src/proof/proof_manager.h1
-rw-r--r--src/proof/sat_proof.cpp19
-rw-r--r--src/proof/sat_proof.h3
-rw-r--r--src/theory/theory_engine.cpp42
-rw-r--r--src/util/options.cpp4
16 files changed, 148 insertions, 93 deletions
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 <iostream>
#include <vector>
#include <cstdlib>
#include <stdint.h>
@@ -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 <unsigned nchild_thresh>
+std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb);
+
/**
* The main template NodeBuilder.
*/
@@ -720,6 +726,10 @@ public:
// private fields
template <unsigned N>
friend class NodeBuilder;
+
+ template <unsigned N>
+ friend std::ostream& operator<<(std::ostream& out, const NodeBuilder<N>& nb);
+
};/* class NodeBuilder<> */
}/* CVC4 namespace */
@@ -1151,7 +1161,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::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<expr::NodeValue*>(&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<nchild_thresh>::maybeCheckType(const TNode n) const
}
#endif /* CVC4_DEBUG */
+template <unsigned nchild_thresh>
+std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& 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<NodeValue*>(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<T>::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<PreRegisterVisitor>::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<SharedTermsVisitor>::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::TheoryTraits<THEORY>::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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback