From 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 5 Oct 2010 22:24:09 +0000 Subject: parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly... --- src/context/cdlist.h | 8 + src/expr/command.cpp | 402 +++++++++++++++++++++++++++++++++++-- src/expr/command.h | 334 ++++++++++++------------------ src/expr/expr_manager_template.cpp | 4 +- src/expr/expr_manager_template.h | 6 +- src/expr/expr_template.cpp | 4 + src/expr/expr_template.h | 5 +- src/expr/metakind_template.h | 2 +- src/expr/node_manager.h | 13 +- src/main/getopt.cpp | 16 +- src/main/main.cpp | 30 +-- src/parser/parser.cpp | 40 +++- src/parser/parser.h | 25 ++- src/parser/smt/smt.h | 12 +- src/parser/smt2/Smt2.g | 260 +++++++++++++++++------- src/parser/smt2/smt2.cpp | 9 +- src/parser/smt2/smt2.h | 20 +- src/parser/smt2/smt2_input.h | 7 +- src/smt/Makefile.am | 4 +- src/smt/bad_option.h | 48 +++++ src/smt/noninteractive_exception.h | 49 +++++ src/smt/smt_engine.cpp | 92 +++++++-- src/smt/smt_engine.h | 147 +++++++++----- src/theory/arith/kinds | 2 +- src/theory/arrays/kinds | 2 +- src/theory/booleans/kinds | 2 +- src/theory/bv/kinds | 2 +- src/theory/interrupted.h | 14 +- src/theory/output_channel.h | 2 +- src/theory/uf/kinds | 2 +- src/util/options.h | 39 ++-- src/util/sexpr.h | 18 +- 32 files changed, 1162 insertions(+), 458 deletions(-) create mode 100644 src/smt/bad_option.h create mode 100644 src/smt/noninteractive_exception.h diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 7e382697c..02418d3df 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -21,6 +21,8 @@ #ifndef __CVC4__CONTEXT__CDLIST_H #define __CVC4__CONTEXT__CDLIST_H +#include + #include "context/context.h" #include "util/Assert.h" @@ -224,6 +226,12 @@ public: public: + typedef std::input_iterator_tag iterator_category; + typedef T value_type; + typedef ptrdiff_t difference_type; + typedef const T* pointer; + typedef const T& reference; + const_iterator() : d_it(NULL) {} inline bool operator==(const const_iterator& i) const { 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 +#include +#include +#include + #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& 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(out, ", ") ); + out << d_declaredSymbols.back(); + out << "])"; +} + +/* class DefineFunctionCommand */ + +DefineFunctionCommand::DefineFunctionCommand(const std::string& name, + const std::vector >& 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 >(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 v = smtEngine->getAssertions(); + copy( v.begin(), v.end(), ostream_iterator(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& ids, const Type& t); - void toStream(std::ostream& out) const; protected: std::vector d_declaredSymbols; Type d_type; -}; +public: + DeclarationCommand(const std::string& id, Type t); + DeclarationCommand(const std::vector& 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 > 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 >& 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 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 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& 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: * AttrKind::value_type if not. */ template - 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; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 08bcbaa7c..4af882aa1 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -70,7 +70,9 @@ enum OptionValue { STRICT_PARSING, DEFAULT_EXPR_DEPTH, PRINT_EXPR_TYPES, - UF_THEORY + UF_THEORY, + INTERACTIVE, + NO_INTERACTIVE };/* enum OptionValue */ /** @@ -117,6 +119,8 @@ static struct option cmdlineOptions[] = { { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, { "uf" , required_argument, NULL, UF_THEORY }, + { "interactive", no_argument , NULL, INTERACTIVE }, + { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -268,6 +272,16 @@ throw(OptionException) { } break; + case INTERACTIVE: + opts->interactive = true; + opts->interactiveSetByUser = true; + break; + + case NO_INTERACTIVE: + opts->interactive = false; + opts->interactiveSetByUser = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/main/main.cpp b/src/main/main.cpp index f0c04e5f6..4f261378d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -110,20 +110,25 @@ int runCvc4(int argc, char* argv[]) { throw Exception("Too many input files specified."); } + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin; + } + // Create the expression manager ExprManager exprMgr; // Create the SmtEngine SmtEngine smt(&exprMgr, &options); - // If no file supplied we read from standard input - bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "" : argv[firstArgIndex]; - ReferenceStat< const char* > s_statFilename("filename",filename); + ReferenceStat< const char* > s_statFilename("filename", filename); StatisticsRegistry::registerStat(&s_statFilename); if(options.lang == parser::LANG_AUTO) { @@ -180,6 +185,9 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; + if( options.interactive ) { + // cout << "CVC4> " << flush; + } while((cmd = parser->nextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); @@ -238,21 +246,19 @@ void doCommand(SmtEngine& smt, Command* cmd) { cout << "Invoking: " << *cmd << endl; } - cmd->invoke(&smt); + if(options.verbosity >= 0) { + cmd->invoke(&smt, cout); + } else { + cmd->invoke(&smt); + } QueryCommand *qc = dynamic_cast(cmd); if(qc != NULL) { lastResult = qc->getResult(); - if(options.verbosity >= 0) { - cout << lastResult << endl; - } } else { CheckSatCommand *csc = dynamic_cast(cmd); if(csc != NULL) { lastResult = csc->getResult(); - if(options.verbosity >= 0) { - cout << lastResult << endl; - } } } } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f73e268a3..39f61c16d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -18,6 +18,7 @@ #include #include +#include #include #include "input.h" @@ -79,6 +80,14 @@ Type Parser::getSort(const std::string& name) { return t; } +Type Parser::getSort(const std::string& name, + const std::vector& params) { + Assert( isDeclared(name, SYM_SORT) ); + Type t = d_declScope.lookupType(name); + Warning() << "FIXME use params to realize parameterized sort\n"; + return t; +} + /* Returns true if name is bound to a boolean variable. */ bool Parser::isBoolean(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); @@ -94,7 +103,7 @@ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); } -Expr +Expr Parser::mkVar(const std::string& name, const Type& type) { Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); @@ -124,10 +133,25 @@ Parser::defineType(const std::string& name, const Type& type) { Assert( isDeclared(name, SYM_SORT) ) ; } +void +Parser::defineParameterizedType(const std::string& name, + const std::vector& params, + const Type& type) { + if(Debug.isOn("parser")) { + Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", ["; + copy(params.begin(), params.end() - 1, + ostream_iterator(Debug("parser"), ", ") ); + Debug("parser") << params.back(); + Debug("parser") << "], " << type << ")" << std::endl; + } + Warning("defineSort unimplemented\n"); + defineType(name,type); +} + Type -Parser::mkSort(const std::string& name) { - Debug("parser") << "newSort(" << name << ")" << std::endl; - Type type = d_exprManager->mkSort(name); +Parser::mkSort(const std::string& name, size_t arity) { + Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl; + Type type = d_exprManager->mkSort(name, arity); defineType(name,type); return type; } @@ -234,10 +258,10 @@ Command* Parser::nextCommand() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(TypeCheckingException& e) { + } catch(Exception& e) { setDone(); stringstream ss; - ss << e.getMessage() << ": " << e.getExpression(); + ss << e; parseError( ss.str() ); } } @@ -257,10 +281,10 @@ Expr Parser::nextExpression() throw(ParserException) { } catch(ParserException& e) { setDone(); throw; - } catch(TypeCheckingException& e) { + } catch(Exception& e) { setDone(); stringstream ss; - ss << e.getMessage() << ": " << e.getExpression(); + ss << e; parseError( ss.str() ); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 1c02aa482..0faf9bebf 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -208,10 +208,16 @@ public: Expr getVariable(const std::string& var_name); /** - * Returns a sort, given a name + * Returns a sort, given a name. */ Type getSort(const std::string& sort_name); + /** + * Returns a sort, given a name and args. + */ + Type getSort(const std::string& sort_name, + const std::vector& params); + /** * Checks if a symbol has been declared. * @param name the symbol name @@ -267,8 +273,10 @@ public: /** Create a new CVC4 variable expression of the given type. */ Expr mkVar(const std::string& name, const Type& type); - /** Create a set of new CVC4 variable expressions of the given - type. */ + /** + * Create a set of new CVC4 variable expressions of the given + * type. + */ const std::vector mkVars(const std::vector names, const Type& type); @@ -278,13 +286,18 @@ public: /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); + /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ + void defineParameterizedType(const std::string& name, + const std::vector& params, + const Type& type); + /** - * Creates a new sort with the given name. + * Creates a new sort with the given name and arity. */ - Type mkSort(const std::string& name); + Type mkSort(const std::string& name, size_t arity = 0); /** - * Creates a new sorts with the given names. + * Creates new sorts with the given names (all of arity 0). */ const std::vector mkSorts(const std::vector& names); diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 23881c8b9..ffc113574 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -87,11 +87,9 @@ public: * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ - void - addTheory(Theory theory); + void addTheory(Theory theory); - bool - logicIsSet(); + bool logicIsSet(); /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. @@ -99,8 +97,7 @@ public: * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - void - setLogic(const std::string& name); + void setLogic(const std::string& name); static Logic toLogic(const std::string& name); @@ -109,7 +106,8 @@ private: void addArithmeticOperators(); void addUf(); static std::hash_map newLogicMap(); -}; +};/* class Smt */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6919c86c4..4c742adfc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -61,7 +61,7 @@ options { using namespace CVC4; using namespace CVC4::parser; -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Smt2*)LEXER->super) } @@ -91,7 +91,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Smt2*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() @@ -112,7 +112,7 @@ parseExpr returns [CVC4::Expr expr] ; /** - * Parses a command + * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ parseCommand returns [CVC4::Command* cmd] @@ -126,15 +126,18 @@ parseCommand returns [CVC4::Command* cmd] command returns [CVC4::Command* cmd] @declarations { std::string name; + std::vector names; Expr expr; Type t; + std::vector terms; std::vector sorts; + std::vector > sortedVars; SExpr sexpr; } : /* set the logic */ SET_LOGIC_TOK SYMBOL { name = AntlrInput::tokenText($SYMBOL); - Debug("parser") << "set logic: '" << name << "' " << std::endl; + Debug("parser") << "set logic: '" << name << "'" << std::endl; if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) { PARSER_STATE->parseError("Only one set-logic is allowed."); } @@ -142,35 +145,113 @@ command returns [CVC4::Command* cmd] $cmd = new SetBenchmarkLogicCommand(name); } | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setInfo(name,sexpr); + PARSER_STATE->setInfo(name,sexpr); cmd = new SetInfoCommand(name,sexpr); } + | /* get-info */ + GET_INFO_TOK KEYWORD + { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); } + | /* set-option */ + SET_OPTION_TOK KEYWORD symbolicExpr[sexpr] + { name = AntlrInput::tokenText($KEYWORD); + PARSER_STATE->setOption(name,sexpr); + cmd = new SetOptionCommand(name,sexpr); } + | /* get-option */ + GET_OPTION_TOK KEYWORD + { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); } | /* sort declaration */ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL - { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; - if( AntlrInput::tokenToInteger(n) > 0 ) { - Unimplemented("Parameterized user sorts."); - } - PARSER_STATE->mkSort(name); + { Debug("parser") << "declare sort: '" << name + << "' arity=" << n << std::endl; + PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n)); $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); } + | /* sort definition */ + DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] + LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK + { + PARSER_STATE->pushScope(); + for(std::vector::const_iterator i = names.begin(), + iend = names.end(); + i != iend; + ++i) { + sorts.push_back(PARSER_STATE->mkSort(*i)); + } + } + sortSymbol[t] + { PARSER_STATE->popScope(); + // Do NOT call mkSort, since that creates a new sort! + // This name is not its own distinct sort, it's an alias. + PARSER_STATE->defineParameterizedType(name, sorts, t); + $cmd = new EmptyCommand; + } | /* function declaration */ - DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - LPAREN_TOK sortList[sorts] RPAREN_TOK + DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t] - { Debug("parser") << "declare fun: '" << name << "' " << std::endl; + { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts,t); } - PARSER_STATE->mkVar(name, t); - $cmd = new DeclarationCommand(name,t); } + PARSER_STATE->mkVar(name, t); + $cmd = new DeclarationCommand(name,t); } + | /* function definition */ + DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK + sortSymbol[t] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define fun: '" << name << "'" << std::endl; + if( sortedVars.size() > 0 ) { + std::vector sorts; + sorts.reserve(sortedVars.size()); + for(std::vector >::const_iterator i = + sortedVars.begin(), iend = sortedVars.end(); + i != iend; + ++i) { + sorts.push_back((*i).second); + } + t = EXPR_MANAGER->mkFunctionType(sorts,t); + } + PARSER_STATE->pushScope(); + for(std::vector >::const_iterator i = + sortedVars.begin(), iend = sortedVars.end(); + i != iend; + ++i) { + PARSER_STATE->mkVar((*i).first, (*i).second); + } + } + term[expr] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + PARSER_STATE->mkVar(name, t); + $cmd = new DefineFunctionCommand(name,sortedVars,t,expr); + } + | /* value query */ + GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK + { if(terms.size() == 1) { + $cmd = new GetValueCommand(terms[0]); + } else { + CommandSequence* seq = new CommandSequence(); + for(std::vector::const_iterator i = terms.begin(), + iend = terms.end(); + i != iend; + ++i) { + seq->addCommand(new GetValueCommand(*i)); + } + $cmd = seq; + } + } | /* assertion */ ASSERT_TOK term[expr] { cmd = new AssertCommand(expr); } | /* checksat */ - CHECKSAT_TOK + CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); } + | /* get-assertions */ + GET_ASSERTIONS_TOK + { cmd = new GetAssertionsCommand; } | EXIT_TOK - { // TODO: Explicitly represent exit as command? - cmd = 0; } + { cmd = NULL; } ; symbolicExpr[CVC4::SExpr& sexpr] @@ -187,12 +268,12 @@ symbolicExpr[CVC4::SExpr& sexpr] { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } - | LPAREN_TOK - (symbolicExpr[sexpr] { children.push_back(sexpr); } )* + | LPAREN_TOK + (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK { sexpr = SExpr(children); } ; - + /** * Matches a term. * @return the expression representing the formula @@ -202,11 +283,11 @@ term[CVC4::Expr& expr] Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; std::string name; - std::vector args; -} + std::vector args; +} : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK - { + LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK + { if( kind == CVC4::kind::EQUAL && args.size() > 0 && args[0].getType() == EXPR_MANAGER->booleanType() ) { @@ -214,13 +295,13 @@ term[CVC4::Expr& expr] kind = CVC4::kind::IFF; } - if( !PARSER_STATE->strictModeEnabled() && - (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && + if( !PARSER_STATE->strictModeEnabled() && + (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); @@ -233,7 +314,7 @@ term[CVC4::Expr& expr] } | /* A non-built-in function application */ - LPAREN_TOK + LPAREN_TOK functionSymbol[expr] { args.push_back(expr); } termList[args,expr] RPAREN_TOK @@ -241,18 +322,18 @@ term[CVC4::Expr& expr] { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } // | /* An ite expression */ - // LPAREN_TOK ITE_TOK + // LPAREN_TOK ITE_TOK // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // RPAREN_TOK // { expr = MK_EXPR(CVC4::kind::ITE, args); } | /* a let binding */ - LPAREN_TOK LET_TOK LPAREN_TOK + LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(); } ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK { PARSER_STATE->defineVar(name,expr); } )+ @@ -270,7 +351,8 @@ term[CVC4::Expr& expr] { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL - { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string + { // FIXME: This doesn't work because an SMT rational is not a + // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } | HEX_LITERAL @@ -290,8 +372,8 @@ term[CVC4::Expr& expr] * vector. * @param formulas the vector to fill with terms * @param expr an Expr reference for the elements of the sequence - */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every + */ +/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every * time through this rule. */ termList[std::vector& formulas, CVC4::Expr& expr] : ( term[expr] { formulas.push_back(expr); } )+ @@ -334,7 +416,7 @@ builtinOp[CVC4::Kind& kind] * @param check what kind of check to do with the symbol */ functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : symbol[name,check,SYM_VARIABLE] + : symbol[name,check,SYM_VARIABLE] ; /** @@ -348,23 +430,38 @@ functionSymbol[CVC4::Expr& fun] { PARSER_STATE->checkFunction(name); fun = PARSER_STATE->getVariable(name); } ; - + /** - * Matches a sequence of sort symbols and fills them into the given vector. + * Matches a sequence of sort symbols and fills them into the given + * vector. */ sortList[std::vector& sorts] @declarations { Type t; } - : ( sortSymbol[t] { sorts.push_back(t); })* + : ( sortSymbol[t] { sorts.push_back(t); } )* + ; + +/** + * Matches a sequence of (variable,sort) symbol pairs and fills them + * into the given vector. + */ +sortedVarList[std::vector >& sortedVars] +@declarations { + std::string name; + Type t; +} + : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK + { sortedVars.push_back(make_pair(name, t)); } + )* ; /** * Matches the sort symbol, which can be an arbitrary symbol. * @param check the check to perform on the name */ -sortName[std::string& name, CVC4::parser::DeclarationCheck check] - : symbol[name,check,SYM_SORT] +sortName[std::string& name, CVC4::parser::DeclarationCheck check] + : symbol[name,check,SYM_SORT] ; sortSymbol[CVC4::Type& t] @@ -372,21 +469,34 @@ sortSymbol[CVC4::Type& t] std::string name; std::vector args; } - : sortName[name,CHECK_NONE] + : sortName[name,CHECK_NONE] { t = PARSER_STATE->getSort(name); } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK - { + { if( name == "Array" ) { if( args.size() != 2 ) { PARSER_STATE->parseError("Illegal array type."); } - t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); } else { PARSER_STATE->parseError("Unhandled parameterized type."); } } ; +/** + * Matches a list of symbols, with check and type arguments as for the + * symbol[] rule below. + */ +symbolList[std::vector& names, + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] +@declarations { + std::string id; +} + : ( symbol[id,check,type] { names.push_back(id); } )* + ; + /** * Matches an symbol and sets the string reference parameter id. * @param id string to hold the symbol @@ -394,8 +504,8 @@ sortSymbol[CVC4::Type& t] * @param type the intended namespace for the symbol */ symbol[std::string& id, - CVC4::parser::DeclarationCheck check, - CVC4::parser::SymbolType type] + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] : SYMBOL { id = AntlrInput::tokenText($SYMBOL); Debug("parser") << "symbol: " << id @@ -411,6 +521,10 @@ CHECKSAT_TOK : 'check-sat'; //DIFFICULTY_TOK : ':difficulty'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; +DEFINE_FUN_TOK : 'define-fun'; +DEFINE_SORT_TOK : 'define-sort'; +GET_VALUE_TOK : 'get-value'; +GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; //FALSE_TOK : 'false'; ITE_TOK : 'ite'; @@ -421,6 +535,8 @@ RPAREN_TOK : ')'; //SAT_TOK : 'sat'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; +SET_OPTION_TOK : 'set-option'; +GET_OPTION_TOK : 'get-option'; //SMT_VERSION_TOK : ':smt-lib-version'; //SOURCE_TOK : ':source'; //STATUS_TOK : ':status'; @@ -456,8 +572,8 @@ TILDE_TOK : '~'; XOR_TOK : 'xor'; /** - * Matches a symbol from the input. A symbol is a "simple" symbol or a - * sequence of printable ASCII characters that starts and ends with | and + * Matches a symbol from the input. A symbol is a "simple" symbol or a + * sequence of printable ASCII characters that starts and ends with | and * does not otherwise contain |. */ SYMBOL @@ -473,11 +589,11 @@ KEYWORD : ':' SIMPLE_SYMBOL ; -/** Matches a "simple" symbol: a non-empty sequence of letters, digits and - * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a - * digit. +/** Matches a "simple" symbol: a non-empty sequence of letters, digits and + * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a + * digit. */ -fragment SIMPLE_SYMBOL +fragment SIMPLE_SYMBOL : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)* ; @@ -485,7 +601,7 @@ fragment SIMPLE_SYMBOL * Matches and skips whitespace in the input. */ WHITESPACE - : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN;; } + : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN; } ; /** @@ -503,19 +619,19 @@ fragment NUMERAL char *start = (char*) GETCHARINDEX(); } : DIGIT+ - { Debug("parser-extra") << "NUMERAL: " - << (uintptr_t)start << ".." << GETCHARINDEX() + { Debug("parser-extra") << "NUMERAL: " + << (uintptr_t)start << ".." << GETCHARINDEX() << " strict? " << (bool)(PARSER_STATE->strictModeEnabled()) << " ^0? " << (bool)(*start == '0') << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1)) << std::endl; } - { !PARSER_STATE->strictModeEnabled() || + { !PARSER_STATE->strictModeEnabled() || *start != '0' || start == (char*)(GETCHARINDEX() - 1) }? ; - + /** - * Matches a decimal constant from the input. + * Matches a decimal constant from the input. */ DECIMAL_LITERAL : NUMERAL '.' DIGIT+ @@ -537,18 +653,18 @@ DECIMAL_LITERAL /** - * Matches a double quoted string literal. Escaping is supported, and escape - * character '\' has to be escaped. + * Matches a double quoted string literal. Escaping is supported, and + * escape character '\' has to be escaped. */ -STRING_LITERAL - : '"' (ESCAPE | ~('"'|'\\'))* '"' +STRING_LITERAL + : '"' (ESCAPE | ~('"'|'\\'))* '"' ; /** * Matches the comments and ignores them */ -COMMENT - : ';' (~('\n' | '\r'))* { $channel = HIDDEN;; } +COMMENT + : ';' (~('\n' | '\r'))* { $channel = HIDDEN; } ; @@ -556,9 +672,9 @@ COMMENT * Matches any letter ('a'-'z' and 'A'-'Z'). */ fragment -ALPHA - : 'a'..'z' - | 'A'..'Z' +ALPHA + : 'a'..'z' + | 'A'..'Z' ; /** @@ -568,10 +684,10 @@ fragment DIGIT : '0'..'9'; fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; -/** Matches the characters that may appear in a "symbol" (i.e., an identifier) +/** Matches the characters that may appear in a "symbol" (i.e., an identifier) */ -fragment SYMBOL_CHAR - : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' +fragment SYMBOL_CHAR + : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' | '&' | '^' | '<' | '>' | '@' ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e704d027d..308f45ed0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -98,7 +98,8 @@ bool Smt2::logicIsSet() { } /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * Sets the logic for the current benchmark. Declares any logic and + * theory symbols. * * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) @@ -124,7 +125,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_NIA: addTheory(THEORY_INTS); break; - + case Smt::QF_LRA: case Smt::QF_RDL: addTheory(THEORY_REALS); @@ -162,5 +163,9 @@ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } +void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { + // TODO: ??? +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fe152a7f6..6398fa735 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -57,28 +57,28 @@ public: * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ - void - addTheory(Theory theory); + void addTheory(Theory theory); - bool - logicIsSet(); + bool logicIsSet(); /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * Sets the logic for the current benchmark. Declares any logic and + * theory symbols. * * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - void - setLogic(const std::string& name); + void setLogic(const std::string& name); - void - setInfo(const std::string& flag, const SExpr& sexpr); + void setInfo(const std::string& flag, const SExpr& sexpr); + + void setOption(const std::string& flag, const SExpr& sexpr); private: void addArithmeticOperators(); -}; +};/* class Smt2 */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 320f5ab75..02a480971 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -64,7 +64,8 @@ public: /** * Create a string input. * - * @param exprManager the manager to use when building expressions from the input + * @param exprManager the manager to use when building expressions + * from the input * @param input the string to read * @param name the "filename" to use when reporting errors */ @@ -81,7 +82,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() + Command* parseCommand() throw(ParserException, TypeCheckingException, AssertionException); /** @@ -90,7 +91,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() + Expr parseExpr() throw(ParserException, TypeCheckingException, AssertionException); };/* class Smt2Input */ diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 90d58904a..192915152 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -7,4 +7,6 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ - smt_engine.h + smt_engine.h \ + noninteractive_exception.h \ + bad_option.h diff --git a/src/smt/bad_option.h b/src/smt/bad_option.h new file mode 100644 index 000000000..800d8e68a --- /dev/null +++ b/src/smt/bad_option.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file bad_option.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 An exception that is thrown when an option setting is not + ** understood. + ** + ** An exception that is thrown when an interactive-only feature while + ** CVC4 is being used in a non-interactive setting (for example, the + ** "(get-assertions)" command in an SMT-LIBv2 script). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__BAD_OPTION_H +#define __CVC4__SMT__BAD_OPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC BadOption : public CVC4::Exception { +public: + BadOption() : + Exception("Unrecognized informational or option key or setting") { + } + + BadOption(const std::string& msg) : + Exception(msg) { + } + + BadOption(const char* msg) : + Exception(msg) { + } +};/* class BadOption */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__BAD_OPTION_H */ diff --git a/src/smt/noninteractive_exception.h b/src/smt/noninteractive_exception.h new file mode 100644 index 000000000..4cf97ab3e --- /dev/null +++ b/src/smt/noninteractive_exception.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file noninteractive_exception.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 An exception that is thrown when an interactive-only + ** feature while CVC4 is being used in a non-interactive setting + ** + ** An exception that is thrown when an interactive-only feature while + ** CVC4 is being used in a non-interactive setting (for example, the + ** "(get-assertions)" command in an SMT-LIBv2 script). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H +#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H + +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception { +public: + NoninteractiveException() : + Exception("Interactive feature used while operating in " + "non-interactive mode") { + } + + NoninteractiveException(const std::string& msg) : + Exception(msg) { + } + + NoninteractiveException(const char* msg) : + Exception(msg) { + } +};/* class NoninteractiveException */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cb97d7f4c..c4eceeb24 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -17,6 +17,9 @@ **/ #include "smt/smt_engine.h" +#include "smt/noninteractive_exception.h" +#include "context/context.h" +#include "context/cdlist.h" #include "expr/command.h" #include "expr/node_builder.h" #include "util/output.h" @@ -25,9 +28,10 @@ #include "prop/prop_engine.h" #include "theory/theory_engine.h" - +using namespace CVC4; +using namespace CVC4::smt; using namespace CVC4::prop; -using CVC4::context::Context; +using namespace CVC4::context; namespace CVC4 { @@ -69,19 +73,30 @@ public: using ::CVC4::smt::SmtEnginePrivate; SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : - d_ctxt(em->getContext()), + d_context(em->getContext()), d_exprManager(em), d_nodeManager(em->getNodeManager()), - d_options(opts) { + d_options(opts), + /* These next few are initialized below, after we have a NodeManager + * in scope. */ + d_decisionEngine(NULL), + d_theoryEngine(NULL), + d_propEngine(NULL), + d_assertionList(NULL) { NodeManagerScope nms(d_nodeManager); d_decisionEngine = new DecisionEngine; // We have mutual dependancy here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_ctxt, opts); - d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt); + d_theoryEngine = new TheoryEngine(d_context, opts); + d_propEngine = new PropEngine(opts, d_decisionEngine, + d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); + + if(d_options->interactive) { + d_assertionList = new(true) CDList(d_context); + } } void SmtEngine::shutdown() { @@ -95,6 +110,8 @@ SmtEngine::~SmtEngine() { shutdown(); + ::delete d_assertionList; + delete d_theoryEngine; delete d_propEngine; delete d_decisionEngine; @@ -105,53 +122,79 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } +void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) { + // FIXME implement me +} + +const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) { + // FIXME implement me + throw BadOption(); +} + +void SmtEngine::defineFunction(const string& name, + const vector >& args, + Type type, + Expr formula) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { return smt.d_theoryEngine->preprocess(n); } Result SmtEngine::check() { - Debug("smt") << "SMT check()" << std::endl; + Debug("smt") << "SMT check()" << endl; return d_propEngine->checkSat(); } Result SmtEngine::quickCheck() { - Debug("smt") << "SMT quickCheck()" << std::endl; + Debug("smt") << "SMT quickCheck()" << endl; return Result(Result::VALIDITY_UNKNOWN); } void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) { - Debug("smt") << "push_back assertion " << n << std::endl; + Debug("smt") << "push_back assertion " << n << endl; smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; + Debug("smt") << "SMT checkSat(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); - Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT query(" << e << ")" << std::endl; + Debug("smt") << "SMT query(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); - Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl; + Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; + Debug("smt") << "SMT assertFormula(" << e << ")" << endl; SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT simplify(" << e << ")" << std::endl; + Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } @@ -160,15 +203,30 @@ Model SmtEngine::getModel() { Unimplemented(); } +Expr SmtEngine::getValue(Expr term) { + NodeManagerScope nms(d_nodeManager); + Unimplemented(); +} + +vector SmtEngine::getAssertions() throw(NoninteractiveException) { + if(!d_options->interactive) { + const char* msg = + "Cannot query the current assertion list when not in interactive mode."; + throw NoninteractiveException(msg); + } + Assert(d_assertionList != NULL); + return vector(d_assertionList->begin(), d_assertionList->end()); +} + void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT push()" << std::endl; + Debug("smt") << "SMT push()" << endl; Unimplemented(); } void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); - Debug("smt") << "SMT pop()" << std::endl; + Debug("smt") << "SMT pop()" << endl; Unimplemented(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b5807852b..56e38af7a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -27,6 +27,9 @@ #include "expr/expr_manager.h" #include "util/result.h" #include "util/model.h" +#include "util/sexpr.h" +#include "smt/noninteractive_exception.h" +#include "smt/bad_option.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -36,6 +39,7 @@ namespace CVC4 { namespace context { class Context; + template class CDList; }/* CVC4::context namespace */ class Command; @@ -63,6 +67,61 @@ namespace smt { // The CNF conversion can go on in PropEngine. class CVC4_PUBLIC SmtEngine { +private: + + /** Our Context */ + context::Context* d_context; + + /** Our expression manager */ + ExprManager* d_exprManager; + + /** Out internal expression/node manager */ + NodeManager* d_nodeManager; + + /** User-level options */ + const Options* d_options; + + /** The decision engine */ + DecisionEngine* d_decisionEngine; + + /** The decision engine */ + TheoryEngine* d_theoryEngine; + + /** The propositional engine */ + prop::PropEngine* d_propEngine; + + /** + * The assertion list, before any conversion, for supporting + * getAssertions(). Only maintained if in interactive mode. + */ + context::CDList* d_assertionList; + + // preprocess() and addFormula() used to be housed here; they are + // now in an SmtEnginePrivate class. See the comment in + // smt_engine.cpp. + + /** + * This is called by the destructor, just before destroying the + * PropEngine, TheoryEngine, and DecisionEngine (in that order). It + * is important because there are destruction ordering issues + * between PropEngine and Theory. + */ + void shutdown(); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + friend class ::CVC4::smt::SmtEnginePrivate; public: @@ -81,6 +140,37 @@ public: */ void doCommand(Command*); + /** + * Set information about the script executing. + */ + void setInfo(const std::string& key, const SExpr& value) throw(BadOption); + + /** + * Query information about the SMT environment. + */ + const SExpr& getInfo(const std::string& key) const throw(BadOption); + + /** + * Set an aspect of the current SMT execution environment. + */ + void setOption(const std::string& key, const SExpr& value) throw(BadOption); + + /** + * Get an aspect of the current SMT execution environment. + */ + const SExpr& getOption(const std::string& key) const throw(BadOption); + + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false iff + * inconsistent. + */ + void defineFunction(const std::string& name, + const std::vector >& args, + Type type, + Expr formula); + /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for @@ -113,64 +203,25 @@ public: Model getModel(); /** - * Push a user-level context. - */ - void push(); - - /** - * Pop a user-level context. Throws an exception if nothing to pop. + * Get the assigned value of a term (only if preceded by a SAT or + * INVALID query). */ - void pop(); - -private: - - /** Our Context */ - CVC4::context::Context* d_ctxt; - - /** Our expression manager */ - ExprManager* d_exprManager; - - /** Out internal expression/node manager */ - NodeManager* d_nodeManager; - - /** User-level options */ - const Options* d_options; - - /** The decision engine */ - DecisionEngine* d_decisionEngine; - - /** The decision engine */ - TheoryEngine* d_theoryEngine; - - /** The propositional engine */ - prop::PropEngine* d_propEngine; - - // preprocess() and addFormula() used to be housed here; they are - // now in an SmtEnginePrivate class. See the comment in - // smt_engine.cpp. + Expr getValue(Expr term); /** - * This is called by the destructor, just before destroying the - * PropEngine, TheoryEngine, and DecisionEngine (in that order). It - * is important because there are destruction ordering issues - * between PropEngine and Theory. + * Get the current set of assertions. */ - void shutdown(); + std::vector getAssertions() throw(NoninteractiveException); /** - * Full check of consistency in current context. Returns true iff - * consistent. + * Push a user-level context. */ - Result check(); + void push(); /** - * Quick check of consistency in current context: calls - * processAssertionList() then look for inconsistency (based only on - * that). + * Pop a user-level context. Throws an exception if nothing to pop. */ - Result quickCheck(); - - friend class ::CVC4::smt::SmtEnginePrivate; + void pop(); };/* class SmtEngine */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 07d48b1f6..5cd4719b1 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -1,7 +1,7 @@ # kinds -*- sh -*- # # For documentation on this file format, please refer to -# src/expr/builtin_kinds. +# src/theory/builtin/kinds. # theory ::CVC4::theory::arith::TheoryArith "theory_arith.h" diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 68daa8cb5..4ad9c7463 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -1,7 +1,7 @@ # kinds -*- sh -*- # # For documentation on this file format, please refer to -# src/expr/builtin_kinds. +# src/theory/builtin/kinds. # theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index 43c37f4b7..ac6b05881 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -1,7 +1,7 @@ # kinds -*- sh -*- # # For documentation on this file format, please refer to -# src/expr/builtin_kinds. +# src/theory/builtin/kinds. # theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h" diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 54f861b76..cc6fe0c20 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -1,7 +1,7 @@ # kinds -*- sh -*- # # For documentation on this file format, please refer to -# src/expr/builtin_kinds. +# src/theory/builtin/kinds. # theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index 616d3da74..d8a54b1e4 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -11,9 +11,19 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief The theory output channel interface. + ** \brief An exception signaling that a Theory should immediately + ** stop performing processing ** - ** The theory output channel interface. + ** An exception signaling that a Theory should immediately stop + ** performing processing and relinquish control to its caller (e.g., + ** in a parallel environment). A Theory might be interrupted if it + ** calls into its CVC4::theory::OutputChannel, and it should only + ** catch this exception to perform emergency repair of any invariants + ** it must re-establish. Further, if this exception is caught by a + ** Theory, the Theory should rethrow the same exception (via "throw;" + ** in the exception block) rather than return, as the Interrupted + ** instance might contain additional information needed for the + ** proper management of CVC4 components. **/ #include "cvc4_private.h" diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index fb2fde589..cdc1e1cc2 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief The theory output channel interface. + ** \brief The theory output channel interface ** ** The theory output channel interface. **/ diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 4bfba382c..13cd5e91b 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -1,7 +1,7 @@ # kinds -*- sh -*- # # For documentation on this file format, please refer to -# src/expr/builtin_kinds. +# src/theory/builtin/kinds. # theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" diff --git a/src/util/options.h b/src/util/options.h index c79bc93b1..c504177bf 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -65,21 +65,34 @@ struct CVC4_PUBLIC Options { /** Should we strictly enforce the language standard while parsing? */ bool strictParsing; - Options() : binary_name(), - statistics(false), - out(0), - err(0), - verbosity(0), - lang(parser::LANG_AUTO), - uf_implementation(MORGAN), - parseOnly(false), - semanticChecks(true), - memoryMap(false), - strictParsing(false) - {} + /** Whether we're in interactive mode or not */ + bool interactive; + + /** + * Whether we're in interactive mode (or not) due to explicit user + * setting (if false, we inferred the proper default setting). + */ + bool interactiveSetByUser; + + Options() : + binary_name(), + statistics(false), + out(0), + err(0), + verbosity(0), + lang(parser::LANG_AUTO), + uf_implementation(MORGAN), + parseOnly(false), + semanticChecks(true), + memoryMap(false), + strictParsing(false), + interactive(false), + interactiveSetByUser(false) { + } };/* struct Options */ -inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) { +inline std::ostream& operator<<(std::ostream& out, + Options::UfImplementation uf) { switch(uf) { case Options::TIM: out << "TIM"; diff --git a/src/util/sexpr.h b/src/util/sexpr.h index d3681f471..9821664bd 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -29,8 +29,8 @@ namespace CVC4 { /** - * A simple S-expression. An S-expression is either an atom with a string value, or a - * list of other S-expressions. + * A simple S-expression. An S-expression is either an atom with a + * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { @@ -61,13 +61,15 @@ public: /** Is this S-expression an atom? */ bool isAtom() const; - /** Get the string value of this S-expression. This will cause an error if this S-expression - * is not an atom. + /** + * Get the string value of this S-expression. This will cause an + * error if this S-expression is not an atom. */ const std::string getValue() const; - /** Get the children of this S-expression. This will cause an error if this S-expression - * is not a list. + /** + * Get the children of this S-expression. This will cause an error + * if this S-expression is not a list. */ const std::vector getChildren() const; }; @@ -93,7 +95,9 @@ inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { std::vector children = sexpr.getChildren(); out << "("; bool first = true; - for( std::vector::iterator it = children.begin(); it != children.end(); ++it ) { + for( std::vector::iterator it = children.begin(); + it != children.end(); + ++it ) { if( first ) { first = false; } else { -- cgit v1.2.3