diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 01f9e687e..afa613f57 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -11,7 +11,7 @@ Version 4.4 - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one. -- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886. +- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, steimann, and Stackoverflow users user297886. Version 4.3.2 diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index e48c23905..9f4f9431c 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1,9 +1,11 @@ #include #include"z3++.h" - using namespace z3; + + + /** Demonstration of how Z3 can be used to prove validity of De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) } @@ -985,6 +987,7 @@ void extract_example() { } int main() { + try { demorgan(); std::cout << "\n"; find_model_example1(); std::cout << "\n"; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 49fa10d94..cff59cd80 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -89,6 +89,7 @@ namespace api { m_bv_util(m()), m_datalog_util(m()), m_fpa_util(m()), + m_dtutil(m()), m_last_result(m()), m_ast_trail(m()), m_replay_stack() { diff --git a/src/api/api_context.h b/src/api/api_context.h index 58394c028..f02dc6f16 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -58,6 +58,7 @@ namespace api { bv_util m_bv_util; datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; + datatype_util m_dtutil; // Support for old solver API smt_params m_fparams; @@ -119,6 +120,7 @@ namespace api { bv_util & bvutil() { return m_bv_util; } datalog::dl_decl_util & datalog_util() { return m_datalog_util; } fpa_util & fpautil() { return m_fpa_util; } + datatype_util& dtutil() { return m_dtutil; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index f3a275508..a9794c980 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -36,7 +36,7 @@ extern "C" { RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); ast_manager& m = mk_c(c)->m(); - datatype_util dt_util(m); + datatype_util& dt_util = mk_c(c)->dtutil(); sort_ref_vector tuples(m); sort* tuple; @@ -102,7 +102,7 @@ extern "C" { RESET_ERROR_CODE(); mk_c(c)->reset_last_result(); ast_manager& m = mk_c(c)->m(); - datatype_util dt_util(m); + datatype_util& dt_util = mk_c(c)->dtutil(); sort_ref_vector sorts(m); sort* e; @@ -451,7 +451,7 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -470,13 +470,13 @@ extern "C" { RESET_ERROR_CODE(); CHECK_VALID_AST(t, 0); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx >= decls->size()) { + if (idx >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } @@ -499,16 +499,16 @@ extern "C" { LOG_Z3_get_datatype_sort_recognizer(c, t, idx); RESET_ERROR_CODE(); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx >= decls->size()) { + if (idx >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + return 0; } func_decl* decl = (*decls)[idx]; decl = dt_util.get_constructor_recognizer(decl); @@ -522,16 +522,16 @@ extern "C" { LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a); RESET_ERROR_CODE(); sort * _t = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(_t)) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } ptr_vector const * decls = dt_util.get_datatype_constructors(_t); - if (!decls || idx_c >= decls->size()) { + if (idx_c >= decls->size()) { SET_ERROR_CODE(Z3_INVALID_ARG); - RETURN_Z3(0); + return 0; } func_decl* decl = (*decls)[idx_c]; if (decl->get_arity() <= idx_a) { @@ -555,7 +555,7 @@ extern "C" { LOG_Z3_get_tuple_sort_mk_decl(c, t); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); @@ -570,7 +570,7 @@ extern "C" { LOG_Z3_get_tuple_sort_num_fields(c, t); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; @@ -593,7 +593,7 @@ extern "C" { LOG_Z3_get_tuple_sort_field_decl(c, t, i); RESET_ERROR_CODE(); sort * tuple = to_sort(t); - datatype_util dt_util(mk_c(c)->m()); + datatype_util& dt_util = mk_c(c)->dtutil(); if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index f7ba98222..62be48a2c 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -44,6 +44,16 @@ namespace Microsoft.Z3 } } + /// + /// Retrieves the inx'th constant declaration in the enumeration. + /// + /// + /// + public FuncDecl ConstDecl(uint inx) + { + return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx)); + } + /// /// The constants in the enumeration. /// @@ -61,7 +71,17 @@ namespace Microsoft.Z3 } /// - /// The test predicates for the constants in the enumeration. + /// Retrieves the inx'th constant in the enumeration. + /// + /// + /// + public Expr Const(uint inx) + { + return Context.MkApp(ConstDecl(inx)); + } + + /// + /// The test predicates (recognizers) for the constants in the enumeration. /// public FuncDecl[] TesterDecls { @@ -76,6 +96,16 @@ namespace Microsoft.Z3 } } + /// + /// Retrieves the inx'th tester/recognizer declaration in the enumeration. + /// + /// + /// + public FuncDecl TesterDecl(uint inx) + { + return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx)); + } + #region Internal internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames) : base(ctx, IntPtr.Zero) diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index e33b9b348..bfe0c50b8 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -34,11 +34,20 @@ public class EnumSort extends Sort t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i)); return t; } + + /** + * Retrieves the inx'th constant declaration in the enumeration. + * @throws Z3Exception on error + **/ + public FuncDecl getConstDecl(int inx) throws Z3Exception + { + return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx)); + } /** * The constants in the enumeration. * @throws Z3Exception on error - * @return an Expr + * @return an Expr[] **/ public Expr[] getConsts() throws Z3Exception { @@ -48,6 +57,16 @@ public class EnumSort extends Sort t[i] = getContext().mkApp(cds[i]); return t; } + + /** + * Retrieves the inx'th constant in the enumeration. + * @throws Z3Exception on error + * @return an Expr + **/ + public Expr getConst(int inx) throws Z3Exception + { + return getContext().mkApp(getConstDecl(inx)); + } /** * The test predicates for the constants in the enumeration. @@ -61,6 +80,15 @@ public class EnumSort extends Sort t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i)); return t; } + + /** + * Retrieves the inx'th tester/recognizer declaration in the enumeration. + * @throws Z3Exception on error + **/ + public FuncDecl getTesterDecl(int inx) throws Z3Exception + { + return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx)); + } EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception { diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d8cf21cda..a7cafbc29 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1390,11 +1390,24 @@ struct let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i)) in mk_list f n + let get_const_decl ( x : sort ) ( inx : int ) = + func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) inx) + + let get_consts ( x : sort ) = + let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) in + let f i = (Expr.mk_const_f (Sort.gc x) (get_const_decl x i)) in + mk_list f n + + let get_const ( x : sort ) ( inx : int ) = + Expr.mk_const_f (Sort.gc x) (get_const_decl x inx) + let get_tester_decls ( x : sort ) = let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x) in - let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in + let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in mk_list f n + let get_tester_decl ( x : sort ) ( inx : int ) = + func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) inx) end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index e223008bb..db0c3f130 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1091,8 +1091,20 @@ sig (** The function declarations of the constants in the enumeration. *) val get_const_decls : Sort.sort -> FuncDecl.func_decl list + (** Retrieves the inx'th constant declaration in the enumeration. *) + val get_const_decl : Sort.sort -> int -> FuncDecl.func_decl + + (** The constants in the enumeration. *) + val get_consts : Sort.sort -> Expr.expr list + + (** Retrieves the inx'th constant in the enumeration. *) + val get_const : Sort.sort -> int -> Expr.expr + (** The test predicates for the constants in the enumeration. *) val get_tester_decls : Sort.sort -> FuncDecl.func_decl list + + (** Retrieves the inx'th tester/recognizer declaration in the enumeration. *) + val get_tester_decl : Sort.sort -> int -> FuncDecl.func_decl end (** Functions to manipulate List expressions *) diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 96b678fb2..3f7f01364 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -168,9 +168,9 @@ class datatype_util { obj_map m_is_recursive; ast_ref_vector m_asts; ptr_vector > m_vectors; - - func_decl * get_constructor(sort * ty, unsigned c_id); + func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); + func_decl * get_constructor(sort * ty, unsigned c_id); public: datatype_util(ast_manager & m); @@ -185,7 +185,12 @@ public: bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } ptr_vector const * get_datatype_constructors(sort * ty); - unsigned get_datatype_num_constructors(sort * ty) { return get_datatype_constructors(ty)->size(); } + unsigned get_datatype_num_constructors(sort * ty) { + SASSERT(is_datatype(ty)); + unsigned tid = ty->get_parameter(1).get_int(); + unsigned o = ty->get_parameter(3 + 2 * tid).get_int(); + return ty->get_parameter(o).get_int(); + } unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); } unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); } func_decl * get_non_rec_constructor(sort * ty); @@ -197,6 +202,7 @@ public: bool are_siblings(sort * s1, sort * s2); void reset(); void display_datatype(sort *s, std::ostream& strm); + }; #endif /* _DATATYPE_DECL_PLUGIN_H_ */ diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 8e2dd326a..89072a795 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1878,6 +1878,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args else if (num == 2 && m_bv_util.is_bv(args[0]) && m_bv_util.get_bv_size(args[0]) == 3 && + m_arith_util.is_int(args[1]) || m_arith_util.is_real(args[1])) { // rm + real -> float mk_to_fp_real(f, f->get_range(), args[0], args[1], result); @@ -2066,7 +2067,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << "x: " << mk_ismt2_pp(x, m) << std::endl;); SASSERT(m_util.is_float(s)); - SASSERT(au().is_real(x)); + SASSERT(au().is_real(x) || au().is_int(x)); unsigned ebits = m_util.get_ebits(s); unsigned sbits = m_util.get_sbits(s); @@ -2089,7 +2090,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * } rational q; - m_util.au().is_numeral(x, q); + bool is_int; + m_util.au().is_numeral(x, q, is_int); scoped_mpf v(m_mpf_manager); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index bd2676ee4..48b7adb8b 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -521,14 +521,26 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } + else if (arity == 2 && + is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) && + is_sort_of(domain[1], m_arith_fid, INT_SORT)) { + // Rounding + 1 Int -> 1 FP + if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) + m_manager->raise_exception("expecting two integer parameters to to_fp"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { m_manager->raise_exception("Unexpected argument combination for (_ to_fp eb sb). Supported argument combinations are: " - "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1))," - "(_ BitVec (eb+sb))," - "(Real)," - "(RoundingMode (_ BitVec (eb+sb)))," - "(RoundingMode (_ FloatingPoint eb' sb'))," - "(RoundingMode Real Int), and" + "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)), " + "(_ BitVec (eb+sb)), " + "(Real), " + "(RoundingMode (_ BitVec (eb+sb))), " + "(RoundingMode (_ FloatingPoint eb' sb')), " + "(RoundingMode Real Int), " + "(RoundingMode Int), and " "(RoundingMode Real)." ); } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 7c9c5813b..30dd08ff4 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -288,7 +288,7 @@ namespace datalog { bool context::unbound_compressor() const { return m_params->unbound_compressor(); } bool context::similarity_compressor() const { return m_params->similarity_compressor(); } unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); } - unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; } + unsigned context::timeout() const { return m_fparams.m_timeout; } unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); } bool context::generate_explanations() const { return m_params->generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index cf2c53913..8a881d71b 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -258,7 +258,7 @@ namespace datalog { bool unbound_compressor() const; bool similarity_compressor() const; unsigned similarity_compressor_threshold() const; - unsigned soft_timeout() const; + unsigned timeout() const; unsigned initial_restart_timeout() const; bool generate_explanations() const; bool explanations_on_relation_level() const; diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index 0cd08e5b3..11f6ae1db 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -59,7 +59,7 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_soft_timeout = 1000; + m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 02b00be39..4e219b2f7 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -128,8 +128,8 @@ namespace datalog { lbool rel_context::saturate(scoped_query& sq) { m_context.ensure_closed(); - bool time_limit = m_context.soft_timeout()!=0; - unsigned remaining_time_limit = m_context.soft_timeout(); + bool time_limit = m_context.timeout()!=0; + unsigned remaining_time_limit = m_context.timeout(); unsigned restart_time = m_context.initial_restart_timeout(); instruction_block termination_code; diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 83842a68b..f13590e35 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -1367,7 +1367,7 @@ namespace datalog { { // m_fparams.m_relevancy_lvl = 0; m_fparams.m_mbqi = false; - m_fparams.m_soft_timeout = 1000; + m_fparams.m_timeout = 1000; } ~imp() {} diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 2f8d9c1ee..a0f56663c 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -34,7 +34,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter - m_soft_timeout = p.soft_timeout(); + m_timeout = p.timeout(); model_params mp(_p); m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 256c5a646..2fbc9b6d4 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -202,7 +202,7 @@ struct smt_params : public preprocessor_params, bool m_preprocess; // temporary hack for disabling all preprocessing.. bool m_user_theory_preprocess_axioms; bool m_user_theory_persist_axioms; - unsigned m_soft_timeout; + unsigned m_timeout; bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_dump_goal_as_smt; @@ -270,7 +270,7 @@ struct smt_params : public preprocessor_params, m_preprocess(true), // temporary hack for disabling all preprocessing.. m_user_theory_preprocess_axioms(false), m_user_theory_persist_axioms(false), - m_soft_timeout(0), + m_timeout(0), m_at_labels_cex(false), m_check_at_labels(false), m_dump_goal_as_smt(false), diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 39818e621..97a326e4d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -15,7 +15,7 @@ def_module_params(module_name='smt', ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), - ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'), + ('timeout', UINT, 0, 'timeout (0 means no timeout)'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 957d5ebe7..d7e18461b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3355,7 +3355,7 @@ namespace smt { if (m_last_search_failure != OK) return true; - if (m_timer.ms_timeout(m_fparams.m_soft_timeout)) { + if (m_timer.ms_timeout(m_fparams.m_timeout)) { m_last_search_failure = TIMEOUT; return true; }