mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix clang warnings

Browse source
This commit is contained in:
Nuno Lopes 2021-02-19 10:59:22 +00:00
parent 5e034e495f
commit d6ce9cce95
6 changed files with 6 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
azure-pipelines.yml
View file

@ -214,7 +214,7 @@ jobs:
- job: "MacOSPython"
displayName: "MacOS build"
pool:
vmImage: "macOS-10.14"
vmImage: "macOS-latest"
steps:
- script: python scripts/mk_make.py -d --java --dotnet
- script: |
@ -244,7 +244,7 @@ jobs:
set -e
mkdir build
cd build
CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir $(cmakeJulia) $(cmakeJava) $(cmakePy) -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
cmake -DJlCxx_DIR=$JlCxxDir $(cmakeJulia) $(cmakeJava) $(cmakePy) -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
ninja
ninja test-z3
cd ..

5
src/model/char_factory.h
View file

@ -20,9 +20,8 @@ Revision History:
#include "model/model_core.h"
#include "model/value_factory.h"
class char_factory : public value_factory {
class char_factory final : public value_factory {
model_core& m_model;
ast_manager& m;
seq_util u;
uint_set m_chars;
unsigned m_next { 'A' };
@ -33,7 +32,6 @@ public:
char_factory(ast_manager & m, family_id fid, model_core& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_trail(m)
{
@ -76,4 +74,3 @@ public:
}
};

3
src/model/seq_factory.h
View file

@ -19,7 +19,6 @@ Author:
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
model_core& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
unsigned m_next;
@ -31,7 +30,6 @@ public:
seq_factory(ast_manager & m, family_id fid, model_core& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
m_unique_delim("!"),
@ -151,4 +149,3 @@ private:
goto try_again;
}
};

3
src/muz/rel/dl_compiler.cpp
View file

@ -868,7 +868,6 @@ namespace datalog {
bool & dealloc, instruction_block & acc) {
uint_set pos_vars;
u_map<expr*> neg_vars;
ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size();
@ -903,7 +902,7 @@ namespace datalog {
if (!pos_vars.contains(v)) {
single_res_expr.push_back(e);
make_add_unbound_column(r, v, pred, single_res, e->get_sort(), single_res, dealloc, acc);
TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m_context.get_manager()) << "\n";);
}
}
}

1
src/smt/theory_char.h
View file

@ -38,7 +38,6 @@ namespace smt {
vector<expr_ref_vector> m_ebits;
unsigned_vector m_var2value;
svector<theory_var> m_value2var;
bool m_enabled { false };
bit_blaster m_bb;
stats m_stats;
symbol m_bits2char;

6
src/tactic/core/symmetry_reduce_tactic.cpp
View file

@ -248,14 +248,12 @@ private:
}
class sort_colors {
ast_manager& m_manager;
app_map& m_app2sortid;
obj_map<sort,unsigned> m_sort2id;
unsigned m_max_id;
public:
sort_colors(ast_manager& m, app_map& app2sort):
m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
sort_colors(app_map& app2sort) : m_app2sortid(app2sort), m_max_id(0) {}
void operator()(app* n) {
sort* s = n->get_sort();
@ -273,7 +271,7 @@ private:
void compute_sort_colors(expr* fml, app_map& app2sortId) {
app2sortId.reset();
sort_colors sc(m(), app2sortId);
sort_colors sc(app2sortId);
for_each_expr(sc, fml);
}