* Author: dejan
*/
-#include "expr/node.h"
+#include "context/context.h"
#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/node_manager.h"
#include "expr/expr_manager.h"
-#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/type.h"
using namespace std;
using namespace CVC4::context;
+using namespace CVC4::kind;
namespace CVC4 {
/** Make a function type with input types from argTypes. */
FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
Type* range) {
+ Assert( argTypes.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->mkFunctionType(argTypes, range);
}
+FunctionType*
+ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
+ Assert( sorts.size() >= 2 );
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkFunctionType(sorts);
+}
+
+FunctionType*
+ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
+ Assert( sorts.size() >= 1 );
+ NodeManagerScope nms(d_nodeManager);
+ return d_nodeManager->mkPredicateType(sorts);
+}
+
Type* ExprManager::mkSort(const std::string& name) {
NodeManagerScope nms(d_nodeManager);
return d_nodeManager->mkSort(name);
return Expr(this, new Node(d_nodeManager->mkVar(type)));
}
+unsigned int ExprManager::minArity(Kind kind) {
+ switch(kind) {
+ case FALSE:
+ case SKOLEM:
+ case TRUE:
+ case VARIABLE:
+ return 0;
+
+ case AND:
+ case NOT:
+ case OR:
+ return 1;
+
+ case APPLY_UF:
+ case DISTINCT:
+ case EQUAL:
+ case IFF:
+ case IMPLIES:
+ case PLUS:
+ case XOR:
+ return 2;
+
+ case ITE:
+ return 3;
+
+ default:
+ Unhandled(kind);
+ }
+}
+
+unsigned int ExprManager::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_UF:
+ case DISTINCT:
+ case PLUS:
+ case OR:
+ return UINT_MAX;
+
+ default:
+ Unhandled(kind);
+ }
+}
+
+
NodeManager* ExprManager::getNodeManager() const {
return d_nodeManager;
}
mkFunctionType(Type* domain,
Type* range);
- /** Make a function type with input types from argTypes. */
+ /** Make a function type with input types from argTypes. <code>argTypes</code>
+ * must have at least one element. */
FunctionType*
mkFunctionType(const std::vector<Type*>& argTypes,
Type* range);
+ /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
+ * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
+ * least 2 elements.
+ */
+ FunctionType*
+ mkFunctionType(const std::vector<Type*>& sorts);
+
+ /** Make a predicate type with input types from <code>sorts</code>. The result with
+ * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
+ * least one element.
+ */
+ FunctionType*
+ mkPredicateType(const std::vector<Type*>& sorts);
+
/** Make a new sort with the given name. */
Type* mkSort(const std::string& name);
Expr mkVar(Type* type, const std::string& name);
Expr mkVar(Type* type);
+ /** Returns the minimum arity of the given kind. */
+ static unsigned int minArity(Kind kind);
+
+ /** Returns the maximum arity of the given kind. */
+ static unsigned int maxArity(Kind kind);
+
private:
/** The context */
context::Context* d_ctxt;
/** Make a function type from domain to range. */
inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
- /** Make a function type with input types from argTypes. */
+ /** Make a function type with input types from argTypes. <code>argTypes</code>
+ * must have at least one element. */
inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
Type* range) const;
+ /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
+ * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
+ * least 2 elements.
+ */
+ inline FunctionType*
+ mkFunctionType(const std::vector<Type*>& sorts);
+
+ /** Make a predicate type with input types from <code>sorts</code>. The result with
+ * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
+ * least one element.
+ */
+ inline FunctionType*
+ mkPredicateType(const std::vector<Type*>& sorts);
+
/** Make a new sort with the given name. */
inline Type* mkSort(const std::string& name) const;
return new FunctionType(argTypes, range);
}
+inline FunctionType*
+NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
+ Assert( sorts.size() >= 2 );
+ std::vector<Type*> argTypes(sorts);
+ Type* rangeType = argTypes.back();
+ argTypes.pop_back();
+ return mkFunctionType(argTypes,rangeType);
+}
+
+inline FunctionType*
+NodeManager::mkPredicateType(const std::vector<Type*>& sorts) {
+ Assert( sorts.size() >= 1 );
+ return mkFunctionType(sorts,booleanType());
+}
inline Type* NodeManager::mkSort(const std::string& name) const {
return new SortType(name);
}
Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: /* A sort declaration (e.g., "T : TYPE") */
- TYPE_TOK { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); }
+ TYPE_TOK
+ { ANTLR_INPUT->newSorts(idList);
+ t = EXPR_MANAGER->kindType(); }
| /* A variable declaration */
type[t] { ANTLR_INPUT->mkVars(idList,t); }
;
*/
type[CVC4::Type*& t]
@init {
+ Type* t2;
std::vector<Type*> typeList;
Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: /* Simple type */
baseType[t]
| /* Single-parameter function type */
- baseType[t] { typeList.push_back(t); }
- ARROW_TOK baseType[t]
- { t = ANTLR_INPUT->functionType(typeList,t); }
+ baseType[t] ARROW_TOK baseType[t2]
+ { t = EXPR_MANAGER->mkFunctionType(t,t2); }
| /* Multi-parameter function type */
LPAREN baseType[t]
{ typeList.push_back(t); }
(COMMA baseType[t] { typeList.push_back(t); } )+
RPAREN ARROW_TOK baseType[t]
- { t = ANTLR_INPUT->functionType(typeList,t); }
+ { t = EXPR_MANAGER->mkFunctionType(typeList,t); }
;
/**
std::string id;
Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); }
+ : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
| typeSymbol[t]
;
Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
std::string name;
}
- : identifier[name,CHECK_DECLARED,SYM_FUNCTION]
+ : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
{ ANTLR_INPUT->checkFunction(name);
- f = ANTLR_INPUT->getFunction(name); }
+ f = ANTLR_INPUT->getVariable(name); }
;
switch( type ) {
case SYM_VARIABLE: // Functions share var namespace
- case SYM_FUNCTION:
return d_varSymbolTable.getObject(name);
default:
return getSymbol(name, SYM_VARIABLE);
}
-Expr Input::getFunction(const std::string& name) {
- return getSymbol(name, SYM_FUNCTION);
-}
-
Type*
Input::getType(const std::string& var_name,
SymbolType type) {
/* Returns true if name is bound to a function. */
bool Input::isFunction(const std::string& name) {
- return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction();
+ return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
}
/* Returns true if name is bound to a function returning boolean. */
bool Input::isPredicate(const std::string& name) {
- return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate();
-}
-
-Type*
-Input::functionType(Type* domainType,
- Type* rangeType) {
- return d_exprManager->mkFunctionType(domainType,rangeType);
-}
-
-Type*
-Input::functionType(const std::vector<Type*>& argTypes,
- Type* rangeType) {
- Assert( argTypes.size() > 0 );
- return d_exprManager->mkFunctionType(argTypes,rangeType);
-}
-
-Type*
-Input::functionType(const std::vector<Type*>& sorts) {
- Assert( sorts.size() > 0 );
- if( sorts.size() == 1 ) {
- return sorts[0];
- } else {
- std::vector<Type*> argTypes(sorts);
- Type* rangeType = argTypes.back();
- argTypes.pop_back();
- return functionType(argTypes,rangeType);
- }
-}
-
-Type* Input::predicateType(const std::vector<Type*>& sorts) {
- if(sorts.size() == 0) {
- return d_exprManager->booleanType();
- } else {
- return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType());
- }
+ return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
}
Expr
return types;
}
-BooleanType* Input::booleanType() {
- return d_exprManager->booleanType();
-}
-
-KindType* Input::kindType() {
- return d_exprManager->kindType();
-}
-
-unsigned int Input::minArity(Kind kind) {
- switch(kind) {
- case FALSE:
- case SKOLEM:
- case TRUE:
- case VARIABLE:
- return 0;
-
- case AND:
- case NOT:
- case OR:
- return 1;
-
- case APPLY_UF:
- case DISTINCT:
- case EQUAL:
- case IFF:
- case IMPLIES:
- case PLUS:
- case XOR:
- return 2;
-
- case ITE:
- return 3;
-
- default:
- Unhandled(kind);
- }
-}
-
-unsigned int Input::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_UF:
- case DISTINCT:
- case PLUS:
- case OR:
- return UINT_MAX;
-
- default:
- Unhandled(kind);
- }
-}
-
bool Input::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
- case SYM_VARIABLE: // Functions share var namespace
- case SYM_FUNCTION:
+ case SYM_VARIABLE:
return d_varSymbolTable.isBound(name);
case SYM_SORT:
return d_sortTable.isBound(name);
return;
}
- unsigned int min = minArity(kind);
- unsigned int max = maxArity(kind);
+ unsigned int min = d_exprManager->minArity(kind);
+ unsigned int max = d_exprManager->maxArity(kind);
if( numArgs < min || numArgs > max ) {
stringstream ss;
enum SymbolType {
/** Variables */
SYM_VARIABLE,
- /** Functions */
- SYM_FUNCTION,
/** Sorts */
SYM_SORT
};
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();
}
*/
Expr getVariable(const std::string& var_name);
- /**
- * Returns a function, given a name and a type.
- * @param name the name of the function
- * @return the function expression
- */
- Expr getFunction(const std::string& name);
-
/**
* Returns a sort, given a name
*/
/** Remove a variable definition (e.g., from a let binding). */
void undefineVar(const std::string& name);
- /** Returns a function type over the given domain and range types. */
- Type* functionType(Type* domain, Type* range);
-
- /** Returns a function type over the given types. argTypes must be
- non-empty. */
- Type* functionType(const std::vector<Type*>& argTypes,
- Type* rangeType);
-
- /**
- * Returns a function type over the given types. If types has only
- * one element, then the type is just types[0].
- *
- * @param types a non-empty list of input and output types.
- */
- Type* functionType(const std::vector<Type*>& types);
-
- /**
- * Returns a predicate type over the given sorts. If sorts is empty,
- * then the type is just BOOLEAN.
-
- * @param sorts a list of input types
- */
- Type* predicateType(const std::vector<Type*>& sorts);
-
/**
* Creates a new sort with the given name.
*/
/** Is the symbol bound to a predicate? */
bool isPredicate(const std::string& name);
- /** Returns the boolean type. */
- BooleanType* booleanType();
-
- /** Returns the kind type (i.e., the type of types). */
- KindType* kindType();
-
- /** Returns the minimum arity of the given kind. */
- static unsigned int minArity(Kind kind);
-
- /** Returns the maximum arity of the given kind. */
- static unsigned int maxArity(Kind kind);
-
/** Throws a <code>ParserException</code> with the given error message.
* Implementations should fill in the <code>ParserException</code> with
* line number information, etc. */
* @param check what kind of check to do with the symbol
*/
functionName[std::string& name, CVC4::parser::DeclarationCheck check]
- : identifier[name,check,SYM_FUNCTION]
+ : identifier[name,check,SYM_VARIABLE]
;
/**
}
: functionName[name,CHECK_DECLARED]
{ ANTLR_INPUT->checkFunction(name);
- fun = ANTLR_INPUT->getFunction(name); }
+ fun = ANTLR_INPUT->getVariable(name); }
;
/**
: ATTR_IDENTIFIER
;
-
-
functionDeclaration
@declarations {
std::string name;
t = sortSymbol // require at least one sort
{ sorts.push_back(t); }
sortList[sorts] RPAREN_TOK
- { t = ANTLR_INPUT->functionType(sorts);
+ { if( sorts.size() == 1 ) {
+ Assert( t == sorts[0] );
+ } else {
+ t = EXPR_MANAGER->mkFunctionType(sorts);
+ }
ANTLR_INPUT->mkVar(name, t); }
;
std::vector<Type*> p_sorts;
}
: LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
- { Type *t = ANTLR_INPUT->predicateType(p_sorts);
+ { Type *t;
+ if( p_sorts.empty() ) {
+ t = EXPR_MANAGER->booleanType();
+ } else {
+ t = EXPR_MANAGER->mkPredicateType(p_sorts);
+ }
ANTLR_INPUT->mkVar(name, t); }
;
{ id = AntlrInput::tokenText($FUN_IDENTIFIER);
Debug("parser") << "fun_identifier: " << id
<< " check? " << toString(check) << std::endl;
- ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
+ ANTLR_INPUT->checkDeclaration(id, check); }
;
using namespace CVC4::parser;
using namespace std;
-/* Set up declaration context for expr inputs */
-
-void setupContext(Input* input) {
- /* a, b, c: BOOLEAN */
- input->mkVar("a",(Type*)input->booleanType());
- input->mkVar("b",(Type*)input->booleanType());
- input->mkVar("c",(Type*)input->booleanType());
- /* t, u, v: TYPE */
- Type *t = input->newSort("t");
- Type *u = input->newSort("u");
- Type *v = input->newSort("v");
- /* f : t->u; g: u->v; h: v->t; */
- input->mkVar("f", input->functionType(t,u));
- input->mkVar("g", input->functionType(u,v));
- input->mkVar("h", input->functionType(v,t));
- /* x:t; y:u; z:v; */
- input->mkVar("x",t);
- input->mkVar("y",u);
- input->mkVar("z",v);
-}
-
/************************** CVC test inputs ********************************/
class ParserBlack : public CxxTest::TestSuite {
ExprManager *d_exprManager;
+ /* Set up declaration context for expr inputs */
+
+ void setupContext(Input* input) {
+ /* a, b, c: BOOLEAN */
+ input->mkVar("a",(Type*)d_exprManager->booleanType());
+ input->mkVar("b",(Type*)d_exprManager->booleanType());
+ input->mkVar("c",(Type*)d_exprManager->booleanType());
+ /* t, u, v: TYPE */
+ Type *t = input->newSort("t");
+ Type *u = input->newSort("u");
+ Type *v = input->newSort("v");
+ /* f : t->u; g: u->v; h: v->t; */
+ input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
+ input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
+ input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+ /* x:t; y:u; z:v; */
+ input->mkVar("x",t);
+ input->mkVar("y",u);
+ input->mkVar("z",v);
+ }
+
void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
for(int i = 0; i < numInputs; ++i) {
try {
projects / cvc5.git / commitdiff