From 8cf21dc2426b8be12915b8dfd59784fff87a5e14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Oct 2014 13:47:55 -0700 Subject: [PATCH] fix tactic parameter checking to API, deal with compiler warnings in api_interp Signed-off-by: Nikolaj Bjorner --- src/api/api_interp.cpp | 26 ++++++++++++++++---------- src/api/api_tactic.cpp | 3 +++ src/api/python/z3.py | 2 +- src/tactic/tactical.cpp | 3 --- src/util/params.cpp | 3 ++- 5 files changed, 22 insertions(+), 15 deletions(-) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 8740e99a5..0bfb2d077 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -145,11 +145,11 @@ extern "C" { Z3_push(ctx); // so we can rewind later - for (int i = 0; i < num; i++) + for (unsigned i = 0; i < num; i++) Z3_assert_cnstr(ctx, cnsts[i]); // assert all the constraints if (theory){ - for (int i = 0; i < num_theory; i++) + for (unsigned i = 0; i < num_theory; i++) Z3_assert_cnstr(ctx, theory[i]); } @@ -180,7 +180,7 @@ extern "C" { theory); if (!incremental) - for (int i = 0; i < num - 1; i++) + for (unsigned i = 0; i < num - 1; i++) Z3_persist_ast(ctx, interps[i], 1); break; @@ -226,13 +226,13 @@ extern "C" { scoped_ptr sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA"))); ptr_vector cnsts_vec(num); // get constraints in a vector - for (int i = 0; i < num; i++){ + for (unsigned i = 0; i < num; i++){ ast *a = to_ast(cnsts[i]); cnsts_vec[i] = a; } ptr_vector itp_vec(num); // get interpolants in a vector - for (int i = 0; i < num - 1; i++){ + for (unsigned i = 0; i < num - 1; i++){ ast *a = to_ast(itp[i]); itp_vec[i] = a; } @@ -240,14 +240,14 @@ extern "C" { ::vector parents_vec; // get parents in a vector if (parents){ parents_vec.resize(num); - for (int i = 0; i < num; i++) + for (unsigned i = 0; i < num; i++) parents_vec[i] = parents[i]; } ptr_vector theory_vec; // get background theory in a vector if (theory){ theory_vec.resize(num_theory); - for (int i = 0; i < num_theory; i++) + for (unsigned i = 0; i < num_theory; i++) theory_vec[i] = to_ast(theory[i]); } @@ -506,16 +506,22 @@ extern "C" { void Z3_write_interpolation_problem(Z3_context ctx, unsigned num, Z3_ast *cnsts, unsigned *parents, const char *filename, unsigned num_theory, Z3_ast *theory){ std::ofstream f(filename); if (num > 0){ +#if 0 + // Suggested shorthand: + ptr_vector cnsts_vec; + cnsts_vec.append(num, to_exprs(cnsts)); + cnsts_vec.append(num_theory, to_exprs(theory)); +#endif ptr_vector cnsts_vec(num); // get constraints in a vector - for (int i = 0; i < num; i++){ + for (unsigned i = 0; i < num; i++){ expr *a = to_expr(cnsts[i]); cnsts_vec[i] = a; } - Z3_ast tree = parents_vector_to_tree(ctx, num, cnsts, parents); - for (int i = 0; i < num_theory; i++){ + for (unsigned i = 0; i < num_theory; i++){ expr *a = to_expr(theory[i]); cnsts_vec.push_back(a); } + Z3_ast tree = parents_vector_to_tree(ctx, num, cnsts, parents); iz3pp(mk_c(ctx)->m(), cnsts_vec, to_expr(tree), f); Z3_dec_ref(ctx, tree); } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 911360047..7dce33971 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -222,6 +222,9 @@ extern "C" { Z3_TRY; LOG_Z3_tactic_using_params(c, t, p); RESET_ERROR_CODE(); + param_descrs r; + to_tactic_ref(t)->collect_param_descrs(r); + to_param_ref(p).validate(r); tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p)); RETURN_TACTIC(new_t); Z3_CATCH_RETURN(0); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 1a5565ab5..82ba85472 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4448,7 +4448,7 @@ def args2params(arguments, keywords, ctx=None): A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) - (params model 1 relevancy 2 elim_and 1) + (params model true relevancy 2 elim_and true) """ if __debug__: _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 168965c17..cfb4ec194 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -1229,9 +1229,6 @@ class using_params_tactical : public unary_tactical { params_ref m_params; public: using_params_tactical(tactic * t, params_ref const & p):unary_tactical(t), m_params(p) { - //param_descrs r; - //collect_param_descrs(r); - //p.validate(r); t->updt_params(p); } diff --git a/src/util/params.cpp b/src/util/params.cpp index 130b18cc9..a2609f840 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -309,7 +309,8 @@ public: p.display(strm, 2, false, false); throw default_exception(strm.str()); } - if (it->second.m_kind != expected) { + if (it->second.m_kind != expected && + !(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { std::stringstream strm; strm << "Parameter " << it->first.str() << " was given argument of type "; strm << it->second.m_kind << ", expected " << expected;