Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/api_solver.cpp

@@ -40,6 +40,11 @@ extern "C" {
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
+        
+        param_descrs r;
+        s->m_solver->collect_param_descrs(r);
+        context_params::collect_solver_param_descrs(r);
+        p.validate(r);
         s->m_solver->updt_params(p);
     }
 
@@ -102,6 +107,7 @@ extern "C" {
         if (!initialized)
             init_solver(c, s);
         to_solver_ref(s)->collect_param_descrs(descrs);
+        context_params::collect_solver_param_descrs(descrs);
         if (!initialized)
             to_solver(s)->m_solver = 0;
         descrs.display(buffer);
@@ -119,6 +125,7 @@ extern "C" {
         if (!initialized)
             init_solver(c, s);
         to_solver_ref(s)->collect_param_descrs(d->m_descrs);
+        context_params::collect_solver_param_descrs(d->m_descrs);
         if (!initialized)
             to_solver(s)->m_solver = 0;
         Z3_param_descrs r = of_param_descrs(d);
@@ -130,11 +137,16 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_set_params(c, s, p);
         RESET_ERROR_CODE();
+
         if (to_solver(s)->m_solver) {
             bool old_model = to_solver(s)->m_params.get_bool("model", true);
             bool new_model = to_param_ref(p).get_bool("model", true);
             if (old_model != new_model)
                 to_solver_ref(s)->set_produce_models(new_model);
+            param_descrs r;
+            to_solver_ref(s)->collect_param_descrs(r);
+            context_params::collect_solver_param_descrs(r);
+            to_param_ref(p).validate(r);
             to_solver_ref(s)->updt_params(to_param_ref(p));
         }
         to_solver(s)->m_params = to_param_ref(p);

src/api/api_tactic.cpp

@@ -450,6 +450,9 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_tactic_apply_ex(c, t, g, p);
         RESET_ERROR_CODE();
+        param_descrs pd;
+        to_tactic_ref(t)->collect_param_descrs(pd);
+        to_param_ref(p).validate(pd);
         Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
         RETURN_Z3(r);
         Z3_CATCH_RETURN(0);

src/api/dotnet/Params.cs

@@ -58,6 +58,16 @@ namespace Microsoft.Z3
             Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
         }
 
+        /// <summary>
+        /// Adds a parameter setting.
+        /// </summary>
+        public void Add(Symbol name, string value)
+        {
+            Contract.Requires(value != null);
+
+            Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
+        }
+
         /// <summary>
         /// Adds a parameter setting.
         /// </summary>
@@ -103,6 +113,16 @@ namespace Microsoft.Z3
             Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
         }
 
+        /// <summary>
+        /// Adds a parameter setting.
+        /// </summary>
+        public void Add(string name, string value)
+        {
+            Contract.Requires(value != null);
+
+            Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
+        }
+
         /// <summary>
         /// A string representation of the parameter set.
         /// </summary>

src/api/java/Params.java

@@ -29,6 +29,17 @@ public class Params extends Z3Object
                 name.getNativeObject(), value);
     }
     
+    /**
+     * Adds a parameter setting.
+     **/
+    public void add(Symbol name, String value) throws Z3Exception
+    {
+
+        Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
+                name.getNativeObject(), 
+                getContext().mkSymbol(value).getNativeObject());
+    }
+
     /**
      * Adds a parameter setting.
      **/
@@ -75,6 +86,17 @@ public class Params extends Z3Object
                 .mkSymbol(name).getNativeObject(), value.getNativeObject());
     }
 
+    /**
+     * Adds a parameter setting.
+     **/
+    public void add(String name, String value) throws Z3Exception
+    {
+
+        Native.paramsSetSymbol(getContext().nCtx(), getNativeObject(),
+                getContext().mkSymbol(name).getNativeObject(),
+                getContext().mkSymbol(value).getNativeObject());
+    }
+    
     /**
      * A string representation of the parameter set.
      **/

src/cmd_context/context_params.cpp

@@ -114,15 +114,19 @@ void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("well_sorted_check", CPK_BOOL, "type checker", "true");
     d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
     d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
-    d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
     d.insert("check_interpolants", CPK_BOOL, "check correctness of interpolants", "false");
-    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
     d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
     d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
     d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
-    d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
     d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
     d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
+    collect_solver_param_descrs(d);
+}
+
+void context_params::collect_solver_param_descrs(param_descrs & d) {
+    d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
+    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
+    d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
 }
 
 params_ref context_params::merge_default_params(params_ref const & p) {

src/cmd_context/context_params.h

@@ -55,6 +55,8 @@ public:
     */
     void get_solver_params(ast_manager const & m, params_ref & p, bool & proofs_enabled, bool & models_enabled, bool & unsat_core_enabled);
 
+    static void collect_solver_param_descrs(param_descrs & d);
+
     /**
        \brief Include in p parameters derived from this context_params.
        These are parameters that are meaningful for tactics and solvers.

src/muz/pdr/pdr_context.cpp

@@ -1274,7 +1274,7 @@ namespace pdr {
           m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
-          m_search(m_params.bfs_model_search(), m),
+          m_search(m_params.bfs_model_search()),
           m_last_result(l_undef),
           m_inductive_lvl(0),
           m_expanded_lvl(0),

src/muz/pdr/pdr_context.h

@@ -245,7 +245,6 @@ namespace pdr {
 
     class model_search {
         typedef ptr_vector<model_node> model_nodes;
-        ast_manager&       m;
         bool               m_bfs;
         model_node*        m_root;
         std::deque<model_node*> m_leaves;
@@ -258,7 +257,7 @@ namespace pdr {
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
         void update_models();
     public:
-        model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
         ~model_search();
 
         void reset();