Skip to content

Commit

Permalink
Rename 'user' to 'user_solver Z3Prover#5586
Browse files Browse the repository at this point in the history
Issue Z3Prover#5586 reported that Android builds (targetting, e.g., x86) failed
to compile due to a conflict between:

* `struct user` in `sys/user.h`; and
* `namespace user` in z3's `user_solver.h`

This issue is resolved by renaming `namespace user` to `namespace
user_solver` (matching the header name) to avoid this conflict.

Reported-by: Jamie Collinson <jamiecollinson@gmail.com>

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
  • Loading branch information
aytey committed Oct 9, 2021
1 parent bfa960c commit f0ab25d
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion src/sat/smt/euf_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -994,7 +994,7 @@ namespace euf {
::solver::push_eh_t& push_eh,
::solver::pop_eh_t& pop_eh,
::solver::fresh_eh_t& fresh_eh) {
m_user_propagator = alloc(user::solver, *this);
m_user_propagator = alloc(user_solver::solver, *this);
m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
for (unsigned i = m_scopes.size(); i-- > 0; )
m_user_propagator->push();
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/euf_solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ namespace euf {
sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman;
scoped_ptr<sat::dual_solver> m_dual_solver;
user::solver* m_user_propagator = nullptr;
user_solver::solver* m_user_propagator = nullptr;
th_solver* m_qsolver = nullptr;
unsigned m_generation = 0;
mutable ptr_vector<expr> m_todo;
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/user_solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ Module Name:
#include "sat/smt/user_solver.h"
#include "sat/smt/euf_solver.h"

namespace user {
namespace user_solver {

solver::solver(euf::solver& ctx) :
th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))
Expand Down
2 changes: 1 addition & 1 deletion src/sat/smt/user_solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Module Name:
#include "solver/solver.h"


namespace user {
namespace user_solver {

class solver : public euf::th_euf_solver, public ::solver::propagate_callback {

Expand Down

0 comments on commit f0ab25d

Please sign in to comment.