mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
deal with compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
eef2ac0ff5
commit
2a6fa4af39
|
@ -63,7 +63,7 @@ Revision History:
|
|||
|
||||
|
||||
--*/
|
||||
#pragma once;
|
||||
#pragma once
|
||||
#include "ast/ast.h"
|
||||
|
||||
enum js_sort_kind {
|
||||
|
|
|
@ -1060,9 +1060,9 @@ namespace sat {
|
|||
uint64_t ba_solver::get_coeff(literal lit) const {
|
||||
int64_t c1 = get_coeff(lit.var());
|
||||
SASSERT(c1 < 0 == lit.sign());
|
||||
uint64_t c = static_cast<uint64_t>(std::abs(c1));
|
||||
m_overflow |= c != c1;
|
||||
return c;
|
||||
int64_t c = std::abs(c1);
|
||||
m_overflow |= (c != c1);
|
||||
return static_cast<uint64_t>(c);
|
||||
}
|
||||
|
||||
ba_solver::wliteral ba_solver::get_wliteral(bool_var v) {
|
||||
|
@ -1630,7 +1630,7 @@ namespace sat {
|
|||
mark_visited(v);
|
||||
if (s().is_marked(v)) {
|
||||
int64_t c = get_coeff(v);
|
||||
if (c == 0 || (c < 0 == consequent.sign())) {
|
||||
if (c == 0 || ((c < 0) == consequent.sign())) {
|
||||
s().reset_mark(v);
|
||||
--m_num_marks;
|
||||
}
|
||||
|
@ -3538,7 +3538,7 @@ namespace sat {
|
|||
}
|
||||
++m_stats.m_num_big_strengthenings;
|
||||
p.set_removed();
|
||||
constraint* c = add_pb_ge(null_literal, wlits, b, p.learned());
|
||||
add_pb_ge(null_literal, wlits, b, p.learned());
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -178,21 +178,21 @@ unsigned read_dimacs(char const * file_name) {
|
|||
std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
|
||||
exit(ERR_OPEN_FILE);
|
||||
}
|
||||
parse_dimacs(in, *g_solver);
|
||||
parse_dimacs(in, solver);
|
||||
}
|
||||
else {
|
||||
parse_dimacs(std::cin, *g_solver);
|
||||
parse_dimacs(std::cin, solver);
|
||||
}
|
||||
IF_VERBOSE(20, g_solver->display_status(verbose_stream()););
|
||||
IF_VERBOSE(20, solver.display_status(verbose_stream()););
|
||||
|
||||
lbool r;
|
||||
vector<sat::literal_vector> tracking_clauses;
|
||||
sat::solver solver2( p, limit);
|
||||
if (p.get_bool("dimacs.core", false)) {
|
||||
sat::solver solver2(p, limit);
|
||||
if (p.get_bool("dimacs.core", false)) {
|
||||
g_solver = &solver2;
|
||||
sat::literal_vector assumptions;
|
||||
track_clauses(solver, solver2, assumptions, tracking_clauses);
|
||||
g_solver = &solver2;
|
||||
r = solver2.check(assumptions.size(), assumptions.c_ptr());
|
||||
r = g_solver->check(assumptions.size(), assumptions.c_ptr());
|
||||
}
|
||||
else {
|
||||
r = g_solver->check();
|
||||
|
|
|
@ -4455,7 +4455,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
recfun::util u(m);
|
||||
recfun::decl::plugin& p = u.get_plugin();
|
||||
func_decl_ref_vector recfuns = u.get_rec_funs();
|
||||
for (func_decl* f : recfuns) {
|
||||
auto& def = u.get_def(f);
|
||||
|
@ -4464,7 +4463,6 @@ namespace smt {
|
|||
func_interp* fi = alloc(func_interp, m, f->get_arity());
|
||||
// reverse argument order so that variable 0 starts at the beginning.
|
||||
expr_ref_vector subst(m);
|
||||
unsigned idx = 0;
|
||||
for (unsigned i = 0; i < f->get_arity(); ++i) {
|
||||
subst.push_back(m.mk_var(i, f->get_domain(i)));
|
||||
}
|
||||
|
|
|
@ -130,7 +130,6 @@ namespace smt {
|
|||
|
||||
void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) {
|
||||
enode* e1 = get_enode(v1);
|
||||
enode* e2 = get_enode(v2);
|
||||
enode* root = e1->get_root();
|
||||
unsigned r;
|
||||
if (u.is_resource(root->get_owner(), r)) {
|
||||
|
@ -712,7 +711,7 @@ namespace smt {
|
|||
|
||||
time_t start_lb = std::numeric_limits<time_t>::max();
|
||||
time_t runtime_lb = std::numeric_limits<time_t>::max();
|
||||
time_t end_ub = 0, runtime_ub = 0;
|
||||
time_t end_ub = 0; // , runtime_ub = 0;
|
||||
for (job_resource const& jr : ji.m_resources) {
|
||||
unsigned r = jr.m_resource_id;
|
||||
res_info const& ri = m_resources[r];
|
||||
|
@ -784,6 +783,7 @@ namespace smt {
|
|||
// resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j);
|
||||
void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) {
|
||||
job_resource const& jr = get_job_resource(j, r);
|
||||
(void) jr;
|
||||
vector<res_available>& available = m_resources[r].m_available;
|
||||
SASSERT(resource_available(jr, available[idx]));
|
||||
literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
|
||||
|
@ -795,6 +795,7 @@ namespace smt {
|
|||
void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) {
|
||||
vector<res_available>& available = m_resources[r].m_available;
|
||||
job_resource const& jr = get_job_resource(j, r);
|
||||
(void) jr;
|
||||
SASSERT(resource_available(jr, available[idx]));
|
||||
literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end);
|
||||
literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start);
|
||||
|
|
|
@ -18,7 +18,7 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#pragma once;
|
||||
#pragma once
|
||||
|
||||
#include "util/uint_set.h"
|
||||
#include "ast/csp_decl_plugin.h"
|
||||
|
|
Loading…
Reference in a new issue