diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 03:31:38 +0000 |
commit | fc14c009e8e9d2274368b54c12f3580a9ec8f718 (patch) | |
tree | 853fdc64b8f6f29dc106e581dfe8ed8e4c569778 /src/util | |
parent | 33988bd64b92960f7bed5c68d1266adc4183454b (diff) |
src/expr/kind.h is now automatically generated.
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 2 | ||||
-rw-r--r-- | src/util/command.cpp | 74 | ||||
-rw-r--r-- | src/util/command.h | 301 |
3 files changed, 0 insertions, 377 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 316c747de..9c3431499 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -10,8 +10,6 @@ libutil_la_SOURCES = \ Assert.cpp \ Makefile.am \ Makefile.in \ - command.cpp \ - command.h \ debug.h \ decision_engine.cpp \ decision_engine.h \ diff --git a/src/util/command.cpp b/src/util/command.cpp deleted file mode 100644 index 58f8b41bb..000000000 --- a/src/util/command.cpp +++ /dev/null @@ -1,74 +0,0 @@ -/********************* -*- C++ -*- */ -/** command.cpp - ** Original author: mdeters - ** Major contributors: dejan - ** 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. - ** - ** Implementation of command objects. - **/ - -#include "util/command.h" -#include "smt/smt_engine.h" - -using namespace std; - -namespace CVC4 { - -ostream& operator<<(ostream& out, const Command* c) { - if (c == NULL) { - out << "null"; - } else { - c->toStream(out); - } - return out; -} - -CommandSequence::~CommandSequence() { - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - delete d_commandSequence[i]; - } -} - -void CommandSequence::invoke(SmtEngine* smtEngine) { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine); - delete d_commandSequence[d_index]; - } -} - -void CheckSatCommand::toStream(ostream& out) const { - if(d_expr.isNull()) { - out << "CheckSat()"; - } else { - out << "CheckSat(" << d_expr << ")"; - } -} - -void CommandSequence::toStream(ostream& out) const { - out << "CommandSequence[" << endl; - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - out << *d_commandSequence[i] << endl; - } - out << "]"; -} - -void DeclarationCommand::toStream(std::ostream& out) const { - out << "Declare("; - bool first = true; - for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { - if(!first) { - out << ", "; - } - out << d_declaredSymbols[i]; - first = false; - } - out << ")"; -} - -}/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h deleted file mode 100644 index 81af801d1..000000000 --- a/src/util/command.h +++ /dev/null @@ -1,301 +0,0 @@ -/********************* -*- C++ -*- */ -/** command.h - ** Original author: mdeters - ** Major contributors: dejan - ** 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) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Implementation of the command pattern on SmtEngines. Command - ** objects are generated by the parser (typically) to implement the - ** commands in parsed input (see Parser::parseNextCommand()), or by - ** client code. - **/ - -#ifndef __CVC4__COMMAND_H -#define __CVC4__COMMAND_H - -#include <iostream> -#include <sstream> -#include <string> -#include <vector> - -#include "cvc4_config.h" -#include "expr/expr.h" -#include "util/result.h" - -namespace CVC4 { - -class SmtEngine; -class Command; - -inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; - -class CVC4_PUBLIC Command { -public: - virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; - virtual ~Command() {}; - virtual void toStream(std::ostream&) const = 0; - std::string toString() const; -};/* class Command */ - -class CVC4_PUBLIC EmptyCommand : public Command { -public: - EmptyCommand(std::string name = ""); - void invoke(CVC4::SmtEngine* smt_engine); - void toStream(std::ostream& out) const; -private: - std::string d_name; -};/* class EmptyCommand */ - -class CVC4_PUBLIC AssertCommand : public Command { -public: - AssertCommand(const BoolExpr& e); - void invoke(CVC4::SmtEngine* smt_engine); - void toStream(std::ostream& out) const; -protected: - BoolExpr d_expr; -};/* class AssertCommand */ - -class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { -public: - DeclarationCommand(const std::vector<std::string>& ids); - void toStream(std::ostream& out) const; -protected: - std::vector<std::string> d_declaredSymbols; -}; - -class CVC4_PUBLIC CheckSatCommand : public Command { -public: - CheckSatCommand(); - CheckSatCommand(const BoolExpr& e); - void invoke(SmtEngine* smt); - Result getResult(); - void toStream(std::ostream& out) const; -protected: - BoolExpr d_expr; - Result d_result; -};/* class CheckSatCommand */ - -class CVC4_PUBLIC QueryCommand : public Command { -public: - QueryCommand(const BoolExpr& e); - void invoke(SmtEngine* smt); - Result getResult(); - void toStream(std::ostream& out) const; -protected: - BoolExpr d_expr; - Result d_result; -};/* class QueryCommand */ - -class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { -public: - /** The status an SMT benchmark can have */ - enum BenchmarkStatus { - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN - }; - SetBenchmarkStatusCommand(BenchmarkStatus status); - void invoke(SmtEngine* smt); - void toStream(std::ostream& out) const; -protected: - BenchmarkStatus d_status; -};/* class SetBenchmarkStatusCommand */ - -inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus bs) - CVC4_PUBLIC; - -class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { -public: - SetBenchmarkLogicCommand(std::string logic); - void invoke(SmtEngine* smt); - void toStream(std::ostream& out) const; -protected: - std::string d_logic; -};/* class SetBenchmarkLogicCommand */ - -class CVC4_PUBLIC CommandSequence : public Command { -public: - CommandSequence(); - ~CommandSequence(); - void invoke(SmtEngine* smt); - void addCommand(Command* cmd); - void toStream(std::ostream& out) const; - - typedef std::vector<Command*>::iterator iterator; - typedef std::vector<Command*>::const_iterator const_iterator; - - const_iterator begin() const { return d_commandSequence.begin(); } - const_iterator end() const { return d_commandSequence.end(); } - - iterator begin() { return d_commandSequence.begin(); } - iterator end() { return d_commandSequence.end(); } - -private: - /** All the commands to be executed (in sequence) */ - std::vector<Command*> d_commandSequence; - /** Next command to be executed */ - unsigned int d_index; -};/* class CommandSequence */ - -}/* CVC4 namespace */ - -/* =========== inline function definitions =========== */ - -#include "smt/smt_engine.h" - -namespace CVC4 { - -inline std::ostream& operator<<(std::ostream& out, const Command& c) { - c.toStream(out); - return out; -} - -/* class Command */ - -inline std::string Command::toString() const { - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -/* class EmptyCommand */ - -inline EmptyCommand::EmptyCommand(std::string name) : - d_name(name) { -} - -inline void EmptyCommand::invoke(SmtEngine* smt_engine) { -} - -inline void EmptyCommand::toStream(std::ostream& out) const { - out << "EmptyCommand(" << d_name << ")"; -} - -/* class AssertCommand */ - -inline AssertCommand::AssertCommand(const BoolExpr& e) : - d_expr(e) { -} - -inline void AssertCommand::invoke(SmtEngine* smt_engine) { - smt_engine->assertFormula(d_expr); -} - -inline void AssertCommand::toStream(std::ostream& out) const { - out << "Assert(" << d_expr << ")"; -} - -/* class CheckSatCommand */ - -inline CheckSatCommand::CheckSatCommand() { -} - -inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) : - d_expr(e) { -} - -inline void CheckSatCommand::invoke(SmtEngine* smt_engine) { - d_result = smt_engine->checkSat(d_expr); -} - -inline Result CheckSatCommand::getResult() { - return d_result; -} - -/* class QueryCommand */ - -inline QueryCommand::QueryCommand(const BoolExpr& e) : - d_expr(e) { -} - -inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) { - d_result = smt_engine->query(d_expr); -} - -inline Result QueryCommand::getResult() { - return d_result; -} - -inline void QueryCommand::toStream(std::ostream& out) const { - out << "Query("; - d_expr.printAst(out, 0); - out << ")"; -} - -/* class CommandSequence */ - -inline CommandSequence::CommandSequence() : - d_index(0) { -} - -inline void CommandSequence::addCommand(Command* cmd) { - d_commandSequence.push_back(cmd); -} - -/* class DeclarationCommand */ - -inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) : - d_declaredSymbols(ids) { -} - -/* class SetBenchmarkStatusCommand */ - -inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) : - d_status(s) { -} - -inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) { - // FIXME: TODO: something to be done with the status -} - -inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkStatus(" << d_status << ")"; -} - -/* class SetBenchmarkLogicCommand */ - -inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) : - d_logic(l) { -} - -inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) { - // FIXME: TODO: something to be done with the logic -} - -inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { - out << "SetBenchmarkLogic(" << d_logic << ")"; -} - -/* output stream insertion operator for benchmark statuses */ -inline std::ostream& operator<<(std::ostream& out, - SetBenchmarkStatusCommand::BenchmarkStatus bs) { - switch(bs) { - - case SetBenchmarkStatusCommand::SMT_SATISFIABLE: - return out << "sat"; - - case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE: - return out << "unsat"; - - case SetBenchmarkStatusCommand::SMT_UNKNOWN: - return out << "unknown"; - - default: - return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]"; - } -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__COMMAND_H */ |