michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add expression offset pair

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-23 10:16:47 -07:00
parent 6a2c9ef076
commit 17e69e32d7
2 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/kernel/expr.h
View file

@ -7,9 +7,10 @@ Author: Leonardo de Moura
#pragma once
#include <iostream>
#include <limits>
#include "name.h"
#include "rc.h"
#include "name.h"
#include "mpz.h"
#include "hash.h"
namespace lean {
/* =======================================
@ -309,12 +310,22 @@ inline mpz const & get_numeral(expr const & e) { return to_numeral
inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b); }
// =======================================
// =======================================
// Expression+Offset
typedef std::pair<expr, unsigned> expr_offset;
typedef std::pair<expr_cell*, unsigned> expr_cell_offset;
// =======================================
// =======================================
// Auxiliary functors
struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } };
struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { return eqp(e1, e2); } };
struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; } };
struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return eqp(p1.first, p2.first) && p1.second == p2.second; } };
struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };
// =======================================
// =======================================

4
src/kernel/sets.h
View file

@ -12,9 +12,10 @@ Author: Leonardo de Moura
namespace lean {
// =======================================
// Expression Set
// Expression Set && Expression Offset Set
// Remark: to expressions are assumed to be equal if they are "pointer-equal"
typedef std::unordered_set<expr, expr_hash, expr_eqp> expr_set;
typedef std::unordered_set<expr_offset, expr_offset_hash, expr_offset_eqp> expr_offset_set;
// =======================================
// =======================================
@ -25,6 +26,7 @@ typedef std::unordered_set<expr, expr_hash, expr_eqp> expr_set;
// does not prevent an expression from being
// garbage collected.
typedef std::unordered_set<expr_cell*, expr_cell_hash, expr_cell_eqp> expr_cell_set;
typedef std::unordered_set<expr_cell_offset, expr_cell_offset_hash, expr_cell_offset_eqp> expr_cell_offset_set;
// =======================================
// =======================================