-CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant
-Institute for Mathematical Sciences, New York University.
+CVC4 is copyright (C) 2009, 2010, 2011 the ACSys research group at the
+Courant Institute for Mathematical Sciences, New York University.
All rights reserved.
CVC4 is open-source; distribution is under the terms of the modified BSD
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
--- Morgan Deters <mdeters@cs.nyu.edu> Thu, 04 Mar 2010 20:46:40 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Fri, 04 Feb 2011 14:56:41 -0500
CVC4 incorporates MiniSat code, excluded from the above copyright.
See src/sat/minisat. Its copyright:
if [ ! -e configure ]; then ./autogen.sh; fi
./configure competition --disable-shared --enable-static-binary
$(MAKE)
- mkdir -p cvc4-smtcomp-2010
- cp -p $(top_builddir)/bin/cvc4 cvc4-smtcomp-2010/run
- tar cfz cvc4-smtcomp-2010.tgz cvc4-smtcomp-2010
+ mkdir -p cvc4-smtcomp-2011
+ cp -p $(top_builddir)/bin/cvc4 cvc4-smtcomp-2011/run
+ tar cfz cvc4-smtcomp-2011.tgz cvc4-smtcomp-2011
done
build_type_suffix=
-for arg in cln staticbinary optimized debugsymbols statistics assertions tracing muzzle coverage profiling; do
+for arg in cln staticbinary optimized debugsymbols statistics replay assertions tracing muzzle coverage profiling; do
if eval [ -n '"${'$arg'+set}"' ]; then
if eval [ '"${'$arg'}"' -eq 0 ]; then
build_type_suffix=$build_type_suffix-no$arg
ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\{0,1\}'`
ac_cvc4_build_profile_set=yes
AC_MSG_NOTICE([CVC4: building profile $ac_option_build])
- for x in optimized statistics assertions tracing muzzle coverage profiling; do
+ for x in optimized statistics replay assertions tracing muzzle coverage profiling; do
if expr "$ac_option" : '.*-no'$x'$' >/dev/null || expr "$ac_option" : '.*-no'$x'-' >/dev/null; then
eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""'
fi
if test -z "${with_build+set}" -o "$with_build" = default; then
with_build=default
fi
-if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
+if test -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}" -a -z "${enable_statistics+set}" -a -z "${enable_replay+set}" -a -z "${with_gmp+set}" -a -z "${with_cln+set}"; then
custom_build_profile=no
else
custom_build_profile=yes
btargs="$btargs nostatistics"
fi
fi
+if test -n "${enable_replay+set}"; then
+ if test "$enable_replay" = yes; then
+ btargs="$btargs replay"
+ else
+ btargs="$btargs noreplay"
+ fi
+fi
AC_MSG_RESULT([$with_build])
AM_INIT_AUTOMAKE([1.11 no-define parallel-tests color-tests])
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
+ if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
+ if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=yes ; fi
+ if test -z "${enable_replay+set}" ; then enable_replay=yes ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
if test -z "${enable_statistics+set}" ; then enable_statistics=no ; fi
+ if test -z "${enable_replay+set}" ; then enable_replay=no ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=no ; fi
if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi
if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi
CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_STATISTICS_ON"
fi
+AC_MSG_CHECKING([whether the replay feature should be turned on in libcvc4])
+
+AC_ARG_ENABLE([replay],
+ [AS_HELP_STRING([--disable-replay],
+ [turn off the replay feature in libcvc4])])
+
+if test -z "${enable_replay+set}"; then
+ enable_replay=yes
+fi
+
+AC_MSG_RESULT([$enable_replay])
+
+if test "$enable_replay" = yes; then
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_REPLAY"
+fi
+
AC_MSG_CHECKING([whether to include assertions in build])
AC_ARG_ENABLE([assertions],
Optimized : $optimized
Debug symbols: $enable_debug_symbols
Statistics : $enable_statistics
+Replay : $enable_replay
Assertions : $enable_assertions
Tracing : $enable_tracing
Muzzle : $enable_muzzle
--- /dev/null
+/********************* */
+/*! \file expr_stream.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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 A stream interface for expressions
+ **
+ ** A stream interface for expressions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR_STREAM_H
+#define __CVC4__EXPR_STREAM_H
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+/**
+ * A pure-virtual stream interface for expressions. Can be used to
+ * communicate streams of expressions between different parts of CVC4.
+ */
+class CVC4_PUBLIC ExprStream {
+public:
+ /** Virtual destructor; this implementation does nothing. */
+ virtual ~ExprStream() {}
+
+ /**
+ * Get the next expression in the stream (advancing the stream
+ * pointer as a side effect.)
+ */
+ virtual Expr nextExpr() = 0;
+};/* class ExprStream */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_STREAM_H */
+
** Major contributors: mdeters
** Minor contributors (to current version): taking, cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
friend class ExprManager;
friend class TypeCheckingException;
friend std::ostream& operator<<(std::ostream& out, const Expr& e);
+ template <bool ref_count> friend class NodeTemplate;
};/* class Expr */
** Major contributors: dejan
** Minor contributors (to current version): taking, cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
*/
NodeTemplate(const NodeTemplate& node);
+ /**
+ * Allow Exprs to become Nodes. This permits flexible translation of
+ * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
+ * function in the public interface, or requiring lots of "friend"
+ * relationships.
+ */
+ NodeTemplate(const Expr& e);
+
/**
* Assignment operator for nodes, copies the relevant information from node
* to this node.
}
}
+template <bool ref_count>
+NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
+ Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
+ Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
+ d_nv = e.d_node->d_nv;
+ // shouldn't ever fail
+ Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
+ if(ref_count) {
+ d_nv->inc();
+ }
+}
+
template <bool ref_count>
NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
** \verbatim
** Original author: cconway
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
** 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
ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
/* Create parser with bogus input. */
d_parser = parserBuilder.withStringInput("").build();
-}
+}/* InteractiveShell::InteractiveShell() */
Command* InteractiveShell::readCommand() {
// d_lastParser = parser;
return cmd_seq;
-}
+}/* InteractiveShell::readCommand() */
+
+}/* CVC4 namespace */
-} // CVC4 namespace
/*! \file interactive_shell.h
** \verbatim
** Original author: cconway
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
namespace CVC4 {
- class Command;
- class ExprManager;
- class Options;
+class Command;
+class ExprManager;
+class Options;
- namespace parser {
- class Parser;
- }
+namespace parser {
+ class Parser;
+}/* CVC4::parser namespace */
class CVC4_PUBLIC InteractiveShell {
std::istream& d_in;
static const std::string INPUT_FILENAME;
public:
- InteractiveShell(ExprManager& exprManager,
- const Options& options);
+ InteractiveShell(ExprManager& exprManager, const Options& options);
+
+ /**
+ * Read a command from the interactive shell. This will read as
+ * many lines as necessary to parse a well-formed command.
+ */
+ Command* readCommand();
+
+ /**
+ * Return the internal parser being used.
+ */
+ parser::Parser* getParser() {
+ return d_parser;
+ }
+
+};/* class InteractiveShell */
- /** Read a command from the interactive shell. This will read as
- many lines as necessary to parse a well-formed command. */
- Command *readCommand();
-};
+}/* CVC4 namespace */
-} // CVC4 namespace
+#endif /* __CVC4__INTERACTIVE_SHELL_H */
-#endif // __CVC4__INTERACTIVE_SHELL_H
/*! \file main.cpp
** \verbatim
** Original author: mdeters
- ** Major contributors: taking, cconway
- ** Minor contributors (to current version): barrett, dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): barrett, dejan, taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
}
}
- if(!Configuration::isMuzzledBuild()) {
- OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
- Debug.getStream() << Expr::setlanguage(language);
- Trace.getStream() << Expr::setlanguage(language);
- Notice.getStream() << Expr::setlanguage(language);
- Chat.getStream() << Expr::setlanguage(language);
- Message.getStream() << Expr::setlanguage(language);
- Warning.getStream() << Expr::setlanguage(language);
+ OutputLanguage outLang = language::toOutputLanguage(options.inputLanguage);
+ // Determine which messages to show based on smtcomp_mode and verbosity
+ if(Configuration::isMuzzledBuild()) {
+ Debug.setStream(CVC4::null_os);
+ Trace.setStream(CVC4::null_os);
+ Notice.setStream(CVC4::null_os);
+ Chat.setStream(CVC4::null_os);
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ } else {
+ if(options.verbosity < 2) {
+ Chat.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 1) {
+ Notice.setStream(CVC4::null_os);
+ }
+ if(options.verbosity < 0) {
+ Message.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ }
+
+ Debug.getStream() << Expr::setlanguage(outLang);
+ Trace.getStream() << Expr::setlanguage(outLang);
+ Notice.getStream() << Expr::setlanguage(outLang);
+ Chat.getStream() << Expr::setlanguage(outLang);
+ Message.getStream() << Expr::setlanguage(outLang);
+ Warning.getStream() << Expr::setlanguage(outLang);
+ }
+
+ Parser* replayParser = NULL;
+ if( options.replayFilename != "" ) {
+ ParserBuilder replayParserBuilder(exprMgr, options.replayFilename, options);
+
+ if( options.replayFilename == "-") {
+ if( inputFromStdin ) {
+ throw OptionException("Replay file and input file can't both be stdin.");
+ }
+ replayParserBuilder.withStreamInput(cin);
+ }
+ replayParser = replayParserBuilder.build();
+ options.replayStream = new Parser::ExprStream(replayParser);
+ }
+ if( options.replayLog != NULL ) {
+ *options.replayLog << Expr::setlanguage(outLang) << Expr::setdepth(-1);
}
// Parse and execute commands until we are done
Command* cmd;
if( options.interactive ) {
- InteractiveShell shell(exprMgr,options);
+ InteractiveShell shell(exprMgr, options);
+ if(replayParser != NULL) {
+ // have the replay parser use the declarations input interactively
+ replayParser->useDeclarationsFrom(shell.getParser());
+ }
while((cmd = shell.readCommand())) {
doCommand(smt,cmd);
delete cmd;
}
Parser *parser = parserBuilder.build();
+ if(replayParser != NULL) {
+ // have the replay parser use the file's declarations
+ replayParser->useDeclarationsFrom(parser);
+ }
while((cmd = parser->nextCommand())) {
doCommand(smt, cmd);
delete cmd;
delete parser;
}
+ if( options.replayStream != NULL ) {
+ // this deletes the expression parser too
+ delete options.replayStream;
+ options.replayStream = NULL;
+ }
+
string result = smt.getInfo(":status").getValue();
int returnValue;
/*! \file parser.cpp
** \verbatim
** Original author: dejan
- ** Major contributors: mdeters, cconway
+ ** Major contributors: cconway, mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) :
d_exprManager(exprManager),
d_input(input),
+ d_declScopeAllocated(),
+ d_declScope(&d_declScopeAllocated),
d_done(false),
d_checksEnabled(true),
d_strictMode(strictMode) {
switch( type ) {
case SYM_VARIABLE: // Functions share var namespace
- return d_declScope.lookup(name);
+ return d_declScope->lookup(name);
default:
Unhandled(type);
Type Parser::getSort(const std::string& name) {
Assert( isDeclared(name, SYM_SORT) );
- Type t = d_declScope.lookupType(name);
+ Type t = d_declScope->lookupType(name);
return t;
}
Type Parser::getSort(const std::string& name,
const std::vector<Type>& params) {
Assert( isDeclared(name, SYM_SORT) );
- Type t = d_declScope.lookupType(name, params);
+ Type t = d_declScope->lookupType(name, params);
return t;
}
bool Parser::isDefinedFunction(const std::string& name) {
// more permissive in type than isFunction(), because defined
// functions can be zero-ary and declared functions cannot.
- return d_declScope.isBoundDefinedFunction(name);
+ return d_declScope->isBoundDefinedFunction(name);
}
/* Returns true if name is bound to a function returning boolean. */
void
Parser::defineVar(const std::string& name, const Expr& val) {
- d_declScope.bind(name, val);
+ d_declScope->bind(name, val);
Assert( isDeclared(name) );
}
void
Parser::defineFunction(const std::string& name, const Expr& val) {
- d_declScope.bindDefinedFunction(name, val);
+ d_declScope->bindDefinedFunction(name, val);
Assert( isDeclared(name) );
}
void
Parser::defineType(const std::string& name, const Type& type) {
- d_declScope.bindType(name, type);
+ d_declScope->bindType(name, type);
Assert( isDeclared(name, SYM_SORT) );
}
Parser::defineType(const std::string& name,
const std::vector<Type>& params,
const Type& type) {
- d_declScope.bindType(name, params, type);
+ d_declScope->bindType(name, params, type);
Assert( isDeclared(name, SYM_SORT) );
}
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
- return d_declScope.isBound(name);
+ return d_declScope->isBound(name);
case SYM_SORT:
- return d_declScope.isBoundType(name);
+ return d_declScope->isBoundType(name);
default:
Unhandled(type);
}
/*! \file parser.h
** \verbatim
** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
#include <set>
#include <list>
-#include "input.h"
-#include "parser_exception.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
+#include "expr/expr.h"
#include "expr/declaration_scope.h"
#include "expr/kind.h"
+#include "expr/expr_stream.h"
namespace CVC4 {
// Forward declarations
class BooleanType;
-class Expr;
class ExprManager;
class Command;
class FunctionType;
/** The input that we're parsing. */
Input *d_input;
- /** The symbol table */
- DeclarationScope d_declScope;
+ /**
+ * The declaration scope that is "owned" by this parser. May or
+ * may not be the current declaration scope in use.
+ */
+ DeclarationScope d_declScopeAllocated;
+
+ /**
+ * This current symbol table used by this parser. Initially points
+ * to d_declScopeAllocated, but can be changed (making this parser
+ * delegate its definitions and lookups to another parser).
+ * See useDeclarationsFrom().
+ */
+ DeclarationScope* d_declScope;
/** The name of the input file. */
// std::string d_filename;
d_input->parseError(msg);
}
- inline void pushScope() { d_declScope.pushScope(); }
- inline void popScope() { d_declScope.popScope(); }
-}; // class Parser
+ inline void pushScope() { d_declScope->pushScope(); }
+ inline void popScope() { d_declScope->popScope(); }
-} // namespace parser
+ /**
+ * Set the current symbol table used by this parser.
+ * From now on, this parser will perform its definitions and
+ * lookups in the declaration scope of the "parser" argument
+ * (but doesn't re-delegate if the other parser's declaration scope
+ * changes later). A NULL argument restores this parser's
+ * "primordial" declaration scope assigned at its creation. Calling
+ * p->useDeclarationsFrom(p) is a no-op.
+ *
+ * This feature is useful when e.g. reading out-of-band expression data:
+ * 1. Parsing --replay log files produced with --replay-log.
+ * 2. Perhaps a multi-query benchmark file is being single-stepped
+ * with intervening queries on stdin that must reference
+ *
+ * However, the feature must be used carefully. Pushes and pops
+ * should be performed with the correct current declaration scope.
+ * Care must be taken to match up declaration scopes, of course;
+ * If variables in the deferred-to parser go out of scope, the
+ * secondary parser will give errors that they are undeclared.
+ * Also, an outer-scope variable shadowed by an inner-scope one of
+ * the same name may be temporarily inaccessible.
+ *
+ * In short, caveat emptor.
+ */
+ void useDeclarationsFrom(Parser* parser) {
+ if(parser == NULL) {
+ d_declScope = &d_declScopeAllocated;
+ } else {
+ d_declScope = parser->d_declScope;
+ }
+ }
-} // namespace CVC4
+ /**
+ * An expression stream interface for a parser. This stream simply
+ * pulls expressions from the given Parser object.
+ *
+ * Here, the ExprStream base class allows a Parser (from the parser
+ * library) and core components of CVC4 (in the core library) to
+ * communicate without polluting the public interface or having them
+ * reach into private (undocumented) interfaces.
+ */
+ class ExprStream : public CVC4::ExprStream {
+ Parser* d_parser;
+ public:
+ ExprStream(Parser* parser) : d_parser(parser) {}
+ ~ExprStream() { delete d_parser; }
+ Expr nextExpr() { return d_parser->nextExpression(); }
+ };/* class Parser::ExprStream */
+};/* class Parser */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__PARSER__PARSER_STATE_H */
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
if(toDepth != 0) {
n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
types, language::output::LANG_SMTLIB_V2);
+ out << " ";
} else {
out << "(...)";
}
using namespace std;
using namespace CVC4::kind;
+#ifdef CVC4_REPLAY
+# define CVC4_USE_REPLAY true
+#else /* CVC4_REPLAY */
+# define CVC4_USE_REPLAY false
+#endif /* CVC4_REPLAY */
+
namespace CVC4 {
namespace prop {
CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar) :
- d_satSolver(satSolver), d_registrar(registrar) {
+ d_satSolver(satSolver),
+ d_registrar(registrar) {
}
void CnfStream::recordTranslation(TNode node) {
}
}
-
TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) :
CnfStream(satSolver, registrar) {
}
}
SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
- Debug("cnf") << "newLiteral(" << node << ")" << endl;
+ Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
// Get the literal for this node
SatLiteral lit;
d_translationCache[node].level = level;
d_translationCache[node.notNode()].level = level;
- // If it's a theory literal, store it for back queries
- if (theoryLiteral) {
+ // If it's a theory literal, need to store it for back queries
+ if ( theoryLiteral ||
+ ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ) {
d_nodeCache[lit] = node;
d_nodeCache[~lit] = node.notNode();
}
// Here, you can have it
Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
+
// have to keep track of this, because with the call to preRegister(),
// the cnf stream is re-entrant!
bool wasAssertingLemma = d_assertingLemma;
SatLiteral CnfStream::getLiteral(TNode node) {
TranslationCache::iterator find = d_translationCache.find(node);
+ Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
SatLiteral literal = find->second.literal;
Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
* Constructs a CnfStream that sends constructs an equi-satisfiable
* set of clauses and sends them to the given sat solver.
* @param satSolver the sat solver to use
+ * @param registrar the entity that takes care of preregistration of Nodes
*/
CnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
/**
* Constructs the stream to use the given sat solver.
* @param satSolver the sat solver to use
+ * @param registrar the entity that takes care of pre-registration of Nodes
*/
TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar);
Lit Solver::pickBranchLit()
{
+#ifdef CVC4_REPLAY
+ Lit nextLit = proxy->getNextReplayDecision();
+ if (nextLit != lit_Undef) {
+ return nextLit;
+ }
+#endif /* CVC4_REPLAY */
+
Var next = var_Undef;
// Random decision:
check_type = CHECK_WITHOUTH_PROPAGATION_FINAL;
continue;
}
+
+#ifdef CVC4_REPLAY
+ proxy->logDecision(next);
+#endif /* CVC4_REPLAY */
}
// Increase decision level and enqueue 'next'
/*! \file sat.cpp
** \verbatim
** Original author: cconway
- ** Major contributors: mdeters, taking
- ** Minor contributors (to current version): dejan
+ ** Major contributors: dejan, mdeters, taking
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
** \todo document this file
**/
-#include "cnf_stream.h"
-#include "prop_engine.h"
-#include "sat.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat.h"
#include "context/context.h"
#include "theory/theory_engine.h"
+#include "expr/expr_stream.h"
namespace CVC4 {
namespace prop {
d_theoryEngine->notifyRestart();
}
+SatLiteral SatSolver::getNextReplayDecision() {
+#ifdef CVC4_REPLAY
+ if(Options::current()->replayStream != NULL) {
+ Expr e = Options::current()->replayStream->nextExpr();
+ if(!e.isNull()) { // we get null node when out of decisions to replay
+ // convert & return
+ return d_cnfStream->getLiteral(e);
+ }
+ }
+ return Minisat::lit_Undef;
+#endif /* CVC4_REPLAY */
+}
+
+void SatSolver::logDecision(SatLiteral lit) {
+#ifdef CVC4_REPLAY
+ if(Options::current()->replayLog != NULL) {
+ Assert(lit != Minisat::lit_Undef, "logging an `undef' decision ?!");
+ *Options::current()->replayLog << d_cnfStream->getNode(lit) << std::endl;
+ }
+#endif /* CVC4_REPLAY */
+}
+
+
}/* CVC4::prop namespace */
}/* CVC4 namespace */
** Major contributors: taking, cconway, dejan
** Minor contributors (to current version): barrett
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
void notifyRestart();
+ SatLiteral getNextReplayDecision();
+
+ void logDecision(SatLiteral lit);
+
};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
#ifdef __CVC4_USE_MINISAT
-inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
- context::Context* context) :
+inline SatSolver::SatSolver(PropEngine* propEngine,
+ TheoryEngine* theoryEngine,
+ context::Context* context) :
d_propEngine(propEngine),
d_cnfStream(NULL),
d_theoryEngine(theoryEngine),
** Major contributors: none
** Minor contributors (to current version): acsys, cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
return IS_STATISTICS_BUILD;
}
+bool Configuration::isReplayBuild() {
+ return IS_REPLAY_BUILD;
+}
+
bool Configuration::isTracingBuild() {
return IS_TRACING_BUILD;
}
** Major contributors: none
** Minor contributors (to current version): acsys
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
static bool isStatisticsBuild();
+ static bool isReplayBuild();
+
static bool isTracingBuild();
static bool isMuzzledBuild();
/*! \file configuration_private.h
** \verbatim
** Original author: mdeters
- ** Major contributors: cconway, acsys
- ** Minor contributors (to current version): none
+ ** Major contributors: acsys
+ ** Minor contributors (to current version): cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
# define IS_STATISTICS_BUILD false
#endif /* CVC4_STATISTICS_ON */
+#ifdef CVC4_REPLAY
+# define IS_REPLAY_BUILD true
+#else /* CVC4_REPLAY */
+# define IS_REPLAY_BUILD false
+#endif /* CVC4_REPLAY */
+
#ifdef CVC4_TRACING
# define IS_TRACING_BUILD true
#else /* CVC4_TRACING */
/*! \file options.cpp
** \verbatim
** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): dejan, barrett
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): barrett, dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
incrementalSolving(false),
+ replayFilename(""),
+ replayStream(NULL),
+ replayLog(NULL),
rewriteArithEqualities(false),
satRandomFreq(0.0),
satRandomSeed(91648253), //Minisat's default value
--produce-models support the get-value command\n\
--produce-assignments support the get-assignment command\n\
--lazy-definition-expansion expand define-fun lazily\n\
+ --replay file replay decisions from file\n\
+ --replay-log file log decisions and propagations to file\n\
--pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\
--random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
--random-seed=S sets the random seed for the sat solver\n\
LAZY_TYPE_CHECKING,
EAGER_TYPE_CHECKING,
INCREMENTAL,
+ REPLAY,
+ REPLAY_LOG,
PIVOT_RULE,
RANDOM_FREQUENCY,
RANDOM_SEED,
{ "strict-parsing", no_argument , NULL, STRICT_PARSING },
{ "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
{ "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
- { "uf" , required_argument, NULL, UF_THEORY },
+ { "uf" , required_argument, NULL, UF_THEORY },
{ "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
{ "interactive", no_argument , NULL, INTERACTIVE },
{ "no-interactive", no_argument , NULL, NO_INTERACTIVE },
{ "produce-models", no_argument , NULL, PRODUCE_MODELS },
{ "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+ { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
+ { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
+ { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
+ { "incremental", no_argument , NULL, INCREMENTAL },
+ { "replay" , required_argument, NULL, REPLAY },
+ { "replay-log" , required_argument, NULL, REPLAY_LOG },
+ { "produce-models", no_argument , NULL, PRODUCE_MODELS },
+ { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
{ "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING },
{ "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
{ "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
- { "incremental", no_argument, NULL, INCREMENTAL },
{ "pivot-rule" , required_argument, NULL, PIVOT_RULE },
{ "random-freq" , required_argument, NULL, RANDOM_FREQUENCY },
{ "random-seed" , required_argument, NULL, RANDOM_SEED },
incrementalSolving = true;
break;
+ case REPLAY:
+#ifdef CVC4_REPLAY
+ if(optarg == NULL || *optarg == '\0') {
+ throw OptionException(string("Bad file name for --replay"));
+ } else {
+ replayFilename = optarg;
+ }
+#else /* CVC4_REPLAY */
+ throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+ break;
+
+ case REPLAY_LOG:
+#ifdef CVC4_REPLAY
+ if(optarg == NULL || *optarg == '\0') {
+ throw OptionException(string("Bad file name for --replay-log"));
+ } else if(!strcmp(optarg, "-")) {
+ replayLog = &cout;
+ } else {
+ replayLog = new ofstream(optarg, ofstream::out | ofstream::trunc);
+ if(!*replayLog) {
+ throw OptionException(string("Cannot open replay-log file: `") + optarg + "'");
+ }
+ }
+#else /* CVC4_REPLAY */
+ throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+ break;
+
case REWRITE_ARITHMETIC_EQUALITIES:
rewriteArithEqualities = true;
break;
printf("\n");
printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
+ printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
** \verbatim
** Original author: mdeters
** Major contributors: cconway
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** 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
#define __CVC4__OPTIONS_H
#include <iostream>
+#include <fstream>
#include <string>
#include "util/exception.h"
namespace CVC4 {
+class ExprStream;
+
/** Class representing an option-parsing exception. */
class OptionException : public CVC4::Exception {
public:
/** Whether incemental solving (push/pop) */
bool incrementalSolving;
+ /** Replay file to use (for decisions); empty if no replay file. */
+ std::string replayFilename;
+
+ /** Replay stream to use (for decisions); NULL if no replay file. */
+ ExprStream* replayStream;
+
+ /** Log to write replay instructions to; NULL if not logging. */
+ std::ostream* replayLog;
+
/** Whether to rewrite equalities in arithmetic theory */
bool rewriteArithEqualities;
-
/**
* Frequency for the sat solver to make random decisions.
* Should be between 0 and 1.
projects / cvc5.git / commitdiff