mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-02 19:26:48 -07:00
parent 6fb4e0d5a9
commit 7b845c7138
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict.cpp
View file

@ -191,7 +191,7 @@ namespace polysat {
SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c){ return !c->has_bvar(); }));
SASSERT(contains_literal(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains_literal(~lit));
@ -219,7 +219,7 @@ namespace polysat {
clause_builder conflict::build_lemma() {
SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c) { return !c->has_bvar(); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](signed_constraint const& c) { return !c->has_bvar(); }));
LOG_H3("Build lemma from core");
LOG("core: " << *this);

4
src/math/polysat/fixplex_def.h
View file

@ -1335,7 +1335,7 @@ namespace polysat {
template<typename Ext>
bool fixplex<Ext>::propagate_strict_bounds(ineq const& i) {
var_t v = i.v, w = i.w;
bool s = i.strict;
//bool s = i.strict;
auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;
@ -1363,7 +1363,7 @@ namespace polysat {
template<typename Ext>
bool fixplex<Ext>::propagate_non_strict_bounds(ineq const& i) {
var_t v = i.v, w = i.w;
bool s = i.strict;
// bool s = i.strict;
auto* vlo = m_vars[v].m_lo_dep, *vhi = m_vars[v].m_hi_dep;
auto* wlo = m_vars[w].m_lo_dep, *whi = m_vars[w].m_hi_dep;

6
src/test/fixplex.cpp
View file

@ -389,7 +389,7 @@ namespace polysat {
std::cout << " test_lp(rows, ineqs, bounds); \n }\n";
}
static unsigned num_test = 0;
// static unsigned num_test = 0;
static void test_lp(
vector<svector<std::pair<unsigned, uint64_t>>> const& rows,
@ -566,9 +566,9 @@ namespace polysat {
static void test_lps() {
random_gen r;
for (unsigned i = 0; i < 10000; ++i)
for (unsigned i = 0; i < 10000; ++i)
test_lps(r, 6, 3, 3, 3);
return;
return;
for (unsigned i = 0; i < 10000; ++i)
test_lps(r, 6, 3, 3, 0);
return;