summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/command.cpp75
-rw-r--r--src/util/command.h50
-rw-r--r--src/util/options.h9
3 files changed, 117 insertions, 17 deletions
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 5a5b766cb..b80851233 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -20,8 +20,9 @@
* Author: dejan
*/
-#include <map>
+#include <sstream>
#include "util/command.h"
+#include "util/Assert.h"
#include "smt/smt_engine.h"
using namespace std;
@@ -29,10 +30,16 @@ using namespace std;
namespace CVC4 {
ostream& operator<<(ostream& out, const Command& c) {
- c.toString(out);
+ c.toStream(out);
return out;
}
+std::string Command::toString() const {
+ stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
EmptyCommand::EmptyCommand(string name) :
d_name(name) {
}
@@ -87,26 +94,26 @@ void CommandSequence::addCommand(Command* cmd) {
d_command_sequence.push_back(cmd);
}
-void EmptyCommand::toString(ostream& out) const {
+void EmptyCommand::toStream(ostream& out) const {
out << "EmptyCommand(" << d_name << ")";
}
-void AssertCommand::toString(ostream& out) const {
+void AssertCommand::toStream(ostream& out) const {
out << "Assert(" << d_expr << ")";
}
-void CheckSatCommand::toString(ostream& out) const {
+void CheckSatCommand::toStream(ostream& out) const {
if(d_expr.isNull())
out << "CheckSat()";
else
out << "CheckSat(" << d_expr << ")";
}
-void QueryCommand::toString(ostream& out) const {
+void QueryCommand::toStream(ostream& out) const {
out << "Query(" << d_expr << ")";
}
-void CommandSequence::toString(ostream& out) const {
+void CommandSequence::toStream(ostream& out) const {
out << "CommandSequence[" << endl;
for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) {
out << *d_command_sequence[i] << endl;
@@ -114,4 +121,58 @@ void CommandSequence::toString(ostream& out) const {
out << "]";
}
+DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+void DeclarationCommand::toStream(std::ostream& out) const {
+ out << "Declare(";
+ bool first = true;
+ for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
+ if(first) {
+ out << ", ";
+ first = false;
+ }
+ out << d_declaredSymbols[i];
+ }
+ out << ")";
+}
+
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+ d_status(status) {
+}
+
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // TODO: something to be done with the status
+}
+
+void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(";
+ switch(d_status) {
+ case SMT_SATISFIABLE:
+ out << "sat";
+ break;
+ case SMT_UNSATISFIABLE:
+ out << "unsat";
+ break;
+ case SMT_UNKNOWN:
+ out << "unknown";
+ break;
+ default:
+ Unhandled("Unknown benchmark status");
+ }
+ out << ")";
+}
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic)
+ {}
+
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // TODO: something to be done with the logic
+}
+
+void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
}/* CVC4 namespace */
diff --git a/src/util/command.h b/src/util/command.h
index 9cc009d01..b41be4592 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -35,14 +35,15 @@ class CVC4_PUBLIC Command {
public:
virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
virtual ~Command() {};
- virtual void toString(std::ostream&) const = 0;
+ 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 toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
private:
std::string d_name;
};/* class EmptyCommand */
@@ -52,18 +53,26 @@ class CVC4_PUBLIC AssertCommand : public Command {
public:
AssertCommand(const BoolExpr& e);
void invoke(CVC4::SmtEngine* smt_engine);
- void toString(std::ostream& out) const;
+ 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);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
};/* class CheckSatCommand */
@@ -73,19 +82,48 @@ class CVC4_PUBLIC QueryCommand : public Command {
public:
QueryCommand(const BoolExpr& e);
void invoke(SmtEngine* smt);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
protected:
BoolExpr d_expr;
};/* 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 QueryCommand */
+
+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 QueryCommand */
+
+
+
class CVC4_PUBLIC CommandSequence : public Command {
public:
CommandSequence();
~CommandSequence();
void invoke(SmtEngine* smt);
void addCommand(Command* cmd);
- void toString(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
private:
/** All the commands to be executed (in sequence) */
std::vector<Command*> d_command_sequence;
diff --git a/src/util/options.h b/src/util/options.h
index 2bfbf675f..d6c4e9009 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -13,11 +13,12 @@
** Global (command-line or equivalent) tuning parameters.
**/
-#include <iostream>
-
#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
+#include <iostream>
+#include "parser/parser.h"
+
namespace CVC4 {
struct Options {
@@ -48,7 +49,7 @@ struct Options {
};
/** The input language */
- InputLanguage lang;
+ parser::Parser::InputLanguage lang;
Options() : binary_name(),
smtcomp_mode(false),
@@ -56,7 +57,7 @@ struct Options {
out(0),
err(0),
verbosity(0),
- lang(LANG_AUTO)
+ lang(parser::Parser::LANG_AUTO)
{}
};/* struct Options */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback