mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

Revert "propagate_ineqs synchronization fix"

Browse source 
This reverts commit 73cebc24c8.
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 15:16:24 +00:00
parent 73cebc24c8
commit 72345026be
3 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/arith/bound_propagator.h
View file

@ -31,7 +31,7 @@ class bound_propagator {
public:
typedef unsigned var;
typedef unsigned assumption;
typedef synch_mpq_manager numeral_manager;
typedef unsynch_mpq_manager numeral_manager;
typedef unsigned_vector assumption_vector;
typedef unsigned constraint_id;
typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;

2
src/tactic/arith/linear_equation.h
View file

@ -52,7 +52,7 @@ public:
class linear_equation_manager {
public:
typedef synch_mpq_manager numeral_manager;
typedef unsynch_mpq_manager numeral_manager;
typedef linear_equation::var var;
typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;
private:

4
src/tactic/arith/propagate_ineqs_tactic.cpp
View file

@ -65,7 +65,7 @@ tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) {
struct propagate_ineqs_tactic::imp {
ast_manager & m;
synch_mpq_manager nm;
unsynch_mpq_manager nm;
small_object_allocator m_allocator;
bound_propagator bp;
arith_util m_util;
@ -73,7 +73,7 @@ struct propagate_ineqs_tactic::imp {
obj_map<expr, a_var> m_expr2var;
expr_ref_vector m_var2expr;
typedef numeral_buffer<mpq, synch_mpq_manager> mpq_buffer;
typedef numeral_buffer<mpq, unsynch_mpq_manager> mpq_buffer;
typedef svector<a_var> var_buffer;
mpq_buffer m_num_buffer;