mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

switch expr_safe_replace to std::unordered_map (#5003)

Browse source 
* switch expr_safe_replace to std::unordered_map

* further tweaks to expr_safe_replace for an overall speedup of 1.x in Z3_substitute
This commit is contained in:
Nuno Lopes 2021-02-08 02:20:48 +00:00 • committed by GitHub
parent 615cafe39b
commit 52e67b0d3e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 25 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/rewriter/expr_safe_replace.h
View file

@ -22,18 +22,15 @@ Revision History:
#pragma once
#include "ast/ast.h"
#include <unordered_map>
class expr_safe_replace {
ast_manager& m;
expr_ref_vector m_src;
expr_ref_vector m_dst;
obj_map<expr, expr*> m_subst;
ptr_vector<expr> m_todo, m_args;
expr_ref_vector m_refs;
obj_map<expr,expr*> m_cache;
void cache_insert(expr* a, expr* b);
expr* cache_find(expr* a);
std::unordered_map<expr*,expr*> m_cache;
public:
expr_safe_replace(ast_manager& m): m(m), m_src(m), m_dst(m), m_refs(m) {}
@ -50,6 +47,6 @@ public:
void reset();
bool empty() const { return m_subst.empty(); }
bool empty() const { return m_src.empty(); }
};