#ifndef __CVC4__CONTEXT__CDMAP_H
#define __CVC4__CONTEXT__CDMAP_H
-#include "context/context.h"
-#include "util/Assert.h"
-
#include <vector>
#include <iterator>
#include <ext/hash_map>
+#include "context/context.h"
+#include "util/Assert.h"
+#include "context/cdmap_forward.h"
+
namespace CVC4 {
namespace context {
// Auxiliary class: almost the same as CDO (see cdo.h)
-template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
-
template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
class CDOmap : public ContextObj {
friend class CDMap<Key, Data, HashFcn>;
--- /dev/null
+/********************* */
+/*! \file cdmap_forward.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a forward declaration header to declare the CDMap<>
+ ** template
+ **
+ ** This is a forward declaration header to declare the CDMap<>
+ ** template. It's useful if you want to forward-declare CDMap<>
+ ** without including the full cdmap.h header, for example, in a
+ ** public header context.
+ **
+ ** For CDMap<> in particular, it's difficult to forward-declare it
+ ** yourself, becase it has a default template argument.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
+#define __CVC4__CONTEXT__CDMAP_FORWARD_H
+
+namespace __gnu_cxx {
+ template <class Key> class hash;
+}/* __gnu_cxx namespace */
+
+namespace CVC4 {
+ namespace context {
+ template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+ class CDMap;
+ }/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
public:
+ // ensure these are publicly accessible
+ static void* operator new(size_t size, bool b) {
+ return ContextObj::operator new(size, b);
+ }
+
+ static void operator delete(void* pMem, bool b) {
+ return ContextObj::operator delete(pMem, b);
+ }
+
+ void deleteSelf() {
+ this->ContextObj::deleteSelf();
+ }
+
+ static void operator delete(void* pMem) {
+ AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
+ }
+
CDSet(Context* context) :
super(context) {
}
command.cpp \
declaration_scope.h \
declaration_scope.cpp \
- expr_manager_scope.h
+ expr_manager_scope.h \
+ sort.h
nodist_libexpr_la_SOURCES = \
kind.h \
metakind.h \
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Convenience class for scoping variable and type declarations (implementation).
+ ** \brief Convenience class for scoping variable and type
+ ** declarations (implementation).
**
- ** Convenience class for scoping variable and type declarations (implementation)
+ ** Convenience class for scoping variable and type declarations
+ ** (implementation).
**/
-#include "declaration_scope.h"
-#include "expr.h"
-#include "type.h"
-
+#include "expr/declaration_scope.h"
+#include "expr/expr.h"
+#include "expr/type.h"
#include "context/cdmap.h"
+#include "context/cdset.h"
#include "context/context.h"
#include <string>
+#include <utility>
-namespace CVC4 {
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
-using namespace context;
+namespace CVC4 {
DeclarationScope::DeclarationScope() :
- d_context(new Context()),
- d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)),
- d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) {
+ d_context(new Context),
+ d_exprMap(new(true) CDMap<std::string, Expr, StringHashFunction>(d_context)),
+ d_typeMap(new(true) CDMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
+ d_functions(new(true) CDSet<Expr, ExprHashFunction>(d_context)) {
}
DeclarationScope::~DeclarationScope() {
d_exprMap->deleteSelf();
d_typeMap->deleteSelf();
+ d_functions->deleteSelf();
delete d_context;
}
-void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () {
- d_exprMap->insert(name,obj);
+void DeclarationScope::bind(const std::string& name, Expr obj) throw() {
+ d_exprMap->insert(name, obj);
}
-bool DeclarationScope::isBound(const std::string& name) const throw () {
+void DeclarationScope::bindDefinedFunction(const std::string& name, Expr obj) throw() {
+ d_exprMap->insert(name, obj);
+ d_functions->insert(obj);
+}
+
+bool DeclarationScope::isBound(const std::string& name) const throw() {
return d_exprMap->find(name) != d_exprMap->end();
}
-Expr DeclarationScope::lookup(const std::string& name) const throw () {
+bool DeclarationScope::isBoundDefinedFunction(const std::string& name) const throw() {
+ CDMap<std::string, Expr, StringHashFunction>::iterator found =
+ d_exprMap->find(name);
+ return found != d_exprMap->end() && d_functions->contains((*found).second);
+}
+
+Expr DeclarationScope::lookup(const std::string& name) const throw(AssertionException) {
return (*d_exprMap->find(name)).second;
}
-void DeclarationScope::bindType(const std::string& name, const Type& t) throw () {
- d_typeMap->insert(name,t);
+void DeclarationScope::bindType(const std::string& name, Type t) throw() {
+ d_typeMap->insert(name, make_pair(vector<Type>(), t));
}
-bool DeclarationScope::isBoundType(const std::string& name) const throw () {
+void DeclarationScope::bindType(const std::string& name,
+ const vector<Type>& params,
+ Type t) throw() {
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "bindType(" << name << ", [";
+ if(params.size() > 0) {
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back();
+ }
+ Debug("sort") << "], " << t << ")" << endl;
+ }
+ d_typeMap->insert(name, make_pair(params, t));
+}
+
+bool DeclarationScope::isBoundType(const std::string& name) const throw() {
return d_typeMap->find(name) != d_typeMap->end();
}
-Type DeclarationScope::lookupType(const std::string& name) const throw () {
- return (*d_typeMap->find(name)).second;
+Type DeclarationScope::lookupType(const std::string& name) const throw(AssertionException) {
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ Assert(p.first.size() == 0,
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided 0",
+ name.c_str(), p.first.size());
+ return p.second;
}
+Type DeclarationScope::lookupType(const std::string& name,
+ const vector<Type>& params) const throw(AssertionException) {
+ pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
+ Assert(p.first.size() == params.size(),
+ "type constructor arity is wrong: "
+ "`%s' requires %u parameters but was provided %u",
+ name.c_str(), p.first.size(), params.size());
+ if(p.first.size() == 0) {
+ Assert(p.second.isSort());
+ return p.second;
+ }
+ if(p.second.isSortConstructor()) {
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "instantiating using a sort constructor" << endl;
+ Debug("sort") << "have formals [";
+ copy( p.first.begin(), p.first.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << p.first.back() << "]" << endl
+ << "parameters [";
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back() << "]" << endl
+ << "type ctor " << name << endl
+ << "type is " << p.second << endl;
+ }
+
+ Type instantiation =
+ SortConstructorType(p.second).instantiate(params);
+
+ Debug("sort") << "instance is " << instantiation << endl;
+
+ return instantiation;
+ } else {
+ Assert(p.second.isSort());
+ if(Debug.isOn("sort")) {
+ Debug("sort") << "instantiating using a sort substitution" << endl;
+ Debug("sort") << "have formals [";
+ copy( p.first.begin(), p.first.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << p.first.back() << "]" << endl
+ << "parameters [";
+ copy( params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("sort"), ", ") );
+ Debug("sort") << params.back() << "]" << endl
+ << "type ctor " << name << endl
+ << "type is " << p.second << endl;
+ }
+
+ Type instantiation = p.second.substitute(p.first, params);
+
+ Debug("sort") << "instance is " << instantiation << endl;
+
+ return instantiation;
+ }
+}
-void DeclarationScope::popScope() throw (ScopeException) {
+void DeclarationScope::popScope() throw(ScopeException) {
if( d_context->getLevel() == 0 ) {
throw ScopeException();
}
d_context->pop();
}
-void DeclarationScope::pushScope() throw () {
+void DeclarationScope::pushScope() throw() {
d_context->push();
}
#ifndef DECLARATION_SCOPE_H
#define DECLARATION_SCOPE_H
+#include <vector>
+#include <utility>
#include <ext/hash_map>
#include "expr/expr.h"
class Type;
namespace context {
+ class Context;
-class Context;
+ template <class Key, class Data, class HashFcn>
+ class CDMap;
-template <class Key, class Data, class HashFcn>
-class CDMap;
-
-} //namespace context
+ template <class V, class HashFcn>
+ class CDSet;
+}/* CVC4::context namespace */
class CVC4_PUBLIC ScopeException : public Exception {
-};
+};/* class ScopeException */
/**
* A convenience class for handling scoped declarations. Implements the usual
context::Context *d_context;
/** A map for expressions. */
- context::CDMap<std::string,Expr,StringHashFunction> *d_exprMap;
+ context::CDMap<std::string, Expr, StringHashFunction> *d_exprMap;
/** A map for types. */
- context::CDMap<std::string,Type,StringHashFunction> *d_typeMap;
+ context::CDMap<std::string, std::pair<std::vector<Type>, Type>, StringHashFunction> *d_typeMap;
+
+ /** A set of defined functions. */
+ context::CDSet<Expr, ExprHashFunction> *d_functions;
public:
/** Create a declaration scope. */
/** Destroy a declaration scope. */
~DeclarationScope();
- /** Bind an expression to a name in the current scope level.
- * If <code>name</code> is already bound in the current level, then the
+ /**
+ * Bind an expression to a name in the current scope level. If
+ * <code>name</code> is already bound in the current level, then the
* binding is replaced. If <code>name</code> is bound in a previous
- * level, then the binding is "covered" by this one until the current
- * scope is popped.
+ * level, then the binding is "covered" by this one until the
+ * current scope is popped.
*
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
*/
- void bind(const std::string& name, const Expr& obj) throw ();
-
- /** Bind a type to a name in the current scope.
- * If <code>name</code> is already bound to a type in the current level,
- * then the binding is replaced. If <code>name</code> is bound in a
- * previous level, then the binding is "covered" by this one until the
- * current scope is popped.
+ void bind(const std::string& name, Expr obj) throw();
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type in the current level, then the binding
+ * is replaced. If <code>name</code> is bound in a previous level,
+ * then the binding is "covered" by this one until the current scope
+ * is popped.
+ *
+ * @param name an identifier
+ * @param t the type to bind to <code>name</code>
+ */
+ void bindDefinedFunction(const std::string& name, Expr obj) throw();
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type in the current level, then the binding
+ * is replaced. If <code>name</code> is bound in a previous level,
+ * then the binding is "covered" by this one until the current scope
+ * is popped.
+ *
+ * @param name an identifier
+ * @param t the type to bind to <code>name</code>
+ */
+ void bindType(const std::string& name, Type t) throw();
+
+ /**
+ * Bind a type to a name in the current scope. If <code>name</code>
+ * is already bound to a type or type constructor in the current
+ * level, then the binding is replaced. If <code>name</code> is
+ * bound in a previous level, then the binding is "covered" by this
+ * one until the current scope is popped.
*
* @param name an identifier
* @param t the type to bind to <code>name</code>
*/
- void bindType(const std::string& name, const Type& t) throw ();
+ void bindType(const std::string& name,
+ const std::vector<Type>& params,
+ Type t) throw();
- /** Check whether a name is bound to an expression.
+ /**
+ * Check whether a name is bound to an expression with either bind()
+ * or bindDefinedFunction().
*
* @param name the identifier to check.
* @returns true iff name is bound in the current scope.
*/
- bool isBound(const std::string& name) const throw ();
+ bool isBound(const std::string& name) const throw();
+
+ /**
+ * Check whether a name was bound to a function with bindDefinedFunction().
+ */
+ bool isBoundDefinedFunction(const std::string& name) const throw();
- /** Check whether a name is bound to a type.
+ /**
+ * Check whether a name is bound to a type (or type constructor).
*
* @param name the identifier to check.
* @returns true iff name is bound to a type in the current scope.
*/
- bool isBoundType(const std::string& name) const throw ();
+ bool isBoundType(const std::string& name) const throw();
- /** Lookup a bound expression.
+ /**
+ * Lookup a bound expression.
*
* @param name the identifier to lookup
* @returns the expression bound to <code>name</code> in the current scope.
*/
- Expr lookup(const std::string& name) const throw ();
+ Expr lookup(const std::string& name) const throw(AssertionException);
- /** Lookup a bound type.
+ /**
+ * Lookup a bound type.
*
- * @param name the identifier to lookup
+ * @param name the type identifier to lookup
* @returns the type bound to <code>name</code> in the current scope.
*/
- Type lookupType(const std::string& name) const throw ();
+ Type lookupType(const std::string& name) const throw(AssertionException);
- /** Pop a scope level. Deletes all bindings since the last call to
+ /**
+ * Lookup a bound parameterized type.
+ *
+ * @param name the type-constructor identifier to lookup
+ * @param params the types to use to parameterize the type
+ * @returns the type bound to <code>name(<i>params</i>)</code> in
+ * the current scope.
+ */
+ Type lookupType(const std::string& name,
+ const std::vector<Type>& params) const throw(AssertionException);
+
+ /**
+ * Pop a scope level. Deletes all bindings since the last call to
* <code>pushScope</code>. Calls to <code>pushScope</code> and
* <code>popScope</code> must be "properly nested." I.e., a call to
* <code>popScope</code> is only legal if the number of prior calls to
* <code>pushScope</code> on this <code>DeclarationScope</code> is strictly
* greater than then number of prior calls to <code>popScope</code>. */
- void popScope() throw (ScopeException);
+ void popScope() throw(ScopeException);
/** Push a scope level. */
- void pushScope() throw ();
+ void pushScope() throw();
+
};/* class DeclarationScope */
-}/* namespace CVC4 */
+}/* CVC4 namespace */
#endif /* DECLARATION_SCOPE_H */
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
- return Expr(this, d_nodeManager->mkNodePtr(kind,
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
child1.getNode(),
child2.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
e.getMessage());
}
}
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
- return Expr(this, d_nodeManager->mkNodePtr(kind,
- child1.getNode(),
- child2.getNode(),
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
+ child1.getNode(),
+ child2.getNode(),
child3.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
e.getMessage());
}
}
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
- return Expr(this, d_nodeManager->mkNodePtr(kind,
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
child1.getNode(),
- child2.getNode(),
+ child2.getNode(),
child3.getNode(),
child4.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
e.getMessage());
}
}
minArity(kind), maxArity(kind), n);
NodeManagerScope nms(d_nodeManager);
try {
- return Expr(this, d_nodeManager->mkNodePtr(kind,
+ return Expr(this, d_nodeManager->mkNodePtr(kind,
child1.getNode(),
- child2.getNode(),
+ child2.getNode(),
child3.getNode(),
child4.getNode(),
child5.getNode()));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
e.getMessage());
}
}
try {
return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
} catch (const TypeCheckingExceptionPrivate& e) {
- throw TypeCheckingException(Expr(this, new Node(e.getNode())),
+ throw TypeCheckingException(Expr(this, new Node(e.getNode())),
e.getMessage());
}
}
/** Make a function type with input types from argTypes. */
FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
- Assert( argTypes.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
+ Assert( argTypes.size() >= 1 );
std::vector<TypeNode> argTypeNodes;
for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
argTypeNodes.push_back(*argTypes[i].d_typeNode);
}
FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
- Assert( sorts.size() >= 2 );
NodeManagerScope nms(d_nodeManager);
+ Assert( sorts.size() >= 2 );
std::vector<TypeNode> sortNodes;
for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
sortNodes.push_back(*sorts[i].d_typeNode);
}
FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
- Assert( sorts.size() >= 1 );
NodeManagerScope nms(d_nodeManager);
+ Assert( sorts.size() >= 1 );
std::vector<TypeNode> sortNodes;
for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
sortNodes.push_back(*sorts[i].d_typeNode);
}
TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
- Assert( types.size() >= 2 );
NodeManagerScope nms(d_nodeManager);
+ Assert( types.size() >= 2 );
std::vector<TypeNode> typeNodes;
for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
typeNodes.push_back(*types[i].d_typeNode);
return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)));
}
-SortType ExprManager::mkSort(const std::string& name, size_t arity) const {
+SortType ExprManager::mkSort(const std::string& name) const {
+ NodeManagerScope nms(d_nodeManager);
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
+}
+
+SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
+ size_t arity) const {
NodeManagerScope nms(d_nodeManager);
- return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, arity)));
+ return Type(d_nodeManager,
+ new TypeNode(d_nodeManager->mkSortConstructor(name, arity)));
}
/**
* amount of checking required to return a valid result.
*
* @param n the Expr for which we want a type
- * @param check whether we should check the type as we compute it
+ * @param check whether we should check the type as we compute it
* (default: false)
*/
Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) {
/* If the number of children is within bounds, then there's nothing to do. */
if( numChildren <= max ) {
return mkExpr(kind,children);
- }
+ }
std::vector<Expr>::const_iterator it = children.begin() ;
std::vector<Expr>::const_iterator end = children.end() ;
/* It would be really weird if this happened (it would require
* min > 2, for one thing), but let's make sure. */
- AlwaysAssert( newChildren.size() >= min,
+ AlwaysAssert( newChildren.size() >= min,
"Too few new children in mkAssociative" );
return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
template <class T>
Expr mkConst(const T&);
- /** Create an Expr by applying an associative operator to the children.
+ /**
+ * Create an Expr by applying an associative operator to the children.
* If <code>children.size()</code> is greater than the max arity for
* <code>kind</code>, then the expression will be broken up into
* suitably-sized chunks, taking advantage of the associativity of
/** Make the type of arrays with the given parameterization */
ArrayType mkArrayType(Type indexType, Type constituentType) const;
- /** Make a new sort with the given name and arity. */
- SortType mkSort(const std::string& name, size_t arity = 0) const;
+ /** Make a new sort with the given name. */
+ SortType mkSort(const std::string& name) const;
+
+ /** Make a new sort from a constructor */
+ SortType mkSort(SortConstructorType constructor,
+ const std::vector<TypeNode>& children) const;
+
+ /** Make a sort constructor from a name and arity */
+ SortConstructorType mkSortConstructor(const std::string& name,
+ size_t arity) const;
/** Get the type of an expression */
Type getType(const Expr& e, bool check = false)
return *d_node > *e.d_node;
}
+unsigned Expr::getId() const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ return d_node->getId();
+}
+
Kind Expr::getKind() const {
ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
/**
* Get the Expr that caused the type-checking to fail.
+ *
* @return the expr
*/
Expr getExpression() const;
/**
* Constructor for internal purposes.
+ *
* @param em the expression manager that handles this expression
* @param node the actual expression node pointer
*/
/**
* Copy constructor, makes a copy of a given expression
+ *
* @param e the expression to copy
*/
Expr(const Expr& e);
* Assignment operator, makes a copy of the given expression. If the
* expression managers of the two expressions differ, the expression of
* the given expression will be used.
+ *
* @param e the expression to assign
* @return the reference to this expression after assignment
*/
/**
* Syntactic comparison operator. Returns true if expressions belong to the
* same expression manager and are syntactically identical.
+ *
* @param e the expression to compare to
* @return true if expressions are syntactically the same, false otherwise
*/
bool operator==(const Expr& e) const;
/**
- * Syntactic dis-equality operator.
+ * Syntactic disequality operator.
+ *
* @param e the expression to compare to
* @return true if expressions differ syntactically, false otherwise
*/
* ordering than all the expressions created later. Null expression is the
* smallest element of the ordering. The behavior of the operator is
* undefined if the expressions come from two different expression managers.
+ *
* @param e the expression to compare to
* @return true if this expression is smaller than the given one
*/
* ordering than all the expressions created later. Null expression is the
* smallest element of the ordering. The behavior of the operator is
* undefined if the expressions come from two different expression managers.
+ *
* @param e the expression to compare to
* @return true if this expression is greater than the given one
*/
* ordering than all the expressions created later. Null expression is the
* smallest element of the ordering. The behavior of the operator is
* undefined if the expressions come from two different expression managers.
+ *
* @param e the expression to compare to
* @return true if this expression is smaller or equal to the given one
*/
* ordering than all the expressions created later. Null expression is the
* smallest element of the ordering. The behavior of the operator is
* undefined if the expressions come from two different expression managers.
+ *
* @param e the expression to compare to
* @return true if this expression is greater or equal to the given one
*/
bool operator>=(const Expr& e) const { return !(*this < e); }
+ /**
+ * Get the ID of this expression (used for the comparison operators).
+ *
+ * @return an identifier uniquely identifying the value this
+ * expression holds.
+ */
+ unsigned getId() const;
+
/**
* Returns the kind of the expression (AND, PLUS ...).
+ *
* @return the kind of the expression
*/
Kind getKind() const;
/**
* Returns the number of children of this expression.
+ *
* @return the number of children
*/
size_t getNumChildren() const;
/**
* Returns the i'th child of this expression.
+ *
* @param i the index of the child to retrieve
* @return the child
*/
/**
* Check if this is an expression that has an operator.
+ *
* @return true if this expression has an operator
*/
bool hasOperator() const;
/**
* Get the operator of this expression.
+ *
* @throws IllegalArgumentException if it has no operator
* @return the operator of this expression
*/
}/* CVC4::expr namespace */
+// for hash_maps, hash_sets..
+struct ExprHashFunction {
+ size_t operator()(CVC4::Expr e) const {
+ return (size_t) e.getId();
+ }
+};/* struct ExprHashFunction */
+
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_H */
exit 1
fi
- if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+ if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then
if [ $lb = 0 ]; then
echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
exit 1
namespace CVC4 {
-TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message)
-: Exception(message), d_node(new Node(node))
-{
+TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
+ string message) :
+ Exception(message),
+ d_node(new Node(node)) {
}
TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
delete d_node;
}
-std::string TypeCheckingExceptionPrivate::toString() const {
- std::stringstream ss;
+string TypeCheckingExceptionPrivate::toString() const {
+ stringstream ss;
ss << "Error type-checking " << d_node << ": " << d_msg;
return ss.str();
}
/**
* Returns a node representing the operator of this expression.
* If this is an APPLY, then the operator will be a functional term.
- * Otherwise, it will be a node with kind BUILTIN
+ * Otherwise, it will be a node with kind BUILTIN.
*/
NodeTemplate<true> getOperator() const;
- /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
+ /**
+ * Returns true if the node has an operator (i.e., it's not a
+ * variable or a constant).
+ */
inline bool hasOperator() const;
/**
size_t operator()(const CVC4::Node& node) const {
return (size_t) node.getId();
}
-};
+};/* struct NodeHashFunction */
// for hash_maps, hash_sets..
struct TNodeHashFunction {
size_t operator()(CVC4::TNode node) const {
return (size_t) node.getId();
}
-};
+};/* struct TNodeHashFunction */
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
/**
* Returns a node representing the operator of this expression.
* If this is an APPLY, then the operator will be a functional term.
- * Otherwise, it will be a node with kind BUILTIN
+ * Otherwise, it will be a node with kind BUILTIN.
*/
template <bool ref_count>
NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
case kind::SORT_TYPE:
typeNode = kindType();
break;
+ case kind::APPLY:
+ typeNode = CVC4::theory::builtin::ApplyTypeRule::computeType(this, n, check);
+ break;
case kind::EQUAL:
typeNode = CVC4::theory::builtin::EqualityTypeRule::computeType(this, n, check);
break;
// TODO: hide this attribute behind a NodeManager interface.
namespace attr {
struct VarNameTag {};
+ struct SortArityTag {};
}/* CVC4::expr::attr namespace */
typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
}/* CVC4::expr namespace */
inline TypeNode mkSort();
/** Make a new sort with the given name and arity. */
- inline TypeNode mkSort(const std::string& name, size_t arity = 0);
+ inline TypeNode mkSort(const std::string& name);
+
+ /** Make a new sort with the given name and arity. */
+ inline TypeNode mkSort(TypeNode constructor,
+ const std::vector<TypeNode>& children);
+
+ /** Make a new sort with the given name and arity. */
+ inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
/**
* Get the type for the given node and optionally do type checking.
}
inline TypeNode NodeManager::mkSort() {
- return NodeBuilder<0>(this, kind::SORT_TYPE).constructTypeNode();
+ NodeBuilder<1> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ return nb.constructTypeNode();
}
-inline TypeNode NodeManager::mkSort(const std::string& name, size_t arity) {
- Assert(arity == 0, "parameterized sorts not yet supported.");
+inline TypeNode NodeManager::mkSort(const std::string& name) {
TypeNode type = mkSort();
type.setAttribute(expr::VarNameAttr(), name);
return type;
}
+inline TypeNode NodeManager::mkSort(TypeNode constructor,
+ const std::vector<TypeNode>& children) {
+ Assert(constructor.getKind() == kind::SORT_TYPE &&
+ constructor.getNumChildren() == 0,
+ "expected a sort constructor");
+ Assert(children.size() > 0, "expected non-zero # of children");
+ uint64_t arity;
+ std::string name;
+ bool hasArityAttribute =
+ getAttribute(constructor.d_nv, expr::SortArityAttr(), arity);
+ Assert(hasArityAttribute, "expected a sort constructor");
+ bool hasNameAttribute =
+ getAttribute(constructor.d_nv, expr::VarNameAttr(), name);
+ Assert(hasNameAttribute, "expected a sort constructor");
+ Assert(arity == children.size(),
+ "arity mismatch in application of sort constructor");
+ NodeBuilder<> nb(this, kind::SORT_TYPE);
+ Node sortTag = Node(constructor.d_nv->d_children[0]);
+ nb << sortTag;
+ nb.append(children);
+ TypeNode type = nb.constructTypeNode();
+ type.setAttribute(expr::VarNameAttr(), name);
+ return type;
+}
+
+inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
+ size_t arity) {
+ Assert(arity > 0);
+ NodeBuilder<> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ TypeNode type = nb.constructTypeNode();
+ type.setAttribute(expr::VarNameAttr(), name);
+ type.setAttribute(expr::SortArityAttr(), arity);
+ return type;
+}
+
inline Node NodeManager::mkNode(Kind kind, TNode child1) {
NodeBuilder<1> nb(this, kind);
nb << child1;
}
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
- TNode child3, TNode child4, TNode child5) {
+ TNode child3, TNode child4, TNode child5) {
NodeBuilder<5> nb(this, kind);
nb << child1 << child2 << child3 << child4 << child5;
return nb.constructNodePtr();
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Implementation of expression types .
+ ** \brief Implementation of expression types
**
- ** Implementation of expression types
+ ** Implementation of expression types.
**/
+#include <iostream>
#include <string>
+#include <vector>
#include "expr/node_manager.h"
#include "expr/type.h"
#include "expr/type_node.h"
#include "util/Assert.h"
+using namespace std;
+
namespace CVC4 {
-std::ostream& operator<<(std::ostream& out, const Type& e) {
+ostream& operator<<(ostream& out, const Type& e) {
e.toStream(out);
return out;
}
return Type(d_nodeManager, new TypeNode(typeNode));
}
-Type::Type(NodeManager* nm, TypeNode* node)
-: d_typeNode(node),
+Type::Type(NodeManager* nm, TypeNode* node) :
+ d_typeNode(node),
d_nodeManager(nm) {
}
delete d_typeNode;
}
-Type::Type()
-: d_typeNode(new TypeNode()),
- d_nodeManager(NULL)
-{
+Type::Type() :
+ d_typeNode(new TypeNode),
+ d_nodeManager(NULL) {
}
-Type::Type(uintptr_t n)
-: d_typeNode(new TypeNode()),
+Type::Type(uintptr_t n) :
+ d_typeNode(new TypeNode),
d_nodeManager(NULL) {
AlwaysAssert(n == 0);
}
-Type::Type(const Type& t)
-: d_typeNode(new TypeNode(*t.d_typeNode)),
- d_nodeManager(t.d_nodeManager)
-{
+Type::Type(const Type& t) :
+ d_typeNode(new TypeNode(*t.d_typeNode)),
+ d_nodeManager(t.d_nodeManager) {
}
bool Type::isNull() const {
Type& Type::operator=(const Type& t) {
NodeManagerScope nms(d_nodeManager);
- if (this != &t) {
+ if(this != &t) {
*d_typeNode = *t.d_typeNode;
d_nodeManager = t.d_nodeManager;
}
return *d_typeNode != *t.d_typeNode;
}
-void Type::toStream(std::ostream& out) const {
+Type Type::substitute(const Type& type, const Type& replacement) const {
+ NodeManagerScope nms(d_nodeManager);
+ return makeType(d_typeNode->substitute(*type.d_typeNode,
+ *replacement.d_typeNode));
+}
+
+Type Type::substitute(const vector<Type>& types,
+ const vector<Type>& replacements) const {
+ NodeManagerScope nms(d_nodeManager);
+
+ vector<TypeNode> typesNodes, replacementsNodes;
+
+ for(vector<Type>::const_iterator i = types.begin(),
+ iend = types.end();
+ i != iend;
+ ++i) {
+ typesNodes.push_back(*(*i).d_typeNode);
+ }
+
+ for(vector<Type>::const_iterator i = replacements.begin(),
+ iend = replacements.end();
+ i != iend;
+ ++i) {
+ replacementsNodes.push_back(*(*i).d_typeNode);
+ }
+
+ return makeType(d_typeNode->substitute(typesNodes, replacementsNodes));
+}
+
+void Type::toStream(ostream& out) const {
NodeManagerScope nms(d_nodeManager);
out << *d_typeNode;
return;
}
/** Cast to a Boolean type */
-Type::operator BooleanType() const throw (AssertionException) {
+Type::operator BooleanType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isBoolean());
return BooleanType(*this);
}
/** Cast to a integer type */
-Type::operator IntegerType() const throw (AssertionException) {
+Type::operator IntegerType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isInteger());
return IntegerType(*this);
}
/** Cast to a real type */
-Type::operator RealType() const throw (AssertionException) {
+Type::operator RealType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isReal());
return RealType(*this);
}
/** Cast to a bit-vector type */
-Type::operator BitVectorType() const throw (AssertionException) {
+Type::operator BitVectorType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isBitVector());
return BitVectorType(*this);
}
/** Cast to a function type */
-Type::operator FunctionType() const throw (AssertionException) {
+Type::operator FunctionType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isFunction());
return FunctionType(*this);
}
/** Cast to a tuple type */
-Type::operator TupleType() const throw (AssertionException) {
+Type::operator TupleType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isTuple());
return TupleType(*this);
}
/** Cast to an array type */
-Type::operator ArrayType() const throw (AssertionException) {
+Type::operator ArrayType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
return ArrayType(*this);
}
}
/** Cast to a sort type */
-Type::operator SortType() const throw (AssertionException) {
+Type::operator SortType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isSort());
return SortType(*this);
}
+/** Is this a sort constructor kind */
+bool Type::isSortConstructor() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isSortConstructor();
+}
+
+/** Cast to a sort type */
+Type::operator SortConstructorType() const throw(AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isSortConstructor());
+ return SortConstructorType(*this);
+}
+
/** Is this a kind type (i.e., the type of a type)? */
bool Type::isKind() const {
NodeManagerScope nms(d_nodeManager);
}
/** Cast to a kind type */
-Type::operator KindType() const throw (AssertionException) {
+Type::operator KindType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isKind());
return KindType(*this);
}
-std::vector<Type> FunctionType::getArgTypes() const {
+vector<Type> FunctionType::getArgTypes() const {
NodeManagerScope nms(d_nodeManager);
- std::vector<Type> args;
- std::vector<TypeNode> argNodes = d_typeNode->getArgTypes();
- std::vector<TypeNode>::iterator it = argNodes.begin();
- std::vector<TypeNode>::iterator it_end = argNodes.end();
+ vector<Type> args;
+ vector<TypeNode> argNodes = d_typeNode->getArgTypes();
+ vector<TypeNode>::iterator it = argNodes.begin();
+ vector<TypeNode>::iterator it_end = argNodes.end();
for(; it != it_end; ++ it) {
args.push_back(makeType(*it));
}
return makeType(d_typeNode->getRangeType());
}
-std::vector<Type> TupleType::getTypes() const {
+vector<Type> TupleType::getTypes() const {
NodeManagerScope nms(d_nodeManager);
- std::vector<Type> types;
- std::vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
- std::vector<TypeNode>::iterator it = typeNodes.begin();
- std::vector<TypeNode>::iterator it_end = typeNodes.end();
+ vector<Type> types;
+ vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
+ vector<TypeNode>::iterator it = typeNodes.begin();
+ vector<TypeNode>::iterator it_end = typeNodes.end();
for(; it != it_end; ++ it) {
types.push_back(makeType(*it));
}
return types;
}
-std::string SortType::getName() const {
+string SortType::getName() const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->getAttribute(expr::VarNameAttr());
}
-BooleanType::BooleanType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+string SortConstructorType::getName() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getAttribute(expr::VarNameAttr());
+}
+
+size_t SortConstructorType::getArity() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->getAttribute(expr::SortArityAttr());
+}
+
+SortType SortConstructorType::instantiate(const vector<Type>& params) const {
+ NodeManagerScope nms(d_nodeManager);
+ vector<TypeNode> paramsNodes;
+ for(vector<Type>::const_iterator i = params.begin(),
+ iend = params.end();
+ i != iend;
+ ++i) {
+ paramsNodes.push_back(*getTypeNode(*i));
+ }
+ return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
+}
+
+BooleanType::BooleanType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isBoolean());
}
-IntegerType::IntegerType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+IntegerType::IntegerType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isInteger());
}
-RealType::RealType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+RealType::RealType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isReal());
}
-BitVectorType::BitVectorType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isBitVector());
}
-FunctionType::FunctionType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+FunctionType::FunctionType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isFunction());
}
-TupleType::TupleType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+TupleType::TupleType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isTuple());
}
-ArrayType::ArrayType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+ArrayType::ArrayType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isArray());
}
-KindType::KindType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+KindType::KindType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isKind());
}
-SortType::SortType(const Type& t) throw (AssertionException)
-: Type(t)
-{
+SortType::SortType(const Type& t) throw(AssertionException) :
+ Type(t) {
Assert(isSort());
}
+SortConstructorType::SortConstructorType(const Type& t)
+ throw(AssertionException) :
+ Type(t) {
+ Assert(isSortConstructor());
+}
+
unsigned BitVectorType::getSize() const {
return d_typeNode->getBitVectorSize();
}
class TupleType;
class KindType;
class SortType;
+class SortConstructorType;
class Type;
/** Strategy for hashing Types */
*/
Type(NodeManager* em, TypeNode* typeNode);
+ /** Accessor for derived classes */
+ static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+
public:
/**
*/
bool isNull() const;
+ /**
+ * Substitution of Types.
+ */
+ Type substitute(const Type& type, const Type& replacement) const;
+
+ /**
+ * Simultaneous substitution of Types.
+ */
+ Type substitute(const std::vector<Type>& types,
+ const std::vector<Type>& replacements) const;
+
/**
* Assignment operator.
* @param t the type to assign to this type
* Cast this type to a Boolean type
* @return the BooleanType
*/
- operator BooleanType() const throw (AssertionException);
+ operator BooleanType() const throw(AssertionException);
/**
* Is this the integer type?
* Cast this type to a integer type
* @return the IntegerType
*/
- operator IntegerType() const throw (AssertionException);
+ operator IntegerType() const throw(AssertionException);
/**
* Is this the real type?
* Cast this type to a real type
* @return the RealType
*/
- operator RealType() const throw (AssertionException);
+ operator RealType() const throw(AssertionException);
/**
* Is this the bit-vector type?
* Cast this type to a bit-vector type
* @return the BitVectorType
*/
- operator BitVectorType() const throw (AssertionException);
+ operator BitVectorType() const throw(AssertionException);
/**
* Is this a function type?
* Cast this type to a function type
* @return the FunctionType
*/
- operator FunctionType() const throw (AssertionException);
+ operator FunctionType() const throw(AssertionException);
/**
* Is this a tuple type?
* Cast this type to a tuple type
* @return the TupleType
*/
- operator TupleType() const throw (AssertionException);
+ operator TupleType() const throw(AssertionException);
/**
* Is this an array type?
* Cast this type to an array type
* @return the ArrayType
*/
- operator ArrayType() const throw (AssertionException);
+ operator ArrayType() const throw(AssertionException);
/**
* Is this a sort kind?
/**
* Cast this type to a sort type
- * @return the function Type
+ * @return the sort type
+ */
+ operator SortType() const throw(AssertionException);
+
+ /**
+ * Is this a sort constructor kind?
+ * @return true if this is a sort constructor kind
+ */
+ bool isSortConstructor() const;
+
+ /**
+ * Cast this type to a sort constructor type
+ * @return the sort constructor type
*/
- operator SortType() const throw (AssertionException);
+ operator SortConstructorType() const throw(AssertionException);
/**
* Is this a kind type (i.e., the type of a type)?
* Cast to a kind type
* @return the kind type
*/
- operator KindType() const throw (AssertionException);
+ operator KindType() const throw(AssertionException);
/**
* Outputs a string representation of this type to the stream.
public:
/** Construct from the base type */
- BooleanType(const Type& type) throw (AssertionException);
+ BooleanType(const Type& type) throw(AssertionException);
};
/**
public:
/** Construct from the base type */
- IntegerType(const Type& type) throw (AssertionException);
+ IntegerType(const Type& type) throw(AssertionException);
};
/**
public:
/** Construct from the base type */
- RealType(const Type& type) throw (AssertionException);
+ RealType(const Type& type) throw(AssertionException);
};
public:
/** Construct from the base type */
- FunctionType(const Type& type) throw (AssertionException);
+ FunctionType(const Type& type) throw(AssertionException);
/** Get the argument types */
std::vector<Type> getArgTypes() const;
public:
/** Construct from the base type */
- TupleType(const Type& type) throw (AssertionException);
+ TupleType(const Type& type) throw(AssertionException);
/** Get the constituent types */
std::vector<Type> getTypes() const;
public:
/** Construct from the base type */
- ArrayType(const Type& type) throw (AssertionException);
+ ArrayType(const Type& type) throw(AssertionException);
/** Get the index type */
Type getIndexType() const;
public:
/** Construct from the base type */
- SortType(const Type& type) throw (AssertionException);
+ SortType(const Type& type) throw(AssertionException);
/** Get the name of the sort */
std::string getName() const;
};
+/**
+ * Class encapsulating a user-defined sort constructor.
+ */
+class CVC4_PUBLIC SortConstructorType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ SortConstructorType(const Type& type) throw(AssertionException);
+
+ /** Get the name of the sort constructor */
+ std::string getName() const;
+
+ /** Get the arity of the sort constructor */
+ size_t getArity() const;
+
+ /** Instantiate a sort using this sort constructor */
+ SortType instantiate(const std::vector<Type>& params) const;
+};
+
/**
* Class encapsulating the kind type (the type of types).
*/
public:
/** Construct from the base type */
- KindType(const Type& type) throw (AssertionException);
+ KindType(const Type& type) throw(AssertionException);
};
public:
/** Construct from the base type */
- BitVectorType(const Type& type) throw (AssertionException);
+ BitVectorType(const Type& type) throw(AssertionException);
/**
* Returns the size of the bit-vector type.
/**
* Output operator for types
* @param out the stream to output to
- * @param e the type to output
+ * @param t the type to output
* @return the stream
*/
std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
** Reference-counted encapsulation of a pointer to node information.
**/
+#include <vector>
+
#include "expr/type_node.h"
+using namespace std;
+
namespace CVC4 {
-TypeNode TypeNode::s_null(&expr::NodeValue::s_null);
+TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
+
+TypeNode TypeNode::substitute(const TypeNode& type,
+ const TypeNode& replacement) const {
+ NodeBuilder<> nb(getKind());
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ // push the operator
+ nb << TypeNode(d_nv->d_children[0]);
+ }
+ for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+ if(*i == type) {
+ nb << replacement;
+ } else {
+ (*i).substitute(type, replacement);
+ }
+ }
+ return nb.constructTypeNode();
+}
+
+TypeNode TypeNode::substitute(const vector<TypeNode>& types,
+ const vector<TypeNode>& replacements) const {
+ vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this);
+ if(j != types.end()) {
+ return replacements[j - types.begin()];
+ } else if(getNumChildren() == 0) {
+ return *this;
+ } else {
+ NodeBuilder<> nb(getKind());
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ // push the operator
+ nb << TypeNode(d_nv->d_children[0]);
+ }
+ for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+ nb << (*i).substitute(types, replacements);
+ }
+ return nb.constructTypeNode();
+ }
+}
bool TypeNode::isBoolean() const {
- return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == BOOLEAN_TYPE;
}
bool TypeNode::isInteger() const {
- return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE;
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == INTEGER_TYPE;
}
bool TypeNode::isReal() const {
return getKind() == kind::TYPE_CONSTANT
- && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE);
+ && ( getConst<TypeConstant>() == REAL_TYPE ||
+ getConst<TypeConstant>() == INTEGER_TYPE );
}
bool TypeNode::isArray() const {
return isFunction() && getRangeType().isBoolean();
}
-std::vector<TypeNode> TypeNode::getArgTypes() const {
+vector<TypeNode> TypeNode::getArgTypes() const {
Assert(isFunction());
- std::vector<TypeNode> args;
- for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
+ vector<TypeNode> args;
+ for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
args.push_back((*this)[i]);
}
return args;
}
/** Is this a tuple type? */
-std::vector<TypeNode> TypeNode::getTupleTypes() const {
+vector<TypeNode> TypeNode::getTupleTypes() const {
Assert(isTuple());
- std::vector<TypeNode> types;
- for (unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
+ vector<TypeNode> types;
+ for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
types.push_back((*this)[i]);
}
return types;
/** Is this a sort kind */
bool TypeNode::isSort() const {
- return getKind() == kind::SORT_TYPE;
+ return getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr());
+}
+
+/** Is this a sort constructor kind */
+bool TypeNode::isSortConstructor() const {
+ return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
}
/** Is this a kind type (i.e., the type of a type)? */
bool TypeNode::isKind() const {
- return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == KIND_TYPE;
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == KIND_TYPE;
}
/** Is this a bit-vector type */
/** Is this a bit-vector type of size <code>size</code> */
bool TypeNode::isBitVector(unsigned size) const {
- return getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size;
+ return getKind() == kind::BITVECTOR_TYPE &&
+ getConst<BitVectorSize>() == size;
}
/** Get the size of this bit-vector type */
friend class NodeBuilder;
/**
- * Assigns the expression value and does reference counting. No assumptions
- * are made on the expression, and should only be used if we know what we
- * are doing.
+ * Assigns the expression value and does reference counting. No
+ * assumptions are made on the expression, and should only be used
+ * if we know what we are doing.
*
* @param ev the expression value to assign
*/
/** Copy constructor */
TypeNode(const TypeNode& node);
+ /**
+ * Destructor. If ref_count is true it will decrement the reference count
+ * and, if zero, collect the NodeValue.
+ */
+ ~TypeNode() throw(AssertionException);
+
/**
* Assignment operator for nodes, copies the relevant information from node
* to this node.
+ *
* @param node the node to copy
* @return reference to this node
*/
TypeNode& operator=(const TypeNode& typeNode);
- /**
- * Destructor. If ref_count is true it will decrement the reference count
- * and, if zero, collect the NodeValue.
- */
- ~TypeNode() throw(AssertionException);
-
/**
* Return the null node.
+ *
* @return the null node
*/
static TypeNode null() {
return s_null;
}
+ /**
+ * Substitution of TypeNodes.
+ */
+ TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const;
+
+ /**
+ * Simultaneous substitution of TypeNodes.
+ */
+ TypeNode substitute(const std::vector<TypeNode>& types,
+ const std::vector<TypeNode>& replacements) const;
+
/**
* Structural comparison operator for expressions.
+ *
* @param typeNode the type node to compare to
* @return true if expressions are equal, false otherwise
*/
bool operator==(const TypeNode& typeNode) const {
return
- d_nv == typeNode.d_nv
- || (typeNode.isReal() && this->isReal());
+ d_nv == typeNode.d_nv ||
+ (typeNode.isReal() && this->isReal());
}
/**
* Structural comparison operator for expressions.
+ *
* @param typeNode the type node to compare to
* @return true if expressions are equal, false otherwise
*/
/**
* We compare by expression ids so, keeping things deterministic and having
* that subexpressions have to be smaller than the enclosing expressions.
+ *
* @param node the node to compare to
* @return true if this expression is smaller
*/
/**
* Returns the i-th child of this node.
+ *
* @param i the index of the child
* @return the node representing the i-th child
*/
- TypeNode operator[](int i) const {
+ inline TypeNode operator[](int i) const {
return TypeNode(d_nv->getChild(i));
}
/**
* Returns the unique id of this node
+ *
* @return the id
*/
- unsigned getId() const {
+ inline unsigned getId() const {
return d_nv->getId();
}
/**
* Returns the kind of this type node.
+ *
* @return the kind
*/
inline Kind getKind() const {
/**
* Returns the metakind of this type node.
+ *
* @return the metakind
*/
inline kind::MetaKind getMetaKind() const {
/**
* Returns the number of children this node has.
+ *
* @return the number of children
*/
inline size_t getNumChildren() const;
/**
* Returns the value of the given attribute that this has been attached.
+ *
* @param attKind the kind of the attribute
* @return the value of the attribute
*/
template <class AttrKind>
- inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+ inline typename AttrKind::value_type
+ getAttribute(const AttrKind& attKind) const;
// Note that there are two, distinct hasAttribute() declarations for
// a reason (rather than using a pointer-valued argument with a
// hasAttribute() implementations.
/**
- * Returns true if this node has been associated an attribute of given kind.
- * Additionaly, if a pointer to the value_kind is give, and the attribute
- * value has been set for this node, it will be returned.
+ * Returns true if this node has been associated an attribute of
+ * given kind. Additionally, if a pointer to the value_kind is
+ * give, and the attribute value has been set for this node, it will
+ * be returned.
+ *
* @param attKind the kind of the attribute
* @return true if this node has the requested attribute
*/
* Returns true if this node has been associated an attribute of given kind.
* Additionaly, if a pointer to the value_kind is give, and the attribute
* value has been set for this node, it will be returned.
+ *
* @param attKind the kind of the attribute
* @param value where to store the value if it exists
* @return true if this node has the requested attribute
/**
* Sets the given attribute of this node to the given value.
+ *
* @param attKind the kind of the atribute
* @param value the value to set the attribute to
*/
/**
* Returns the iterator pointing to the first child.
+ *
* @return the iterator
*/
inline iterator begin() {
}
/**
- * Returns the iterator pointing to the end of the children (one beyond the
- * last one.
+ * Returns the iterator pointing to the end of the children (one
+ * beyond the last one.
+ *
* @return the end of the children iterator.
*/
inline iterator end() {
/**
* Returns the const_iterator pointing to the first child.
+ *
* @return the const_iterator
*/
inline const_iterator begin() const {
}
/**
- * Returns the const_iterator pointing to the end of the children (one
- * beyond the last one.
+ * Returns the const_iterator pointing to the end of the children
+ * (one beyond the last one.
+ *
* @return the end of the children const_iterator.
*/
inline const_iterator end() const {
}
/**
- * Converts this node into a string representation.
- * @return the string representation of this node.
+ * Converts this type into a string representation.
+ *
+ * @return the string representation of this type.
*/
inline std::string toString() const {
return d_nv->toString();
/**
* Converst this node into a string representation and sends it to the
* given stream
+ *
* @param out the sream to serialise this node to
*/
inline void toStream(std::ostream& out, int toDepth = -1,
/**
* Very basic pretty printer for Node.
+ *
* @param o output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
/**
* Returns true if this type is a null type.
+ *
* @return true if null
*/
bool isNull() const {
/** Is this a sort kind */
bool isSort() const;
+ /** Is this a sort constructor kind */
+ bool isSortConstructor() const;
+
/** Is this a kind type (i.e., the type of a type)? */
bool isKind() const;
/**
* Indents the given stream a given amount of spaces.
+ *
* @param out the stream to indent
* @param indent the numer of spaces
*/
/**
* Serializes a given node to the given stream.
+ *
* @param out the output stream to use
* @param node the node to output to the stream
* @return the changed stream.
// for hash_maps, hash_sets..
struct TypeNodeHashStrategy {
- static inline size_t hash(const CVC4::TypeNode& node) {
+ static inline size_t hash(const TypeNode& node) {
return (size_t) node.getId();
}
};/* struct TypeNodeHashStrategy */
inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
- Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+ Assert(typeNode.d_nv != NULL,
+ "Expecting a non-NULL expression value on RHS!");
if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
d_nv->dec();
d_nv = typeNode.d_nv;
return getSymbol(name, SYM_VARIABLE);
}
+Expr Parser::getFunction(const std::string& name) {
+ return getSymbol(name, SYM_VARIABLE);
+}
+
Type
Parser::getType(const std::string& var_name,
SymbolType type) {
Assert( isDeclared(var_name, type) );
- Type t = getSymbol(var_name,type).getType();
+ Type t = getSymbol(var_name, type).getType();
return t;
}
Type Parser::getSort(const std::string& name,
const std::vector<Type>& params) {
Assert( isDeclared(name, SYM_SORT) );
- Type t = d_declScope.lookupType(name);
- Warning() << "FIXME use params to realize parameterized sort\n";
+ Type t = d_declScope.lookupType(name, params);
return t;
}
return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
}
+/* Returns true if name is bound to a defined function. */
+bool Parser::isDefinedFunction(const std::string& name) {
+ return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+}
+
/* Returns true if name is bound to a function returning boolean. */
bool Parser::isPredicate(const std::string& name) {
return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
Expr
Parser::mkVar(const std::string& name, const Type& type) {
- Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
+ Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
Expr expr = d_exprManager->mkVar(name, type);
- defineVar(name,expr);
+ defineVar(name, expr);
+ return expr;
+}
+
+Expr
+Parser::mkFunction(const std::string& name, const Type& type) {
+ Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
+ Expr expr = d_exprManager->mkVar(name, type);
+ defineFunction(name, expr);
return expr;
}
const std::vector<Expr>
Parser::mkVars(const std::vector<std::string> names,
- const Type& type) {
+ const Type& type) {
std::vector<Expr> vars;
for(unsigned i = 0; i < names.size(); ++i) {
- vars.push_back(mkVar(names[i],type));
+ vars.push_back(mkVar(names[i], type));
}
return vars;
}
void
Parser::defineVar(const std::string& name, const Expr& val) {
- d_declScope.bind(name,val);
- Assert(isDeclared(name));
+ d_declScope.bind(name, val);
+ Assert( isDeclared(name) );
+}
+
+void
+Parser::defineFunction(const std::string& name, const Expr& val) {
+ d_declScope.bindDefinedFunction(name, val);
+ Assert( isDeclared(name) );
}
void
Parser::defineType(const std::string& name, const Type& type) {
- d_declScope.bindType(name,type);
- Assert( isDeclared(name, SYM_SORT) ) ;
+ d_declScope.bindType(name, type);
+ Assert( isDeclared(name, SYM_SORT) );
+}
+
+void
+Parser::defineType(const std::string& name,
+ const std::vector<Type>& params,
+ const Type& type) {
+ d_declScope.bindType(name, params, type);
+ Assert( isDeclared(name, SYM_SORT) );
}
void
const Type& type) {
if(Debug.isOn("parser")) {
Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
- copy(params.begin(), params.end() - 1,
- ostream_iterator<Type>(Debug("parser"), ", ") );
- Debug("parser") << params.back();
+ if(params.size() > 0) {
+ copy(params.begin(), params.end() - 1,
+ ostream_iterator<Type>(Debug("parser"), ", ") );
+ Debug("parser") << params.back();
+ }
Debug("parser") << "], " << type << ")" << std::endl;
}
- Warning("defineSort unimplemented\n");
- defineType(name,type);
+ defineType(name, params, type);
+}
+
+Type
+Parser::mkSort(const std::string& name) {
+ Debug("parser") << "newSort(" << name << ")" << std::endl;
+ Type type = d_exprManager->mkSort(name);
+ defineType(name, type);
+ return type;
}
Type
-Parser::mkSort(const std::string& name, size_t arity) {
- Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl;
- Type type = d_exprManager->mkSort(name, arity);
- defineType(name,type);
+Parser::mkSortConstructor(const std::string& name, size_t arity) {
+ Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
+ << std::endl;
+ Type type = d_exprManager->mkSortConstructor(name, arity);
+ defineType(name, vector<Type>(arity), type);
return type;
}
if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
}
- checkArity(kind,numArgs);
+ checkArity(kind, numArgs);
}
void Parser::addOperator(Kind kind) {
bool strictModeEnabled() { return d_strictMode; }
- /** Get the name of the input file. */
-/*
- inline const std::string getFilename() {
- return d_filename;
- }
-*/
-
/**
- * Sets the logic for the current benchmark. Declares any logic symbols.
+ * Returns a variable, given a name.
*
- * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+ * @param name the name of the variable
+ * @return the variable expression
*/
-// void setLogic(const std::string& name);
+ Expr getVariable(const std::string& name);
/**
- * Returns a variable, given a name and a type.
+ * Returns a function, given a name.
+ *
* @param var_name the name of the variable
* @return the variable expression
*/
- Expr getVariable(const std::string& var_name);
+ Expr getFunction(const std::string& name);
/**
* Returns a sort, given a name.
Type getSort(const std::string& sort_name);
/**
- * Returns a sort, given a name and args.
+ * Returns a (parameterized) sort, given a name and args.
*/
Type getSort(const std::string& sort_name,
const std::vector<Type>& params);
/**
* Checks whether the given name is bound to a function.
* @param name the name to check
- * @throws ParserException if checks are enabled and name is not bound to a function
+ * @throws ParserException if checks are enabled and name is not
+ * bound to a function
*/
void checkFunction(const std::string& name) throw (ParserException);
* Check that <code>kind</code> can accept <code>numArgs</code> arguments.
* @param kind the built-in operator to check
* @param numArgs the number of actual arguments
- * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
- * applied to <code>numArgs</code> arguments.
+ * @throws ParserException if checks are enabled and the operator
+ * <code>kind</code> cannot be applied to <code>numArgs</code>
+ * arguments.
*/
void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
- /** Check that <code>kind</code> is a legal operator in the current logic and
- * that it can accept <code>numArgs</code> arguments.
+ /**
+ * Check that <code>kind</code> is a legal operator in the current
+ * logic and that it can accept <code>numArgs</code> arguments.
*
* @param kind the built-in operator to check
* @param numArgs the number of actual arguments
- * @throws ParserException if the parser mode is strict and the operator <code>kind</kind>
- * has not been enabled
+ * @throws ParserException if the parser mode is strict and the
+ * operator <code>kind</kind> has not been enabled
*/
void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
/**
* Returns the type for the variable with the given name.
+ *
* @param var_name the symbol to lookup
* @param type the (namespace) type of the symbol
*/
Expr mkVar(const std::string& name, const Type& type);
/**
- * Create a set of new CVC4 variable expressions of the given
- * 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);
+ /** Create a new CVC4 function expression of the given type. */
+ Expr mkFunction(const std::string& name, const Type& type);
+
/** Create a new variable definition (e.g., from a let binding). */
void defineVar(const std::string& name, const Expr& val);
+ /** Create a new function definition (e.g., from a define-fun). */
+ void defineFunction(const std::string& name, const Expr& val);
+
/** Create a new type definition. */
void defineType(const std::string& name, const Type& type);
+ /** Create a new (parameterized) type definition. */
+ void defineType(const std::string& name,
+ const std::vector<Type>& params, const Type& type);
+
/** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
void defineParameterizedType(const std::string& name,
const std::vector<Type>& params,
const Type& type);
/**
- * Creates a new sort with the given name and arity.
+ * Creates a new sort with the given name.
+ */
+ Type mkSort(const std::string& name);
+
+ /**
+ * Creates a new sort constructor with the given name and arity.
*/
- Type mkSort(const std::string& name, size_t arity = 0);
+ Type mkSortConstructor(const std::string& name, size_t arity);
/**
* Creates new sorts with the given names (all of arity 0).
/** Is the symbol bound to a function? */
bool isFunction(const std::string& name);
+ /** Is the symbol bound to a defined function? */
+ bool isDefinedFunction(const std::string& name);
+
/** Is the symbol bound to a predicate? */
bool isPredicate(const std::string& name);
case THEORY_ARRAYS_EX: {
Type indexType = mkSort("Index");
Type elementType = mkSort("Element");
-
- defineType("Array",getExprManager()->mkArrayType(indexType,elementType));
+
+ defineType("Array", getExprManager()->mkArrayType(indexType,elementType));
addOperator(kind::SELECT);
addOperator(kind::STORE);
grammar Smt2;
options {
- language = 'C'; // C output for antlr
-// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
+ language = 'C'; // C output for antlr
+ //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions
k = 2;
}
DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL
{ Debug("parser") << "declare sort: '" << name
<< "' arity=" << n << std::endl;
- PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n));
- $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); }
+ unsigned arity = AntlrInput::tokenToUnsigned(n);
+ if(arity == 0) {
+ PARSER_STATE->mkSort(name);
+ $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+ } else {
+ PARSER_STATE->mkSortConstructor(name, arity);
+ $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType());
+ }
+ }
| /* sort definition */
DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT]
LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- PARSER_STATE->mkVar(name, t);
- $cmd = new DefineFunctionCommand(name,sortedVars,t,expr);
+ PARSER_STATE->mkFunction(name, t);
+ $cmd = new DefineFunctionCommand(name, sortedVars, t, expr);
}
| /* value query */
GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
| /* A non-built-in function application */
LPAREN_TOK
- functionSymbol[expr]
- { args.push_back(expr); }
+ functionName[name,CHECK_DECLARED]
+ { args.push_back(Expr()); }
termList[args,expr] RPAREN_TOK
- // TODO: check arity
- { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); }
-
- // | /* An ite expression */
- // LPAREN_TOK ITE_TOK
- // term[expr]
- // { args.push_back(expr); }
- // term[expr]
- // { args.push_back(expr); }
- // term[expr]
- // { args.push_back(expr); }
- // RPAREN_TOK
- // { expr = MK_EXPR(CVC4::kind::ITE, args); }
+ { PARSER_STATE->checkFunction(name);
+ const bool isDefinedFunction =
+ PARSER_STATE->isDefinedFunction(name);
+ expr = isDefinedFunction ?
+ PARSER_STATE->getFunction(name) :
+ PARSER_STATE->getVariable(name);
+ args[0] = expr;
+ // TODO: check arity
+ expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); }
| /* a let binding */
LPAREN_TOK LET_TOK LPAREN_TOK
}
t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
} else {
- PARSER_STATE->parseError("Unhandled parameterized type.");
+ t = PARSER_STATE->getSort(name, args);
}
}
;
// Base SMT-LIB tokens
ASSERT_TOK : 'assert';
-//CATEGORY_TOK : ':category';
CHECKSAT_TOK : 'check-sat';
-//DIFFICULTY_TOK : ':difficulty';
DECLARE_FUN_TOK : 'declare-fun';
DECLARE_SORT_TOK : 'declare-sort';
DEFINE_FUN_TOK : 'define-fun';
GET_VALUE_TOK : 'get-value';
GET_ASSERTIONS_TOK : 'get-assertions';
EXIT_TOK : 'exit';
-//FALSE_TOK : 'false';
ITE_TOK : 'ite';
LET_TOK : 'let';
LPAREN_TOK : '(';
-//NOTES_TOK : ':notes';
RPAREN_TOK : ')';
-//SAT_TOK : 'sat';
SET_LOGIC_TOK : 'set-logic';
SET_INFO_TOK : 'set-info';
+GET_INFO_TOK : 'get-info';
SET_OPTION_TOK : 'set-option';
GET_OPTION_TOK : 'get-option';
-//SMT_VERSION_TOK : ':smt-lib-version';
-//SOURCE_TOK : ':source';
-//STATUS_TOK : ':status';
-//TRUE_TOK : 'true';
-//UNKNOWN_TOK : 'unknown';
-//UNSAT_TOK : 'unsat';
// operators (NOTE: theory symbols go here)
AMPERSAND_TOK : '&';
;
/**
- * Matches an integer constant from the input (non-empty sequence of digits, with
- * no leading zeroes).
+ * Matches an integer constant from the input (non-empty sequence of
+ * digits, with no leading zeroes).
*/
INTEGER_LITERAL
: NUMERAL
;
-/** Match an integer constant. In non-strict mode, this is any sequence of
- * digits. In strict mode, non-zero integers can't have leading zeroes. */
+/**
+ * Match an integer constant. In non-strict mode, this is any sequence
+ * of digits. In strict mode, non-zero integers can't have leading
+ * zeroes.
+ */
fragment NUMERAL
@init {
char *start = (char*) GETCHARINDEX();
;
/**
- * Matches a decimal constant from the input.
- */
+ * Matches a decimal constant from the input.
+ */
DECIMAL_LITERAL
: NUMERAL '.' DIGIT+
;
fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
-/** Matches the characters that may appear in a "symbol" (i.e., an identifier)
+/**
+ * Matches the characters that may appear in a "symbol" (i.e., an identifier)
*/
fragment SYMBOL_CHAR
: '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
d_theoryEngine, d_context);
d_theoryEngine->setPropEngine(d_propEngine);
+ d_functions = new(true) FunctionMap(d_context);
+
if(d_options->interactive) {
- d_assertionList = new(true) CDList<Expr>(d_context);
+ d_assertionList = new(true) AssertionList(d_context);
}
}
shutdown();
- ::delete d_assertionList;
+ if(d_assertionList != NULL) {
+ d_assertionList->deleteSelf();
+ }
+
+ d_functions->deleteSelf();
delete d_theoryEngine;
delete d_propEngine;
Type type,
Expr formula) {
NodeManagerScope nms(d_nodeManager);
- Unimplemented();
+ d_functions->insert(name, make_pair(make_pair(args, type), formula));
}
Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) {
#include "expr/expr.h"
#include "expr/expr_manager.h"
+#include "context/cdmap_forward.h"
#include "util/result.h"
#include "util/model.h"
#include "util/sexpr.h"
+#include "util/hash.h"
#include "smt/noninteractive_exception.h"
#include "smt/bad_option.h"
class CVC4_PUBLIC SmtEngine {
private:
+ /** A name/type pair, used for signatures */
+ typedef std::pair<std::string, Type> TypedArg;
+ /** A vector of typed formals, and a return type */
+ typedef std::pair<std::vector<TypedArg>, Type> FunctionSignature;
+ /** The type of our internal map of defined functions */
+ typedef context::CDMap<std::string, std::pair<FunctionSignature, Expr>,
+ StringHashFunction>
+ FunctionMap;
+
+ /** The type of our internal assertion list */
+ typedef context::CDList<Expr> AssertionList;
+
/** Our Context */
context::Context* d_context;
-
/** Our expression manager */
ExprManager* d_exprManager;
-
/** Out internal expression/node manager */
NodeManager* d_nodeManager;
-
/** User-level options */
const Options* d_options;
-
/** The decision engine */
DecisionEngine* d_decisionEngine;
-
/** The decision engine */
TheoryEngine* d_theoryEngine;
-
/** The propositional engine */
prop::PropEngine* d_propEngine;
-
+ /** An index of our defined functions */
+ FunctionMap* d_functions;
/**
- * The assertion list, before any conversion, for supporting
+ * The assertion list (before any conversion) for supporting
* getAssertions(). Only maintained if in interactive mode.
*/
- context::CDList<Expr>* d_assertionList;
-
- // preprocess() and addFormula() used to be housed here; they are
- // now in an SmtEnginePrivate class. See the comment in
- // smt_engine.cpp.
+ AssertionList* d_assertionList;
/**
* This is called by the destructor, just before destroying the
# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
# not stored that way. If you ask for the operator of (EQUAL a b),
# you'll get a special, singleton (BUILTIN EQUAL) Node.
-constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \
- "expr/kind.h" "The kind of nodes representing built-in operators"
+constant BUILTIN \
+ ::CVC4::Kind \
+ ::CVC4::kind::KindHashStrategy \
+ "expr/kind.h" \
+ "The kind of nodes representing built-in operators"
+
+variable FUNCTION "function"
+parameterized APPLY FUNCTION 1: "defined function application"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
namespace theory {
namespace builtin {
+class ApplyTypeRule {
+ public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate) {
+ TNode f = n.getOperator();
+ TypeNode fType = f.getType(check);
+ if( !fType.isFunction() ) {
+ throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
+ }
+ if( check ) {
+ if (n.getNumChildren() != fType.getNumChildren() - 1) {
+ throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
+ }
+ TNode::iterator argument_it = n.begin();
+ TNode::iterator argument_it_end = n.end();
+ TypeNode::iterator argument_type_it = fType.begin();
+ for(; argument_it != argument_it_end; ++argument_it) {
+ if((*argument_it).getType() != *argument_type_it) {
+ throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+ }
+ }
+ }
+ return fType.getRangeType();
+ }
+};/* class ApplyTypeRule */
+
+
class EqualityTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
::CVC4::BitVectorHashStrategy \
"util/bitvector.h" \
"a fixed-width bit-vector constant"
-
+
operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
operator BITVECTOR_AND 2 "bitwise and"
-operator BITVECTOR_OR 2 "bitwise or"
-operator BITVECTOR_XOR 2 "bitwise xor"
+operator BITVECTOR_OR 2 "bitwise or"
+operator BITVECTOR_XOR 2 "bitwise xor"
operator BITVECTOR_NOT 2 "bitwise not"
operator BITVECTOR_NAND 2 "bitwise nand"
operator BITVECTOR_NOR 2 "bitwise nor"
operator BITVECTOR_PLUS 2 "bit-vector addition"
operator BITVECTOR_SUB 2 "bit-vector subtraction"
operator BITVECTOR_NEG 1 "bit-vector unary negation"
-operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
-operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"
+operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)"
+operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)"
operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right"
-
+
parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract"
parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat"
parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend"
theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
-variable SORT_TYPE "sort type"
+
+variable SORT_TAG "sort tag"
+parameterized SORT_TYPE SORT_TAG 0: "sort type"
** \todo document this file
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__HASH_H
#define __CVC4__HASH_H
projects / cvc5.git / commitdiff