From f519c58acec47c11c64eab4a145f8735fa63a6e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 30 Dec 2020 14:37:30 -0800 Subject: [PATCH] Add groovy R.U.Stan option to retrieve models even when they don't exist #4924 Usage: z3 4924.smt2 smt.candidate_models=true --- src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_solver.cpp | 13 +++++++------ src/smt/tactic/smt_tactic.cpp | 4 ++-- 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 80da7191b..7308b7f0b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -20,6 +20,7 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), + ('candidate_models', BOOL, False, 'create candidate models even when quantifier or theory reasoning is incomplete'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'), ('cube_depth', UINT, 1, 'cube depth.'), diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index b78dd5b6c..c13b9ebda 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -16,16 +16,17 @@ Author: Notes: --*/ -#include "solver/solver_na2as.h" -#include "smt/smt_kernel.h" + +#include "util/dec_ref_util.h" #include "ast/reg_decl_plugins.h" -#include "smt/params/smt_params.h" -#include "smt/params/smt_params_helper.hpp" -#include "solver/mus.h" #include "ast/for_each_expr.h" #include "ast/ast_smt2_pp.h" #include "ast/func_decl_dependencies.h" -#include "util/dec_ref_util.h" +#include "smt/smt_kernel.h" +#include "smt/params/smt_params.h" +#include "smt/params/smt_params_helper.hpp" +#include "solver/solver_na2as.h" +#include "solver/mus.h" namespace { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index c8ff45488..4bd8445b8 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -72,7 +72,8 @@ public: } void updt_params_core(params_ref const & p) { - m_candidate_models = p.get_bool("candidate_models", false); + smt_params_helper _p(p); + m_candidate_models = _p.candidate_models(); m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true); } @@ -89,7 +90,6 @@ public: } void collect_param_descrs(param_descrs & r) override { - r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete."); r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal."); smt_params_helper::collect_param_descrs(r); }