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

Remove debug function

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-17 13:22:22 -07:00
parent ac3bbed311
commit 3f9b5bce99
2 changed files with 9 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/muz/spacer/spacer_context.cpp
View file

@ -1001,6 +1001,14 @@ void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref&
}
}
static bool is_all_non_null(app_ref_vector const& v)
{
for (unsigned i = 0; i < v.size(); ++i) {
if (!v[i]) { return false; }
}
return true;
}
void pred_transformer::init_rule(
decl2rel const& pts,
datalog::rule const& rule,
@ -1035,7 +1043,7 @@ void pred_transformer::init_rule(
fml = mk_and (tail);
ground_free_vars (fml, var_reprs, aux_vars, ut_size == 0);
SASSERT(check_filled(var_reprs));
SASSERT(is_all_non_null(var_reprs));
expr_ref tmp(m);
var_subst (m, false)(fml,
@ -1074,13 +1082,6 @@ void pred_transformer::init_rule(
tout << "\n";);
}
bool pred_transformer::check_filled(app_ref_vector const& v) const
{
for (unsigned i = 0; i < v.size(); ++i) {
if (!v[i]) { return false; }
}
return true;
}
// create constants for free variables in tail.
void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars,

2
src/muz/spacer/spacer_context.h
View file

@ -320,8 +320,6 @@ class pred_transformer {
void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
// Debugging
bool check_filled(app_ref_vector const& v) const;
void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r);
expr* mk_fresh_reach_case_var ();