mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

port Jakob's update to union_find from polysat branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-18 09:25:24 -08:00
parent 2f2bf749b9
commit 085b5e2588
4 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/array_solver.h
View file

@ -32,7 +32,7 @@ namespace array {
typedef sat::literal literal;
typedef sat::bool_var bool_var;
typedef sat::literal_vector literal_vector;
typedef union_find<solver, euf::solver> array_union_find;
typedef union_find<solver> array_union_find;
struct stats {

2
src/sat/smt/bv_solver.h
View file

@ -49,7 +49,7 @@ namespace bv {
typedef std::pair<numeral, unsigned> value_sort_pair;
typedef pair_hash<obj_hash<numeral>, unsigned_hash> value_sort_pair_hash;
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
typedef union_find<solver, euf::solver> bv_union_find;
typedef union_find<solver> bv_union_find;
typedef std::pair<theory_var, unsigned> var_pos;
friend class ackerman;

2
src/sat/smt/dt_solver.h
View file

@ -36,7 +36,7 @@ namespace dt {
typedef sat::bool_var bool_var;
typedef sat::literal literal;
typedef sat::literal_vector literal_vector;
typedef union_find<solver, euf::solver> dt_union_find;
typedef union_find<solver> dt_union_find;
struct var_data {
ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched.

2
src/util/union_find.h
View file

@ -35,7 +35,7 @@ private:
_trail_stack m_stack;
};
template<typename Ctx = union_find_default_ctx, typename StackCtx = Ctx>
template<typename Ctx = union_find_default_ctx>
class union_find {
Ctx & m_ctx;
trail_stack & m_trail_stack;