diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 402 | ||||
-rw-r--r-- | src/expr/command.h | 334 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 6 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_template.h | 5 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 13 |
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; |