namespace CVC4 {
ExprManager::ExprManager()
- : d_nm(new NodeManager()),
- d_booleanType(new BooleanType(this)),
- d_kindType(new KindType(this)) {
+ : d_nm(new NodeManager()) {
}
ExprManager::~ExprManager() {
}
const BooleanType* ExprManager::booleanType() {
- return d_booleanType;
+ return BooleanType::getInstance();
}
const KindType* ExprManager::kindType() {
- return d_kindType;
+ return KindType::getInstance();
}
Expr ExprManager::mkExpr(Kind kind) {
const FunctionType*
ExprManager::mkFunctionType(const Type* domain,
const Type* range) {
- return new FunctionType(this,domain,range);
+ return FunctionType::getInstance(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);
+ return FunctionType::getInstance(this,argTypes,range);
}
const Type* ExprManager::mkSort(std::string name) {
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
d_exprManager(exprManager), d_name(name) {
}
-// Type Type::operator=(const Type& t) {
-// if( this != &t ) {
-// d_name == t.d_name;
-// }
+Type::Type(std::string name) :
+ d_name(name) {
+}
bool Type::operator==(const Type& t) const {
- return d_name == t.d_name;
+ return d_exprManager == t.d_exprManager && d_name == t.d_name;
}
bool Type::operator!=(const Type& t) const {
return d_name;
}
-// void Type::toStream(std::ostream& out) const {
-// out << getName();
-// }
+BooleanType BooleanType::s_instance;
-BooleanType::BooleanType(ExprManager* exprManager)
- : Type(exprManager,std::string("BOOLEAN")) {
+BooleanType::BooleanType() : Type(std::string("BOOLEAN")) {
}
BooleanType::~BooleanType() {
}
+BooleanType*
+BooleanType::getInstance() {
+ return &s_instance;
+}
+
bool BooleanType::isBoolean() const {
return true;
}
FunctionType::FunctionType(ExprManager* exprManager,
- const Type* domain,
+ const std::vector<const Type*>& argTypes,
const Type* range)
- : Type(exprManager), d_argTypes(), d_rangeType(range) {
- d_argTypes.push_back(domain);
+ : Type(exprManager), d_argTypes(argTypes), d_rangeType(range) {
+ Assert( argTypes.size() > 0 );
}
// 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) {
+FunctionType*
+FunctionType::getInstance(ExprManager* exprManager,
+ const Type* domain,
+ const Type* range) {
+ std::vector<const Type*> argTypes;
+ argTypes.push_back(domain);
+ return getInstance(exprManager,argTypes,range);
+}
+
+ //FIXME: should be singleton
+FunctionType*
+FunctionType::getInstance(ExprManager* exprManager,
+ const std::vector<const Type*>& argTypes,
+ const Type* range) {
Assert( argTypes.size() > 0 );
+ return new FunctionType(exprManager,argTypes,range);
}
+
const std::vector<const Type*> FunctionType::getArgTypes() const {
return d_argTypes;
}
d_rangeType->toStream(out);
}
-KindType::KindType(ExprManager* exprManager)
- : Type(exprManager,std::string("KIND")) {
+KindType KindType::s_instance;
+
+KindType::KindType() : Type(std::string("KIND")) {
}
KindType::~KindType() {
return true;
}
+KindType*
+KindType::getInstance() {
+ return &s_instance;
+}
+
SortType::SortType(ExprManager* exprManager,std::string name)
: Type(exprManager,name) {
}
/**
* 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() { };
-
+ /** Comparision for equality */
bool operator==(const Type& t) const;
+
+ /** Comparison for disequality */
bool operator!=(const Type& e) const;
+ /** Get the ExprManager associated with this type. May be NULL for
+ singleton types. */
ExprManager* getExprManager() const;
+ /** Get the name of this type. May be empty for composite types. */
std::string getName() const;
+ /** Is this the boolean type? */
virtual bool isBoolean() const {
return false;
}
+ /** Is this a function type? */
virtual bool isFunction() const {
return false;
}
+ /** Is this a predicate type? NOTE: all predicate types are also
+ function types. */
virtual bool isPredicate() const {
return false;
}
+ /** Is this a kind type (i.e., the type of a type)? */
virtual bool isKind() const {
return false;
}
+ /** Outputs a string representation of this type to the stream. */
virtual void toStream(std::ostream& out) const {
out << getName();
}
protected:
+ /** Create a type associated with exprManager. */
+ Type(ExprManager* const exprManager);
+
+ /** Create a type associated with exprManager with the given name. */
+ Type(ExprManager* const exprManager, std::string name);
+
+ /** Create a type with the given name. */
+ Type(std::string name);
+
+ /** Destructor */
+ virtual ~Type() { };
+
+ /** The associated ExprManager */
ExprManager* d_exprManager;
+
+ /** The name of the type (may be empty). */
std::string d_name;
};
+/**
+ * Singleton class encapsulating the boolean type.
+ */
class BooleanType : public Type {
- public:
- BooleanType(ExprManager* exprManager);
- ~BooleanType();
+
+public:
+ static BooleanType* getInstance();
+
+ /** Is this the boolean type? (Returns true.) */
bool isBoolean() const;
+
+private:
+ /** Create a type associated with exprManager. */
+ BooleanType();
+
+ /** Do-nothing private copy constructor operator, to prevent
+ copy-construction. */
+ BooleanType(const BooleanType&);
+
+ /** Destructor */
+ ~BooleanType();
+
+ /** Do-nothing private assignment operator, to prevent
+ assignment. */
+ BooleanType& operator=(const BooleanType&);
+
+ /** The singleton instance */
+ static BooleanType s_instance;
};
+/**
+ * Class encapsulating a function type.
+ * TODO: Override == to check component types?
+ */
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();
+
+public:
+ static FunctionType* getInstance(ExprManager* exprManager,
+ const Type* domain,
+ const Type* range);
+
+ static FunctionType* getInstance(ExprManager* exprManager,
+ const std::vector<const Type*>& argTypes,
+ const Type* range);
+
+
+ /** Retrieve the argument types. The vector will be non-empty. */
const std::vector<const Type*> getArgTypes() const;
+
+ /** Get the range type (i.e., the type of the result). */
const Type* getRangeType() const;
+
+ /** Is this as function type? (Returns true.) */
bool isFunction() const;
+
+ /** Is this as predicate type? (Returns true if range is
+ boolean.) */
bool isPredicate() const;
+
+ /** Outputs a string representation of this type to the stream,
+ in the format "D -> R" or "(A, B, C) -> R". */
void toStream(std::ostream& out) const;
- private:
- std::vector<const Type*> d_argTypes;
+private:
+
+ /** Construct a function type associated with exprManager,
+ given a vector of argument types and the range type.
+
+ @param argTypes a non-empty vector of input types
+ @param range the result type
+ */
+ FunctionType(ExprManager* exprManager,
+ const std::vector<const Type*>& argTypes,
+ const Type* range);
+
+ /** Destructor */
+ ~FunctionType();
+
+ /** The list of input types. */
+ const std::vector<const Type*> d_argTypes;
+
+ /** The result type. */
const Type* d_rangeType;
+
};
+
+/** Class encapsulating the kind type (the type of types).
+ TODO: Should be a singleton per-ExprManager.
+*/
class KindType : public Type {
- public:
- KindType(ExprManager* exprManager);
- ~KindType();
+
+public:
+
+ /** Create a type associated with exprManager. */
+ static KindType* getInstance();
+
+ /** Is this the kind type? (Returns true.) */
bool isKind() const;
+
+private:
+
+ /** Create a type associated with exprManager. */
+ KindType();
+
+ /* Do-nothing private copy constructor, to prevent
+ copy construction. */
+ KindType(const KindType&);
+
+ /** Destructor */
+ ~KindType();
+
+ /* Do-nothing private assignment operator, to prevent
+ assignment. */
+ KindType& operator=(const KindType&);
+
+ /** The singleton instance */
+ static KindType s_instance;
};
+/** Class encapsulating a user-defined sort.
+ TODO: Should sort be uniquely named per-exprManager and not conflict
+ with any builtins? */
class SortType : public Type {
- public:
+
+public:
+
+ /** Create a sort associated with exprManager with the given name. */
SortType(ExprManager* exprManager, std::string name);
+
+ /** Destructor */
~SortType();
};
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_VARIABLE: // Functions share var namespace
case SYM_FUNCTION:
return d_varSymbolTable.getObject(name);
default:
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) {
return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction();
}
-/* Returns true if name is either a boolean variable OR a function
- returning boolean. */
+/* Returns true if name is bound to a function returning boolean. */
bool AntlrParser::isPredicate(std::string name) {
return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate();
}
return result;
}
-const FunctionType*
+const Type*
AntlrParser::functionType(const Type* domainType,
const Type* rangeType) {
return d_exprManager->mkFunctionType(domainType,rangeType);
}
-const FunctionType*
+const Type*
AntlrParser::functionType(const std::vector<const Type*>& argTypes,
const Type* rangeType) {
Assert( argTypes.size() > 0 );
return d_exprManager->mkFunctionType(argTypes,rangeType);
}
-const FunctionType*
+const Type*
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]);
+ return sorts[0];
} else {
- return mkVar(name, functionType(sorts));
+ std::vector<const Type*> argTypes(sorts);
+ const Type* rangeType = argTypes.back();
+ argTypes.pop_back();
+ return functionType(argTypes,rangeType);
}
}
-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) {
return 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;
return UINT_MAX;
default:
- Unhandled("kind in minArity");
+ Unhandled("kind in maxArity");
}
}
bool AntlrParser::isDeclared(string name, SymbolType type) {
switch(type) {
- case SYM_VARIABLE: // Predicates and functions share var namespace
- // case SYM_PREDICATE:
+ case SYM_VARIABLE: // Functions share var namespace
case SYM_FUNCTION:
return d_varSymbolTable.isBound(name);
case SYM_SORT:
* @return the variable expression
*/
Expr getVariable(std::string var_name);
- Expr getFunction(std::string var_name);
- /* Expr getPredicate(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(std::string name);
/**
* Returns a sort, given a name
const Type* getSort(std::string sort_name);
/**
- * Types of symbols.
+ * Types of symbols. Used to define namespaces.
*/
enum SymbolType {
/** Variables */
SYM_VARIABLE,
- /** Predicates */
- /* SYM_PREDICATE, */
/** Functions */
SYM_FUNCTION,
/** Sorts */
};
/**
- * Checks if the variable has been declared.
- * @param the variable name
+ * Checks if a symbol has been declared.
+ * @param name the symbol name
+ * @param type the symbol type
*/
- bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
+ bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE);
/**
- * Return true if the the declaration policy we want to enforce is true.
- * @param varName the symbol to check
+ * Return true if the the declaration policy we want to enforce holds
+ * for the given symbol.
+ * @param name the symbol to check
* @oaram check the kind of check to perform
+ * @param type the type of the symbol
* @return true if the check holds
*/
- bool checkDeclaration(std::string varName,
+ bool checkDeclaration(std::string name,
DeclarationCheck check,
SymbolType type = SYM_VARIABLE);
- /** Returns the type for the variable with the given name. */
+ /**
+ * Returns the type for the variable with the given name.
+ * @param name the symbol to lookup
+ * @param type the (namespace) type of the symbol
+ */
const Type* getType(std::string var_name,
SymbolType type = SYM_VARIABLE);
*/
Expr mkExpr(Kind kind, const std::vector<Expr>& children);
- /* Create a new CVC4 variable expression . */
+ /** Create a new CVC4 variable expression of the given type. */
Expr mkVar(const std::string name, const Type* type);
+ /** Create a set of new CVC4 variable expressions of the given
+ type. */
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);
+ const Type* functionType(const Type* domain, const Type* range);
- /**
- * 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
- */
- Expr newFunction(std::string name,
- const std::vector<const Type*>& sorts);
+ /** Returns a function type over the given types. argTypes must be
+ non-empty. */
+ const Type* functionType(const std::vector<const Type*>& argTypes,
+ const Type* rangeType);
- /**
- * Creates new functions over the given sorts. Each function has
- * arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
- * @param name the name of the function
- * @param sorts the sorts
+ /**
+ * 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.
*/
- const std::vector<Expr>
- newFunctions(const std::vector<std::string>& names,
- const std::vector<const Type*>& sorts);
+ const Type* functionType(const std::vector<const Type*>& types);
- /** 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 (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
- */
- Expr newPredicate(std::string name, const std::vector<const Type*>& sorts);
+ /**
+ * Returns a predicate type over the given sorts. If sorts is empty,
+ * then the type is just BOOLEAN.
- /**
- * 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
+ * @param sorts a list of input types
*/
- const std::vector<Expr>
- newPredicates(const std::vector<std::string>& names,
- const std::vector<const Type*>& sorts);
+ const Type* predicateType(const std::vector<const Type*>& sorts);
/**
* Creates a new sort with the given name.
const std::vector<const Type*>
newSorts(const std::vector<std::string>& names);
+ /** Is the symbol bound to a boolean variable? */
bool isBoolean(std::string name);
+
+ /** Is the symbol bound to a function? */
bool isFunction(std::string name);
+
+ /** Is the symbol bound to a predicate? */
bool isPredicate(std::string name);
+ /** Returns the boolean type. */
const BooleanType* booleanType();
+
+ /** Returns the kind type (i.e., the type of types). */
const KindType* kindType();
- unsigned int minArity(Kind kind);
- unsigned int maxArity(Kind kind);
+ /** Returns the minimum arity of the given kind. */
+ static unsigned int minArity(Kind kind);
- /**
- * Returns the precedence rank of the kind.
- */
- static unsigned getPrecedence(Kind kind);
+ /** Returns the maximum arity of the given kind. */
+ static unsigned int maxArity(Kind kind);
+ /** Returns a string representation of the given object (for
+ debugging). */
inline std::string toString(DeclarationCheck check) {
switch(check) {
case CHECK_NONE: return "CHECK_NONE";
}
}
+ /** Returns a string representation of the given object (for
+ debugging). */
inline std::string toString(SymbolType type) {
switch(type) {
case SYM_VARIABLE: return "SYM_VARIABLE";
/** The sort table */
SymbolTable<const Type*> d_sortTable;
+ /** Lookup a symbol in the given namespace. */
Expr getSymbol(std::string var_name, SymbolType type);
-
};
t = sortSymbol // require at least one sort
{ sorts.push_back(t); }
sortList[sorts] RPAREN
- { newFunction(name, sorts); }
+ { t = functionType(sorts);
+ mkVar(name, t); }
;
/**
{
string p_name;
std::vector<const Type*> p_sorts;
+ const Type *t;
}
: LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN
- { newPredicate(p_name, p_sorts); }
+ { t = predicateType(p_sorts);
+ mkVar(p_name, t); }
;
sortDeclaration
projects / cvc5.git / commitdiff