diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 0004aaa42..56a89d346 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -542,22 +542,6 @@ inline unsigned ast_array_hash(T * const * array, unsigned size, unsigned init_v } } } -unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} -unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init) { - return ast_array_hash(ns, sz, init); -} - unsigned get_node_hash(ast const * n) { unsigned a, b, c; diff --git a/src/ast/ast.h b/src/ast/ast.h index d7a715cd1..b4b3b1b2f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -970,11 +970,6 @@ inline quantifier const * to_quantifier(ast const * n) { SASSERT(is_quantifier(n unsigned get_node_hash(ast const * n); bool compare_nodes(ast const * n1, ast const * n2); unsigned get_node_size(ast const * n); -unsigned get_asts_hash(unsigned sz, ast * const* ns, unsigned init); -unsigned get_apps_hash(unsigned sz, app * const* ns, unsigned init); -unsigned get_exprs_hash(unsigned sz, expr * const* ns, unsigned init); -unsigned get_sorts_hash(unsigned sz, sort * const* ns, unsigned init); -unsigned get_decl_hash(unsigned sz, func_decl* const* ns, unsigned init); // This is the internal comparison functor for hash-consing AST nodes. struct ast_eq_proc {