summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp402
-rw-r--r--src/expr/command.h334
-rw-r--r--src/expr/expr_manager_template.cpp4
-rw-r--r--src/expr/expr_manager_template.h6
-rw-r--r--src/expr/expr_template.cpp4
-rw-r--r--src/expr/expr_template.h5
-rw-r--r--src/expr/metakind_template.h2
-rw-r--r--src/expr/node_manager.h13
8 files changed, 527 insertions, 243 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 6c466a74c..a1486fcab 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -16,13 +16,24 @@
** Implementation of command objects.
**/
+#include <iostream>
+#include <vector>
+#include <utility>
+#include <iterator>
+
#include "expr/command.h"
#include "smt/smt_engine.h"
+#include "util/output.h"
using namespace std;
namespace CVC4 {
+std::ostream& operator<<(std::ostream& out, const Command& c) {
+ c.toStream(out);
+ return out;
+}
+
ostream& operator<<(ostream& out, const Command* command) {
if(command == NULL) {
out << "null";
@@ -32,12 +43,136 @@ ostream& operator<<(ostream& out, const Command* command) {
return out;
}
+/* class Command */
+
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
+ invoke(smtEngine);
+ printResult(out);
+}
+
+std::string Command::toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+void Command::printResult(std::ostream& out) const {
+}
+
+/* class EmptyCommand */
+
+EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
+}
+
+void EmptyCommand::invoke(SmtEngine* smtEngine) {
+ /* empty commands have no implementation */
+}
+
+void EmptyCommand::toStream(std::ostream& out) const {
+ out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+AssertCommand::AssertCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+void AssertCommand::invoke(SmtEngine* smtEngine) {
+ smtEngine->assertFormula(d_expr);
+}
+
+void AssertCommand::toStream(std::ostream& out) const {
+ out << "Assert(" << d_expr << ")";
+}
+
+/* class PushCommand */
+
+void PushCommand::invoke(SmtEngine* smtEngine) {
+ smtEngine->push();
+}
+
+void PushCommand::toStream(std::ostream& out) const {
+ out << "Push()";
+}
+
+/* class PopCommand */
+
+void PopCommand::invoke(SmtEngine* smtEngine) {
+ smtEngine->pop();
+}
+
+void PopCommand::toStream(std::ostream& out) const {
+ out << "Pop()";
+}
+
+/* class CheckSatCommand */
+
+CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
+ d_expr(expr) {
+}
+
+void CheckSatCommand::invoke(SmtEngine* smtEngine) {
+ d_result = smtEngine->checkSat(d_expr);
+}
+
+void CheckSatCommand::toStream(std::ostream& out) const {
+ if(d_expr.isNull()) {
+ out << "CheckSat()";
+ } else {
+ out << "CheckSat(" << d_expr << ")";
+ }
+}
+
+Result CheckSatCommand::getResult() const {
+ return d_result;
+}
+
+void CheckSatCommand::printResult(std::ostream& out) const {
+ out << d_result << endl;
+}
+
+/* class QueryCommand */
+
+QueryCommand::QueryCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+void QueryCommand::invoke(SmtEngine* smtEngine) {
+ d_result = smtEngine->query(d_expr);
+}
+
+Result QueryCommand::getResult() const {
+ return d_result;
+}
+
+void QueryCommand::printResult(std::ostream& out) const {
+ out << d_result << endl;
+}
+
+void QueryCommand::toStream(std::ostream& out) const {
+ out << "Query(";
+ d_expr.printAst(out, 0);
+ out << ")";
+}
+
+/* class CommandSequence */
+
+CommandSequence::CommandSequence() :
+ d_index(0) {
+}
+
CommandSequence::~CommandSequence() {
for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
delete d_commandSequence[i];
}
}
+void CommandSequence::addCommand(Command* cmd) {
+ d_commandSequence.push_back(cmd);
+}
+
void CommandSequence::invoke(SmtEngine* smtEngine) {
for(; d_index < d_commandSequence.size(); ++d_index) {
d_commandSequence[d_index]->invoke(smtEngine);
@@ -45,11 +180,10 @@ void CommandSequence::invoke(SmtEngine* smtEngine) {
}
}
-void CheckSatCommand::toStream(std::ostream& out) const {
- if(d_expr.isNull()) {
- out << "CheckSat()";
- } else {
- out << "CheckSat(" << d_expr << ")";
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine, out);
+ delete d_commandSequence[d_index];
}
}
@@ -61,33 +195,257 @@ void CommandSequence::toStream(std::ostream& out) const {
out << "]";
}
+/* class DeclarationCommand */
+
+DeclarationCommand::DeclarationCommand(const std::string& id, Type t) :
+ d_type(t) {
+ d_declaredSymbols.push_back(id);
+}
+
+DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type t) :
+ d_declaredSymbols(ids),
+ d_type(t) {
+}
+
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 << "Declare([";
+ copy( d_declaredSymbols.begin(), d_declaredSymbols.end() - 1,
+ ostream_iterator<string>(out, ", ") );
+ out << d_declaredSymbols.back();
+ out << "])";
+}
+
+/* class DefineFunctionCommand */
+
+DefineFunctionCommand::DefineFunctionCommand(const std::string& name,
+ const std::vector<std::pair<std::string, Type> >& args,
+ Type type,
+ Expr formula) :
+ d_name(name),
+ d_args(args),
+ d_type(type),
+ d_formula(formula) {
+}
+
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
+ smtEngine->defineFunction(d_name, d_args, d_type, d_formula);
+}
+
+void DefineFunctionCommand::toStream(std::ostream& out) const {
+ out << "DefineFunction( \"" << d_name << "\", [";
+ copy( d_args.begin(), d_args.end() - 1,
+ ostream_iterator<std::pair<std::string, Type> >(out, ", ") );
+ out << d_args.back();
+ out << "], << " << d_type << " >>, << " << d_formula << " >> )";
+}
+
+/* class GetValueCommand */
+
+GetValueCommand::GetValueCommand(Expr term) :
+ d_term(term) {
+}
+
+void GetValueCommand::invoke(SmtEngine* smtEngine) {
+ d_result = smtEngine->getValue(d_term);
+}
+
+Expr GetValueCommand::getResult() const {
+ return d_result;
+}
+
+void GetValueCommand::printResult(std::ostream& out) const {
+ out << d_result << endl;
+}
+
+void GetValueCommand::toStream(std::ostream& out) const {
+ out << "GetValue( << " << d_term << " >> )";
+}
+
+/* class GetAssertionsCommand */
+
+GetAssertionsCommand::GetAssertionsCommand() {
+}
+
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
+ stringstream ss;
+ const vector<Expr> v = smtEngine->getAssertions();
+ copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+ d_result = ss.str();
+}
+
+std::string GetAssertionsCommand::getResult() const {
+ return d_result;
+}
+
+void GetAssertionsCommand::printResult(std::ostream& out) const {
+ out << d_result;
+}
+
+void GetAssertionsCommand::toStream(std::ostream& out) const {
+ out << "GetAssertions()";
+}
+
+/* class SetBenchmarkStatusCommand */
+
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+ d_status(status) {
+}
+
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
+ // FIXME: TODO: something to be done with the status
+}
+
+void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
+ d_logic(logic) {
+}
+
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
+ // FIXME: TODO: something to be done with the logic
+}
+
+void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* class SetInfoCommand */
+
+SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
+ d_flag(flag),
+ d_sexpr(sexpr) {
+}
+
+void SetInfoCommand::invoke(SmtEngine* smtEngine) {
+ try {
+ smtEngine->setInfo(d_flag, d_sexpr);
+ //d_result = "success";
+ } catch(BadOption& bo) {
+ d_result = "unsupported";
}
- out << ")";
}
-void PushCommand::invoke(SmtEngine* smtEngine) {
- smtEngine->push();
+std::string SetInfoCommand::getResult() const {
+ return d_result;
}
-void PushCommand::toStream(std::ostream& out) const {
- out << "Push()";
+void SetInfoCommand::printResult(std::ostream& out) const {
+ if(d_result != "") {
+ out << d_result << endl;
+ }
}
-void PopCommand::invoke(SmtEngine* smtEngine) {
- smtEngine->pop();
+void SetInfoCommand::toStream(std::ostream& out) const {
+ out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
}
-void PopCommand::toStream(std::ostream& out) const {
- out << "Pop()";
+/* class GetInfoCommand */
+
+GetInfoCommand::GetInfoCommand(std::string flag) :
+ d_flag(flag) {
+}
+
+void GetInfoCommand::invoke(SmtEngine* smtEngine) {
+ try {
+ d_result = smtEngine->getInfo(d_flag).getValue();
+ } catch(BadOption& bo) {
+ d_result = "unsupported";
+ }
+}
+
+std::string GetInfoCommand::getResult() const {
+ return d_result;
+}
+
+void GetInfoCommand::printResult(std::ostream& out) const {
+ if(d_result != "") {
+ out << d_result << endl;
+ }
+}
+
+void GetInfoCommand::toStream(std::ostream& out) const {
+ out << "GetInfo(" << d_flag << ")";
+}
+
+/* class SetOptionCommand */
+
+SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) :
+ d_flag(flag),
+ d_sexpr(sexpr) {
+}
+
+void SetOptionCommand::invoke(SmtEngine* smtEngine) {
+ try {
+ smtEngine->setOption(d_flag, d_sexpr);
+ //d_result = "success";
+ } catch(BadOption& bo) {
+ d_result = "unsupported";
+ }
+}
+
+std::string SetOptionCommand::getResult() const {
+ return d_result;
+}
+
+void SetOptionCommand::printResult(std::ostream& out) const {
+ if(d_result != "") {
+ out << d_result << endl;
+ }
+}
+
+void SetOptionCommand::toStream(std::ostream& out) const {
+ out << "SetOption(" << d_flag << ", " << d_sexpr << ")";
+}
+
+/* class GetOptionCommand */
+
+GetOptionCommand::GetOptionCommand(std::string flag) :
+ d_flag(flag) {
+}
+
+void GetOptionCommand::invoke(SmtEngine* smtEngine) {
+ try {
+ d_result = smtEngine->getOption(d_flag).getValue();
+ } catch(BadOption& bo) {
+ d_result = "unsupported";
+ }
+}
+
+std::string GetOptionCommand::getResult() const {
+ return d_result;
+}
+
+void GetOptionCommand::printResult(std::ostream& out) const {
+ if(d_result != "") {
+ out << d_result << endl;
+ }
+}
+
+void GetOptionCommand::toStream(std::ostream& out) const {
+ out << "GetOption(" << d_flag << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+std::ostream& operator<<(std::ostream& out,
+ BenchmarkStatus status) {
+ switch(status) {
+
+ case SMT_SATISFIABLE:
+ return out << "sat";
+
+ case SMT_UNSATISFIABLE:
+ return out << "unsat";
+
+ case SMT_UNKNOWN:
+ return out << "unknown";
+
+ default:
+ return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+ }
}
}/* CVC4 namespace */
diff --git a/src/expr/command.h b/src/expr/command.h
index 388ad62e6..0c78dd1c6 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -39,7 +39,7 @@ 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;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
/** The status an SMT benchmark can have */
@@ -52,115 +52,203 @@ enum BenchmarkStatus {
SMT_UNKNOWN
};
-inline std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status)
- CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out,
+ BenchmarkStatus status) CVC4_PUBLIC;
class CVC4_PUBLIC Command {
public:
- virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+ virtual void invoke(SmtEngine* smtEngine) = 0;
+ virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
virtual ~Command() {};
virtual void toStream(std::ostream&) const = 0;
std::string toString() const;
+ virtual void printResult(std::ostream& out) const;
};/* class Command */
+/**
+ * EmptyCommands (and its subclasses) are the residue of a command
+ * after the parser handles them (and there's nothing left to do).
+ */
class CVC4_PUBLIC EmptyCommand : public Command {
+protected:
+ std::string d_name;
public:
EmptyCommand(std::string name = "");
- void invoke(CVC4::SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
-private:
- std::string d_name;
};/* class EmptyCommand */
class CVC4_PUBLIC AssertCommand : public Command {
+protected:
+ BoolExpr d_expr;
public:
AssertCommand(const BoolExpr& e);
- void invoke(CVC4::SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
-protected:
- BoolExpr d_expr;
};/* class AssertCommand */
class CVC4_PUBLIC PushCommand : public Command {
public:
- void invoke(CVC4::SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
};/* class PushCommand */
class CVC4_PUBLIC PopCommand : public Command {
public:
- void invoke(CVC4::SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
};/* class PopCommand */
-
class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
-public:
- DeclarationCommand(const std::string& id, const Type& t);
- DeclarationCommand(const std::vector<std::string>& ids, const Type& t);
- void toStream(std::ostream& out) const;
protected:
std::vector<std::string> d_declaredSymbols;
Type d_type;
-};
+public:
+ DeclarationCommand(const std::string& id, Type t);
+ DeclarationCommand(const std::vector<std::string>& ids, Type t);
+ void toStream(std::ostream& out) const;
+};/* class DeclarationCommand */
-class CVC4_PUBLIC CheckSatCommand : public Command {
+class CVC4_PUBLIC DefineFunctionCommand : public Command {
+protected:
+ std::string d_name;
+ std::vector<std::pair<std::string, Type> > d_args;
+ Type d_type;
+ Expr d_formula;
public:
- CheckSatCommand(const BoolExpr& expr);
- void invoke(SmtEngine* smt);
- Result getResult();
+ DefineFunctionCommand(const std::string& name,
+ const std::vector<std::pair<std::string, Type> >& args,
+ Type type, Expr formula);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
+};/* class DefineFunctionCommand */
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
protected:
BoolExpr d_expr;
Result d_result;
+public:
+ CheckSatCommand(const BoolExpr& expr);
+ void invoke(SmtEngine* smtEngine);
+ Result getResult() const;
+ void printResult(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
};/* 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;
+public:
+ QueryCommand(const BoolExpr& e);
+ void invoke(SmtEngine* smtEngine);
+ Result getResult() const;
+ void printResult(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
};/* class QueryCommand */
-class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+class CVC4_PUBLIC GetValueCommand : public Command {
+protected:
+ Expr d_term;
+ Expr d_result;
public:
- SetBenchmarkStatusCommand(BenchmarkStatus status);
- void invoke(SmtEngine* smt);
+ GetValueCommand(Expr term);
+ void invoke(SmtEngine* smtEngine);
+ Expr getResult() const;
+ void printResult(std::ostream& out) const;
+ void toStream(std::ostream& out) const;
+};/* class GetValueCommand */
+
+class CVC4_PUBLIC GetAssertionsCommand : public Command {
+protected:
+ std::string d_result;
+public:
+ GetAssertionsCommand();
+ void invoke(SmtEngine* smtEngine);
+ std::string getResult() const;
+ void printResult(std::ostream& out) const;
void toStream(std::ostream& out) const;
+};/* class GetAssertionsCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
protected:
BenchmarkStatus d_status;
+public:
+ SetBenchmarkStatusCommand(BenchmarkStatus status);
+ void invoke(SmtEngine* smtEngine);
+ void toStream(std::ostream& out) const;
};/* class SetBenchmarkStatusCommand */
-
class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+protected:
+ std::string d_logic;
public:
SetBenchmarkLogicCommand(std::string logic);
- void invoke(SmtEngine* smt);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
-protected:
- std::string d_logic;
};/* class SetBenchmarkLogicCommand */
class CVC4_PUBLIC SetInfoCommand : public Command {
+protected:
+ std::string d_flag;
+ SExpr d_sexpr;
+ std::string d_result;
public:
SetInfoCommand(std::string flag, SExpr& sexpr);
- void invoke(SmtEngine* smt);
+ void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
+ std::string getResult() const;
+ void printResult(std::ostream& out) const;
+};/* class SetInfoCommand */
+
+class CVC4_PUBLIC GetInfoCommand : public Command {
+protected:
+ std::string d_flag;
+ std::string d_result;
+public:
+ GetInfoCommand(std::string flag);
+ void invoke(SmtEngine* smtEngine);
+ void toStream(std::ostream& out) const;
+ std::string getResult() const;
+ void printResult(std::ostream& out) const;
+};/* class GetInfoCommand */
+
+class CVC4_PUBLIC SetOptionCommand : public Command {
protected:
std::string d_flag;
SExpr d_sexpr;
-};/* class SetInfoCommand */
+ std::string d_result;
+public:
+ SetOptionCommand(std::string flag, SExpr& sexpr);
+ void invoke(SmtEngine* smtEngine);
+ void toStream(std::ostream& out) const;
+ std::string getResult() const;
+ void printResult(std::ostream& out) const;
+};/* class SetOptionCommand */
+
+class CVC4_PUBLIC GetOptionCommand : public Command {
+protected:
+ std::string d_flag;
+ std::string d_result;
+public:
+ GetOptionCommand(std::string flag);
+ void invoke(SmtEngine* smtEngine);
+ void toStream(std::ostream& out) const;
+ std::string getResult() const;
+ void printResult(std::ostream& out) const;
+};/* class GetOptionCommand */
class CVC4_PUBLIC CommandSequence : public Command {
+private:
+ /** All the commands to be executed (in sequence) */
+ std::vector<Command*> d_commandSequence;
+ /** Next command to be executed */
+ unsigned int d_index;
public:
CommandSequence();
~CommandSequence();
- void invoke(SmtEngine* smt);
+ void invoke(SmtEngine* smtEngine);
+ void invoke(SmtEngine* smtEngine, std::ostream& out);
void addCommand(Command* cmd);
void toStream(std::ostream& out) const;
@@ -172,178 +260,8 @@ public:
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* smtEngine) {
-}
-
-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* smtEngine) {
- smtEngine->assertFormula(d_expr);
-}
-
-inline void AssertCommand::toStream(std::ostream& out) const {
- out << "Assert(" << d_expr << ")";
-}
-
-/* class CheckSatCommand */
-
-inline CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
- d_expr(expr) {
-}
-
-inline void CheckSatCommand::invoke(SmtEngine* smtEngine) {
- d_result = smtEngine->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* smtEngine) {
- d_result = smtEngine->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::string& id, const Type& t) :
- d_type(t)
-{
- d_declaredSymbols.push_back(id);
-}
-
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) :
- d_declaredSymbols(ids),
- d_type(t)
-{
-}
-
-/* class SetBenchmarkStatusCommand */
-
-inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
- d_status(status) {
-}
-
-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 logic) :
- d_logic(logic) {
-}
-
-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 << ")";
-}
-
-inline SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
- d_flag(flag),
- d_sexpr(sexpr) {
-}
-
-inline void SetInfoCommand::invoke(SmtEngine* smt) { }
-
-inline void SetInfoCommand::toStream(std::ostream& out) const {
- out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
-}
-
-/* output stream insertion operator for benchmark statuses */
-inline std::ostream& operator<<(std::ostream& out,
- BenchmarkStatus status) {
- switch(status) {
-
- case SMT_SATISFIABLE:
- return out << "sat";
-
- case SMT_UNSATISFIABLE:
- return out << "unsat";
-
- case SMT_UNKNOWN:
- return out << "unknown";
-
- default:
- return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
- }
-}
-
-}/* CVC4 namespace */
-
#endif /* __CVC4__COMMAND_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index da209c581..56b89c125 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -268,9 +268,9 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
}
-SortType ExprManager::mkSort(const std::string& name) const {
+SortType ExprManager::mkSort(const std::string& name, size_t arity) const {
NodeManagerScope nms(d_nodeManager);
- return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, arity)));
}
/**
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8e02c8ca4..316a9b7b1 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -224,11 +224,11 @@ public:
/** Make the type of arrays with the given parameterization */
ArrayType mkArrayType(Type indexType, Type constituentType) const;
- /** Make a new sort with the given name. */
- SortType mkSort(const std::string& name) const;
+ /** Make a new sort with the given name and arity. */
+ SortType mkSort(const std::string& name, size_t arity = 0) const;
/** Get the type of an expression */
- Type getType(const Expr& e, bool check = false)
+ Type getType(const Expr& e, bool check = false)
throw (TypeCheckingException);
// variables are special, because duplicates are permitted
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 54e20667f..83d5dc47f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -42,6 +42,10 @@ const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
}/* CVC4::expr namespace */
+std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
+ return out << e.getMessage() << ": " << e.getExpression();
+}
+
std::ostream& operator<<(std::ostream& out, const Expr& e) {
e.toStream(out);
return out;
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 349795156..fee8e70db 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -83,7 +83,10 @@ public:
std::string toString() const;
friend class ExprManager;
-};
+};/* class TypeCheckingException */
+
+std::ostream& operator<<(std::ostream& out,
+ const TypeCheckingException& e) CVC4_PUBLIC;
/**
* Class encapsulating CVC4 expressions and methods for constructing new
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index ad698975f..a336662c3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -98,7 +98,7 @@ struct NodeValueConstPrinter {
* "metakind" is an ugly name but it's not used by client code, just
* by the expr package, and the intent here is to keep it from
* polluting the kind namespace. For more documentation on what these
- * mean, see src/expr/builtin_kinds.
+ * mean, see src/theory/builtin/kinds.
*/
enum MetaKind_t {
INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 77f00ab33..ca93473db 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -395,7 +395,7 @@ public:
* <code>AttrKind::value_type</code> if not.
*/
template <class AttrKind>
- inline typename AttrKind::value_type
+ inline typename AttrKind::value_type
getAttribute(TNode n, const AttrKind& attr) const;
/**
@@ -504,11 +504,11 @@ public:
/** Make the type of arrays with the given parameterization */
inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
- /** Make a new sort. */
+ /** Make a new (anonymous) sort of arity 0. */
inline TypeNode mkSort();
- /** Make a new sort with the given name. */
- inline TypeNode mkSort(const std::string& name);
+ /** Make a new sort with the given name and arity. */
+ inline TypeNode mkSort(const std::string& name, size_t arity = 0);
/**
* Get the type for the given node and optionally do type checking.
@@ -532,7 +532,7 @@ public:
* amount of checking required to return a valid result.
*
* @param n the Node for which we want a type
- * @param check whether we should check the type as we compute it
+ * @param check whether we should check the type as we compute it
* (default: false)
*/
TypeNode getType(TNode n, bool check = false)
@@ -765,7 +765,8 @@ inline TypeNode NodeManager::mkSort() {
return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
}
-inline TypeNode NodeManager::mkSort(const std::string& name) {
+inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) {
+ Assert(arity == 0, "parameterized sorts not yet supported.");
TypeNode type = mkSort();
type.setAttribute(expr::VarNameAttr(), name);
return type;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback