From 0e4e72b1bc70adcd1f05268bfcbce87a33e010af Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 14 Oct 2014 13:22:12 +0100 Subject: [PATCH 1/5] Added new params.Add functions to the .NET and Java APIs. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Params.cs | 20 ++++++++++++++++++++ src/api/java/Params.java | 22 ++++++++++++++++++++++ 2 files changed, 42 insertions(+) diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index 56a7a891f..c33728491 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -58,6 +58,16 @@ namespace Microsoft.Z3 Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value); } + /// + /// Adds a parameter setting. + /// + 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); + } + /// /// Adds a parameter setting. /// @@ -103,6 +113,16 @@ namespace Microsoft.Z3 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject); } + /// + /// Adds a parameter setting. + /// + 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); + } + /// /// A string representation of the parameter set. /// diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 68af4386b..cf3d8c759 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -28,6 +28,17 @@ public class Params extends Z3Object Native.paramsSetDouble(getContext().nCtx(), getNativeObject(), 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. **/ From 10c5ed634470c635326f9c8a13fdbf690134ac04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2014 11:29:05 -0700 Subject: [PATCH 2/5] add parameter validation in two remaining local cases Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 3 +++ src/api/api_tactic.cpp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index c8b1723f1..6fc0c1c72 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -130,6 +130,9 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); + param_descrs r; + to_solver_ref(s)->collect_param_descrs(r); + to_param_ref(p).validate(r); 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); diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 7dce33971..adfd0fb71 100644 --- a/src/api/api_tactic.cpp +++ b/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); From 92166eb5cb6efe0f08ac6824e7c75c6074a24988 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2014 13:12:40 -0700 Subject: [PATCH 3/5] deal with warning for unused parameter Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 2 +- src/muz/pdr/pdr_context.h | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index f07964395..a1f3af401 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/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), diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index a85011600..e21f46412 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -245,7 +245,6 @@ namespace pdr { class model_search { typedef ptr_vector model_nodes; - ast_manager& m; bool m_bfs; model_node* m_root; std::deque 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(); From 136b172b5a3ef2dd943b1af1534416d9abbe956f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 09:58:54 -0700 Subject: [PATCH 4/5] move parameter validation for when solver object is actually crated Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6fc0c1c72..65b2a9047 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,10 @@ 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); + p.validate(r); s->m_solver->updt_params(p); } @@ -130,14 +134,15 @@ extern "C" { Z3_TRY; LOG_Z3_solver_set_params(c, s, p); RESET_ERROR_CODE(); - param_descrs r; - to_solver_ref(s)->collect_param_descrs(r); - to_param_ref(p).validate(r); + 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); + 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); From c739d803ab0ea7543234d6300841b3809823ce2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2014 13:42:56 -0700 Subject: [PATCH 5/5] include model/proof/unsat_core as part of model parameters Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 4 ++++ src/cmd_context/context_params.cpp | 10 +++++++--- src/cmd_context/context_params.h | 2 ++ 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 65b2a9047..b9b3d8166 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -43,6 +43,7 @@ extern "C" { 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); } @@ -106,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); @@ -123,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); @@ -142,6 +145,7 @@ extern "C" { 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)); } diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 0ec44e0cf..d796dc9b1 100644 --- a/src/cmd_context/context_params.cpp +++ b/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) { diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 7271bb84f..e26fd3fe5 100644 --- a/src/cmd_context/context_params.h +++ b/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.