fix tactic parameter checking to API, deal with compiler warnings in api_interp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<solver> sp((*(sf))(_m, p, false, true, false, symbol("AUFLIA")));
 
         ptr_vector<ast> 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<ast> 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<int> 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<ast> 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<expr> cnsts_vec;
+            cnsts_vec.append(num, to_exprs(cnsts));
+            cnsts_vec.append(num_theory, to_exprs(theory));
+#endif
             ptr_vector<expr> 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);
         }

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);

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.")

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);
     }
 

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;