#ifndef __CVC4__CONTEXT__CDLIST_H
#define __CVC4__CONTEXT__CDLIST_H
+#include <iterator>
+
#include "context/context.h"
#include "util/Assert.h"
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 {
** 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";
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);
}
}
-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];
}
}
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 */
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 */
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;
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 */
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)));
}
/**
/** 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
}/* 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;
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
* "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 */
* <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;
/**
/** 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.
* 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)
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;
STRICT_PARSING,
DEFAULT_EXPR_DEPTH,
PRINT_EXPR_TYPES,
- UF_THEORY
+ UF_THEORY,
+ INTERACTIVE,
+ NO_INTERACTIVE
};/* enum OptionValue */
/**
{ "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! */
}
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");
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 ? "<stdin>" : 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) {
// 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);
cout << "Invoking: " << *cmd << endl;
}
- cmd->invoke(&smt);
+ if(options.verbosity >= 0) {
+ cmd->invoke(&smt, cout);
+ } else {
+ cmd->invoke(&smt);
+ }
QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd);
if(qc != NULL) {
lastResult = qc->getResult();
- if(options.verbosity >= 0) {
- cout << lastResult << endl;
- }
} else {
CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd);
if(csc != NULL) {
lastResult = csc->getResult();
- if(options.verbosity >= 0) {
- cout << lastResult << endl;
- }
}
}
}
#include <iostream>
#include <fstream>
+#include <iterator>
#include <stdint.h>
#include "input.h"
return t;
}
+Type Parser::getSort(const std::string& name,
+ const std::vector<Type>& 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();
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);
Assert( isDeclared(name, SYM_SORT) ) ;
}
+void
+Parser::defineParameterizedType(const std::string& name,
+ const std::vector<Type>& params,
+ const Type& type) {
+ if(Debug.isOn("parser")) {
+ Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
+ copy(params.begin(), params.end() - 1,
+ ostream_iterator<Type>(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;
}
} catch(ParserException& e) {
setDone();
throw;
- } catch(TypeCheckingException& e) {
+ } catch(Exception& e) {
setDone();
stringstream ss;
- ss << e.getMessage() << ": " << e.getExpression();
+ ss << e;
parseError( ss.str() );
}
}
} catch(ParserException& e) {
setDone();
throw;
- } catch(TypeCheckingException& e) {
+ } catch(Exception& e) {
setDone();
stringstream ss;
- ss << e.getMessage() << ": " << e.getExpression();
+ ss << e;
parseError( ss.str() );
}
}
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<Type>& params);
+
/**
* Checks if a symbol has been declared.
* @param name the symbol name
/** 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<Expr>
mkVars(const std::vector<std::string> names, const Type& type);
/** 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<Type>& 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<Type>
mkSorts(const std::vector<std::string>& names);
* @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.
* @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);
void addArithmeticOperators();
void addUf();
static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap();
-};
+};/* class Smt */
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
using namespace CVC4;
using namespace CVC4::parser;
-#undef PARSER_STATE
+#undef PARSER_STATE
#define PARSER_STATE ((Smt2*)LEXER->super)
}
/* 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()
;
/**
- * 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]
command returns [CVC4::Command* cmd]
@declarations {
std::string name;
+ std::vector<std::string> names;
Expr expr;
Type t;
+ std::vector<Expr> terms;
std::vector<Type> sorts;
+ std::vector<std::pair<std::string, Type> > 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.");
}
$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<std::string>::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<CVC4::Type> sorts;
+ sorts.reserve(sortedVars.size());
+ for(std::vector<std::pair<std::string, CVC4::Type> >::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<std::pair<std::string, CVC4::Type> >::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<Expr>::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]
{ 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
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Kind kind;
std::string name;
- std::vector<Expr> args;
-}
+ std::vector<Expr> 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() ) {
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);
}
| /* A non-built-in function application */
- LPAREN_TOK
+ LPAREN_TOK
functionSymbol[expr]
{ args.push_back(expr); }
termList[args,expr] RPAREN_TOK
{ 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); } )+
{ 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
* 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<CVC4::Expr>& formulas, CVC4::Expr& expr]
: ( term[expr] { formulas.push_back(expr); } )+
* @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]
;
/**
{ 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<CVC4::Type>& 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<std::pair<std::string, CVC4::Type> >& 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]
std::string name;
std::vector<CVC4::Type> 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<std::string>& 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
* @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
//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';
//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';
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
: ':' 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)*
;
* Matches and skips whitespace in the input.
*/
WHITESPACE
- : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN;; }
+ : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN; }
;
/**
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+
/**
- * 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; }
;
* Matches any letter ('a'-'z' and 'A'-'Z').
*/
fragment
-ALPHA
- : 'a'..'z'
- | 'A'..'Z'
+ALPHA
+ : 'a'..'z'
+ | 'A'..'Z'
;
/**
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
+ : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
| '&' | '^' | '<' | '>' | '@'
;
}
/**
- * 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)
case Smt::QF_NIA:
addTheory(THEORY_INTS);
break;
-
+
case Smt::QF_LRA:
case Smt::QF_RDL:
addTheory(THEORY_REALS);
// TODO: ???
}
+void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
+ // TODO: ???
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
* @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 */
/**
* 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
*/
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
+ Command* parseCommand()
throw(ParserException, TypeCheckingException, AssertionException);
/**
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
+ Expr parseExpr()
throw(ParserException, TypeCheckingException, AssertionException);
};/* class Smt2Input */
libsmt_la_SOURCES = \
smt_engine.cpp \
- smt_engine.h
+ smt_engine.h \
+ noninteractive_exception.h \
+ bad_option.h
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
**/
#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"
#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 {
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<Expr>(d_context);
+ }
}
void SmtEngine::shutdown() {
shutdown();
+ ::delete d_assertionList;
+
delete d_theoryEngine;
delete d_propEngine;
delete d_decisionEngine;
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<pair<string, Type> >& 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();
}
Unimplemented();
}
+Expr SmtEngine::getValue(Expr term) {
+ NodeManagerScope nms(d_nodeManager);
+ Unimplemented();
+}
+
+vector<Expr> 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<Expr>(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();
}
#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)
namespace context {
class Context;
+ template <class T> class CDList;
}/* CVC4::context namespace */
class Command;
// 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<Expr>* 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:
*/
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<std::pair<std::string, Type> >& args,
+ Type type,
+ Expr formula);
+
/**
* Add a formula to the current context: preprocess, do per-theory
* setup, use processAssertionList(), asserting to T-solver for
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<Expr> 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 */
# 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"
# 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"
# 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"
# 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"
** 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"
** 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.
**/
# 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"
/** 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";
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 {
/** 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<SExpr> getChildren() const;
};
std::vector<SExpr> children = sexpr.getChildren();
out << "(";
bool first = true;
- for( std::vector<SExpr>::iterator it = children.begin(); it != children.end(); ++it ) {
+ for( std::vector<SExpr>::iterator it = children.begin();
+ it != children.end();
+ ++it ) {
if( first ) {
first = false;
} else {
projects / cvc5.git / commitdiff