/**
* 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
#ifndef __CVC4__NODE_BUILDER_H
#define __CVC4__NODE_BUILDER_H
+#include <iostream>
#include <vector>
#include <cstdlib>
#include <stdint.h>
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.
*/
// 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 */
** 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
}
#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 */
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();
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
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;
}
interactive_shell.cpp \
main.h \
main.cpp \
- usage.h \
util.cpp
cvc4_SOURCES =
+++ /dev/null
-/********************* */
-/*! \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 */
#define MK_EXPR EXPR_MANAGER->mkExpr
#undef MK_CONST
#define MK_CONST EXPR_MANAGER->mkConst
+#define UNSUPPORTED PARSER_STATE->unimplementedFeature
}/* parser::postinclude */
| /* 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
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';
+/********************* */
+/*! \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;
** \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
CnfProof(CVC4::prop::CnfStream* cnfStream);
};
-} /* CVC4 namespace*/
+} /* CVC4 namespace */
#endif /* __CVC4__CNF_PROOF_H */
/********************* */
-/*! \file sat_proof.h
+/*! \file proof.h
** \verbatim
** Original author: lianah
** Major contributors: none
#define __CVC4__PROOF_H
#include "util/options.h"
-//#define CVC4_PROOFS
#ifdef CVC4_PROOF
# define PROOF(x) if(Options::current()->proof) { x; }
+/********************* */
+/*! \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"
** \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
+/********************* */
+/*! \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"
* 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);
// 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;
break;
}
}
-
+
// Clear any leftover propagated equalities
d_propagatedEqualities.clear();
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];
return d_atomPreprocessingCache[assertion];
}
-void TheoryEngine::assertFact(TNode node)
+void TheoryEngine::assertFact(TNode node)
{
Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
// 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);
}
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;
}
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
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]);
}
}
}
- }
+ }
}
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
}
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];
Node explanation = theoryOf(explainingTheory)->explain((*find).second.node);
explainEqualities(explainingTheory, explanation, builder);
}
- }
+ }
}
}
}
+ if(incrementalSolving && proof) {
+ throw OptionException(string("The use of --incremental with --proof is not yet supported"));
+ }
+
return optind;
}
projects / cvc5.git / commitdiff