mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

propagate_ineqs synchronization fix

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 13:25:40 +00:00
parent a78dd680fb
commit 73cebc24c8
3 changed files with 4 additions and 4 deletions
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: public:
typedef unsigned var; typedef unsigned var;
typedef unsigned assumption; typedef unsigned assumption;
typedef unsynch_mpq_manager numeral_manager; typedef synch_mpq_manager numeral_manager;
typedef unsigned_vector assumption_vector; typedef unsigned_vector assumption_vector;
typedef unsigned constraint_id; typedef unsigned constraint_id;
typedef numeral_buffer<mpz, numeral_manager> mpz_buffer; 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 { class linear_equation_manager {
public: public:
typedef unsynch_mpq_manager numeral_manager; typedef synch_mpq_manager numeral_manager;
typedef linear_equation::var var; typedef linear_equation::var var;
typedef numeral_buffer<mpz, numeral_manager> mpz_buffer; typedef numeral_buffer<mpz, numeral_manager> mpz_buffer;
private: 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 { struct propagate_ineqs_tactic::imp {
ast_manager & m; ast_manager & m;
unsynch_mpq_manager nm; synch_mpq_manager nm;
small_object_allocator m_allocator; small_object_allocator m_allocator;
bound_propagator bp; bound_propagator bp;
arith_util m_util; arith_util m_util;
@ -73,7 +73,7 @@ struct propagate_ineqs_tactic::imp {
obj_map<expr, a_var> m_expr2var; obj_map<expr, a_var> m_expr2var;
expr_ref_vector m_var2expr; expr_ref_vector m_var2expr;
typedef numeral_buffer<mpq, unsynch_mpq_manager> mpq_buffer; typedef numeral_buffer<mpq, synch_mpq_manager> mpq_buffer;
typedef svector<a_var> var_buffer; typedef svector<a_var> var_buffer;
mpq_buffer m_num_buffer; mpq_buffer m_num_buffer;