diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/expr | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/expr')
31 files changed, 655 insertions, 379 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 352647642..738604f90 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -16,6 +16,7 @@ libexpr_la_SOURCES = \ type.cpp \ node_value.h \ node_manager.h \ + type_checker.h \ attribute.h \ attribute_internals.h \ attribute.cpp \ @@ -37,7 +38,8 @@ nodist_libexpr_la_SOURCES = \ expr.h \ expr.cpp \ expr_manager.h \ - expr_manager.cpp + expr_manager.cpp \ + type_checker.cpp EXTRA_DIST = \ kind_template.h \ @@ -47,6 +49,7 @@ EXTRA_DIST = \ expr_manager_template.cpp \ expr_template.h \ expr_template.cpp \ + type_checker_template.cpp \ mkkind \ mkmetakind \ mkexpr @@ -59,6 +62,7 @@ BUILT_SOURCES = \ expr.cpp \ expr_manager.h \ expr_manager.cpp \ + type_checker.cpp \ $(top_builddir)/src/theory/.subdirs CLEANFILES = \ @@ -68,6 +72,7 @@ CLEANFILES = \ expr.cpp \ expr_manager.h \ expr_manager.cpp \ + type_checker.cpp \ $(top_builddir)/src/theory/.subdirs include @top_srcdir@/src/theory/Makefile.subdirs @@ -127,3 +132,11 @@ expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.su $< \ `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) + +type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkexpr + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkexpr \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 85c0fe528..d58173454 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -5,7 +5,7 @@ ** Major contributors: dejan ** 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) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 9b21184d0..3da3799be 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -5,7 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): cconway, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 2783e8eaa..5fb4d1fbd 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -78,6 +78,10 @@ EmptyCommand::EmptyCommand(std::string name) : d_name(name) { } +std::string EmptyCommand::getName() const { + return d_name; +} + void EmptyCommand::invoke(SmtEngine* smtEngine) { /* empty commands have no implementation */ } @@ -88,6 +92,10 @@ AssertCommand::AssertCommand(const BoolExpr& e) : d_expr(e) { } +BoolExpr AssertCommand::getExpr() const { + return d_expr; +} + void AssertCommand::invoke(SmtEngine* smtEngine) { smtEngine->assertFormula(d_expr); } @@ -106,10 +114,18 @@ void PopCommand::invoke(SmtEngine* smtEngine) { /* class CheckSatCommand */ +CheckSatCommand::CheckSatCommand() : + d_expr() { +} + CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : d_expr(expr) { } +BoolExpr CheckSatCommand::getExpr() const { + return d_expr; +} + void CheckSatCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->checkSat(d_expr); } @@ -128,6 +144,10 @@ QueryCommand::QueryCommand(const BoolExpr& e) : d_expr(e) { } +BoolExpr QueryCommand::getExpr() const { + return d_expr; +} + void QueryCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->query(d_expr); } @@ -145,6 +165,23 @@ void QueryCommand::printResult(std::ostream& out) const { QuitCommand::QuitCommand() { } +void QuitCommand::invoke(SmtEngine* smtEngine) { + Dump("benchmark") << *this; +} + +/* class CommentCommand */ + +CommentCommand::CommentCommand(std::string comment) : d_comment(comment) { +} + +std::string CommentCommand::getComment() const { + return d_comment; +} + +void CommentCommand::invoke(SmtEngine* smtEngine) { + Dump("benchmark") << *this; +} + /* class CommandSequence */ CommandSequence::CommandSequence() : @@ -175,51 +212,150 @@ void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { } } -/* class DeclarationCommand */ +CommandSequence::const_iterator CommandSequence::begin() const { + return d_commandSequence.begin(); +} + +CommandSequence::const_iterator CommandSequence::end() const { + return d_commandSequence.end(); +} + +CommandSequence::iterator CommandSequence::begin() { + return d_commandSequence.begin(); +} + +CommandSequence::iterator CommandSequence::end() { + return d_commandSequence.end(); +} + +/* class DeclarationSequenceCommand */ + +/* class DeclarationDefinitionCommand */ + +DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) : + d_symbol(id) { +} + +std::string DeclarationDefinitionCommand::getSymbol() const { + return d_symbol; +} + +/* class DeclareFunctionCommand */ + +DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) : + DeclarationDefinitionCommand(id), + d_type(t) { +} + +Type DeclareFunctionCommand::getType() const { + return d_type; +} + +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) { + Dump("declarations") << *this << endl; +} + +/* class DeclareTypeCommand */ + +DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) : + DeclarationDefinitionCommand(id), + d_arity(arity), + d_type(t) { +} + +size_t DeclareTypeCommand::getArity() const { + return d_arity; +} + +Type DeclareTypeCommand::getType() const { + return d_type; +} + +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) { + Dump("declarations") << *this << endl; +} + +/* class DefineTypeCommand */ -DeclarationCommand::DeclarationCommand(const std::string& id, Type t) : +DefineTypeCommand::DefineTypeCommand(const std::string& id, + Type t) : + DeclarationDefinitionCommand(id), + d_params(), d_type(t) { - d_declaredSymbols.push_back(id); } -DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, Type t) : - d_declaredSymbols(ids), +DefineTypeCommand::DefineTypeCommand(const std::string& id, + const std::vector<Type>& params, + Type t) : + DeclarationDefinitionCommand(id), + d_params(params), d_type(t) { } -const std::vector<std::string>& DeclarationCommand::getDeclaredSymbols() const { - return d_declaredSymbols; +const std::vector<Type>& DefineTypeCommand::getParameters() const { + return d_params; } -Type DeclarationCommand::getDeclaredType() const { +Type DefineTypeCommand::getType() const { return d_type; } +void DefineTypeCommand::invoke(SmtEngine* smtEngine) { + Dump("declarations") << *this << endl; +} + /* class DefineFunctionCommand */ -DefineFunctionCommand::DefineFunctionCommand(Expr func, +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, + Expr formula) : + DeclarationDefinitionCommand(id), + d_func(func), + d_formals(), + d_formula(formula) { +} + +DefineFunctionCommand::DefineFunctionCommand(const std::string& id, + Expr func, const std::vector<Expr>& formals, Expr formula) : + DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), d_formula(formula) { } +Expr DefineFunctionCommand::getFunction() const { + return d_func; +} + +const std::vector<Expr>& DefineFunctionCommand::getFormals() const { + return d_formals; +} + +Expr DefineFunctionCommand::getFormula() const { + return d_formula; +} + void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { - smtEngine->defineFunction(d_func, d_formals, d_formula); + Dump("declarations") << *this << endl; + if(!d_func.isNull()) { + smtEngine->defineFunction(d_func, d_formals, d_formula); + } } -/* class DefineFunctionCommand */ +/* class DefineNamedFunctionCommand */ -DefineNamedFunctionCommand::DefineNamedFunctionCommand(Expr func, +DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, + Expr func, const std::vector<Expr>& formals, Expr formula) : - DefineFunctionCommand(func, formals, formula) { + DefineFunctionCommand(id, func, formals, formula) { } void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { this->DefineFunctionCommand::invoke(smtEngine); - if(d_func.getType().isBoolean()) { + if(!d_func.isNull() && d_func.getType().isBoolean()) { smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); } @@ -231,6 +367,10 @@ SimplifyCommand::SimplifyCommand(Expr term) : d_term(term) { } +Expr SimplifyCommand::getTerm() const { + return d_term; +} + void SimplifyCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->simplify(d_term); } @@ -249,6 +389,10 @@ GetValueCommand::GetValueCommand(Expr term) : d_term(term) { } +Expr GetValueCommand::getTerm() const { + return d_term; +} + void GetValueCommand::invoke(SmtEngine* smtEngine) { d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term, smtEngine->getValue(d_term)); @@ -305,6 +449,10 @@ SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : d_status(status) { } +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const { + return d_status; +} + void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { stringstream ss; ss << d_status; @@ -326,6 +474,10 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : d_logic(logic) { } +std::string SetBenchmarkLogicCommand::getLogic() const { + return d_logic; +} + void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setLogic(d_logic); @@ -337,11 +489,19 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { /* class SetInfoCommand */ -SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) : +SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) : d_flag(flag), d_sexpr(sexpr) { } +std::string SetInfoCommand::getFlag() const { + return d_flag; +} + +SExpr SetInfoCommand::getSExpr() const { + return d_sexpr; +} + void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); @@ -369,6 +529,10 @@ GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) { } +std::string GetInfoCommand::getFlag() const { + return d_flag; +} + void GetInfoCommand::invoke(SmtEngine* smtEngine) { try { stringstream ss; @@ -391,11 +555,19 @@ void GetInfoCommand::printResult(std::ostream& out) const { /* class SetOptionCommand */ -SetOptionCommand::SetOptionCommand(std::string flag, SExpr& sexpr) : +SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) : d_flag(flag), d_sexpr(sexpr) { } +std::string SetOptionCommand::getFlag() const { + return d_flag; +} + +SExpr SetOptionCommand::getSExpr() const { + return d_sexpr; +} + void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); @@ -423,6 +595,10 @@ GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) { } +std::string GetOptionCommand::getFlag() const { + return d_flag; +} + void GetOptionCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getOption(d_flag).getValue(); @@ -446,17 +622,19 @@ void GetOptionCommand::printResult(std::ostream& out) const { DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : d_datatypes() { d_datatypes.push_back(datatype); - Debug("datatypes") << "Create datatype command." << endl; } DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) : d_datatypes(datatypes) { - Debug("datatypes") << "Create datatype command." << endl; +} + +const std::vector<DatatypeType>& +DatatypeDeclarationCommand::getDatatypes() const { + return d_datatypes; } void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { - Debug("datatypes") << "Invoke datatype command." << endl; - //smtEngine->addDatatypeDefinitions(d_datatype); + Dump("declarations") << *this << endl; } /* output stream insertion operator for benchmark statuses */ diff --git a/src/expr/command.h b/src/expr/command.h index 50d382038..5cf4f6fa0 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -2,8 +2,8 @@ /*! \file command.h ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway + ** Major contributors: none + ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -59,26 +59,31 @@ std::ostream& operator<<(std::ostream& out, class CVC4_PUBLIC Command { public: + virtual ~Command() {} + virtual void invoke(SmtEngine* smtEngine) = 0; virtual void invoke(SmtEngine* smtEngine, std::ostream& out); - virtual ~Command() {}; + virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, OutputLanguage language = language::output::LANG_AST) const; + 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). + * EmptyCommands 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 = ""); + std::string getName() const; void invoke(SmtEngine* smtEngine); - std::string getName() const { return d_name; } };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { @@ -86,8 +91,8 @@ protected: BoolExpr d_expr; public: AssertCommand(const BoolExpr& e); + BoolExpr getExpr() const; void invoke(SmtEngine* smtEngine); - BoolExpr getExpr() const { return d_expr; } };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { @@ -100,30 +105,59 @@ public: void invoke(SmtEngine* smtEngine); };/* class PopCommand */ -class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { +class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { +protected: + std::string d_symbol; +public: + DeclarationDefinitionCommand(const std::string& id); + std::string getSymbol() const; +};/* class DeclarationDefinitionCommand */ + +class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { +protected: + Type d_type; +public: + DeclareFunctionCommand(const std::string& id, Type type); + Type getType() const; + void invoke(SmtEngine* smtEngine); +};/* class DeclareFunctionCommand */ + +class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { +protected: + size_t d_arity; + Type d_type; +public: + DeclareTypeCommand(const std::string& id, size_t arity, Type t); + size_t getArity() const; + Type getType() const; + void invoke(SmtEngine* smtEngine); +};/* class DeclareTypeCommand */ + +class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { protected: - std::vector<std::string> d_declaredSymbols; + std::vector<Type> d_params; Type d_type; public: - DeclarationCommand(const std::string& id, Type t); - DeclarationCommand(const std::vector<std::string>& ids, Type t); - const std::vector<std::string>& getDeclaredSymbols() const; - Type getDeclaredType() const; -};/* class DeclarationCommand */ + DefineTypeCommand(const std::string& id, Type t); + DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t); + const std::vector<Type>& getParameters() const; + Type getType() const; + void invoke(SmtEngine* smtEngine); +};/* class DefineTypeCommand */ -class CVC4_PUBLIC DefineFunctionCommand : public Command { +class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { protected: Expr d_func; std::vector<Expr> d_formals; Expr d_formula; public: - DefineFunctionCommand(Expr func, - const std::vector<Expr>& formals, - Expr formula); + DefineFunctionCommand(const std::string& id, Expr func, Expr formula); + DefineFunctionCommand(const std::string& id, Expr func, + const std::vector<Expr>& formals, Expr formula); + Expr getFunction() const; + const std::vector<Expr>& getFormals() const; + Expr getFormula() const; void invoke(SmtEngine* smtEngine); - Expr getFunction() const { return d_func; } - const std::vector<Expr>& getFormals() const { return d_formals; } - Expr getFormula() const { return d_formula; } };/* class DefineFunctionCommand */ /** @@ -133,9 +167,8 @@ public: */ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { public: - DefineNamedFunctionCommand(Expr func, - const std::vector<Expr>& formals, - Expr formula); + DefineNamedFunctionCommand(const std::string& id, Expr func, + const std::vector<Expr>& formals, Expr formula); void invoke(SmtEngine* smtEngine); };/* class DefineNamedFunctionCommand */ @@ -144,9 +177,10 @@ protected: BoolExpr d_expr; Result d_result; public: + CheckSatCommand(); CheckSatCommand(const BoolExpr& expr); + BoolExpr getExpr() const; void invoke(SmtEngine* smtEngine); - BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; };/* class CheckSatCommand */ @@ -157,8 +191,8 @@ protected: Result d_result; public: QueryCommand(const BoolExpr& e); + BoolExpr getExpr() const; void invoke(SmtEngine* smtEngine); - BoolExpr getExpr() const { return d_expr; } Result getResult() const; void printResult(std::ostream& out) const; };/* class QueryCommand */ @@ -170,8 +204,8 @@ protected: Expr d_result; public: SimplifyCommand(Expr term); + Expr getTerm() const; void invoke(SmtEngine* smtEngine); - Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; };/* class SimplifyCommand */ @@ -182,8 +216,8 @@ protected: Expr d_result; public: GetValueCommand(Expr term); + Expr getTerm() const; void invoke(SmtEngine* smtEngine); - Expr getTerm() const { return d_term; } Expr getResult() const; void printResult(std::ostream& out) const; };/* class GetValueCommand */ @@ -214,8 +248,8 @@ protected: BenchmarkStatus d_status; public: SetBenchmarkStatusCommand(BenchmarkStatus status); + BenchmarkStatus getStatus() const; void invoke(SmtEngine* smtEngine); - BenchmarkStatus getStatus() const { return d_status; } };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { @@ -224,8 +258,8 @@ protected: std::string d_logic; public: SetBenchmarkLogicCommand(std::string logic); + std::string getLogic() const; void invoke(SmtEngine* smtEngine); - std::string getLogic() const { return d_logic; } };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { @@ -234,10 +268,10 @@ protected: SExpr d_sexpr; std::string d_result; public: - SetInfoCommand(std::string flag, SExpr& sexpr); + SetInfoCommand(std::string flag, const SExpr& sexpr); + std::string getFlag() const; + SExpr getSExpr() const; void invoke(SmtEngine* smtEngine); - std::string getFlag() const { return d_flag; } - SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetInfoCommand */ @@ -248,8 +282,8 @@ protected: std::string d_result; public: GetInfoCommand(std::string flag); + std::string getFlag() const; void invoke(SmtEngine* smtEngine); - std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetInfoCommand */ @@ -260,10 +294,10 @@ protected: SExpr d_sexpr; std::string d_result; public: - SetOptionCommand(std::string flag, SExpr& sexpr); + SetOptionCommand(std::string flag, const SExpr& sexpr); + std::string getFlag() const; + SExpr getSExpr() const; void invoke(SmtEngine* smtEngine); - std::string getFlag() const { return d_flag; } - SExpr getSExpr() const { return d_sexpr; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class SetOptionCommand */ @@ -274,8 +308,8 @@ protected: std::string d_result; public: GetOptionCommand(std::string flag); + std::string getFlag() const; void invoke(SmtEngine* smtEngine); - std::string getFlag() const { return d_flag; } std::string getResult() const; void printResult(std::ostream& out) const; };/* class GetOptionCommand */ @@ -286,15 +320,24 @@ private: public: DatatypeDeclarationCommand(const DatatypeType& datatype); DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); + const std::vector<DatatypeType>& getDatatypes() const; void invoke(SmtEngine* smtEngine); - const std::vector<DatatypeType>& getDatatypes() const { return d_datatypes; } };/* class DatatypeDeclarationCommand */ -class CVC4_PUBLIC QuitCommand : public EmptyCommand { +class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand(); + void invoke(SmtEngine* smtEngine); };/* class QuitCommand */ +class CVC4_PUBLIC CommentCommand : public Command { + std::string d_comment; +public: + CommentCommand(std::string comment); + std::string getComment() const; + void invoke(SmtEngine* smtEngine); +};/* class CommentCommand */ + class CVC4_PUBLIC CommandSequence : public Command { private: /** All the commands to be executed (in sequence) */ @@ -304,20 +347,27 @@ private: public: CommandSequence(); ~CommandSequence(); + + void addCommand(Command* cmd); + void invoke(SmtEngine* smtEngine); void invoke(SmtEngine* smtEngine, std::ostream& out); - void addCommand(Command* cmd); typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; - const_iterator begin() const { return d_commandSequence.begin(); } - const_iterator end() const { return d_commandSequence.end(); } + const_iterator begin() const; + const_iterator end() const; + + iterator begin(); + iterator end(); - iterator begin() { return d_commandSequence.begin(); } - iterator end() { return d_commandSequence.end(); } };/* class CommandSequence */ +class CVC4_PUBLIC DeclarationSequence : public CommandSequence { +public: +};/* class DeclarationSequence */ + }/* CVC4 namespace */ #endif /* __CVC4__COMMAND_H */ diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h index 655accde3..451250e52 100644 --- a/src/expr/convenience_node_builders.h +++ b/src/expr/convenience_node_builders.h @@ -5,7 +5,7 @@ ** 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) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp index ae91efa68..37c709b6a 100644 --- a/src/expr/declaration_scope.cpp +++ b/src/expr/declaration_scope.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index d695a3bf8..4bce5e1be 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 038f58f95..f013c1644 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: cconway, mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -116,6 +116,10 @@ ExprManager::~ExprManager() { delete d_ctxt; } +const Options* ExprManager::getOptions() const { + return d_nodeManager->getOptions(); +} + BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index eb67277a1..2828ae381 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): taking, cconway + ** Minor contributors (to current version): ajreynol, taking, cconway ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -114,6 +114,9 @@ public: */ ~ExprManager(); + /** Get this node manager's options */ + const Options* getOptions() const; + /** Get the type for booleans */ BooleanType booleanType() const; diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h index a6b99fb73..990ce9982 100644 --- a/src/expr/expr_stream.h +++ b/src/expr/expr_stream.h @@ -5,7 +5,7 @@ ** 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) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 7c2d02809..619fd5280 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -21,15 +21,19 @@ #include "expr/expr_manager_scope.h" #include "util/Assert.h" +#include <iterator> +#include <utility> + ${includes} // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 31 "${template}" +#line 34 "${template}" using namespace CVC4::kind; +using namespace std; namespace CVC4 { @@ -73,7 +77,7 @@ TypeCheckingException::~TypeCheckingException() throw () { } void TypeCheckingException::toStream(std::ostream& os) const { - os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr; + os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; } Expr TypeCheckingException::getExpression() const { @@ -208,6 +212,59 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) { return d_exprManager->getType(*this, check); } +Expr Expr::substitute(Expr e, Expr replacement) const { + return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)))); +} + +template <class Iterator> +class NodeIteratorAdaptor : public std::iterator<std::input_iterator_tag, Node> { + Iterator d_iterator; +public: + NodeIteratorAdaptor(Iterator i) : d_iterator(i) { + } + NodeIteratorAdaptor& operator++() { ++d_iterator; return *this; } + NodeIteratorAdaptor operator++(int) { NodeIteratorAdaptor i(d_iterator); ++d_iterator; return i; } + bool operator==(NodeIteratorAdaptor i) { return d_iterator == i.d_iterator; } + bool operator!=(NodeIteratorAdaptor i) { return !(*this == i); } + Node operator*() { return Node::fromExpr(*d_iterator); } +};/* class NodeIteratorAdaptor */ + +template <class Iterator> +static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) { + return NodeIteratorAdaptor<Iterator>(i); +} + +Expr Expr::substitute(const std::vector<Expr> exes, + const std::vector<Expr>& replacements) const { + return Expr(d_exprManager, + new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()), + mkNodeIteratorAdaptor(exes.end()), + mkNodeIteratorAdaptor(replacements.begin()), + mkNodeIteratorAdaptor(replacements.end())))); +} + +template <class Iterator> +class NodePairIteratorAdaptor : public std::iterator<std::input_iterator_tag, pair<Node, Node> > { + Iterator d_iterator; +public: + NodePairIteratorAdaptor(Iterator i) : d_iterator(i) { + } + NodePairIteratorAdaptor& operator++() { ++d_iterator; return *this; } + NodePairIteratorAdaptor operator++(int) { NodePairIteratorAdaptor i(d_iterator); ++d_iterator; return i; } + bool operator==(NodePairIteratorAdaptor i) { return d_iterator == i.d_iterator; } + bool operator!=(NodePairIteratorAdaptor i) { return !(*this == i); } + pair<Node, Node> operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); } +};/* class NodePairIteratorAdaptor */ + +template <class Iterator> +static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterator i) { + return NodePairIteratorAdaptor<Iterator>(i); +} + +Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const { + return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); +} + Expr::const_iterator::const_iterator() : d_iterator(NULL) { } @@ -280,6 +337,12 @@ Expr::operator bool() const { return !isNull(); } +bool Expr::isVariable() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->getMetaKind() == kind::metakind::VARIABLE; +} + bool Expr::isConst() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index bffb37ddb..e95e434fe 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -35,12 +35,13 @@ ${includes} #include "util/exception.h" #include "util/language.h" +#include "util/hash.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 44 "${template}" +#line 45 "${template}" namespace CVC4 { @@ -121,6 +122,11 @@ std::ostream& operator<<(std::ostream& out, */ std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC; +// for hash_maps, hash_sets.. +struct ExprHashFunction { + size_t operator()(CVC4::Expr e) const; +};/* struct ExprHashFunction */ + /** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. @@ -344,6 +350,22 @@ public: Type getType(bool check = false) const throw (TypeCheckingException); /** + * Substitute "replacement" in for "e". + */ + Expr substitute(Expr e, Expr replacement) const; + + /** + * Substitute "replacements" in for "exes". + */ + Expr substitute(const std::vector<Expr> exes, + const std::vector<Expr>& replacements) const; + + /** + * Substitute pairs of (ex,replacement) from the given map. + */ + Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const; + + /** * Returns the string representation of the expression. * @return a string representation of the expression */ @@ -365,18 +387,28 @@ public: /** * Check if this is a null expression. + * * @return true if a null expression */ bool isNull() const; /** * Check if this is a null expression. + * * @return true if NOT a null expression */ operator bool() const; /** + * Check if this is an expression representing a variable. + * + * @return true if a variable expression + */ + bool isVariable() const; + + /** * Check if this is an expression representing a constant. + * * @return true if a constant expression */ bool isConst() const; @@ -541,7 +573,7 @@ public: /** * Make a Boolean if-then-else expression using this expression as the - * condition, and given the then and else parts + * condition, and given the then and else parts. * @param then_e the then branch expression * @param else_e the else branch expression * @return the if-then-else expression @@ -550,13 +582,14 @@ public: /** * Make a term if-then-else expression using this expression as the - * condition, and given the then and else parts + * condition, and given the then and else parts. * @param then_e the then branch expression * @param else_e the else branch expression * @return the if-then-else expression */ Expr iteExpr(const Expr& then_e, const Expr& else_e) const; -}; + +};/* class BoolExpr */ namespace expr { @@ -791,7 +824,7 @@ public: ${getConst_instantiations} -#line 795 "${template}" +#line 828 "${template}" namespace expr { @@ -839,12 +872,9 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) { }/* CVC4::expr namespace */ -// for hash_maps, hash_sets.. -struct ExprHashFunction { - size_t operator()(CVC4::Expr e) const { - return (size_t) e.getId(); - } -};/* struct ExprHashFunction */ +inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { + return (size_t) e.getId(); +} }/* CVC4 namespace */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index a02339e5e..974bd6791 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -1,7 +1,7 @@ /********************* */ /*! \file kind_map.h ** \verbatim - ** Original author: mdeters + ** Original author: dejan ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 5f9aa6619..a954a7f70 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 479ef6d11..69f7019ab 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -107,6 +107,25 @@ function endtheory { seen_endtheory=true } +function typechecker { + # typechecker header + lineno=${BASH_LINENO[0]} + check_theory_seen + typechecker_includes="${typechecker_includes} +#include \"$1\"" +} + +function typerule { + # typerule OPERATOR typechecking-class + lineno=${BASH_LINENO[0]} + check_theory_seen + typerules="${typerules} + case kind::$1: + typeNode = $2::computeType(nodeManager, n, check); + break; +" +} + function sort { # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"] lineno=${BASH_LINENO[0]} @@ -225,6 +244,8 @@ for var in \ getConst_implementations \ mkConst_instantiations \ mkConst_implementations \ + typechecker_includes \ + typerules \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done diff --git a/src/expr/mkkind b/src/expr/mkkind index 47d02863e..abb238f1a 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -118,6 +118,18 @@ function endtheory { seen_endtheory=true } +function typechecker { + # typechecker header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function typerule { + # typerule OPERATOR typechecking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # properties prop* lineno=${BASH_LINENO[0]} diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 46a69dee5..d84691e14 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -93,6 +93,18 @@ function endtheory { seen_endtheory=true } +function typechecker { + # typechecker header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function typerule { + # typerule OPERATOR typechecking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # rewriter class header lineno=${BASH_LINENO[0]} diff --git a/src/expr/node.h b/src/expr/node.h index f501dba21..0f4b55d4a 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -28,6 +28,8 @@ #include <string> #include <iostream> #include <utility> +#include <algorithm> +#include <functional> #include <stdint.h> #include "expr/type.h" @@ -832,16 +834,23 @@ public: */ inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const; - NodeTemplate<true> eqNode(const NodeTemplate& right) const; + template <bool ref_count2> + NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const; NodeTemplate<true> notNode() const; - NodeTemplate<true> andNode(const NodeTemplate& right) const; - NodeTemplate<true> orNode(const NodeTemplate& right) const; - NodeTemplate<true> iteNode(const NodeTemplate& thenpart, - const NodeTemplate& elsepart) const; - NodeTemplate<true> iffNode(const NodeTemplate& right) const; - NodeTemplate<true> impNode(const NodeTemplate& right) const; - NodeTemplate<true> xorNode(const NodeTemplate& right) const; + template <bool ref_count2> + NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const; + template <bool ref_count2> + NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const; + template <bool ref_count2, bool ref_count3> + NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart, + const NodeTemplate<ref_count3>& elsepart) const; + template <bool ref_count2> + NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const; + template <bool ref_count2> + NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const; + template <bool ref_count2> + NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const; };/* class NodeTemplate<ref_count> */ @@ -1085,8 +1094,9 @@ operator=(const NodeTemplate<!ref_count>& e) { } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); } @@ -1098,44 +1108,50 @@ NodeTemplate<true> NodeTemplate<ref_count>::notNode() const { } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::AND, *this, right); } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::OR, *this, right); } template <bool ref_count> +template <bool ref_count2, bool ref_count3> NodeTemplate<true> -NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart, - const NodeTemplate<ref_count>& elsepart) const { +NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart, + const NodeTemplate<ref_count3>& elsepart) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); } template <bool ref_count> +template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const { +NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); } @@ -1273,11 +1289,13 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, } // otherwise compute - Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin, + Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd), "Substitution iterator ranges must be equal size" ); - Iterator1 j = find(nodesBegin, nodesEnd, *this); + Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this)); if(j != nodesEnd) { - Node n = *(replacementsBegin + (j - nodesBegin)); + Iterator2 b = replacementsBegin; + std::advance(b, std::distance(nodesBegin, j)); + Node n = *b; cache[*this] = n; return n; } else if(getNumChildren() == 0) { diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 156d14299..2cb2527b2 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -5,7 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index ce3db4a40..3b4d8ac66 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -18,21 +18,15 @@ ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). **/ -#include "node_manager.h" - -#include "theory/builtin/theory_builtin_type_rules.h" -#include "theory/booleans/theory_bool_type_rules.h" -#include "theory/uf/theory_uf_type_rules.h" -#include "theory/arith/theory_arith_type_rules.h" -#include "theory/arrays/theory_arrays_type_rules.h" -#include "theory/bv/theory_bv_type_rules.h" -#include "theory/datatypes/theory_datatypes_type_rules.h" +#include "expr/node_manager.h" #include "util/Assert.h" #include "util/options.h" #include "util/stats.h" #include "util/tls.h" +#include "expr/type_checker.h" + #include <algorithm> #include <stack> #include <ext/hash_set> @@ -241,234 +235,6 @@ void NodeManager::reclaimZombies() { } }/* NodeManager::reclaimZombies() */ -TypeNode NodeManager::computeType(TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - TypeNode typeNode; - - // Infer the type - switch(n.getKind()) { - case kind::VARIABLE: - typeNode = getAttribute(n, TypeAttr()); - break; - case kind::SKOLEM: - typeNode = getAttribute(n, TypeAttr()); - break; - case kind::BUILTIN: - typeNode = builtinOperatorType(); - break; - case kind::SORT_TYPE: - typeNode = kindType(); - break; - case kind::APPLY: - typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check); - break; - case kind::EQUAL: - typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check); - break; - case kind::DISTINCT: - typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n, check); - break; - case kind::TUPLE: - typeNode = CVC4::theory::builtin::TupleTypeRule::computeType(this, n, check); - break; - case kind::CONST_BOOLEAN: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::NOT: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::AND: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::IFF: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::IMPLIES: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::OR: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::XOR: - typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check); - break; - case kind::ITE: - typeNode = CVC4::theory::boolean::IteTypeRule::computeType(this, n, check); - break; - case kind::APPLY_UF: - typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check); - break; - case kind::PLUS: - typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check); - break; - case kind::MULT: - typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check); - break; - case kind::MINUS: - typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check); - break; - case kind::UMINUS: - typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check); - break; - case kind::DIVISION: - typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check); - break; - case kind::CONST_RATIONAL: - typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check); - break; - case kind::CONST_INTEGER: - typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n, check); - break; - case kind::LT: - typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check); - break; - case kind::LEQ: - typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check); - break; - case kind::GT: - typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check); - break; - case kind::GEQ: - typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n, check); - break; - case kind::SELECT: - typeNode = CVC4::theory::arrays::ArraySelectTypeRule::computeType(this, n, check); - break; - case kind::STORE: - typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n, check); - break; - case kind::CONST_BITVECTOR: - typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_AND: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_OR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_XOR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_NOT: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_NAND: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_NOR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_XNOR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_COMP: - typeNode = CVC4::theory::bv::BitVectorCompRule::computeType(this, n, check); - break; - case kind::BITVECTOR_MULT: - typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check); - break; - case kind::BITVECTOR_PLUS: - typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SUB: - typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check); - break; - case kind::BITVECTOR_NEG: - typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n, check); - break; - case kind::BITVECTOR_UDIV: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_UREM: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SDIV: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SREM: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SMOD: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SHL: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_LSHR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ASHR: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ROTATE_LEFT: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ROTATE_RIGHT: - typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ULT: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ULE: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_UGT: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_UGE: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SLT: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SLE: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SGT: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SGE: - typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_EXTRACT: - typeNode = CVC4::theory::bv::BitVectorExtractTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_CONCAT: - typeNode = CVC4::theory::bv::BitVectorConcatRule::computeType(this, n, check); - break; - case kind::BITVECTOR_REPEAT: - typeNode = CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_ZERO_EXTEND: - typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check); - break; - case kind::BITVECTOR_SIGN_EXTEND: - typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check); - break; - case kind::APPLY_CONSTRUCTOR: - typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check); - break; - case kind::APPLY_SELECTOR: - typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check); - break; - case kind::APPLY_TESTER: - typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check); - break; - case kind::APPLY_TYPE_ASCRIPTION: - typeNode = CVC4::theory::datatypes::DatatypeAscriptionTypeRule::computeType(this, n, check); - break; - default: - Debug("getType") << "FAILURE" << std::endl; - Unhandled(n.getKind()); - } - - setAttribute(n, TypeAttr(), typeNode); - setAttribute(n, TypeCheckedAttr(), - check || getAttribute(n, TypeCheckedAttr())); - - return typeNode; -} - TypeNode NodeManager::getType(TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { // Many theories' type checkers call Node::getType() directly. @@ -510,7 +276,7 @@ TypeNode NodeManager::getType(TNode n, bool check) if( readyToCompute ) { /* All the children have types, time to compute */ - typeNode = computeType(m, check); + typeNode = TypeChecker::computeType(this, m, check); worklist.pop(); } } // end while @@ -520,7 +286,7 @@ TypeNode NodeManager::getType(TNode n, bool check) } else if( !hasType || needsCheck ) { /* We can compute the type top-down, without worrying about deep recursion. */ - typeNode = computeType(n, check); + typeNode = TypeChecker::computeType(this, n, check); } /* The type should be have been computed and stored. */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0ac215f1e..6adcb62a9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A manager for Nodes. + ** \brief A manager for Nodes ** ** A manager for Nodes. ** @@ -48,6 +48,8 @@ class StatisticsRegistry; namespace expr { +class TypeChecker; + // Definition of an attribute for the variable name. // TODO: hide this attribute behind a NodeManager interface. namespace attr { @@ -64,6 +66,7 @@ class NodeManager { template <unsigned nchild_thresh> friend class CVC4::NodeBuilder; friend class NodeManagerScope; friend class expr::NodeValue; + friend class expr::TypeChecker; /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { @@ -250,9 +253,6 @@ class NodeManager { // undefined private copy constructor (disallow copy) NodeManager(const NodeManager&) CVC4_UNDEFINED; - TypeNode computeType(TNode n, bool check = false) - throw (TypeCheckingExceptionPrivate, AssertionException); - void init(); public: diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index c38243b0a..37c28ab07 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -5,7 +5,7 @@ ** 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) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 666462875..5fe48b01d 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -2,10 +2,10 @@ /*! \file node_value.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan + ** Major contributors: dejan + ** 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) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 2c11b58d5..71aa37926 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -2,10 +2,10 @@ /*! \file node_value.h ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): cconway, taking + ** Major contributors: none + ** Minor contributors (to current version): cconway, taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/expr/type.cpp b/src/expr/type.cpp index e162065b0..28bcb460f 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: dejan, mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type.h b/src/expr/type.h index a63ca6cf0..5bff8d12a 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -2,8 +2,8 @@ /*! \file type.h ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -397,7 +397,7 @@ class CVC4_PUBLIC BooleanType : public Type { public: /** Construct from the base type */ - BooleanType(const Type& type) throw(AssertionException); + BooleanType(const Type& type = Type()) throw(AssertionException); };/* class BooleanType */ /** @@ -408,7 +408,7 @@ class CVC4_PUBLIC IntegerType : public Type { public: /** Construct from the base type */ - IntegerType(const Type& type) throw(AssertionException); + IntegerType(const Type& type = Type()) throw(AssertionException); };/* class IntegerType */ /** @@ -419,7 +419,7 @@ class CVC4_PUBLIC RealType : public Type { public: /** Construct from the base type */ - RealType(const Type& type) throw(AssertionException); + RealType(const Type& type = Type()) throw(AssertionException); };/* class RealType */ /** @@ -441,7 +441,7 @@ class CVC4_PUBLIC FunctionType : public Type { public: /** Construct from the base type */ - FunctionType(const Type& type) throw(AssertionException); + FunctionType(const Type& type = Type()) throw(AssertionException); /** Get the argument types */ std::vector<Type> getArgTypes() const; @@ -458,7 +458,7 @@ class CVC4_PUBLIC TupleType : public Type { public: /** Construct from the base type */ - TupleType(const Type& type) throw(AssertionException); + TupleType(const Type& type = Type()) throw(AssertionException); /** Get the constituent types */ std::vector<Type> getTypes() const; @@ -472,7 +472,7 @@ class CVC4_PUBLIC ArrayType : public Type { public: /** Construct from the base type */ - ArrayType(const Type& type) throw(AssertionException); + ArrayType(const Type& type = Type()) throw(AssertionException); /** Get the index type */ Type getIndexType() const; @@ -489,7 +489,7 @@ class CVC4_PUBLIC SortType : public Type { public: /** Construct from the base type */ - SortType(const Type& type) throw(AssertionException); + SortType(const Type& type = Type()) throw(AssertionException); /** Get the name of the sort */ std::string getName() const; @@ -510,7 +510,7 @@ class CVC4_PUBLIC SortConstructorType : public Type { public: /** Construct from the base type */ - SortConstructorType(const Type& type) throw(AssertionException); + SortConstructorType(const Type& type = Type()) throw(AssertionException); /** Get the name of the sort constructor */ std::string getName() const; @@ -530,7 +530,7 @@ class CVC4_PUBLIC KindType : public Type { public: /** Construct from the base type */ - KindType(const Type& type) throw(AssertionException); + KindType(const Type& type = Type()) throw(AssertionException); };/* class KindType */ /** @@ -541,7 +541,7 @@ class CVC4_PUBLIC BitVectorType : public Type { public: /** Construct from the base type */ - BitVectorType(const Type& type) throw(AssertionException); + BitVectorType(const Type& type = Type()) throw(AssertionException); /** * Returns the size of the bit-vector type. @@ -559,7 +559,7 @@ class CVC4_PUBLIC DatatypeType : public Type { public: /** Construct from the base type */ - DatatypeType(const Type& type) throw(AssertionException); + DatatypeType(const Type& type = Type()) throw(AssertionException); /** Get the underlying datatype */ const Datatype& getDatatype() const; @@ -599,7 +599,7 @@ class CVC4_PUBLIC ConstructorType : public Type { public: /** Construct from the base type */ - ConstructorType(const Type& type) throw(AssertionException); + ConstructorType(const Type& type = Type()) throw(AssertionException); /** Get the range type */ DatatypeType getRangeType() const; @@ -621,7 +621,7 @@ class CVC4_PUBLIC SelectorType : public Type { public: /** Construct from the base type */ - SelectorType(const Type& type) throw(AssertionException); + SelectorType(const Type& type = Type()) throw(AssertionException); /** Get the domain type for this selector (the datatype type) */ DatatypeType getDomain() const; @@ -639,7 +639,7 @@ class CVC4_PUBLIC TesterType : public Type { public: /** Construct from the base type */ - TesterType(const Type& type) throw(AssertionException); + TesterType(const Type& type = Type()) throw(AssertionException); /** Get the type that this tester tests (the datatype type) */ DatatypeType getDomain() const; diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h new file mode 100644 index 000000000..0c8093469 --- /dev/null +++ b/src/expr/type_checker.h @@ -0,0 +1,40 @@ +/********************* */ +/*! \file type_checker.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: cconway, dejan + ** Minor contributors (to current version): acsys, taking + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 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 A type checker + ** + ** A type checker. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR__TYPE_CHECKER_H +#define __CVC4__EXPR__TYPE_CHECKER_H + +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +class TypeChecker { +public: + + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check = false) + throw (TypeCheckingExceptionPrivate, AssertionException); + +};/* class TypeChecker */ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__TYPE_CHECKER_H */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp new file mode 100644 index 000000000..2791376b5 --- /dev/null +++ b/src/expr/type_checker_template.cpp @@ -0,0 +1,66 @@ +/********************* */ +/*! \file type_checker_template.cpp + ** \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, 2011 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 TypeChecker implementation + ** + ** TypeChecker implementation. + **/ + +#line 20 "${template}" + +#include "expr/type_checker.h" +#include "expr/node_manager.h" + +${typechecker_includes} + +#line 27 "${template}" + +namespace CVC4 { +namespace expr { + +TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TypeNode typeNode; + + // Infer the type + switch(n.getKind()) { + case kind::VARIABLE: + case kind::SKOLEM: + typeNode = nodeManager->getAttribute(n, NodeManager::TypeAttr()); + break; + case kind::BUILTIN: + typeNode = nodeManager->builtinOperatorType(); + break; + case kind::SORT_TYPE: + typeNode = nodeManager->kindType(); + break; + +${typerules} + +#line 51 "${template}" + + default: + Debug("getType") << "FAILURE" << std::endl; + Unhandled(n.getKind()); + } + + nodeManager->setAttribute(n, NodeManager::TypeAttr(), typeNode); + nodeManager->setAttribute(n, NodeManager::TypeCheckedAttr(), + check || nodeManager->getAttribute(n, NodeManager::TypeCheckedAttr())); + + return typeNode; + +}/* TypeChecker::computeType */ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 76a084204..51d86904a 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -2,8 +2,8 @@ /*! \file type_node.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: mdeters + ** Minor contributors (to current version): taking, ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 3f4e52d36..25af3aae6 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: mdeters - ** Minor contributors (to current version): taking + ** Minor contributors (to current version): taking, ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences |