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
"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
node.h \
node_builder.h \
expr.h \
+ type.h \
node_value.h \
node_manager.h \
expr_manager.h \
expr_manager.cpp \
node_value.cpp \
expr.cpp \
+ type.cpp \
command.h \
command.cpp
class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
public:
- DeclarationCommand(const std::vector<std::string>& ids);
+ DeclarationCommand(const std::vector<std::string>& ids, const Type* t);
void toStream(std::ostream& out) const;
protected:
std::vector<std::string> d_declaredSymbols;
/* class DeclarationCommand */
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+inline
+DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids,
+ const Type* t) :
d_declaredSymbols(ids) {
}
#include "expr/node.h"
#include "expr/expr.h"
+#include "expr/type.h"
#include "expr/node_manager.h"
#include "expr/expr_manager.h"
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)));
}
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<const Type*>& 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()));
}
namespace CVC4 {
class Expr;
+class Type;
+class BooleanType;
+class FunctionType;
+class KindType;
class NodeManager;
class SmtEngine;
*/
~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
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& 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<const Type*>& 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.
--- /dev/null
+/********************* -*- 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 <string>
+
+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("<undefined>")) {
+}
+
+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<const Type*>& argTypes,
+ const Type* range)
+ : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) {
+ Assert( argTypes.size() > 0 );
+}
+
+const std::vector<const Type*> 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() {
+}
+
+
+}
--- /dev/null
+/********************* -*- 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 <string>
+#include <vector>
+
+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<const Type*>& argTypes,
+ const Type* range);
+ ~FunctionType();
+ const std::vector<const Type*> getArgTypes() const;
+ const Type* getRangeType() const;
+ bool isFunction() const;
+ bool isPredicate() const;
+ void toStream(std::ostream& out) const;
+
+ private:
+ std::vector<const Type*> 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
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
*/
#include <iostream>
+#include <limits.h>
#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;
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 {
}
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) {
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<std::string>& 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<const Type*>& argTypes,
+ const Type* rangeType) {
+ Assert( argTypes.size() > 0 );
+ return d_exprManager->mkFunctionType(argTypes,rangeType);
+}
+
+const FunctionType*
+AntlrParser::functionType(const std::vector<const Type*>& sorts) {
+ Assert( sorts.size() > 1 );
+ std::vector<const Type*> argTypes(sorts);
+ const Type* rangeType = argTypes.back();
+ argTypes.pop_back();
+ return functionType(argTypes,rangeType);
+}
+
+Expr AntlrParser::newFunction(std::string name,
+ const std::vector<const Type*>& 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<std::string>& sorts) {
- Debug("parser") << "newPredicate(" << name << ")" << std::endl;
+const std::vector<Expr>
+AntlrParser::newFunctions(const std::vector<std::string>& names,
+ const std::vector<const Type*>& sorts) {
+ const FunctionType* t = functionType(sorts);
+ return mkVars(names, t);
+}
+
+const Type* AntlrParser::predicateType(const std::vector<const Type*>& 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<const Type*>& sorts) {
+ const Type* t = predicateType(sorts);
+ return mkVar(name, t);
+}
+
+const std::vector<Expr>
+AntlrParser::newPredicates(const std::vector<std::string>& names,
+ const std::vector<const Type*>& 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<Expr>
+AntlrParser::mkVars(const std::vector<std::string> names,
+ const Type* type) {
+ std::vector<Expr> vars;
+ for(unsigned i = 0; i < names.size(); ++i) {
+ vars.push_back(mkVar(names[i], type));
}
+ return vars;
}
-void AntlrParser::newPredicates(const std::vector<std::string>& names,
- const std::vector<std::string>& 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<const Type*>
+AntlrParser::newSorts(const std::vector<std::string>& names) {
+ std::vector<const Type*> 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<std::string>& 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");
}
}
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!");
}
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:
namespace CVC4 {
class Command;
+class Type;
+class FunctionType;
namespace parser {
* @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.
/** Variables */
SYM_VARIABLE,
/** Predicates */
- SYM_PREDICATE,
+ /* SYM_PREDICATE, */
/** Functions */
- SYM_FUNCTION
+ SYM_FUNCTION,
+ /** Sorts */
+ SYM_SORT
};
/**
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.
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
+ /* Create a new CVC4 variable expression . */
+ Expr mkVar(const std::string name, const Type* type);
+
+ const std::vector<Expr>
+ mkVars(const std::vector<std::string> 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<const Type*>& 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<const Type*>& 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<std::string>& sorts);
+ Expr newFunction(std::string name,
+ const std::vector<const Type*>& sorts);
/**
* Creates new functions over the given sorts. Each function has
* @param name the name of the function
* @param sorts the sorts
*/
- void newFunctions(const std::vector<std::string>& names,
- const std::vector<std::string>& sorts);
+ const std::vector<Expr>
+ newFunctions(const std::vector<std::string>& names,
+ const std::vector<const Type*>& 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<const Type*>& 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<std::string>& sorts);
+ Expr newPredicate(std::string name, const std::vector<const Type*>& 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<std::string>& names, const std::vector<
- std::string>& sorts);
+ const std::vector<Expr>
+ newPredicates(const std::vector<std::string>& names,
+ const std::vector<const Type*>& 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<std::string>& names);
+ const std::vector<const Type*>
+ newSorts(const std::vector<std::string>& 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 */
/** The symbol table lookup */
SymbolTable<Expr> d_varSymbolTable;
+ /** A temporary hack: keep all the variable types in their own special
+ table. These should actually be Expr attributes. */
+ SymbolTable<const Type*> d_varTypeTable;
+
/** The sort table */
- SymbolTable<std::string> d_sortTable;
+ SymbolTable<const Type*> d_sortTable;
+
+ Expr getSymbol(std::string var_name, SymbolType type);
+
};
+
+
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
tokens {
// Types
BOOLEAN = "BOOLEAN";
+ TYPE = "TYPE";
// Boolean oparators
AND = "AND";
IF = "IF";
COMMA : ',';
IMPLIES : "=>";
IFF : "<=>";
+RIGHT_ARROW : "->";
+EQUAL : "=";
/**
* Matches any letter ('a'-'z' and 'A'-'Z').
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" {
command returns [CVC4::Command* cmd = 0]
{
Expr f;
- vector<string> 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<string> 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<string> 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<std::string>& 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<const Type*> 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<std::string>& idList, DeclarationCheck check = CHECK_NONE]
+identifierList[std::vector<std::string>& idList,
+ DeclarationCheck check = CHECK_NONE]
{
string id;
}
/**
* 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");
* 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); }
;
/**
* @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<CVC4::Expr>& 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<Expr> 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<Expr> 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<Expr> 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<Expr> 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<Expr> 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<CVC4::Expr> 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]
;
// 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";
}
header "post_include_cpp" {
+#include "expr/type.h"
+#include "util/output.h"
#include <vector>
using namespace std;
| 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<Expr> children;
+ vector<Expr> 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<Expr>& 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<Expr> 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<Expr> 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 */
;
/**
* vector.
* @param formulas the vector to fill with formulas
*/
-annotatedTerms[std::vector<Expr>& terms]
-{
- Expr t;
-}
- : ( t = annotatedFormula { terms.push_back(t); } )+
- ;
-
-baseTerm returns [CVC4::Expr term]
+annotatedFormulas[std::vector<Expr>& 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. */
;
/**
: 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]
;
/**
string name;
}
: name = functionName[CHECK_DECLARED]
- { fun = getVariable(name); }
+ { fun = getFunction(name); }
;
/**
* @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<string> sorts;
+ const Type* t;
+ std::vector<const Type*> 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); }
;
predicateDeclaration
{
string p_name;
- vector<string> p_sorts;
+ std::vector<const Type*> 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); }
;
/**
* Matches a sequence of sort symbols and fills them into the given vector.
*/
-sortNames[std::vector<std::string>& sorts,DeclarationCheck check = CHECK_NONE]
+sortList[std::vector<const Type*>& sorts]
{
- std::string name;
+ const Type* t;
}
- : ( name = sortName[check]
- { sorts.push_back(name); })*
+ : ( t = sortSymbol { sorts.push_back(t); })*
;
/**
: 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;
+ }
+ }
+ ;
+
/**
* 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();
}
/**
--- /dev/null
+% 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);
#include "expr/expr_manager.h"
#include "parser/parser.h"
#include "expr/command.h"
+#include "util/output.h"
using namespace CVC4;
using namespace CVC4::parser;
"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",
};
"(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);
/* 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() );
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;
}
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() );
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:
}
void testBadCvc4Exprs() {
- tryBadExprs(Parser::LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs);
+ tryBadExprs(Parser::LANG_CVC4,cvc4ExprContext,badCvc4Exprs,numBadCvc4Exprs);
}
void testGoodSmtInputs() {
}
void testBadSmtExprs() {
- tryBadExprs(Parser::LANG_SMTLIB,badSmtExprs,numBadSmtExprs);
+ tryBadExprs(Parser::LANG_SMTLIB,smtExprContext,badSmtExprs,numBadSmtExprs);
}
};
projects / cvc5.git / commitdiff