From c991b73b95734fb306badeafb5f387623c7fb790 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Sat, 6 Feb 2010 03:06:07 +0000 Subject: [PATCH] Preliminary support for types in parser --- configure | 28 +-- src/expr/Makefile.am | 2 + src/expr/command.h | 6 +- src/expr/expr_manager.cpp | 35 ++- src/expr/expr_manager.h | 29 ++- src/expr/type.cpp | 142 ++++++++++++ src/expr/type.h | 122 ++++++++++ src/parser/Makefile.am | 2 +- src/parser/antlr_parser.cpp | 263 ++++++++++++++++++---- src/parser/antlr_parser.h | 132 ++++++++--- src/parser/cvc/cvc_lexer.g | 3 + src/parser/cvc/cvc_parser.g | 294 +++++++++++++++++-------- src/parser/smt/smt_lexer.g | 2 +- src/parser/smt/smt_parser.g | 238 +++++++++----------- src/parser/symbol_table.h | 8 +- test/regress/regress0/boolean-prec.cvc | 6 + test/unit/parser/parser_black.h | 46 +++- 17 files changed, 1008 insertions(+), 350 deletions(-) create mode 100644 src/expr/type.cpp create mode 100644 src/expr/type.h create mode 100644 test/regress/regress0/boolean-prec.cvc diff --git a/configure b/configure index f32d1810a..24bd90127 100755 --- a/configure +++ b/configure @@ -16462,7 +16462,7 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" mk_include=include -ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/context/Makefile src/Makefile src/util/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/main/Makefile src/theory/Makefile src/theory/uf/Makefile src/theory/arith/Makefile src/theory/bool/Makefile src/smt/Makefile src/prop/Makefile src/prop/minisat/Makefile src/expr/Makefile test/system/Makefile test/Makefile test/unit/Makefile test/regress/Makefile test/regress/regress0/Makefile test/regress/regress1/Makefile test/regress/regress2/Makefile test/regress/regress3/Makefile" +ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/util/Makefile src/expr/Makefile src/theory/bool/Makefile src/theory/uf/Makefile src/theory/arith/Makefile src/theory/Makefile src/context/Makefile src/parser/cvc/Makefile src/parser/Makefile src/parser/smt/Makefile src/prop/Makefile src/prop/minisat/Makefile src/main/Makefile src/Makefile src/smt/Makefile test/unit/Makefile test/system/Makefile test/Makefile test/regress/regress3/Makefile test/regress/Makefile test/regress/regress0/Makefile test/regress/regress2/Makefile test/regress/regress1/Makefile" cat >confcache <<\_ACEOF @@ -17546,29 +17546,29 @@ do "Makefile") CONFIG_FILES="$CONFIG_FILES Makefile" ;; "contrib/Makefile") CONFIG_FILES="$CONFIG_FILES contrib/Makefile" ;; "doc/Makefile") CONFIG_FILES="$CONFIG_FILES doc/Makefile" ;; - "src/context/Makefile") CONFIG_FILES="$CONFIG_FILES src/context/Makefile" ;; - "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;; "src/util/Makefile") CONFIG_FILES="$CONFIG_FILES src/util/Makefile" ;; - "src/parser/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/Makefile" ;; - "src/parser/cvc/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/cvc/Makefile" ;; - "src/parser/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/smt/Makefile" ;; - "src/main/Makefile") CONFIG_FILES="$CONFIG_FILES src/main/Makefile" ;; - "src/theory/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/Makefile" ;; + "src/expr/Makefile") CONFIG_FILES="$CONFIG_FILES src/expr/Makefile" ;; + "src/theory/bool/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/bool/Makefile" ;; "src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;; "src/theory/arith/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/arith/Makefile" ;; - "src/theory/bool/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/bool/Makefile" ;; - "src/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/smt/Makefile" ;; + "src/theory/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/Makefile" ;; + "src/context/Makefile") CONFIG_FILES="$CONFIG_FILES src/context/Makefile" ;; + "src/parser/cvc/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/cvc/Makefile" ;; + "src/parser/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/Makefile" ;; + "src/parser/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/parser/smt/Makefile" ;; "src/prop/Makefile") CONFIG_FILES="$CONFIG_FILES src/prop/Makefile" ;; "src/prop/minisat/Makefile") CONFIG_FILES="$CONFIG_FILES src/prop/minisat/Makefile" ;; - "src/expr/Makefile") CONFIG_FILES="$CONFIG_FILES src/expr/Makefile" ;; + "src/main/Makefile") CONFIG_FILES="$CONFIG_FILES src/main/Makefile" ;; + "src/Makefile") CONFIG_FILES="$CONFIG_FILES src/Makefile" ;; + "src/smt/Makefile") CONFIG_FILES="$CONFIG_FILES src/smt/Makefile" ;; + "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;; "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;; "test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;; - "test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;; + "test/regress/regress3/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress3/Makefile" ;; "test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;; "test/regress/regress0/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress0/Makefile" ;; - "test/regress/regress1/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress1/Makefile" ;; "test/regress/regress2/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress2/Makefile" ;; - "test/regress/regress3/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress3/Makefile" ;; + "test/regress/regress1/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/regress1/Makefile" ;; *) as_fn_error "invalid argument: \`$ac_config_target'" "$LINENO" 5;; esac diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 3212fc0a0..90ec89968 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -11,6 +11,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ + type.h \ node_value.h \ node_manager.h \ expr_manager.h \ @@ -22,6 +23,7 @@ libexpr_la_SOURCES = \ expr_manager.cpp \ node_value.cpp \ expr.cpp \ + type.cpp \ command.h \ command.cpp diff --git a/src/expr/command.h b/src/expr/command.h index 923af0a4d..b6f1987a2 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -64,7 +64,7 @@ protected: class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { public: - DeclarationCommand(const std::vector& ids); + DeclarationCommand(const std::vector& ids, const Type* t); void toStream(std::ostream& out) const; protected: std::vector d_declaredSymbols; @@ -241,7 +241,9 @@ inline void CommandSequence::addCommand(Command* cmd) { /* class DeclarationCommand */ -inline DeclarationCommand::DeclarationCommand(const std::vector& ids) : +inline +DeclarationCommand::DeclarationCommand(const std::vector& ids, + const Type* t) : d_declaredSymbols(ids) { } diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index d81466305..ee61c14c9 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/expr.h" +#include "expr/type.h" #include "expr/node_manager.h" #include "expr/expr_manager.h" @@ -30,13 +31,23 @@ using namespace std; namespace CVC4 { ExprManager::ExprManager() -: d_nm(new NodeManager()) { + : d_nm(new NodeManager()), + d_booleanType(new BooleanType(this)), + d_kindType(new KindType(this)) { } ExprManager::~ExprManager() { delete d_nm; } +const BooleanType* ExprManager::booleanType() { + return d_booleanType; +} + +const KindType* ExprManager::kindType() { + return d_kindType; +} + Expr ExprManager::mkExpr(Kind kind) { return Expr(this, new Node(d_nm->mkNode(kind))); } @@ -82,7 +93,27 @@ Expr ExprManager::mkExpr(Kind kind, const vector& children) { return Expr(this, new Node(d_nm->mkNode(kind, nodes))); } -Expr ExprManager::mkVar() { +/** Make a function type from domain to range. */ +const FunctionType* +ExprManager::mkFunctionType(const Type* domain, + const Type* range) { + return new FunctionType(this,domain,range); +} + +/** Make a function type with input types from argTypes. */ +const FunctionType* +ExprManager::mkFunctionType(const std::vector& argTypes, + const Type* range) { + return new FunctionType(this,argTypes,range); +} + +const Type* ExprManager::mkSort(std::string name) { + // FIXME: Sorts should be unique per-ExprManager + return new SortType(this,name); +} + +Expr ExprManager::mkVar(const Type* type) { + // FIXME: put the type into an attribute table return Expr(this, new Node(d_nm->mkVar())); } diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 32aa41dfe..41766d64b 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -23,6 +23,10 @@ namespace CVC4 { class Expr; +class Type; +class BooleanType; +class FunctionType; +class KindType; class NodeManager; class SmtEngine; @@ -42,6 +46,11 @@ public: */ ~ExprManager(); + /** Get the type for booleans. */ + const BooleanType* booleanType(); + /** Get the type for sorts. */ + const KindType* kindType(); + /** * Make a unary expression of a given kind (TRUE, FALSE,...). * @param kind the kind of expression @@ -80,14 +89,28 @@ public: */ Expr mkExpr(Kind kind, const std::vector& children); + /** Make a function type from domain to range. */ + const FunctionType* + mkFunctionType(const Type* domain, + const Type* range); + + /** Make a function type with input types from argTypes. */ + const FunctionType* + mkFunctionType(const std::vector& argTypes, + const Type* range); + + /** Make a new sort with the given name. */ + const Type* mkSort(std::string name); + // variables are special, because duplicates are permitted - Expr mkVar(); + Expr mkVar(const Type* type); private: - /** The internal node manager */ NodeManager* d_nm; - + BooleanType* d_booleanType; + KindType* d_kindType; + /** * Returns the internal node manager. This should only be used by internal * users, i.e. the friend classes. diff --git a/src/expr/type.cpp b/src/expr/type.cpp new file mode 100644 index 000000000..5052a3b79 --- /dev/null +++ b/src/expr/type.cpp @@ -0,0 +1,142 @@ +/********************* -*- C++ -*- */ +/** type.h + ** Original author: cconway + ** 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. + ** + ** Implementation of expression types + **/ + +#include "expr/expr_manager.h" +#include "expr/type.h" +#include "util/Assert.h" +#include + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const Type& e) { + e.toStream(out); + return out; +} + +Type::Type(ExprManager* exprManager) : + d_exprManager(exprManager), d_name(std::string("")) { +} + +Type::Type(ExprManager* exprManager, std::string name) : + d_exprManager(exprManager), d_name(name) { +} + +// Type Type::operator=(const Type& t) { +// if( this != &t ) { +// d_name == t.d_name; +// } + +bool Type::operator==(const Type& t) const { + return d_name == t.d_name; +} + +bool Type::operator!=(const Type& t) const { + return !(*this == t); +} + +ExprManager* Type::getExprManager() const { + return d_exprManager; +} + +std::string Type::getName() const { + return d_name; +} + +// void Type::toStream(std::ostream& out) const { +// out << getName(); +// } + +BooleanType::BooleanType(ExprManager* exprManager) + : Type(exprManager,std::string("BOOLEAN")) { +} + +BooleanType::~BooleanType() { +} + +bool BooleanType::isBoolean() const { + return true; +} + +FunctionType::FunctionType(ExprManager* exprManager, + const Type* domain, + const Type* range) + : Type(exprManager), d_argTypes(), d_rangeType(range) { + d_argTypes.push_back(domain); +} + + // FIXME: What becomes of argument types? +FunctionType::~FunctionType() { +} + +FunctionType::FunctionType(ExprManager* exprManager, + const std::vector& argTypes, + const Type* range) + : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) { + Assert( argTypes.size() > 0 ); +} + +const std::vector FunctionType::getArgTypes() const { + return d_argTypes; +} + +const Type* FunctionType::getRangeType() const { + return d_rangeType; +} + +bool FunctionType::isFunction() const { + return true; +} + +bool FunctionType::isPredicate() const { + return d_rangeType == d_exprManager->booleanType(); +} + +void FunctionType::toStream(std::ostream& out) const { + if( d_argTypes.size() > 1 ) { + out << "("; + } + for( unsigned int i=0; i < d_argTypes.size(); ++i ) { + if( i > 0 ) { + out << ","; + } + d_argTypes[i]->toStream(out); + } + if( d_argTypes.size() > 1 ) { + out << ")"; + } + out << " -> "; + d_rangeType->toStream(out); +} + +KindType::KindType(ExprManager* exprManager) + : Type(exprManager,std::string("KIND")) { +} + +KindType::~KindType() { +} + +bool KindType::isKind() const { + return true; +} + +SortType::SortType(ExprManager* exprManager,std::string name) + : Type(exprManager,name) { +} + +SortType::~SortType() { +} + + +} diff --git a/src/expr/type.h b/src/expr/type.h new file mode 100644 index 000000000..87c3d8f5c --- /dev/null +++ b/src/expr/type.h @@ -0,0 +1,122 @@ +/********************* -*- C++ -*- */ +/** type.h + ** Original author: cconway + ** 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. + ** + ** Interface for expression types + **/ + +#ifndef __CVC4__TYPE_H +#define __CVC4__TYPE_H + +#include "cvc4_config.h" + +#include +#include + +namespace CVC4 { + +class ExprManager; + +/** + * Class encapsulating CVC4 expression types. + * NOTE: This is very much a stub interface!!! I'm putting this here + * so the parser can do some very simple type differentiation, but + * this is obviously hopelessly inadequate. -Chris + */ +class Type { + public: + Type() { }; + Type(ExprManager* const exprManager); + Type(ExprManager* const exprManager, std::string name); + virtual ~Type() { }; + + bool operator==(const Type& t) const; + bool operator!=(const Type& e) const; + + ExprManager* getExprManager() const; + + std::string getName() const; + + virtual bool isBoolean() const { + return false; + } + + virtual bool isFunction() const { + return false; + } + + virtual bool isPredicate() const { + return false; + } + + virtual bool isKind() const { + return false; + } + + virtual void toStream(std::ostream& out) const { + out << getName(); + } + +protected: + ExprManager* d_exprManager; + std::string d_name; +}; + +class BooleanType : public Type { + public: + BooleanType(ExprManager* exprManager); + ~BooleanType(); + bool isBoolean() const; +}; + +class FunctionType : public Type { + public: + FunctionType(ExprManager* exprManager, + const Type* domain, + const Type* range); + FunctionType(ExprManager* exprManager, + const std::vector& argTypes, + const Type* range); + ~FunctionType(); + const std::vector getArgTypes() const; + const Type* getRangeType() const; + bool isFunction() const; + bool isPredicate() const; + void toStream(std::ostream& out) const; + + private: + std::vector d_argTypes; + const Type* d_rangeType; +}; + +class KindType : public Type { + public: + KindType(ExprManager* exprManager); + ~KindType(); + bool isKind() const; +}; + +class SortType : public Type { + public: + SortType(ExprManager* exprManager, std::string name); + ~SortType(); +}; + +/** + * Output operator for types + * @param out the stream to output to + * @param e the type to output + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC ; +} + +#endif // __CVC4__TYPE_H diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index fe906cbe0..3ecde0169 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall -fvisibility=hidden -Wno-deprecated SUBDIRS = smt cvc diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 34691dc33..5a9af8d4a 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -21,11 +21,13 @@ */ #include +#include #include "antlr_parser.h" #include "util/output.h" #include "util/Assert.h" #include "expr/command.h" +#include "expr/type.h" using namespace std; using namespace CVC4; @@ -46,9 +48,58 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : antlr::LLkParser(lexer, k) { } -Expr AntlrParser::getVariable(std::string var_name) { - Expr e = d_varSymbolTable.getObject(var_name); - return e; +Expr AntlrParser::getSymbol(std::string name, SymbolType type) { + Assert( isDeclared(name,type) ); + switch( type ) { + case SYM_VARIABLE: // Predicates and functions share var namespace + // case SYM_PREDICATE: + case SYM_FUNCTION: + return d_varSymbolTable.getObject(name); + default: + Unhandled("Unhandled symbol type!"); + } +} + +Expr AntlrParser::getVariable(std::string name) { + return getSymbol(name,SYM_VARIABLE); +} + +Expr AntlrParser::getFunction(std::string name) { + return getSymbol(name,SYM_FUNCTION); +} + +// Expr AntlrParser::getPredicate(std::string name) { +// return getSymbol(name,SYM_PREDICATE); +// } + +const Type* +AntlrParser::getType(std::string var_name, + SymbolType type) { + Assert( isDeclared(var_name, type) ); + const Type* t = d_varTypeTable.getObject(var_name); + return t; +} + +const Type* AntlrParser::getSort(std::string name) { + Assert( isDeclared(name,SYM_SORT) ); + const Type* t = d_sortTable.getObject(name); + return t; +} + +/* Returns true if name is bound to a boolean variable. */ +bool AntlrParser::isBoolean(std::string name) { + return isDeclared(name,SYM_VARIABLE) && getType(name)->isBoolean(); +} + +/* Returns true if name is bound to a function. */ +bool AntlrParser::isFunction(std::string name) { + return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction(); +} + +/* Returns true if name is either a boolean variable OR a function + returning boolean. */ +bool AntlrParser::isPredicate(std::string name) { + return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate(); } Expr AntlrParser::getTrueExpr() const { @@ -60,7 +111,9 @@ Expr AntlrParser::getFalseExpr() const { } Expr AntlrParser::mkExpr(Kind kind, const Expr& child) { - return d_exprManager->mkExpr(kind, child); + Expr result = d_exprManager->mkExpr(kind, child); + Debug("parser") << "mkExpr() => " << result << std::endl; + return result; } Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) { @@ -82,50 +135,173 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return result; } -void AntlrParser::newFunction(std::string name, - const std::vector< std::string>& sorts) { - // FIXME: Need to actually create a function type - d_varSymbolTable.bindName(name, d_exprManager->mkVar()); +const FunctionType* +AntlrParser::functionType(const Type* domainType, + const Type* rangeType) { + return d_exprManager->mkFunctionType(domainType,rangeType); } -void AntlrParser::newFunctions(const std::vector& names, - const std::vector< std::string>& sorts) { - for(unsigned i = 0; i < names.size(); ++i) { - newFunction(names[i], sorts); +const FunctionType* +AntlrParser::functionType(const std::vector& argTypes, + const Type* rangeType) { + Assert( argTypes.size() > 0 ); + return d_exprManager->mkFunctionType(argTypes,rangeType); +} + +const FunctionType* +AntlrParser::functionType(const std::vector& sorts) { + Assert( sorts.size() > 1 ); + std::vector argTypes(sorts); + const Type* rangeType = argTypes.back(); + argTypes.pop_back(); + return functionType(argTypes,rangeType); +} + +Expr AntlrParser::newFunction(std::string name, + const std::vector& sorts) { + Assert( sorts.size() > 0 ); + if( sorts.size() == 1 ) { + return mkVar(name, sorts[0]); + } else { + return mkVar(name, functionType(sorts)); } } -void AntlrParser::newPredicate(std::string name, - const std::vector& sorts) { - Debug("parser") << "newPredicate(" << name << ")" << std::endl; +const std::vector +AntlrParser::newFunctions(const std::vector& names, + const std::vector& sorts) { + const FunctionType* t = functionType(sorts); + return mkVars(names, t); +} + +const Type* AntlrParser::predicateType(const std::vector& sorts) { if(sorts.size() == 0) { - d_varSymbolTable.bindName(name, d_exprManager->mkVar()); + return d_exprManager->booleanType(); } else { - Unhandled("Non unary predicate not supported yet!"); + return d_exprManager->mkFunctionType(sorts,d_exprManager->booleanType()); + } +} + +Expr +AntlrParser::newPredicate(std::string name, + const std::vector& sorts) { + const Type* t = predicateType(sorts); + return mkVar(name, t); +} + +const std::vector +AntlrParser::newPredicates(const std::vector& names, + const std::vector& sorts) { + const Type* t = predicateType(sorts); + return mkVars(names, t); +} + +Expr +AntlrParser::mkVar(const std::string name, const Type* type) { + Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; + Assert( !isDeclared(name) ) ; + Expr expr = d_exprManager->mkVar(type); + d_varSymbolTable.bindName(name, expr); + d_varTypeTable.bindName(name,type); + Assert( isDeclared(name) ) ; + return expr; +} + +const std::vector +AntlrParser::mkVars(const std::vector names, + const Type* type) { + std::vector vars; + for(unsigned i = 0; i < names.size(); ++i) { + vars.push_back(mkVar(names[i], type)); } + return vars; } -void AntlrParser::newPredicates(const std::vector& names, - const std::vector& sorts) { + +const Type* +AntlrParser::newSort(std::string name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Assert( !isDeclared(name,SYM_SORT) ) ; + const Type* type = d_exprManager->mkSort(name); + d_sortTable.bindName(name,type); + Assert( isDeclared(name,SYM_SORT) ) ; + return type; +} + +const std::vector +AntlrParser::newSorts(const std::vector& names) { + std::vector types; for(unsigned i = 0; i < names.size(); ++i) { - newPredicate(names[i], sorts); + types.push_back(newSort(names[i])); } + return types; } -bool AntlrParser::isSort(std::string name) { - return d_sortTable.isBound(name); +const BooleanType* AntlrParser::booleanType() { + return d_exprManager->booleanType(); } -void AntlrParser::newSort(std::string name) { - Assert( !isSort(name) ) ; - // Trivial binding - d_sortTable.bindName(name,name); - Assert( isSort(name) ) ; +const KindType* AntlrParser::kindType() { + return d_exprManager->kindType(); } -void AntlrParser::newSorts(const std::vector& names) { - for(unsigned i = 0; i < names.size(); ++i) { - newSort(names[i]); +unsigned int AntlrParser::minArity(Kind kind) { + switch(kind) { + case FALSE: + case SKOLEM: + case TRUE: + case VARIABLE: + return 0; + + case NOT: + return 1; + + case AND: + case APPLY: + case EQUAL: + case IFF: + case IMPLIES: + case PLUS: + case OR: + case XOR: + return 2; + + case ITE: + return 3; + + default: + Unhandled("kind in minArity"); + } +} + +unsigned int AntlrParser::maxArity(Kind kind) { + switch(kind) { + case FALSE: + case SKOLEM: + case TRUE: + case VARIABLE: + return 0; + + case NOT: + return 1; + + case EQUAL: + case IFF: + case IMPLIES: + case XOR: + return 2; + + case ITE: + return 3; + + case AND: + case APPLY: + case PLUS: + case OR: + return UINT_MAX; + + default: + Unhandled("kind in minArity"); } } @@ -135,8 +311,12 @@ void AntlrParser::setExpressionManager(ExprManager* em) { bool AntlrParser::isDeclared(string name, SymbolType type) { switch(type) { - case SYM_VARIABLE: + case SYM_VARIABLE: // Predicates and functions share var namespace + // case SYM_PREDICATE: + case SYM_FUNCTION: return d_varSymbolTable.isBound(name); + case SYM_SORT: + return d_sortTable.isBound(name); default: Unhandled("Unhandled symbol type!"); } @@ -149,25 +329,14 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(1).get()->getColumn()); } -bool AntlrParser::checkDeclaration(string varName, DeclarationCheck check) { - switch(check) { - case CHECK_DECLARED: - return isDeclared(varName, SYM_VARIABLE); - case CHECK_UNDECLARED: - return !isDeclared(varName, SYM_VARIABLE); - case CHECK_NONE: - return true; - default: - Unhandled("Unknown check type!"); - } -} - -bool AntlrParser::checkSort(std::string name, DeclarationCheck check) { +bool AntlrParser::checkDeclaration(string varName, + DeclarationCheck check, + SymbolType type) { switch(check) { case CHECK_DECLARED: - return isSort(name); + return isDeclared(varName, type); case CHECK_UNDECLARED: - return !isSort(name); + return !isDeclared(varName, type); case CHECK_NONE: return true; default: diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 5a7291be6..3cfe4fc5d 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -31,6 +31,8 @@ namespace CVC4 { class Command; +class Type; +class FunctionType; namespace parser { @@ -110,23 +112,13 @@ protected: * @return the variable expression */ Expr getVariable(std::string var_name); + Expr getFunction(std::string var_name); + /* Expr getPredicate(std::string var_name); */ /** - * Return true if the the declaration policy we want to enforce is true. - * @param varName the symbol to check - * @oaram check the kind of check to perform - * @return true if the check holds + * Returns a sort, given a name */ - bool checkDeclaration(std::string varName, DeclarationCheck check); - - /** - * Return true if the the declaration policy we want to enforce is true - * on the given sort name. - * @param name the sort symbol to check - * @oaram check the kind of check to perform - * @return true if the check holds - */ - bool checkSort(std::string name, DeclarationCheck check); + const Type* getSort(std::string sort_name); /** * Types of symbols. @@ -135,9 +127,11 @@ protected: /** Variables */ SYM_VARIABLE, /** Predicates */ - SYM_PREDICATE, + /* SYM_PREDICATE, */ /** Functions */ - SYM_FUNCTION + SYM_FUNCTION, + /** Sorts */ + SYM_SORT }; /** @@ -147,10 +141,19 @@ protected: bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE); /** - * Checks if the sort has been declared. - * @param the sort name + * Return true if the the declaration policy we want to enforce is true. + * @param varName the symbol to check + * @oaram check the kind of check to perform + * @return true if the check holds */ - bool isSort(std::string name); + bool checkDeclaration(std::string varName, + DeclarationCheck check, + SymbolType type = SYM_VARIABLE); + + + /** Returns the type for the variable with the given name. */ + const Type* getType(std::string var_name, + SymbolType type = SYM_VARIABLE); /** * Returns the true expression. @@ -199,14 +202,32 @@ protected: */ Expr mkExpr(Kind kind, const std::vector& children); + /* Create a new CVC4 variable expression . */ + Expr mkVar(const std::string name, const Type* type); + + const std::vector + mkVars(const std::vector names, + const Type* type); + + + /** Returns a function type over the given domain and range types. */ + const FunctionType* functionType(const Type* domain, const Type* range); + /** Returns a function type over the given types. argTypes must have + at least 1 element. */ + const FunctionType* functionType(const std::vector& argTypes, + const Type* rangeType); + /** Returns a function type over the given types. types must have + at least 2 elements (i.e., a domain and range). */ + const FunctionType* functionType(const std::vector& types); + /** * Creates a new function over the given sorts. The function * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. * @param name the name of the function * @param sorts the sorts */ - void newFunction(std::string name, - const std::vector& sorts); + Expr newFunction(std::string name, + const std::vector& sorts); /** * Creates new functions over the given sorts. Each function has @@ -214,40 +235,75 @@ protected: * @param name the name of the function * @param sorts the sorts */ - void newFunctions(const std::vector& names, - const std::vector& sorts); + const std::vector + newFunctions(const std::vector& names, + const std::vector& sorts); + + /** Returns a predicate type over the given sorts. sorts must be + non-empty. If sorts has size 1, then the type is just BOOLEAN. */ + const Type* predicateType(const std::vector& sorts); /** - * Creates a new predicate over the given sorts. The predicate has - * arity sorts.size(). + * Creates a new predicate (a function with range boolean) over the + * given sorts. The predicate has sorts.size(). * @param name the name of the predicate * @param sorts the sorts */ - void newPredicate(std::string name, const std::vector& sorts); + Expr newPredicate(std::string name, const std::vector& sorts); /** - * Creates new predicates over the given sorts. Each predicate - * will have arity sorts.size(). + * Creates new predicates (a function with range boolean) over the + * given sorts. Each predicate will have arity sorts.size(). * @param p_names the names of the predicates */ - void newPredicates(const std::vector& names, const std::vector< - std::string>& sorts); + const std::vector + newPredicates(const std::vector& names, + const std::vector& sorts); /** * Creates a new sort with the given name. */ - void newSort(std::string name); + const Type* newSort(std::string name); /** * Creates a new sorts with the given names. */ - void newSorts(const std::vector& names); + const std::vector + newSorts(const std::vector& names); + + bool isBoolean(std::string name); + bool isFunction(std::string name); + bool isPredicate(std::string name); + + const BooleanType* booleanType(); + const KindType* kindType(); + + unsigned int minArity(Kind kind); + unsigned int maxArity(Kind kind); /** * Returns the precedence rank of the kind. */ static unsigned getPrecedence(Kind kind); + inline std::string toString(DeclarationCheck check) { + switch(check) { + case CHECK_NONE: return "CHECK_NONE"; + case CHECK_DECLARED: return "CHECK_DECLARED"; + case CHECK_UNDECLARED: return "CHECK_UNDECLARED"; + default: Unreachable(); + } + } + + inline std::string toString(SymbolType type) { + switch(type) { + case SYM_VARIABLE: return "SYM_VARIABLE"; + case SYM_FUNCTION: return "SYM_FUNCTION"; + case SYM_SORT: return "SYM_SORT"; + default: Unreachable(); + } + } + private: /** The expression manager */ @@ -256,10 +312,20 @@ private: /** The symbol table lookup */ SymbolTable d_varSymbolTable; + /** A temporary hack: keep all the variable types in their own special + table. These should actually be Expr attributes. */ + SymbolTable d_varTypeTable; + /** The sort table */ - SymbolTable d_sortTable; + SymbolTable d_sortTable; + + Expr getSymbol(std::string var_name, SymbolType type); + }; + + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g index afcc7597d..b5bf90015 100644 --- a/src/parser/cvc/cvc_lexer.g +++ b/src/parser/cvc/cvc_lexer.g @@ -39,6 +39,7 @@ options { tokens { // Types BOOLEAN = "BOOLEAN"; + TYPE = "TYPE"; // Boolean oparators AND = "AND"; IF = "IF"; @@ -67,6 +68,8 @@ tokens { COMMA : ','; IMPLIES : "=>"; IFF : "<=>"; +RIGHT_ARROW : "->"; +EQUAL : "="; /** * Matches any letter ('a'-'z' and 'A'-'Z'). diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 662888050..30df2d439 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -16,6 +16,8 @@ header "post_include_hpp" { #include "parser/antlr_parser.h" #include "expr/command.h" +#include "expr/type.h" +#include "util/output.h" } header "post_include_cpp" { @@ -68,29 +70,72 @@ parseExpr returns [CVC4::Expr expr] command returns [CVC4::Command* cmd = 0] { Expr f; - vector ids; + Debug("parser") << "command: " << LT(1)->getText() << endl; } : ASSERT f = formula SEMICOLON { cmd = new AssertCommand(f); } | QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); } | CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); } | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); } - | identifierList[ids, CHECK_UNDECLARED] COLON type { - // FIXME: switch on type (may not be predicates) - vector sorts; - newPredicates(ids,sorts); - cmd = new DeclarationCommand(ids); - } - SEMICOLON + | cmd = declaration | EOF ; /** - * Mathches a list of identifiers separated by a comma and puts them in the + * Match a declaration + */ + +declaration returns [CVC4::DeclarationCommand* cmd] +{ + vector ids; + const Type* t; + Debug("parser") << "declaration: " << LT(1)->getText() << endl; +} + : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON + { cmd = new DeclarationCommand(ids,t); } + ; + +/** Match the right-hand side of a declaration. Returns the type. */ +declType[std::vector& idList] returns [const CVC4::Type* t] +{ + Debug("parser") << "declType: " << LT(1)->getText() << endl; +} + : /* A sort declaration (e.g., "T : TYPE") */ + TYPE { newSorts(idList); t = kindType(); } + | /* A variable declaration */ + t = type { mkVars(idList,t); } + ; + +/** + * Match the type in a declaration and do the declaration binding. + * TODO: Actually parse sorts into Type objects. + */ +type returns [const CVC4::Type* t] +{ + const Type *t1, *t2; + Debug("parser") << "type: " << LT(1)->getText() << endl; +} + : /* Simple type */ + t = baseType + | /* Single-parameter function type */ + t1 = baseType RIGHT_ARROW t2 = baseType + { t = functionType(t1,t2); } + | /* Multi-parameter function type */ + LPAREN t1 = baseType + { std::vector argTypes; + argTypes.push_back(t1); } + (COMMA t1 = baseType { argTypes.push_back(t1); } )+ + RPAREN RIGHT_ARROW t2 = baseType + { t = functionType(argTypes,t2); } + ; + +/** + * Matches a list of identifiers separated by a comma and puts them in the * given list. * @param idList the list to fill with identifiers. * @param check what kinds of check to perform on the symbols */ -identifierList[std::vector& idList, DeclarationCheck check = CHECK_NONE] +identifierList[std::vector& idList, + DeclarationCheck check = CHECK_NONE] { string id; } @@ -102,10 +147,12 @@ identifierList[std::vector& idList, DeclarationCheck check = CHECK_ /** * Matches an identifier and returns a string. */ -identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] +identifier[DeclarationCheck check = CHECK_NONE, + SymbolType type = SYM_VARIABLE] +returns [std::string id] : x:IDENTIFIER { id = x->getText(); } - { checkDeclaration(id, check) }? + { checkDeclaration(id, check, type) }? exception catch [antlr::SemanticException& ex] { switch (check) { case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); @@ -119,8 +166,25 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] * Matches a type. * TODO: parse more types */ -type - : BOOLEAN +baseType returns [const CVC4::Type* t] +{ + std::string id; + Debug("parser") << "base type: " << LT(1)->getText() << endl; +} + : BOOLEAN { t = booleanType(); } + | t = typeSymbol + ; + +/** + * Matches a type identifier + */ +typeSymbol returns [const CVC4::Type* t] +{ + std::string id; + Debug("parser") << "type symbol: " << LT(1)->getText() << endl; +} + : id = identifier[CHECK_DECLARED,SYM_SORT] + { t = getSort(id); } ; /** @@ -128,159 +192,197 @@ type * @return the expression representing the formula */ formula returns [CVC4::Expr formula] - : formula = boolFormula +{ + Debug("parser") << "formula: " << LT(1)->getText() << endl; +} + : formula = iffFormula ; /** - * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of - * operands (primaryBoolFormulas) and operators (Kinds) and then calls the - * createPrecedenceExpr method to build the expression using the precedence - * and associativity of the operators. - * @return the expression representing the formula + * Matches a comma-separated list of formulas */ -boolFormula returns [CVC4::Expr formula] - : formula = boolAndFormula +formulaList[std::vector& formulas] +{ + Expr f; +} + : f = formula { formulas.push_back(f); } + ( COMMA f = formula + { formulas.push_back(f); } + )* ; /** - * Matches a Boolean AND formula of a given kind by doing a recursive descent. + * Matches a Boolean IFF formula (right-associative) */ -boolAndFormula returns [CVC4::Expr andFormula] +iffFormula returns [CVC4::Expr f] { Expr e; - vector exprs; + Debug("parser") << "<=> formula: " << LT(1)->getText() << endl; } - : e = boolXorFormula { exprs.push_back(e); } - ( AND e = boolXorFormula { exprs.push_back(e); } )* - { - andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); - } + : f = impliesFormula + ( IFF e = iffFormula + { f = mkExpr(CVC4::IFF, f, e); } + )? ; /** - * Matches a Boolean XOR formula of a given kind by doing a recursive descent. + * Matches a Boolean IMPLIES formula (right-associative) */ -boolXorFormula returns [CVC4::Expr xorFormula] +impliesFormula returns [CVC4::Expr f] { Expr e; - vector exprs; + Debug("parser") << "=> Formula: " << LT(1)->getText() << endl; } - : e = boolOrFormula { exprs.push_back(e); } - ( XOR e = boolOrFormula { exprs.push_back(e); } )* - { - xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]); - } + : f = orFormula + ( IMPLIES e = impliesFormula + { f = mkExpr(CVC4::IFF, f, e); } + )? ; /** - * Matches a Boolean OR formula of a given kind by doing a recursive descent. + * Matches a Boolean OR formula (left-associative) */ -boolOrFormula returns [CVC4::Expr orFormula] +orFormula returns [CVC4::Expr f] { Expr e; vector exprs; + Debug("parser") << "OR Formula: " << LT(1)->getText() << endl; } - : e = boolImpliesFormula { exprs.push_back(e); } - ( OR e = boolImpliesFormula { exprs.push_back(e); } )* + : e = xorFormula { exprs.push_back(e); } + ( OR e = xorFormula { exprs.push_back(e); } )* { - orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); } ; /** - * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent. + * Matches a Boolean XOR formula (left-associative) */ -boolImpliesFormula returns [CVC4::Expr impliesFormula] +xorFormula returns [CVC4::Expr f] { - vector exprs; Expr e; + Debug("parser") << "XOR formula: " << LT(1)->getText() << endl; } - : e = boolIffFormula { exprs.push_back(e); } - ( IMPLIES e = boolIffFormula { exprs.push_back(e); } + : f = andFormula + ( XOR e = andFormula + { f = mkExpr(CVC4::XOR,f, e); } )* - { - impliesFormula = exprs.back(); - for (int i = exprs.size() - 2; i >= 0; -- i) { - impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula); - } - } ; /** - * Matches a Boolean IFF formula of a given kind by doing a recursive descent. + * Matches a Boolean AND formula (left-associative) */ -boolIffFormula returns [CVC4::Expr iffFormula] +andFormula returns [CVC4::Expr f] { Expr e; + vector exprs; + Debug("parser") << "AND Formula: " << LT(1)->getText() << endl; } - : iffFormula = primaryBoolFormula - ( IFF e = primaryBoolFormula - { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); } - )* + : e = notFormula { exprs.push_back(e); } + ( AND e = notFormula { exprs.push_back(e); } )* + { + f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + } ; /** - * Parses a primary Boolean formula. A primary Boolean formula is either a - * Boolean atom (variables and predicates) a negation of a primary Boolean - * formula or a formula enclosed in parenthesis. + * Parses a NOT formula. * @return the expression representing the formula */ -primaryBoolFormula returns [CVC4::Expr formula] - : formula = boolAtom - | formula = iteFormula - | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); } - | LPAREN formula = boolFormula RPAREN +notFormula returns [CVC4::Expr f] +{ + Debug("parser") << "NOT formula: " << LT(1)->getText() << endl; +} + : /* negation */ + NOT f = notFormula + { f = mkExpr(CVC4::NOT, f); } + | /* a boolean atom */ + f = predFormula ; +predFormula returns [CVC4::Expr f] +{ + Debug("parser") << "predicate formula: " << LT(1)->getText() << endl; +} + : { Expr e; } + f = term + (EQUAL e = term + { f = mkExpr(CVC4::EQUAL, f, e); } + )? + ; // TODO: lt, gt, etc. + /** - * Parses an ITE boolean formula. + * Parses a term. */ -iteFormula returns [CVC4::Expr formula] +term returns [CVC4::Expr t] { - Expr iteCondition, iteThen, iteElse; + std::string name; + Debug("parser") << "term: " << LT(1)->getText() << endl; } - : IF iteCondition = boolFormula - THEN iteThen = boolFormula - iteElse = iteElseFormula - ENDIF - { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + : /* function application */ + { isFunction(LT(1)->getText()) }? + name = functionSymbol[CHECK_DECLARED] + { + std::vector args; + args.push_back( getFunction(name) ); + } + LPAREN formulaList[args] RPAREN + // TODO: check arity + { t = mkExpr(CVC4::APPLY, args); } + + | /* if-then-else */ + t = iteTerm + + | /* parenthesized sub-formula */ + LPAREN t = formula RPAREN + + /* constants */ + | TRUE { t = getTrueExpr(); } + | FALSE { t = getFalseExpr(); } + + | /* variable */ + name = identifier[CHECK_DECLARED] + { t = getVariable(name); } ; /** - * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... + * Parses an ITE term. */ -iteElseFormula returns [CVC4::Expr formula] +iteTerm returns [CVC4::Expr t] { Expr iteCondition, iteThen, iteElse; + Debug("parser") << "ite: " << LT(1)->getText() << endl; } - : ELSE formula = boolFormula - | ELSEIF iteCondition = boolFormula - THEN iteThen = boolFormula - iteElse = iteElseFormula - { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + : IF iteCondition = formula + THEN iteThen = formula + iteElse = iteElseTerm + ENDIF + { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } ; /** - * Parses the Boolean atoms (variables and predicates). - * @return the expression representing the atom. + * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... */ -boolAtom returns [CVC4::Expr atom] +iteElseTerm returns [CVC4::Expr t] { - string p; + Expr iteCondition, iteThen, iteElse; + Debug("parser") << "else: " << LT(1)->getText() << endl; } - : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); } - exception catch [antlr::SemanticException ex] { - rethrow(ex, "Undeclared variable " + p); - } - | TRUE { atom = getTrueExpr(); } - | FALSE { atom = getFalseExpr(); } + : ELSE t = formula + | ELSEIF iteCondition = formula + THEN iteThen = formula + iteElse = iteElseTerm + { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } ; /** - * Parses a predicate symbol (an identifier). + * Parses a function symbol (an identifier). * @param what kind of check to perform on the id * @return the predicate symol */ -predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] - : pSymbol = identifier[check] +functionSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string symbol] +{ + Debug("parser") << "function symbol: " << LT(1)->getText() << endl; + +} : symbol = identifier[check,SYM_FUNCTION] ; diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index d71edfbc3..695b7b787 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -37,11 +37,11 @@ tokens { // Base SMT-LIB tokens DISTINCT = "distinct"; ITE = "ite"; + IF_THEN_ELSE = "if_then_else"; TRUE = "true"; FALSE = "false"; NOT = "not"; IMPLIES = "implies"; - IF_THEN_ELSE = "if_then_else"; AND = "and"; OR = "or"; XOR = "xor"; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 47e275171..28101532b 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -19,6 +19,8 @@ header "post_include_hpp" { } header "post_include_cpp" { +#include "expr/type.h" +#include "util/output.h" #include using namespace std; @@ -108,94 +110,64 @@ benchAttribute returns [Command* smt_command = 0] | annotation ; -/** - * Matches an identifier and returns a string. - * @param check what kinds of check to do on the symbol - * @return the id string - */ -identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] - : x:IDENTIFIER - { id = x->getText(); } - { checkDeclaration(id, check) }? - exception catch [antlr::SemanticException& ex] { - switch (check) { - case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); - case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); - default: throw ex; - } - } - ; - /** * Matches an annotated formula. * @return the expression representing the formula */ annotatedFormula returns [CVC4::Expr formula] { + Debug("parser") << "annotated formula: " << LT(1)->getText() << endl; Kind kind; - vector children; + vector args; } - : formula = annotatedAtom - | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN - { formula = mkExpr(kind, children); } - /* TODO: let, flet, quantifiers */ - ; + : /* a built-in operator application */ + LPAREN kind = builtinOp annotatedFormulas[args] RPAREN + { args.size() >= minArity(kind) + && args.size() <= maxArity(kind) }? + { formula = mkExpr(kind,args); } + exception catch [antlr::SemanticException& ex] { + stringstream ss; + ss << "Expected "; + if( args.size() < minArity(kind) ) { + ss << "at least " << minArity(kind) << " "; + } else { + ss << "at most " << maxArity(kind) << " "; + } + ss << "arguments for operator '" << kind << "'. "; + ss << "Found: " << args.size(); + rethrow(ex, ss.str()); + } -/** - * Matches a sequence of annotaed formulas and puts them into the formulas - * vector. - * @param formulas the vector to fill with formulas - */ -annotatedFormulas[std::vector& formulas] -{ - Expr f; -} - : ( f = annotatedFormula { formulas.push_back(f); } )+ - ; + | /* A non-built-in function application */ + { isFunction(LT(2)->getText()) }? + { Expr f; } + LPAREN f = functionSymbol + { args.push_back(f); } + annotatedFormulas[args] RPAREN + // TODO: check arity + { formula = mkExpr(CVC4::APPLY,args); } -/** - * Matches an annotated proposition atom, which is either a propositional atom - * or built of other atoms using a predicate symbol. - * @return expression representing the atom - */ -annotatedAtom returns [CVC4::Expr atom] -{ - Kind kind; - string predName; - Expr pred; - vector children; -} - : atom = propositionalAtom - | LPAREN kind = arithPredicate annotatedTerms[children] RPAREN - { atom = mkExpr(kind,children); } - | LPAREN pred = predicateSymbol - { children.push_back(pred); } - annotatedTerms[children] RPAREN - { atom = mkExpr(CVC4::APPLY,children); } - ; + | /* An ite expression */ + LPAREN (ITE | IF_THEN_ELSE) + { Expr test, trueExpr, falseExpr; } + test = annotatedFormula + trueExpr = annotatedFormula + falseExpr = annotatedFormula + RPAREN + { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); } -/** - * Matches an annotated term. - * @return the expression representing the term - */ -annotatedTerm returns [CVC4::Expr term] -{ - Kind kind; - Expr f, t1, t2; - vector children; -} - : term = baseTerm - | LPAREN f = functionSymbol - { children.push_back(f); } - annotatedTerms[children] RPAREN - { term = mkExpr(CVC4::APPLY, children); } - // | LPAREN kind = arithFunction annotatedTerms[children] RPAREN - // { term = mkExpr(kind,children); } - | LPAREN ITE - f = annotatedFormula - t1 = annotatedTerm - t2 = annotatedTerm RPAREN - { term = mkExpr(CVC4::ITE, f, t1, t2); } + | /* a parenthesized sub-formula */ + LPAREN formula = annotatedFormula RPAREN + + | /* a variable */ + { std::string name; } + name = identifier[CHECK_DECLARED] + { formula = getVariable(name); } + + /* constants */ + | TRUE { formula = getTrueExpr(); } + | FALSE { formula = getFalseExpr(); } + /* TODO: let, flet, quantifiers, arithmetic constants */ ; /** @@ -203,50 +175,29 @@ annotatedTerm returns [CVC4::Expr term] * vector. * @param formulas the vector to fill with formulas */ -annotatedTerms[std::vector& terms] -{ - Expr t; -} - : ( t = annotatedFormula { terms.push_back(t); } )+ - ; - -baseTerm returns [CVC4::Expr term] +annotatedFormulas[std::vector& formulas] { - string name; + Expr f; } - : name = identifier[CHECK_DECLARED] { term = getVariable(name); } - /* TODO: constants */ + : ( f = annotatedFormula { formulas.push_back(f); } )+ ; /** * Matches on of the unary Boolean connectives. * @return the kind of the Bollean connective */ -boolConnective returns [CVC4::Kind kind] +builtinOp returns [CVC4::Kind kind] +{ + Debug("parser") << "builtin: " << LT(1)->getText() << endl; +} : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } | OR { kind = CVC4::OR; } | XOR { kind = CVC4::XOR; } | IFF { kind = CVC4::IFF; } - ; - -/** - * Matches a propositional atom and returns the expression of the atom. - * @return atom the expression of the atom - */ -propositionalAtom returns [CVC4::Expr atom] -{ - std::string p; -} - : atom = predicateSymbol - | TRUE { atom = getTrueExpr(); } - | FALSE { atom = getFalseExpr(); } - ; - -arithPredicate returns [CVC4::Kind kind] - : EQUAL { kind = CVC4::EQUAL; } - /* TODO: lt, gt */ + | EQUAL { kind = CVC4::EQUAL; } + /* TODO: lt, gt, plus, minus, etc. */ ; /** @@ -257,23 +208,12 @@ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] : p = identifier[check] ; -/** - * Matches an previously declared predicate symbol (returning an Expr) - */ -predicateSymbol returns [CVC4::Expr pred] -{ - string name; -} - : name = predicateName[CHECK_DECLARED] - { pred = getVariable(name); } - ; - /** * Matches a (possibly undeclared) function identifier (returning the string) * @param check what kind of check to do with the symbol */ functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name] - : name = identifier[check] + : name = identifier[check,SYM_FUNCTION] ; /** @@ -284,7 +224,7 @@ functionSymbol returns [CVC4::Expr fun] string name; } : name = functionName[CHECK_DECLARED] - { fun = getVariable(name); } + { fun = getFunction(name); } ; /** @@ -299,19 +239,26 @@ attribute * @param check the check to perform on the name */ sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] - : name = identifier[CHECK_NONE] - /* We pass CHECK_NONE to identifier, because identifier checks - in the variable namespace, not the sorts namespace. */ - { checkSort(name,check) }? + : name = identifier[check,SYM_SORT] + ; + +sortSymbol returns [const CVC4::Type* t] +{ + std::string name; +} + : name = sortName { t = getSort(name); } ; functionDeclaration { string name; - vector sorts; + const Type* t; + std::vector sorts; } - : LPAREN name = functionName[CHECK_UNDECLARED] - sortNames[sorts, CHECK_DECLARED] RPAREN + : LPAREN name = functionName[CHECK_UNDECLARED] + t = sortSymbol // require at least one sort + { sorts.push_back(t); } + sortList[sorts] RPAREN { newFunction(name, sorts); } ; @@ -321,10 +268,9 @@ functionDeclaration predicateDeclaration { string p_name; - vector p_sorts; + std::vector p_sorts; } - : LPAREN p_name = predicateName[CHECK_UNDECLARED] - sortNames[p_sorts, CHECK_DECLARED] RPAREN + : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN { newPredicate(p_name, p_sorts); } ; @@ -339,12 +285,11 @@ sortDeclaration /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortNames[std::vector& sorts,DeclarationCheck check = CHECK_NONE] +sortList[std::vector& sorts] { - std::string name; + const Type* t; } - : ( name = sortName[check] - { sorts.push_back(name); })* + : ( t = sortSymbol { sorts.push_back(t); })* ; /** @@ -363,3 +308,28 @@ annotation : attribute (USER_VALUE)? ; +/** + * Matches an identifier and returns a string. + * @param check what kinds of check to do on the symbol + * @return the id string + */ +identifier[DeclarationCheck check = CHECK_NONE, + SymbolType type = SYM_VARIABLE] +returns [std::string id] +{ + Debug("parser") << "identifier: " << LT(1)->getText() + << " check? " << toString(check) + << " type? " << toString(type) << endl; +} + : x:IDENTIFIER + { id = x->getText(); } + { checkDeclaration(id, check,type) }? + exception catch [antlr::SemanticException& ex] { + switch (check) { + case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); + case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); + default: throw ex; + } + } + ; + diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index e4aec930e..d790a1c84 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -78,14 +78,12 @@ public: /** * Returns the last binding expression of the name. + * Requires the name to have a binding in the table. */ ObjectType getObject(const std::string name) throw () { - ObjectType result; table_iterator find = d_nameBindings.find(name); - if(find != d_nameBindings.end()) { - result = find->second.top(); - } - return result; + Assert(find != d_nameBindings.end()); + return find->second.top(); } /** diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc new file mode 100644 index 000000000..4f84de94d --- /dev/null +++ b/test/regress/regress0/boolean-prec.cvc @@ -0,0 +1,6 @@ +% Expect: VALID +% Simple test for right precedence of AND, <=>, NOT. + +A, B, C: BOOLEAN; + +QUERY (NOT A AND NOT B <=> C) <=> (((NOT A) AND (NOT B)) <=> C); diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 26c572ce6..5d6326166 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -21,6 +21,7 @@ #include "expr/expr_manager.h" #include "parser/parser.h" #include "expr/command.h" +#include "util/output.h" using namespace CVC4; using namespace CVC4::parser; @@ -35,6 +36,8 @@ const string goodCvc4Inputs[] = { "CHECKSAT FALSE;", "a, b : BOOLEAN;", "a, b : BOOLEAN; QUERY (a => b) AND a => b;", + "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", + "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", "%% nothing but a comment", "% a comment\nASSERT TRUE; %a command\n% another comment", }; @@ -89,21 +92,33 @@ const string goodSmtInputs[] = { "(benchmark baz :extrapreds ( (a) (b) ) )", "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", + "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", ";; nothing but a comment", "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" }; const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); -const string smtExprContext = "(benchmark foo :extrapreds ((a) (b) (c)) )"; - -/* The following expressions are good in a context where a, b, and c have been declared as BOOLEAN. */ +/* The parser is just going to read this benchmark and leave its decls + in the context. The SMT exprs below will then be able to refer to them, + even though they're "out of scope." */ +const string smtExprContext = + "(benchmark foo\n" + " :extrasorts (t u v)\n" + " :extrapreds ((a) (b) (c))\n" + " :extrafuns ((f t u) (g u v) (h v t) (x t) (y u) (z v)))\n"; + +/* The following expressions are good in a context where a, b, and c + have been declared as BOOLEAN, t, u, v, are sorts, f, g, h are + functions, and x, y, z are variables. */ const string goodSmtExprs[] = { "(and a b)", "(or (and a b) c)", "(implies (and (implies a b) a) b)", "(and (iff a b) (not a))", - "(iff (xor a b) (and (or a b) (not (and a b))))" + "(iff (xor a b) (and (or a b) (not (and a b))))", + "(ite a (f x) y)", + "(if_then_else a (f x) y)" }; const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); @@ -120,24 +135,26 @@ const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); /* The following expressions are bad even in a context where a, b, and c have been declared as BOOLEAN. */ const string badSmtExprs[] = { - "(and a)", // wrong arity + "(and)", // wrong arity "(and a b", // no closing paren "(a and b)", // infix "(OR (AND a b) c)", // wrong case "(a IMPLIES b)", // infix AND wrong case "(not a b)", // wrong arity - "not a" // needs parens + "not a", // needs parens + "(ite a x)" // wrong arity }; const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); -class SmtParserBlack : public CxxTest::TestSuite { +class ParserBlack : public CxxTest::TestSuite { ExprManager *d_exprManager; void tryGoodInputs(Parser::InputLanguage d_lang, const string goodInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { try { // cout << "Testing good input: '" << goodInputs[i] << "'\n"; + // Debug.on("parser"); istringstream stream(goodInputs[i]); Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT( !smtParser->done() ); @@ -149,7 +166,8 @@ class SmtParserBlack : public CxxTest::TestSuite { TS_ASSERT( smtParser->done() ); delete smtParser; } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInputs[i] << endl; + cout << "\nGood input failed:\n" << goodInputs[i] << endl + << e << endl; throw e; } @@ -174,6 +192,7 @@ class SmtParserBlack : public CxxTest::TestSuite { for(int i = 0; i < numExprs; ++i) { try { // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; + // Debug.on("parser"); istringstream stream(context + goodBooleanExprs[i]); Parser* parser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT( !parser->done() ); @@ -189,21 +208,24 @@ class SmtParserBlack : public CxxTest::TestSuite { delete parser; } catch (Exception& e) { cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; + cout << e; throw e; } } } - void tryBadExprs(Parser::InputLanguage d_lang,const string badBooleanExprs[], int numExprs) { + void tryBadExprs(Parser::InputLanguage d_lang,const string& context, const string badBooleanExprs[], int numExprs) { + //Debug.on("parser"); for(int i = 0; i < numExprs; ++i) { // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; - istringstream stream(badBooleanExprs[i]); + istringstream stream(context + badBooleanExprs[i]); Parser* smtParser = Parser::getNewParser(d_exprManager, d_lang, stream); TS_ASSERT_THROWS ( smtParser->parseNextExpression(); cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, ParserException ); } + //Debug.off("parser"); } public: @@ -224,7 +246,7 @@ public: } void testBadCvc4Exprs() { - tryBadExprs(Parser::LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); + tryBadExprs(Parser::LANG_CVC4,cvc4ExprContext,badCvc4Exprs,numBadCvc4Exprs); } void testGoodSmtInputs() { @@ -240,6 +262,6 @@ public: } void testBadSmtExprs() { - tryBadExprs(Parser::LANG_SMTLIB,badSmtExprs,numBadSmtExprs); + tryBadExprs(Parser::LANG_SMTLIB,smtExprContext,badSmtExprs,numBadSmtExprs); } }; -- 2.30.2