From d6ce9cce956acaa0200cf4e3985b164c8d693da1 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 19 Feb 2021 10:59:22 +0000
Subject: [PATCH] fix clang warnings
---
azure-pipelines.yml | 4 ++--
src/model/char_factory.h | 5 +----
src/model/seq_factory.h | 3 ---
src/muz/rel/dl_compiler.cpp | 3 +--
src/smt/theory_char.h | 1 -
src/tactic/core/symmetry_reduce_tactic.cpp | 6 ++----
6 files changed, 6 insertions(+), 16 deletions(-)
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 3c2173a76..1735f2337 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -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 ..
diff --git a/src/model/char_factory.h b/src/model/char_factory.h
index 0e99ecd79..55baad26d 100644
--- a/src/model/char_factory.h
+++ b/src/model/char_factory.h
@@ -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:
}
};
-
diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h
index ce395cef5..d40a7f7bd 100644
--- a/src/model/seq_factory.h
+++ b/src/model/seq_factory.h
@@ -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;
}
};
-
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 589540b6f..dea02d533 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -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";);
}
}
}
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index 146d522e4..cd37732b8 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -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;
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index aa19428d6..6f215e922 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -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);
}