mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

removing pragmas to make travis happy

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 22:28:41 -04:00
parent c506f3ddc9
commit 66108085fa
3 changed files with 2 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -260,7 +260,6 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
else { m_ctx->assert_expr(bg[i]); }
unsigned soft_sz = soft.size();
#pragma unused(soft_sz)
lbool res = internal_check_assumptions(hard, soft);
if (!m_use_push_bg) { m_ctx->pop(1); }

4
src/muz/spacer/spacer_unsat_core_learner.cpp
View file

@ -25,9 +25,7 @@ Revision History:
namespace spacer
{
#pragma mark - proof iterators
# pragma mark - main methods
unsat_core_learner::~unsat_core_learner()
{
std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<unsat_core_plugin>());
@ -262,7 +260,6 @@ void unsat_core_learner::finalize()
}
}
#pragma mark - API
bool unsat_core_learner::is_a_marked(proof* p)
{
@ -290,7 +287,6 @@ void unsat_core_learner::set_closed(proof* p, bool value)
m_unsat_core.push_back(lemma);
}
# pragma mark - checking for b_symbols
class collect_pure_proc {
func_decl_set& m_symbs;

9
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -32,7 +32,6 @@ Revision History:
namespace spacer
{
#pragma mark - unsat_core_plugin_lemma
void unsat_core_plugin_lemma::compute_partial_core(proof* step)
{
@ -105,7 +104,6 @@ void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const
}
#pragma mark - unsat_core_plugin_farkas_lemma
void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step)
{
ast_manager &m = m_learner.m;
@ -285,7 +283,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
}
}
#pragma mark - unsat_core_plugin_farkas_optimized
void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step)
{
SASSERT(m_learner.is_a_marked(step));
@ -444,7 +441,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
res = mk_not(m, negated_linear_combination); //TODO: rewrite the get-method to return nonnegated stuff?
}
#pragma mark - unsat_core_plugin_farkas_bounded
void unsat_core_plugin_farkas_lemma_bounded::finalize()
{
@ -557,7 +553,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
app_ref sum(m);
sum = util.mk_int(0);
for (int k=0; k < n; ++k)
for (unsigned k=0; k < n; ++k)
{
sum = util.mk_add(sum, util.mk_mul(coeffs[i][k].get(), bounded_vectors[j][k].get()));
}
@ -579,7 +575,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
{
ptr_vector<app> literals;
vector<rational> coefficients;
for (int j=0; j < matrix.num_cols(); ++j)
for (unsigned j=0; j < matrix.num_cols(); ++j)
{
expr_ref evaluation(m);
@ -601,7 +597,6 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
}
}
#pragma mark - unsat_core_plugin_min_cut
unsat_core_plugin_min_cut::unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner), m(m){}
void unsat_core_plugin_min_cut::compute_partial_core(proof* step)