diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_stream.h | 47 | ||||
-rw-r--r-- | src/expr/expr_template.h | 3 | ||||
-rw-r--r-- | src/expr/node.h | 22 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 9 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 44 | ||||
-rw-r--r-- | src/main/main.cpp | 74 | ||||
-rw-r--r-- | src/parser/parser.cpp | 26 | ||||
-rw-r--r-- | src/parser/parser.h | 86 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 | ||||
-rw-r--r-- | src/prop/cnf_stream.cpp | 19 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 11 | ||||
-rw-r--r-- | src/prop/sat.cpp | 36 | ||||
-rw-r--r-- | src/prop/sat.h | 11 | ||||
-rw-r--r-- | src/util/configuration.cpp | 6 | ||||
-rw-r--r-- | src/util/configuration.h | 4 | ||||
-rw-r--r-- | src/util/configuration_private.h | 12 | ||||
-rw-r--r-- | src/util/options.cpp | 54 | ||||
-rw-r--r-- | src/util/options.h | 17 |
19 files changed, 398 insertions, 88 deletions
diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h new file mode 100644 index 000000000..a6b99fb73 --- /dev/null +++ b/src/expr/expr_stream.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \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 */ + diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2e27b4f66..ba695355e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -5,7 +5,7 @@ ** 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 @@ -432,6 +432,7 @@ protected: 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 */ diff --git a/src/expr/node.h b/src/expr/node.h index 03840e670..d67bc2e2b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -5,7 +5,7 @@ ** 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 @@ -225,6 +225,14 @@ public: 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. * @param node the node to copy @@ -915,6 +923,18 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) { } 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!"); if(ref_count) { diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index f99eef4a1..dc9d0604d 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -3,7 +3,7 @@ ** \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 @@ -40,7 +40,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); -} +}/* InteractiveShell::InteractiveShell() */ Command* InteractiveShell::readCommand() { @@ -139,6 +139,7 @@ Command* InteractiveShell::readCommand() { // d_lastParser = parser; return cmd_seq; -} +}/* InteractiveShell::readCommand() */ + +}/* CVC4 namespace */ -} // CVC4 namespace diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index faa80fb84..a08e2cbb4 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -2,10 +2,10 @@ /*! \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 @@ -24,13 +24,13 @@ 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; @@ -41,14 +41,24 @@ class CVC4_PUBLIC InteractiveShell { 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 diff --git a/src/main/main.cpp b/src/main/main.cpp index 655562512..56c4bb422 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -2,10 +2,10 @@ /*! \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 @@ -228,20 +228,60 @@ int runCvc4(int argc, char* argv[]) { } } - 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; @@ -255,6 +295,10 @@ int runCvc4(int argc, char* argv[]) { } 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; @@ -263,6 +307,12 @@ int runCvc4(int argc, char* argv[]) { 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; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 90e13022c..0ebccf720 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -2,10 +2,10 @@ /*! \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 @@ -42,6 +42,8 @@ namespace parser { 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) { @@ -54,7 +56,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - return d_declScope.lookup(name); + return d_declScope->lookup(name); default: Unhandled(type); @@ -80,14 +82,14 @@ Parser::getType(const std::string& var_name, 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; } @@ -105,7 +107,7 @@ bool Parser::isFunction(const std::string& name) { 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. */ @@ -141,19 +143,19 @@ Parser::mkVars(const std::vector<std::string> names, 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) ); } @@ -161,7 +163,7 @@ void 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) ); } @@ -210,9 +212,9 @@ Parser::mkSorts(const std::vector<std::string>& names) { 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); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 9765f352b..15fe5126c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -2,10 +2,10 @@ /*! \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 @@ -25,16 +25,17 @@ #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; @@ -106,8 +107,19 @@ class CVC4_PUBLIC Parser { /** 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; @@ -361,12 +373,60 @@ public: 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 */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 1e36b211d..91a529bc2 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -5,7 +5,7 @@ ** 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 @@ -173,6 +173,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(toDepth != 0) { n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1, types, language::output::LANG_SMTLIB_V2); + out << " "; } else { out << "(...)"; } diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index fc7fa600a..6732b09bc 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -31,11 +31,18 @@ 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) { @@ -46,7 +53,6 @@ void CnfStream::recordTranslation(TNode node) { } } - TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registrar registrar) : CnfStream(satSolver, registrar) { } @@ -88,7 +94,7 @@ bool CnfStream::hasLiteral(TNode n) const { } 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; @@ -108,14 +114,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { 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; @@ -155,6 +163,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { 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; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 28b2cfb03..ef75e635b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -180,6 +180,7 @@ public: * 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); @@ -255,6 +256,7 @@ public: /** * 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); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index fd4b18222..10cd02f94 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -395,6 +395,13 @@ void Solver::popTrail() { 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: @@ -1051,6 +1058,10 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_WITHOUTH_PROPAGATION_FINAL; continue; } + +#ifdef CVC4_REPLAY + proxy->logDecision(next); +#endif /* CVC4_REPLAY */ } // Increase decision level and enqueue 'next' diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 1db7bf446..a6adecb1d 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -2,10 +2,10 @@ /*! \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 @@ -17,11 +17,12 @@ ** \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 { @@ -106,5 +107,28 @@ void SatSolver::notifyRestart() { 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 */ diff --git a/src/prop/sat.h b/src/prop/sat.h index b80b0f705..c00115cd8 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -5,7 +5,7 @@ ** 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 @@ -250,14 +250,19 @@ public: 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), diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 94ade5a52..afd30bba9 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -5,7 +5,7 @@ ** 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 @@ -40,6 +40,10 @@ bool Configuration::isStatisticsBuild() { return IS_STATISTICS_BUILD; } +bool Configuration::isReplayBuild() { + return IS_REPLAY_BUILD; +} + bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index 150354c29..3aae370d9 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -5,7 +5,7 @@ ** 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 @@ -43,6 +43,8 @@ public: static bool isStatisticsBuild(); + static bool isReplayBuild(); + static bool isTracingBuild(); static bool isMuzzledBuild(); diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h index c0ce86c97..4f7501a08 100644 --- a/src/util/configuration_private.h +++ b/src/util/configuration_private.h @@ -2,10 +2,10 @@ /*! \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 @@ -34,6 +34,12 @@ namespace CVC4 { # 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 */ diff --git a/src/util/options.cpp b/src/util/options.cpp index 88c8a2958..03dedfe00 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -2,10 +2,10 @@ /*! \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 @@ -77,6 +77,9 @@ Options::Options() : 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 @@ -111,6 +114,8 @@ static const string optionsDescription = "\ --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\ @@ -169,6 +174,8 @@ enum OptionValue { LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, INCREMENTAL, + REPLAY, + REPLAY_LOG, PIVOT_RULE, RANDOM_FREQUENCY, RANDOM_SEED, @@ -219,16 +226,23 @@ static struct option cmdlineOptions[] = { { "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 }, @@ -430,6 +444,35 @@ throw(OptionException) { 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; @@ -480,6 +523,7 @@ throw(OptionException) { 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"); diff --git a/src/util/options.h b/src/util/options.h index dc0d231bd..8273db458 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -3,9 +3,9 @@ ** \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 @@ -22,6 +22,7 @@ #define __CVC4__OPTIONS_H #include <iostream> +#include <fstream> #include <string> #include "util/exception.h" @@ -30,6 +31,8 @@ namespace CVC4 { +class ExprStream; + /** Class representing an option-parsing exception. */ class OptionException : public CVC4::Exception { public: @@ -128,10 +131,18 @@ struct CVC4_PUBLIC Options { /** 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. |