diff --git a/scripts/update_api.py b/scripts/update_api.py index 78fad45be..4452ae613 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -73,7 +73,7 @@ Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctype # Mapping to .NET types Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'int', SYMBOL : 'IntPtr', + FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'bool', SYMBOL : 'IntPtr', PRINT_MODE : 'uint', ERROR_CODE : 'uint' } # Mapping to Java types diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 3ffee518e..98417cc7b 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -35,7 +35,7 @@ public: fail_if_proof_generation("ackermannize", g); TRACE("ackermannize", g->display(tout << "in\n");); - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); lackr lackr(m, m_p, m_st, flas, nullptr); diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 9e87a1a69..c5e04ab23 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -134,7 +134,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator, info->abstract(arg, aarg); expr_ref arg_value(m); evaluator(aarg, arg_value); - args.push_back(arg_value); + args.push_back(std::move(arg_value)); } if (fi->get_entry(args.c_ptr()) == nullptr) { TRACE("ackr_model", diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index b739af9d3..8c18df7b2 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -23,8 +23,8 @@ #include "ast/for_each_expr.h" #include "model/model_smt2_pp.h" -lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas, - solver * uffree_solver) +lackr::lackr(ast_manager& m, const params_ref& p, lackr_stats& st, + const ptr_vector& formulas, solver * uffree_solver) : m_m(m) , m_p(p) , m_formulas(formulas) @@ -173,11 +173,10 @@ void lackr::abstract() { } m_info->seal(); // perform abstraction of the formulas - const unsigned sz = m_formulas.size(); - for (unsigned i = 0; i < sz; ++i) { + for (expr * f : m_formulas) { expr_ref a(m_m); - m_info->abstract(m_formulas.get(i), a); - m_abstr.push_back(a); + m_info->abstract(f, a); + m_abstr.push_back(std::move(a)); } } @@ -249,13 +248,9 @@ lbool lackr::lazy() { // Collect all uninterpreted terms, skipping 0-arity. // bool lackr::collect_terms() { - ptr_vector stack; + ptr_vector stack = m_formulas; expr * curr; expr_mark visited; - for(unsigned i = 0; i < m_formulas.size(); ++i) { - stack.push_back(m_formulas.get(i)); - TRACE("lackr", tout << "infla: " <& formulas, solver * uffree_solver); ~lackr(); void updt_params(params_ref const & _p); @@ -82,7 +82,7 @@ class lackr { typedef ackr_helper::app_set app_set; ast_manager& m_m; params_ref m_p; - expr_ref_vector m_formulas; + const ptr_vector& m_formulas; expr_ref_vector m_abstr; fun2terms_map m_fun2terms; ackr_info_ref m_info; diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 9bb236fe2..a79f55855 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -120,12 +120,8 @@ extern "C" { } Z3_bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) { - Z3_TRY; LOG_Z3_is_algebraic_number(c, a); - RESET_ERROR_CODE(); - expr * e = to_expr(a); - return mk_c(c)->autil().is_irrational_algebraic_numeral(e); - Z3_CATCH_RETURN(Z3_FALSE); + return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a)); } Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) { diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 5993e9fdd..295977a06 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -218,10 +218,9 @@ namespace api { // Corner case bug: n may be in m_last_result, and this is the only reference to n. // When, we execute reset() it is deleted // To avoid this bug, I bump the reference counter before reseting m_last_result - m().inc_ref(n); + ast_ref node(n, m()); m_last_result.reset(); - m_last_result.push_back(n); - m().dec_ref(n); + m_last_result.push_back(std::move(node)); } else { m_ast_trail.push_back(n); diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index c7ca1851e..64ec88d09 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -43,7 +43,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_ast(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 596b2943f..9dcb3ef82 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -37,7 +37,7 @@ namespace Microsoft.Z3 { Contract.Requires(k != null); - return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject) != 0; + return Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); } /// diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index 66054761a..c6055db14 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 890d86619..ba76ae7eb 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1963,7 +1963,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); CheckContextMatch(t); - return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed) ? 1 : 0)); + return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (signed))); } /// @@ -1980,7 +1980,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvadd_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -2031,7 +2031,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvsub_no_underflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -2080,7 +2080,7 @@ namespace Microsoft.Z3 CheckContextMatch(t1); CheckContextMatch(t2); - return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned) ? 1 : 0)); + return new BoolExpr(this, Native.Z3_mk_bvmul_no_overflow(nCtx, t1.NativeObject, t2.NativeObject, (isSigned))); } /// @@ -3135,9 +3135,7 @@ namespace Microsoft.Z3 public BitVecNum MkBV(bool[] bits) { Contract.Ensures(Contract.Result() != null); - int[] _bits = new int[bits.Length]; - for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0; - return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); + return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, bits)); } @@ -4186,7 +4184,7 @@ namespace Microsoft.Z3 public FPNum MkFPInf(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0)); + return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative)); } /// @@ -4197,7 +4195,7 @@ namespace Microsoft.Z3 public FPNum MkFPZero(FPSort s, bool negative) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0)); + return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative)); } /// @@ -4243,7 +4241,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, sgn, exp, sig, s.NativeObject)); } /// @@ -4256,7 +4254,7 @@ namespace Microsoft.Z3 public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { Contract.Ensures(Contract.Result() != null); - return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn ? 1 : 0, exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, sgn, exp, sig, s.NativeObject)); } /// diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index f09eecbdd..99745ffff 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -179,7 +179,7 @@ namespace Microsoft.Z3 /// public bool IsNumeral { - get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) ; } } /// @@ -188,7 +188,7 @@ namespace Microsoft.Z3 /// True if the term is well-sorted, false otherwise. public bool IsWellSorted { - get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) ; } } /// @@ -239,7 +239,7 @@ namespace Microsoft.Z3 /// public bool IsAlgebraicNumber { - get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); } } #endregion @@ -256,7 +256,7 @@ namespace Microsoft.Z3 return (IsExpr && Native.Z3_is_eq_sort(Context.nCtx, Native.Z3_mk_bool_sort(Context.nCtx), - Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0); + Native.Z3_get_sort(Context.nCtx, NativeObject)) ); } } @@ -423,7 +423,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT); } @@ -789,7 +789,7 @@ namespace Microsoft.Z3 /// Check whether expression is a string constant. /// /// a Boolean - public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } + public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject); } } /// /// Retrieve string corresponding to string constant. @@ -1336,7 +1336,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_RELATION_SORT); } @@ -1458,7 +1458,7 @@ namespace Microsoft.Z3 { get { - return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 && + return (Native.Z3_is_app(Context.nCtx, NativeObject) && Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT); } } @@ -1789,7 +1789,7 @@ namespace Microsoft.Z3 [Pure] internal override void CheckNativeObject(IntPtr obj) { - if (Native.Z3_is_app(Context.nCtx, obj) == 0 && + if (Native.Z3_is_app(Context.nCtx, obj) == false && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST && Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST) throw new Z3Exception("Underlying object is not a term"); @@ -1822,11 +1822,13 @@ namespace Microsoft.Z3 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s); - if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast? + if (Z3_sort_kind.Z3_REAL_SORT == sk && + Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast? return new AlgebraicNum(ctx, obj); - if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0) + if (Native.Z3_is_numeral_ast(ctx.nCtx, obj)) { + switch (sk) { case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index 808752eaa..4a2575fe4 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -52,7 +52,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Sign is not a Boolean value"); return res != 0; } @@ -86,7 +86,7 @@ namespace Microsoft.Z3 get { UInt64 result = 0; - if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0) + if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == false) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return result; } @@ -111,7 +111,7 @@ namespace Microsoft.Z3 /// public string Exponent(bool biased = true) { - return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0); + return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased); } /// @@ -120,7 +120,7 @@ namespace Microsoft.Z3 public Int64 ExponentInt64(bool biased = true) { Int64 result = 0; - if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0) + if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased) == false) throw new Z3Exception("Exponent is not a 64 bit integer"); return result; } @@ -133,43 +133,43 @@ namespace Microsoft.Z3 /// public BitVecExpr ExponentBV(bool biased = true) { - return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0)); + return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased)); } /// /// Indicates whether the numeral is a NaN. /// - public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } } + public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is a +oo or -oo. /// - public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } } + public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is +zero or -zero. /// - public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } } + public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is normal. /// - public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } } + public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is subnormal. /// - public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } } + public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is positive. /// - public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } } + public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) ; } } /// /// Indicates whether the numeral is negative. /// - public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } } + public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) ; } } #region Internal internal FPNum(Context ctx, IntPtr obj) diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs index 52c0af8bd..fb51e1014 100644 --- a/src/api/dotnet/FiniteDomainNum.cs +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -39,7 +39,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -53,7 +53,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -67,7 +67,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -81,7 +81,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 0587a2276..39ddfad83 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -38,7 +38,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context.nCtx == b.Context.nCtx && - Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_func_decl(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index acf3fab32..f242003a8 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -65,7 +65,7 @@ namespace Microsoft.Z3 public static string GetParameter(string id) { IntPtr t; - if (Native.Z3_global_param_get(id, out t) == 0) + if (Native.Z3_global_param_get(id, out t) == false) return null; else return Marshal.PtrToStringAnsi(t); @@ -91,7 +91,7 @@ namespace Microsoft.Z3 /// all contexts globally. public static void ToggleWarningMessages(bool enabled) { - Native.Z3_toggle_warning_messages((enabled) ? 1 : 0); + Native.Z3_toggle_warning_messages(enabled); } /// diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 03e573538..a5e35fcd5 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -103,7 +103,7 @@ namespace Microsoft.Z3 /// public bool Inconsistent { - get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) ; } } /// @@ -163,7 +163,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedSat { - get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) ; } } /// @@ -171,7 +171,7 @@ namespace Microsoft.Z3 /// public bool IsDecidedUnsat { - get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) ; } } /// @@ -251,7 +251,7 @@ namespace Microsoft.Z3 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) - : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0)) + : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models), (unsatCores), (proofs))) { Contract.Requires(ctx != null); } diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs index 64fd78ad2..78fee44f4 100644 --- a/src/api/dotnet/IntNum.cs +++ b/src/api/dotnet/IntNum.cs @@ -49,7 +49,7 @@ namespace Microsoft.Z3 get { UInt64 res = 0; - if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a 64 bit unsigned"); return res; } @@ -63,7 +63,7 @@ namespace Microsoft.Z3 get { int res = 0; - if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int"); return res; } @@ -77,7 +77,7 @@ namespace Microsoft.Z3 get { Int64 res = 0; - if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not an int64"); return res; } @@ -91,7 +91,7 @@ namespace Microsoft.Z3 get { uint res = 0; - if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0) + if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == false) throw new Z3Exception("Numeral is not a uint"); return res; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index d11a57052..2c6d12dc0 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -86,7 +86,7 @@ namespace Microsoft.Z3 return null; else { - if (Native.Z3_is_as_array(Context.nCtx, n) == 0) + if (Native.Z3_is_as_array(Context.nCtx, n) == false) throw new Z3Exception("Argument was not an array constant"); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); return FuncInterp(new FuncDecl(Context, fd)); @@ -227,7 +227,7 @@ namespace Microsoft.Z3 Contract.Ensures(Contract.Result() != null); IntPtr v = IntPtr.Zero; - if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0) + if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion), ref v) == false) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index 5b143d525..eeda55755 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -35,7 +35,7 @@ namespace Microsoft.Z3 { Contract.Requires(name != null); - Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value)); return this; } @@ -90,7 +90,7 @@ namespace Microsoft.Z3 /// public Params Add(string name, bool value) { - Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0); + Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value)); return this; } diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index e34b4ef97..d729f7424 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// public bool IsUniversal { - get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_quantifier_forall(Context.nCtx, NativeObject); } } /// @@ -41,7 +41,7 @@ namespace Microsoft.Z3 /// public bool IsExistential { - get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject) != 0; } + get { return Native.Z3_is_quantifier_exists(Context.nCtx, NativeObject); } } /// @@ -193,7 +193,7 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) , weight, AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(sorts), AST.ArrayToNative(sorts), Symbol.ArrayToNative(names), @@ -201,7 +201,7 @@ namespace Microsoft.Z3 } else { - NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_ex(ctx.nCtx, (isForall), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), AST.ArrayLength(noPatterns), AST.ArrayToNative(noPatterns), @@ -229,14 +229,14 @@ namespace Microsoft.Z3 if (noPatterns == null && quantifierID == null && skolemID == null) { - NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) , weight, AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), body.NativeObject); } else { - NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall) ? 1 : 0, weight, + NativeObject = Native.Z3_mk_quantifier_const_ex(ctx.nCtx, (isForall), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), AST.ArrayLength(bound), AST.ArrayToNative(bound), AST.ArrayLength(patterns), AST.ArrayToNative(patterns), diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index e6f195434..66acc5c0f 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -41,7 +41,7 @@ namespace Microsoft.Z3 (!Object.ReferenceEquals(a, null) && !Object.ReferenceEquals(b, null) && a.Context == b.Context && - Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0); + Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject)); } /// diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index c94af625c..6708035bc 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -134,9 +134,9 @@ namespace Microsoft.Z3 { Entry e; string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); - if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) + if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) ) e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); - else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0) + else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) ) e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); else throw new Z3Exception("Unknown data entry value"); diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 357d79bcb..211601713 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -49,7 +49,7 @@ void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { char const * s = d.m_str; while (*s) { - char c = *s; + unsigned char c = *s; if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') || c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' || c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' || @@ -57,7 +57,7 @@ static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { out << c; } else { - char str[4] = {'0', '0', '0', 0}; + unsigned char str[4] = {'0', '0', '0', 0}; str[2] = '0' + (c % 10); c /= 10; str[1] = '0' + (c % 10); diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index fe5bc3af5..be3a02019 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -638,6 +638,11 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int return true; } +bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { + return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); +} + + #define IS_INT_EXPR_DEPTH_LIMIT 100 bool arith_recognizers::is_int_expr(expr const *e) const { if (is_int(e)) return true; @@ -678,7 +683,7 @@ void arith_util::init_plugin() { m_plugin = static_cast(m_manager.get_plugin(m_afid)); } -bool arith_util::is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val) { +bool arith_util::is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val) { if (!is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM)) return false; am().set(val, to_irrational_algebraic_numeral(n)); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index d7340297b..17b8fa1d0 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -229,7 +229,7 @@ public: family_id get_family_id() const { return m_afid; } bool is_arith_expr(expr const * n) const { return is_app(n) && to_app(n)->get_family_id() == m_afid; } - bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } + bool is_irrational_algebraic_numeral(expr const * n) const; bool is_numeral(expr const * n, rational & val, bool & is_int) const; bool is_numeral(expr const * n, rational & val) const { bool is_int; return is_numeral(n, val, is_int); } bool is_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_NUM); } @@ -338,8 +338,7 @@ public: return plugin().am(); } - bool is_irrational_algebraic_numeral(expr const * n) const { return is_app_of(n, m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); } - bool is_irrational_algebraic_numeral(expr const * n, algebraic_numbers::anum & val); + bool is_irrational_algebraic_numeral2(expr const * n, algebraic_numbers::anum & val); algebraic_numbers::anum const & to_irrational_algebraic_numeral(expr const * n); sort * mk_int() { return m_manager.mk_sort(m_afid, INT_SORT); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 5cd09263d..3a55bbb0b 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1199,7 +1199,7 @@ void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, pa for (unsigned i = 0; i < sz; ++i) { format_ref fr(fm(m)); pr(es[i], num_vars, var_prefix, fr, var_names); - fmts.push_back(fr); + fmts.push_back(std::move(fr)); } r = mk_seq(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f()); } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b079fc2ca..dd3f35a2a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -3108,12 +3108,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex expr_ref exp_bv(m), exp_all_ones(m); exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits))); - m_extra_assertions.push_back(exp_all_ones); + m_extra_assertions.push_back(std::move(exp_all_ones)); expr_ref sig_bv(m), sig_is_non_zero(m); sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); - m_extra_assertions.push_back(sig_is_non_zero); + m_extra_assertions.push_back(std::move(sig_is_non_zero)); } TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 379020331..7451795f3 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1159,49 +1159,44 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) { result = m_util.mk_numeral(floor(a), true); return BR_DONE; } - else if (m_util.is_to_real(arg, x)) { + + if (m_util.is_to_real(arg, x)) { result = x; return BR_DONE; } - else { - if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) { - // Try to apply simplifications such as: - // (to_int (+ 1.0 (to_real x))) --> (+ 1 x) - // if all arguments of arg are - // - integer numerals, OR - // - to_real applications - // then, to_int can be eliminated - unsigned num_args = to_app(arg)->get_num_args(); - unsigned i = 0; - for (; i < num_args; i++) { - expr * c = to_app(arg)->get_arg(i); - if (m_util.is_numeral(c, a) && a.is_int()) - continue; - if (m_util.is_to_real(c)) - continue; - break; // failed + if (m_util.is_add(arg) || m_util.is_mul(arg) || m_util.is_power(arg)) { + // Try to apply simplifications such as: + // (to_int (+ 1.0 (to_real x)) y) --> (+ 1 x (to_int y)) + + expr_ref_buffer int_args(m()), real_args(m()); + for (expr* c : *to_app(arg)) { + if (m_util.is_numeral(c, a) && a.is_int()) { + int_args.push_back(m_util.mk_numeral(a, true)); } - if (i == num_args) { - // simplification can be applied - expr_ref_buffer new_args(m()); - for (i = 0; i < num_args; i++) { - expr * c = to_app(arg)->get_arg(i); - if (m_util.is_numeral(c, a) && a.is_int()) { - new_args.push_back(m_util.mk_numeral(a, true)); - } - else { - VERIFY (m_util.is_to_real(c, x)); - new_args.push_back(x); - } - } - SASSERT(num_args == new_args.size()); - result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), new_args.size(), new_args.c_ptr()); - return BR_REWRITE1; + else if (m_util.is_to_real(c, x)) { + int_args.push_back(x); + } + else { + real_args.push_back(c); } } - return BR_FAILED; + if (real_args.empty()) { + result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr()); + return BR_REWRITE1; + } + if (!int_args.empty() && (m_util.is_add(arg) || m_util.is_mul(arg))) { + decl_kind k = to_app(arg)->get_decl()->get_decl_kind(); + expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m()); + expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m()); + int_args.reset(); + int_args.push_back(t1); + int_args.push_back(m_util.mk_to_int(t2)); + result = m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()); + return BR_REWRITE3; + } } + return BR_FAILED; } br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index a0adb6398..c81c7385a 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -1383,7 +1383,7 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { --i; tmp = args[i].get(); tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp); - args[i] = tmp; + args[i] = std::move(tmp); sz += get_bv_size(to_app(arg)->get_arg(i)); } result = m_autil.mk_add(args.size(), args.c_ptr()); @@ -2400,8 +2400,8 @@ bool bv_rewriter::isolate_term(expr* lhs, expr* rhs, expr_ref& result) { return false; } unsigned sz = to_app(rhs)->get_num_args(); - expr_ref t1(m()), t2(m()); - t1 = to_app(rhs)->get_arg(0); + expr * t1 = to_app(rhs)->get_arg(0); + expr_ref t2(m()); if (sz > 2) { t2 = m().mk_app(get_fid(), OP_BADD, sz-1, to_app(rhs)->get_args()+1); } @@ -2597,14 +2597,10 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { result = m().mk_bool_val(new_lhs == new_rhs); return BR_DONE; } - } - else { - new_lhs = lhs; - new_rhs = rhs; + lhs = new_lhs; + rhs = new_rhs; } - lhs = new_lhs; - rhs = new_rhs; // Try to rewrite t1 + t2 = c --> t1 = c - t2 // Reason: it is much cheaper to bit-blast. if (isolate_term(lhs, rhs, result)) { diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index ad9350eca..433ef6f66 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -125,7 +125,7 @@ struct bv_trailing::imp { for (unsigned i = 0; i < num; ++i) { expr * const curr = a->get_arg(i); VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1)); - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); } result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); return to_rm; @@ -150,7 +150,7 @@ struct bv_trailing::imp { numeral c_val; unsigned c_sz; if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) - new_args.push_back(tmp); + new_args.push_back(std::move(tmp)); const unsigned sz = m_util.get_bv_size(coefficient); const unsigned new_sz = sz - retv; @@ -204,7 +204,7 @@ struct bv_trailing::imp { expr_ref_vector new_args(m); for (unsigned j = 0; j < i; ++j) new_args.push_back(a->get_arg(j)); - if (new_last) new_args.push_back(new_last); + if (new_last) new_args.push_back(std::move(new_last)); result = new_args.size() == 1 ? new_args.get(0) : m_util.mk_concat(new_args.size(), new_args.c_ptr()); return retv; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 4fbf77ec9..eb819c988 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -35,6 +35,7 @@ Notes: #include "ast/ast_util.h" #include "ast/well_sorted.h" +namespace { struct th_rewriter_cfg : public default_rewriter_cfg { bool_rewriter m_b_rw; arith_rewriter m_a_rw; @@ -337,16 +338,16 @@ struct th_rewriter_cfg : public default_rewriter_cfg { family_id fid = t->get_family_id(); if (fid == m_a_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true; - case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true; + case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; + case OP_MUL: n = m_a_util.mk_numeral(rational::one(), m().get_sort(t)); return true; default: return false; } } if (fid == m_bv_rw.get_fid()) { switch (t->get_decl_kind()) { - case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true; - case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true; + case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), m().get_sort(t)); return true; + case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), m().get_sort(t)); return true; default: return false; } @@ -468,9 +469,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // terms matched... bool is_int = m_a_util.is_int(t1); if (!new_t1) - new_t1 = m_a_util.mk_numeral(rational(0), is_int); + new_t1 = m_a_util.mk_numeral(rational::zero(), is_int); if (!new_t2) - new_t2 = m_a_util.mk_numeral(rational(0), is_int); + new_t2 = m_a_util.mk_numeral(rational::zero(), is_int); // mk common part ptr_buffer args; for (unsigned i = 0; i < num1; i++) { @@ -709,6 +710,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { }; +} template class rewriter_tpl; @@ -764,8 +766,8 @@ unsigned th_rewriter::get_num_steps() const { void th_rewriter::cleanup() { ast_manager & m = m_imp->m(); - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + m_imp->~imp(); + new (m_imp) imp(m, m_params); } void th_rewriter::reset() { diff --git a/src/ast/substitution/substitution.cpp b/src/ast/substitution/substitution.cpp index 39e9e07a2..7e981aab8 100644 --- a/src/ast/substitution/substitution.cpp +++ b/src/ast/substitution/substitution.cpp @@ -196,16 +196,16 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e expr_ref_vector pats(m_manager), no_pats(m_manager); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_pattern(i), off), s1, t1, er); - pats.push_back(er); + pats.push_back(std::move(er)); } for (unsigned i = 0; i < q->get_num_no_patterns(); ++i) { subst.apply(num_actual_offsets, deltas, expr_offset(q->get_no_pattern(i), off), s1, t1, er); - no_pats.push_back(er); + no_pats.push_back(std::move(er)); } subst.apply(num_actual_offsets, deltas, body, s1, t1, er); er = m_manager.update_quantifier(q, pats.size(), pats.c_ptr(), no_pats.size(), no_pats.c_ptr(), er); m_todo.pop_back(); - m_new_exprs.push_back(er); + m_new_exprs.push_back(std::move(er)); m_apply_cache.insert(n, er); break; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1950e35f9..0b4c5cd3d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -493,6 +493,7 @@ cmd_context::~cmd_context() { if (m_main_ctx) { set_verbose_stream(std::cerr); } + pop(m_scopes.size()); finalize_cmds(); finalize_tactic_cmds(); finalize_probes(); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 5a0f6468b..8c88b1680 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "cmd_context/pdecl.h" #include "ast/datatype_decl_plugin.h" +#include "ast/ast_pp.h" #include using namespace format_ns; @@ -768,9 +769,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { } else { out << "(" << m_decl->get_name(); - for (unsigned i = 0; i < m_args.size(); i++) { - out << " "; - m.display(out, m_args[i]); + for (auto arg : m_args) { + m.display(out << " ", arg); } out << ")"; } @@ -782,8 +782,8 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { } else { ptr_buffer b; - for (unsigned i = 0; i < m_args.size(); i++) - b.push_back(m.pp(m_args[i])); + for (auto arg : m_args) + b.push_back(m.pp(arg)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str().c_str()); } } @@ -807,8 +807,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { } else { out << "(_ " << m_decl->get_name(); - for (unsigned i = 0; i < m_indices.size(); i++) { - out << " " << m_indices[i]; + for (auto idx : m_indices) { + out << " " << idx; } out << ")"; } @@ -821,8 +821,8 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info { else { ptr_buffer b; b.push_back(mk_string(m.m(), m_decl->get_name().str().c_str())); - for (unsigned i = 0; i < m_indices.size(); i++) - b.push_back(mk_unsigned(m.m(), m_indices[i])); + for (auto idx : m_indices) + b.push_back(mk_unsigned(m.m(), idx)); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), "_"); } } @@ -853,6 +853,15 @@ pdecl_manager::pdecl_manager(ast_manager & m): pdecl_manager::~pdecl_manager() { dec_ref(m_list); reset_sort_info(); + for (auto const& kv : m_sort2psort) { + del_decl_core(kv.m_value); + TRACE("pdecl_manager", tout << "orphan: " << mk_pp(kv.m_key, m()) << "\n";); + } + for (auto* p : m_table) { + del_decl_core(p); + } + m_sort2psort.reset(); + m_table.reset(); SASSERT(m_sort2psort.empty()); SASSERT(m_table.empty()); } @@ -946,13 +955,15 @@ void pdecl_manager::del_decl_core(pdecl * p) { } void pdecl_manager::del_decl(pdecl * p) { - TRACE("register_psort", tout << "del psort "; p->display(tout); tout << "\n";); + TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); if (p->is_psort()) { psort * _p = static_cast(p); - if (_p->is_sort_wrapper()) + if (_p->is_sort_wrapper()) { m_sort2psort.erase(static_cast(_p)->get_sort()); - else + } + else { m_table.erase(_p); + } } del_decl_core(p); } diff --git a/src/model/model.cpp b/src/model/model.cpp index 97a2917b7..83adfc87e 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -260,7 +260,7 @@ struct model::occs_collector { void operator()(func_decl* f) { ts.add_occurs(f); } - void operator()(ast* ) {} + void operator()(ast*) {} }; @@ -319,7 +319,7 @@ void model::collect_occs(top_sort& ts, func_decl* f) { void model::collect_occs(top_sort& ts, expr* e) { occs_collector collector(ts); - for_each_ast(collector, e); + for_each_ast(collector, e, true); } bool model::can_inline_def(top_sort& ts, func_decl* f) { diff --git a/src/model/model_core.h b/src/model/model_core.h index d705e432d..7f5051386 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -48,6 +48,14 @@ public: func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; } bool eval(func_decl * f, expr_ref & r) const; + bool is_true_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_true(r); + } + bool is_false_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_false(r); + } unsigned get_num_constants() const { return m_const_decls.size(); } unsigned get_num_functions() const { return m_func_decls.size(); } diff --git a/src/muz/base/fp_params.pyg b/src/muz/base/fp_params.pyg index c96a12ca2..981b99de7 100644 --- a/src/muz/base/fp_params.pyg +++ b/src/muz/base/fp_params.pyg @@ -150,6 +150,8 @@ def_module_params('fp', ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'), ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'), + ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), + ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.iuc', UINT, 1, '0 = use old implementation of unsat-core-generation, ' + '1 = use new implementation of IUC generation, ' + @@ -160,13 +162,10 @@ def_module_params('fp', '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'), ('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'), - ('spacer.reuse_pobs', BOOL, True, 'Reuse pobs'), ('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'), ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'), - ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), - ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'), ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"), ('spacer.min_level', UINT, 0, 'Minimal level to explore'), diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 40569295b..07dc1a372 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -55,6 +55,8 @@ Notes: #include "muz/spacer/spacer_sat_answer.h" +#define WEAKNESS_MAX 65535 + namespace spacer { /// pob -- proof obligation @@ -66,8 +68,8 @@ pob::pob (pob* parent, pred_transformer& pt, m_binding(m_pt.get_ast_manager()), m_new_post (m_pt.get_ast_manager ()), m_level (level), m_depth (depth), - m_open (true), m_use_farkas (true), m_weakness(0), - m_blocked_lvl(0) { + m_open (true), m_use_farkas (true), m_in_queue(false), + m_weakness(0), m_blocked_lvl(0) { if (add_to_parent && m_parent) { m_parent->add_child(*this); } @@ -79,6 +81,7 @@ void pob::set_post(expr* post) { } void pob::set_post(expr* post, app_ref_vector const &binding) { + SASSERT(!is_in_queue()); normalize(post, m_post, m_pt.get_context().simplify_pob(), m_pt.get_context().use_euf_gen()); @@ -88,6 +91,7 @@ void pob::set_post(expr* post, app_ref_vector const &binding) { } void pob::inherit(pob const &p) { + SASSERT(!is_in_queue()); SASSERT(m_parent == p.m_parent); SASSERT(&m_pt == &p.m_pt); SASSERT(m_post == p.m_post); @@ -105,17 +109,10 @@ void pob::inherit(pob const &p) { m_derivation = nullptr; } -void pob::clean () { - if (m_new_post) { - m_post = m_new_post; - m_new_post.reset(); - } -} - void pob::close () { if (!m_open) { return; } - reset (); + m_derivation = nullptr; m_open = false; for (unsigned i = 0, sz = m_kids.size (); i < sz; ++i) { m_kids [i]->close(); } @@ -129,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) { } } - + std::ostream &pob::display(std::ostream &out, bool full) const { + out << pt().head()->get_name () + << " level: " << level() + << " depth: " << depth() + << " post_id: " << post()->get_id() + << (is_in_queue() ? " in_queue" : ""); + if (full) out << "\n" << m_post; + return out; + } // ---------------- // pob_queue @@ -137,17 +142,24 @@ void pob::get_skolems(app_ref_vector &v) { pob* pob_queue::top () { /// nothing in the queue - if (m_obligations.empty()) { return nullptr; } + if (m_data.empty()) { return nullptr; } /// top queue element is above max level - if (m_obligations.top()->level() > m_max_level) { return nullptr; } + if (m_data.top()->level() > m_max_level) { return nullptr; } /// top queue element is at the max level, but at a higher than base depth - if (m_obligations.top ()->level () == m_max_level && - m_obligations.top()->depth() > m_min_depth) { return nullptr; } + if (m_data.top ()->level () == m_max_level && + m_data.top()->depth() > m_min_depth) { return nullptr; } /// there is something good in the queue - return m_obligations.top ().get (); + return m_data.top (); } +void pob_queue::pop() { + pob *p = m_data.top(); + p->set_in_queue(false); + m_data.pop(); +} + + void pob_queue::set_root(pob& root) { m_root = &root; @@ -156,19 +168,28 @@ void pob_queue::set_root(pob& root) reset(); } -pob_queue::~pob_queue() {} - void pob_queue::reset() { - while (!m_obligations.empty()) { m_obligations.pop(); } - if (m_root) { m_obligations.push(m_root); } + while (!m_data.empty()) { + pob *p = m_data.top(); + m_data.pop(); + p->set_in_queue(false); + } + if (m_root) { + SASSERT(!m_root->is_in_queue()); + m_root->set_in_queue(true); + m_data.push(m_root.get()); + } } void pob_queue::push(pob &n) { - TRACE("pob_queue", - tout << "pob_queue::push(" << n.post()->get_id() << ")\n";); - m_obligations.push (&n); - n.get_context().new_pob_eh(&n); + if (!n.is_in_queue()) { + TRACE("pob_queue", + tout << "pob_queue::push(" << n.post()->get_id() << ")\n";); + n.set_in_queue(true); + m_data.push (&n); + n.get_context().new_pob_eh(&n); + } } // ---------------- @@ -266,6 +287,8 @@ pob *derivation::create_next_child(model &mdl) m_evars.reset(); pt().mbp(vars, m_trans, mdl, true, pt().get_context().use_ground_pob()); + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); m_evars.append (vars); vars.reset(); } @@ -295,6 +318,8 @@ pob *derivation::create_next_child(model &mdl) vars.append(m_evars); pt().mbp(vars, post, mdl, true, pt().get_context().use_ground_pob()); + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); //qe::reduce_array_selects (*mev.get_model (), post); } else { @@ -398,6 +423,8 @@ pob *derivation::create_next_child () this->pt().mbp(vars, m_trans, *mdl, true, this->pt().get_context().use_ground_pob()); // keep track of implicitly quantified variables + CTRACE("spacer", !vars.empty(), + tout << "Failed to eliminate: " << vars << "\n";); m_evars.append (vars); vars.reset(); } @@ -462,8 +489,11 @@ void derivation::premise::set_summary (expr * summary, bool must, lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : m_ref_count(0), m(manager), m_body(body, m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl), - m_pob(nullptr), m_ctp(nullptr), m_external(false), m_bumped(0) { + m_zks(m), m_bindings(m), + m_pob(nullptr), m_ctp(nullptr), + m_lvl(lvl), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(WEAKNESS_MAX), + m_external(false), m_blocked(false) { SASSERT(m_body); normalize(m_body, m_body); } @@ -471,8 +501,11 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) : lemma::lemma(pob_ref const &p) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) { + m_zks(m), m_bindings(m), + m_pob(p), m_ctp(nullptr), + m_lvl(p->level()), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(p->weakness()), + m_external(false), m_blocked(false) { SASSERT(m_pob); m_pob->get_skolems(m_zks); add_binding(m_pob->get_binding()); @@ -482,8 +515,11 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : m_ref_count(0), m(p->get_ast_manager()), m_body(m), m_cube(m), - m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl), - m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) + m_zks(m), m_bindings(m), + m_pob(p), m_ctp(nullptr), + m_lvl(p->level()), m_init_lvl(m_lvl), + m_bumped(0), m_weakness(p->weakness()), + m_external(false), m_blocked(false) { if (m_pob) { m_pob->get_skolems(m_zks); @@ -510,7 +546,8 @@ void lemma::mk_expr_core() { SASSERT(!m_cube.empty()); m_body = ::mk_and(m_cube); // normalize works better with a cube - normalize(m_body, m_body); + normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */); + m_body = ::push_not(m_body); if (!m_zks.empty() && has_zk_const(m_body)) { @@ -820,7 +857,7 @@ const datalog::rule *pred_transformer::find_rule(model &model) { for (auto &kv : m_pt_rules) { app *tag = kv.m_value->tag(); - if (model.eval(tag->get_decl(), val) && m.is_true(val)) { + if (model.is_true_decl(tag->get_decl())) { return &kv.m_value->rule(); } } @@ -1162,7 +1199,16 @@ expr_ref pred_transformer::get_origin_summary (model &mdl, } // bail out of if the model is insufficient - if (!mdl.is_true(summary)) return expr_ref(m); + // (skip quantified lemmas cause we can't validate them in the model) + // TBD: for quantified lemmas use current instances + flatten_and(summary); + for (auto *s : summary) { + if (!is_quantifier(s) && !mdl.is_true(s)) { + TRACE("spacer", tout << "Summary not true in the model: " + << mk_pp(s, m) << "\n";); + return expr_ref(m); + } + } // -- pick an implicant expr_ref_vector lits(m); @@ -1347,7 +1393,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, if (is_sat == l_true || is_sat == l_undef) { if (core) { core->reset(); } - if (model) { + if (model && model->get()) { r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach); TRACE ("spacer", tout << "reachable " << "is_concrete " << is_concrete << " rused: "; @@ -1387,7 +1433,12 @@ bool pred_transformer::is_ctp_blocked(lemma *lem) { // -- find rule of the ctp const datalog::rule *r; r = find_rule(*ctp); - if (r == nullptr) {return false;} + if (r == nullptr) { + // no rules means lemma is blocked forever because + // it does not satisfy some derived facts + lem->set_blocked(true); + return true; + } // -- find predicates along the rule find_predecessors(*r, m_predicates); @@ -1410,6 +1461,8 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem, unsigned& solver_level, expr_ref_vector* core) { + if (lem->is_blocked()) return false; + m_stats.m_num_is_invariant++; if (is_ctp_blocked(lem)) { m_stats.m_num_ctp_blocked++; @@ -1451,7 +1504,7 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem, SASSERT (level <= solver_level); } else if (r == l_true) { - // optionally remove unused symbols from the model + // TBD: optionally remove unused symbols from the model if (mdl_ref_ptr) {lem->set_ctp(*mdl_ref_ptr);} } else {lem->reset_ctp();} @@ -2120,25 +2173,17 @@ void pred_transformer::frames::simplify_formulas () /// pred_transformer::pobs -pob* pred_transformer::pobs::mk_pob(pob *parent, - unsigned level, unsigned depth, - expr *post, app_ref_vector const &b) { - - if (!m_pt.ctx.reuse_pobs()) { - pob* n = alloc(pob, parent, m_pt, level, depth); - n->set_post(post, b); - return n; - } - +pob* pred_transformer::pob_manager::mk_pob(pob *parent, + unsigned level, unsigned depth, + expr *post, + app_ref_vector const &b) { // create a new pob and set its post to normalize it pob p(parent, m_pt, level, depth, false); p.set_post(post, b); if (m_pobs.contains(p.post())) { - auto &buf = m_pobs[p.post()]; - for (unsigned i = 0, sz = buf.size(); i < sz; ++i) { - pob *f = buf.get(i); - if (f->parent() == parent) { + for (auto *f : m_pobs[p.post()]) { + if (f->parent() == parent && !f->is_in_queue()) { f->inherit(p); return f; } @@ -2160,7 +2205,21 @@ pob* pred_transformer::pobs::mk_pob(pob *parent, return n; } - +pob* pred_transformer::pob_manager::find_pob(pob* parent, expr *post) { + pob p(parent, m_pt, 0, 0, false); + p.set_post(post); + pob *res = nullptr; + if (m_pobs.contains(p.post())) { + for (auto *f : m_pobs[p.post()]) { + if (f->parent() == parent) { + // try to find pob not already in queue + if (!f->is_in_queue()) return f; + res = f; + } + } + } + return res; +} // ---------------- @@ -2207,7 +2266,6 @@ void context::updt_params() { m_use_ctp = m_params.spacer_ctp(); m_use_inc_clause = m_params.spacer_use_inc_clause(); m_blast_term_ite = m_params.spacer_blast_term_ite(); - m_reuse_pobs = m_params.spacer_reuse_pobs(); m_use_ind_gen = m_params.spacer_use_inductive_generalizer(); m_use_array_eq_gen = m_params.spacer_use_array_eq_generalizer(); m_validate_lemmas = m_params.spacer_validate_lemmas(); @@ -3055,27 +3113,19 @@ bool context::check_reachability () } SASSERT (m_pob_queue.top ()); - // -- remove all closed nodes and updated all dirty nodes + // -- remove all closed nodes // -- this is necessary because there is no easy way to // -- remove nodes from the priority queue. - while (m_pob_queue.top ()->is_closed () || - m_pob_queue.top()->is_dirty()) { - pob_ref n = m_pob_queue.top (); - m_pob_queue.pop (); - if (n->is_closed()) { - IF_VERBOSE (1, - verbose_stream () << "Deleting closed node: " - << n->pt ().head ()->get_name () - << "(" << n->level () << ", " << n->depth () << ")" - << " " << n->post ()->get_id () << "\n";); - if (m_pob_queue.is_root(*n)) { return true; } - SASSERT (m_pob_queue.top ()); - } else if (n->is_dirty()) { - n->clean (); - // -- the node n might not be at the top after it is cleaned - m_pob_queue.push (*n); - } else - { UNREACHABLE(); } + while (m_pob_queue.top ()->is_closed ()) { + pob_ref n = m_pob_queue.top(); + m_pob_queue.pop(); + IF_VERBOSE (1, + verbose_stream () << "Deleting closed node: " + << n->pt ().head ()->get_name () + << "(" << n->level () << ", " << n->depth () << ")" + << " " << n->post ()->get_id () << "\n";); + if (m_pob_queue.is_root(*n)) {return true;} + SASSERT (m_pob_queue.top ()); } SASSERT (m_pob_queue.top ()); @@ -3169,6 +3219,7 @@ bool context::is_reachable(pob &n) unsigned num_reuse_reach = 0; unsigned saved = n.level (); + // TBD: don't expose private field n.m_level = infty_level (); lbool res = n.pt().is_reachable(n, nullptr, &mdl, uses_level, is_concrete, r, @@ -3413,10 +3464,21 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) // Optionally update the node to be the negation of the lemma if (v && m_use_lemma_as_pob) { - n.new_post (mk_and(lemma->get_cube())); - n.set_farkas_generalizer (false); - // XXX hack while refactoring is in progress - n.clean(); + expr_ref c(m); + c = mk_and(lemma->get_cube()); + // check that the post condition is different + if (c != n.post()) { + pob *f = n.pt().find_pob(n.parent(), c); + // skip if a similar pob is already in the queue + if (f != &n && (!f || !f->is_in_queue())) { + f = n.pt().mk_pob(n.parent(), n.level(), + n.depth(), c, n.get_binding()); + SASSERT(!f->is_in_queue()); + f->inc_level(); + //f->set_farkas_generalizer(false); + out.push_back(f); + } + } } // schedule the node to be placed back in the queue @@ -3434,7 +3496,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) } case l_undef: // something went wrong - if (n.weakness() < 100 /* MAX_WEAKENSS */) { + if (n.weakness() < 10 /* MAX_WEAKENSS */) { bool has_new_child = false; SASSERT(m_weak_abs); m_stats.m_expand_pob_undef++; @@ -3932,7 +3994,7 @@ bool context::is_inductive() { } /// pob_lt operator -inline bool pob_lt::operator() (const pob *pn1, const pob *pn2) const +inline bool pob_lt_proc::operator() (const pob *pn1, const pob *pn2) const { SASSERT (pn1); SASSERT (pn2); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 37b035b98..36f898ed1 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -122,12 +122,14 @@ class lemma { expr_ref_vector m_cube; app_ref_vector m_zks; app_ref_vector m_bindings; + pob_ref m_pob; + model_ref m_ctp; // counter-example to pushing unsigned m_lvl; // current level of the lemma unsigned m_init_lvl; // level at which lemma was created - pob_ref m_pob; - model_ref m_ctp; // counter-example to pushing - bool m_external; - unsigned m_bumped; + unsigned m_bumped:16; + unsigned m_weakness:16; + unsigned m_external:1; + unsigned m_blocked:1; void mk_expr_core(); void mk_cube_core(); @@ -154,12 +156,15 @@ public: bool has_pob() {return m_pob;} pob_ref &get_pob() {return m_pob;} - inline unsigned weakness(); + unsigned weakness() {return m_weakness;} void add_skolem(app *zk, app* b); - inline void set_external(bool ext){m_external = ext;} - inline bool external() { return m_external;} + void set_external(bool ext){m_external = ext;} + bool external() { return m_external;} + + bool is_blocked() {return m_blocked;} + void set_blocked(bool v) {m_blocked=v;} bool is_inductive() const {return is_infty_level(m_lvl);} unsigned level () const {return m_lvl;} @@ -268,18 +273,31 @@ class pred_transformer { }; /** - manager of proof-obligations (pobs) + manager of proof-obligations (pob_manager) + + Pobs are determined uniquely by their post-condition and a parent pob. + They are managed by pob_manager and remain live through the + life of the manager */ - class pobs { + class pob_manager { + // a buffer that contains space for one pob and allocates more + // space if needed typedef ptr_buffer pob_buffer; + // Type for the map from post-conditions to pobs. The common + // case is that each post-condition corresponds to a single + // pob. Other cases are handled by expanding the buffer typedef obj_map expr2pob_buffer; + // parent predicate transformer pred_transformer &m_pt; + // map from post-conditions to pobs expr2pob_buffer m_pobs; + + // a store pob_ref_vector m_pinned; public: - pobs(pred_transformer &pt) : m_pt(pt) {} + pob_manager(pred_transformer &pt) : m_pt(pt) {} pob* mk_pob(pob *parent, unsigned level, unsigned depth, expr *post, app_ref_vector const &b); @@ -290,6 +308,7 @@ class pred_transformer { } unsigned size() const {return m_pinned.size();} + pob* find_pob(pob* parent, expr *post); }; class pt_rule { @@ -361,7 +380,7 @@ class pred_transformer { ptr_vector m_rules; // rules used to derive transformer scoped_ptr m_solver; // solver context ref m_reach_solver; // context for reachability facts - pobs m_pobs; // proof obligations created so far + pob_manager m_pobs; // proof obligations created so far frames m_frames; // frames with lemmas reach_fact_ref_vector m_reach_facts; // reach facts unsigned m_rf_init_sz; // number of reach fact from INIT @@ -481,6 +500,9 @@ public: expr *post, app_ref_vector const &b){ return m_pobs.mk_pob(parent, level, depth, post, b); } + pob* find_pob(pob *parent, expr *post) { + return m_pobs.find_pob(parent, post); + } pob* mk_pob(pob *parent, unsigned level, unsigned depth, expr *post) { @@ -548,6 +570,7 @@ public: * A proof obligation. */ class pob { + // TBD: remove this friend class context; unsigned m_ref_count; /// parent node @@ -562,14 +585,15 @@ class pob { /// new post to be swapped in for m_post expr_ref m_new_post; /// level at which to decide the post - unsigned m_level; - - unsigned m_depth; + unsigned m_level:16; + unsigned m_depth:16; /// whether a concrete answer to the post is found - bool m_open; + unsigned m_open:1; /// whether to use farkas generalizer to construct a lemma blocking this node - bool m_use_farkas; + unsigned m_use_farkas:1; + /// true if this pob is in pob_queue + unsigned m_in_queue:1; unsigned m_weakness; /// derivation representing the position of this node in the parent's rule @@ -584,17 +608,25 @@ class pob { // depth -> watch std::map m_expand_watches; unsigned m_blocked_lvl; + public: pob (pob* parent, pred_transformer& pt, unsigned level, unsigned depth=0, bool add_to_parent=true); ~pob() {if (m_parent) { m_parent->erase_child(*this); }} + // TBD: move into constructor and make private + void set_post(expr *post, app_ref_vector const &binding); + void set_post(expr *post); + unsigned weakness() {return m_weakness;} void bump_weakness() {m_weakness++;} void reset_weakness() {m_weakness=0;} - void inc_level () {m_level++; m_depth++;reset_weakness();} + void inc_level () { + SASSERT(!is_in_queue()); + m_level++; m_depth++;reset_weakness(); + } void inherit(pob const &p); void set_derivation (derivation *d) {m_derivation = d;} @@ -614,32 +646,25 @@ public: unsigned level () const { return m_level; } unsigned depth () const {return m_depth;} unsigned width () const {return m_kids.size();} - unsigned blocked_at(unsigned lvl=0){return (m_blocked_lvl = std::max(lvl, m_blocked_lvl)); } + unsigned blocked_at(unsigned lvl=0){ + return (m_blocked_lvl = std::max(lvl, m_blocked_lvl)); + } + bool is_in_queue() const {return m_in_queue;} + void set_in_queue(bool v) {m_in_queue = v;} bool use_farkas_generalizer () const {return m_use_farkas;} void set_farkas_generalizer (bool v) {m_use_farkas = v;} expr* post() const { return m_post.get (); } - void set_post(expr *post); - void set_post(expr *post, app_ref_vector const &binding); - - /// indicate that a new post should be set for the node - void new_post(expr *post) {if (post != m_post) {m_new_post = post;}} - /// true if the node needs to be updated outside of the priority queue - bool is_dirty () {return m_new_post;} - /// clean a dirty node - void clean(); - - void reset () {clean (); m_derivation = nullptr; m_open = true;} bool is_closed () const { return !m_open; } void close(); - const ptr_vector &children() {return m_kids;} + const ptr_vector &children() const {return m_kids;} void add_child (pob &v) {m_kids.push_back (&v);} void erase_child (pob &v) {m_kids.erase (&v);} - const ptr_vector &lemmas() {return m_lemmas;} + const ptr_vector &lemmas() const {return m_lemmas;} void add_lemma(lemma* new_lemma) {m_lemmas.push_back(new_lemma);} bool is_ground () const { return m_binding.empty (); } @@ -652,8 +677,14 @@ public: */ void get_skolems(app_ref_vector& v); - void on_expand() { m_expand_watches[m_depth].start(); if (m_parent.get()){m_parent.get()->on_expand();} } - void off_expand() { m_expand_watches[m_depth].stop(); if (m_parent.get()){m_parent.get()->off_expand();} }; + void on_expand() { + m_expand_watches[m_depth].start(); + if (m_parent.get()){m_parent.get()->on_expand();} + } + void off_expand() { + m_expand_watches[m_depth].stop(); + if (m_parent.get()){m_parent.get()->off_expand();} + } double get_expand_time(unsigned depth) { return m_expand_watches[depth].get_seconds();} void inc_ref () {++m_ref_count;} @@ -662,6 +693,7 @@ public: if (m_ref_count == 0) {dealloc(this);} } + std::ostream &display(std::ostream &out, bool full = false) const; class on_expand_event { pob &m_p; @@ -671,26 +703,20 @@ public: }; }; +inline std::ostream &operator<<(std::ostream &out, pob const &p) { + return p.display(out); +} -struct pob_lt : - public std::binary_function -{bool operator() (const pob *pn1, const pob *pn2) const;}; - -struct pob_gt : - public std::binary_function { - pob_lt lt; - bool operator() (const pob *n1, const pob *n2) const - {return lt(n2, n1);} +struct pob_lt_proc : public std::binary_function { + bool operator() (const pob *pn1, const pob *pn2) const; }; -struct pob_ref_gt : - public std::binary_function { - pob_gt gt; - bool operator() (const pob_ref &n1, const pob_ref &n2) const - {return gt (n1.get (), n2.get ());} +struct pob_gt_proc : public std::binary_function { + bool operator() (const pob *n1, const pob *n2) const { + return pob_lt_proc()(n2, n1); + } }; -inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;} /** */ class derivation { @@ -767,36 +793,41 @@ public: class pob_queue { + + typedef std::priority_queue, pob_gt_proc> pob_queue_ty; pob_ref m_root; unsigned m_max_level; unsigned m_min_depth; - std::priority_queue, - pob_ref_gt> m_obligations; + pob_queue_ty m_data; public: pob_queue(): m_root(nullptr), m_max_level(0), m_min_depth(0) {} - ~pob_queue(); + ~pob_queue() {} void reset(); - pob * top (); - void pop () {m_obligations.pop ();} + pob* top(); + void pop(); void push (pob &n); void inc_level () { - SASSERT (!m_obligations.empty () || m_root); + SASSERT (!m_data.empty () || m_root); m_max_level++; m_min_depth++; - if (m_root && m_obligations.empty()) { m_obligations.push(m_root); } + if (m_root && m_data.empty()) { + SASSERT(!m_root->is_in_queue()); + m_root->set_in_queue(true); + m_data.push(m_root.get()); + } } pob& get_root() const {return *m_root.get ();} void set_root(pob& n); - bool is_root (pob& n) const {return m_root.get () == &n;} + bool is_root(pob& n) const {return m_root.get () == &n;} unsigned max_level() const {return m_max_level;} unsigned min_depth() const {return m_min_depth;} - size_t size() const {return m_obligations.size();} + size_t size() const {return m_data.size();} }; @@ -910,7 +941,6 @@ class context { bool m_use_ctp; bool m_use_inc_clause; bool m_blast_term_ite; - bool m_reuse_pobs; bool m_use_ind_gen; bool m_use_array_eq_gen; bool m_validate_lemmas; @@ -1007,7 +1037,6 @@ public: bool use_ctp() {return m_use_ctp;} bool use_inc_clause() {return m_use_inc_clause;} bool blast_term_ite() {return m_blast_term_ite;} - bool reuse_pobs() {return m_reuse_pobs;} bool elim_aux() {return m_elim_aux;} bool reach_dnf() {return m_reach_dnf;} diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index a68db4c0a..27b8ee357 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -322,6 +322,24 @@ void iuc_solver::get_iuc(expr_ref_vector &core) // -- new hypothesis reducer else { +#if 0 + static unsigned bcnt = 0; + { + bcnt++; + TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";); + if (bcnt == 123) { + std::ofstream ofs; + ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot"); + iuc_proof iuc_pf_before(m, res.get(), core_lits); + iuc_pf_before.display_dot(ofs); + ofs.close(); + + proof_checker pc(m); + expr_ref_vector side(m); + ENSURE(pc.check(res, side)); + } + } +#endif scoped_watch _t_ (m_hyp_reduce2_sw); // pre-process proof for better iuc extraction @@ -356,6 +374,22 @@ void iuc_solver::get_iuc(expr_ref_vector &core) iuc_proof iuc_pf(m, res, core_lits); +#if 0 + static unsigned cnt = 0; + { + cnt++; + TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";); + if (cnt == 123) { + std::ofstream ofs; + ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot"); + iuc_pf.display_dot(ofs); + ofs.close(); + proof_checker pc(m); + expr_ref_vector side(m); + ENSURE(pc.check(res, side)); + } + } +#endif unsat_core_learner learner(m, iuc_pf); unsat_core_plugin* plugin; diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 7bd21a1b5..004ea6754 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m, m_use_push_bg(p.spacer_keep_proxy()) { + m_random.set_seed(p.spacer_random_seed()); m_solvers[0] = solver0; m_solvers[1] = solver1; @@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, hard.append(_hard.size(), _hard.c_ptr()); flatten_and(hard); + shuffle(hard.size(), hard.c_ptr(), m_random); + m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get(); // can be disabled if use_push_bg == true diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 1db65dc3e..0eed969bd 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -61,6 +61,8 @@ private: bool m_use_push_bg; unsigned m_current_level; // set when m_in_level + random_gen m_random; + void assert_level_atoms(unsigned level); void ensure_level(unsigned lvl); diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index f66fe7b29..dd40d8546 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -80,6 +80,51 @@ struct index_lt_proc : public std::binary_function { } }; + + struct has_nlira_functor { + struct found{}; + + ast_manager &m; + arith_util u; + + has_nlira_functor(ast_manager &_m) : m(_m), u(m) {} + + void operator()(var *) {} + void operator()(quantifier *) {} + void operator()(app *n) { + family_id fid = n->get_family_id(); + if (fid != u.get_family_id()) return; + + switch(n->get_decl_kind()) { + case OP_MUL: + if (n->get_num_args() != 2) + throw found(); + if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1))) + throw found(); + return; + case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD: + if (!u.is_numeral(n->get_arg(1))) + throw found(); + return; + default: + return; + } + return; + } + }; + + bool has_nlira(expr_ref_vector &v) { + has_nlira_functor fn(v.m()); + expr_fast_mark1 visited; + try { + for (expr *e : v) + quick_for_each_expr(fn, visited, e); + } + catch (has_nlira_functor::found e) { + return true; + } + return false; + } } namespace spacer { @@ -114,7 +159,7 @@ void lemma_quantifier_generalizer::find_candidates(expr *e, if (!contains_selects(e, m)) return; app_ref_vector indices(m); - get_select_indices(e, indices, m); + get_select_indices(e, indices); app_ref_vector extra(m); expr_sparse_mark marked_args; @@ -155,7 +200,7 @@ bool lemma_quantifier_generalizer::match_sk_idx(expr *e, app_ref_vector const &z if (!contains_selects(e, m)) return false; app_ref_vector indicies(m); - get_select_indices(e, indicies, m); + get_select_indices(e, indicies); if (indicies.size() > 2) return false; unsigned i=0; @@ -191,9 +236,15 @@ expr* times_minus_one(expr *e, arith_util &arith) { Find sub-expression of the form (select A (+ sk!0 t)) and replaces (+ sk!0 t) --> sk!0 and sk!0 --> (+ sk!0 (* (- 1) t)) - Current implementation is an ugly hack for one special case + + rewrites bind to (+ bsk!0 t) where bsk!0 is the original binding for sk!0 + + Current implementation is an ugly hack for one special + case. Should be rewritten based on an equality solver from qe */ -void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector const &zks, expr_ref &bind) { +void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, + app_ref_vector const &zks, + expr_ref &bind) { if (zks.size() != 1) return; arith_util arith(m); @@ -219,8 +270,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector kids_bind.push_back(bind); } else { - kids.push_back (times_minus_one(arg, arith)); - kids_bind.push_back (times_minus_one(arg, arith)); + kids.push_back(times_minus_one(arg, arith)); + kids_bind.push_back(arg); } } if (!found) continue; @@ -228,7 +279,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector rep = arith.mk_add(kids.size(), kids.c_ptr()); bind = arith.mk_add(kids_bind.size(), kids_bind.c_ptr()); TRACE("spacer_qgen", - tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n";); + tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n" + << "bind is: " << bind << "\n";); break; } } @@ -255,15 +307,17 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector lb and ub are null if no bound was found */ -void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var *var, +void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, + var *var, expr_ref_vector &gnd_cube, expr_ref_vector &abs_cube, - expr *&lb, expr *&ub, unsigned &stride) { + expr *&lb, expr *&ub, + unsigned &stride) { // create an abstraction function that maps candidate term to variables expr_safe_replace sub(m); // term -> var - sub.insert(term , var); + sub.insert(term, var); rational val; if (m_arith.is_numeral(term, val)) { bool is_int = val.is_int(); @@ -285,19 +339,17 @@ void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var for (expr *lit : m_cube) { expr_ref abs_lit(m); - sub (lit, abs_lit); - if (lit == abs_lit) { - gnd_cube.push_back(lit); - } + sub(lit, abs_lit); + if (lit == abs_lit) {gnd_cube.push_back(lit);} else { expr *e1, *e2; // generalize v=num into v>=num if (m.is_eq(abs_lit, e1, e2) && (e1 == var || e2 == var)) { - if (m_arith.is_numeral(e1)) { - abs_lit = m_arith.mk_ge (var, e1); + if (m_arith.is_numeral(e1)) { + abs_lit = m_arith.mk_ge(var, e1); } else if (m_arith.is_numeral(e2)) { abs_lit = m_arith.mk_ge(var, e2); - } + } } abs_cube.push_back(abs_lit); if (contains_selects(abs_lit, m)) { @@ -454,9 +506,15 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride); if (abs_cube.empty()) {return false;} + if (has_nlira(abs_cube)) { + TRACE("spacer_qgen", + tout << "non-linear expression: " << abs_cube << "\n";); + return false; + } TRACE("spacer_qgen", tout << "abs_cube is: " << mk_and(abs_cube) << "\n"; + tout << "term: " << mk_pp(term, m) << "\n"; tout << "lb = "; if (lb) tout << mk_pp(lb, m); else tout << "none"; tout << "\n"; @@ -464,7 +522,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { if (ub) tout << mk_pp(ub, m); else tout << "none"; tout << "\n";); - if (!lb && !ub) + if (!lb && !ub) return false; // -- guess lower or upper bound if missing @@ -473,7 +531,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { lb = abs_cube.back(); } if (!ub) { - abs_cube.push_back (m_arith.mk_lt(var, term)); + abs_cube.push_back (m_arith.mk_le(var, term)); ub = abs_cube.back(); } @@ -489,10 +547,10 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { TRACE("spacer_qgen", tout << "mod=" << mod << " init=" << init << " stride=" << stride << "\n"; tout.flush();); - abs_cube.push_back(m.mk_eq( - m_arith.mk_mod(var, m_arith.mk_numeral(rational(stride), true)), - m_arith.mk_numeral(rational(mod), true))); - } + abs_cube.push_back + (m.mk_eq(m_arith.mk_mod(var, + m_arith.mk_numeral(rational(stride), true)), + m_arith.mk_numeral(rational(mod), true)));} // skolemize expr_ref gnd(m); @@ -512,21 +570,21 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { << "New CUBE is: " << gnd_cube << "\n";); SASSERT(zks.size() >= static_cast(m_offset)); - // lift quantified variables to top of select + // lift quantified variables to top of select expr_ref ext_bind(m); ext_bind = term; cleanup(gnd_cube, zks, ext_bind); - // XXX better do that check before changing bind in cleanup() - // XXX Or not because substitution might introduce _n variable into bind + // XXX better do that check before changing bind in cleanup() + // XXX Or not because substitution might introduce _n variable into bind if (m_ctx.get_manager().is_n_formula(ext_bind)) { - // XXX this creates an instance, but not necessarily the needed one + // XXX this creates an instance, but not necessarily the needed one - // XXX This is sound because any instance of - // XXX universal quantifier is sound + // XXX This is sound because any instance of + // XXX universal quantifier is sound - // XXX needs better long term solution. leave - // comment here for the future + // XXX needs better long term solution. leave + // comment here for the future m_ctx.get_manager().formula_n2o(ext_bind, ext_bind, 0); } @@ -542,46 +600,50 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { return false; } -bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &c, expr_ref &pattern, unsigned &stride) { +bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &cube, + expr_ref &pattern, + unsigned &stride) { expr_ref tmp(m); - tmp = mk_and(c); + tmp = mk_and(cube); normalize(tmp, tmp, false, true); - c.reset(); - flatten_and(tmp, c); + cube.reset(); + flatten_and(tmp, cube); app_ref_vector indices(m); - get_select_indices(pattern, indices, m); + get_select_indices(pattern, indices); - // TODO - if (indices.size() > 1) - return false; + CTRACE("spacer_qgen", indices.empty(), + tout << "Found no select indices in: " << pattern << "\n";); + + // TBD: handle multi-dimensional arrays and literals with multiple + // select terms + if (indices.size() != 1) return false; app *p_index = indices.get(0); - if (is_var(p_index)) return false; - std::vector instances; - for (expr* lit : c) { + unsigned_vector instances; + for (expr* lit : cube) { if (!contains_selects(lit, m)) continue; indices.reset(); - get_select_indices(lit, indices, m); + get_select_indices(lit, indices); - // TODO: - if (indices.size() > 1) + // TBD: handle multi-dimensional arrays + if (indices.size() != 1) continue; app *candidate = indices.get(0); unsigned size = p_index->get_num_args(); unsigned matched = 0; - for (unsigned p=0; p < size; p++) { + for (unsigned p = 0; p < size; p++) { expr *arg = p_index->get_arg(p); if (is_var(arg)) { rational val; - if (p < candidate->get_num_args() && - m_arith.is_numeral(candidate->get_arg(p), val) && + if (p < candidate->get_num_args() && + m_arith.is_numeral(candidate->get_arg(p), val) && val.is_unsigned()) { instances.push_back(val.get_unsigned()); } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 42b40c665..ec01218f1 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -666,9 +666,6 @@ namespace { flatten_and(out, v); if (v.size() > 1) { - // sort arguments of the top-level and - std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); - if (use_simplify_bounds) { // remove redundant inequalities simplify_bounds(v); @@ -680,6 +677,8 @@ namespace { v.reset(); egraph.to_lits(v); } + // sort arguments of the top-level and + std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); TRACE("spacer_normalize", tout << "Normalized:\n" @@ -900,17 +899,22 @@ namespace { struct collect_indices { app_ref_vector& m_indices; array_util a; - collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {} + collect_indices(app_ref_vector& indices): m_indices(indices), + a(indices.get_manager()) {} void operator()(expr* n) {} void operator()(app* n) { - if (a.is_select(n)) - for (unsigned i = 1; i < n->get_num_args(); ++i) - if (is_app(n->get_arg(i))) - m_indices.push_back(to_app(n->get_arg(i))); + if (a.is_select(n)) { + // for all but first argument + for (unsigned i = 1; i < n->get_num_args(); ++i) { + expr *arg = n->get_arg(i); + if (is_app(arg)) + m_indices.push_back(to_app(arg)); + } + } } }; - void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) { + void get_select_indices(expr* fml, app_ref_vector &indices) { collect_indices ci(indices); for_each_expr(ci, fml); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index 9912769c5..8da574d0e 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -121,7 +121,7 @@ namespace spacer { void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml); bool contains_selects (expr* fml, ast_manager& m); - void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); + void get_select_indices (expr* fml, app_ref_vector& indices); void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 3223706d4..da45d17ca 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -320,8 +320,8 @@ namespace eq { << "sz is " << sz << "\n" << "subst_map[inx]: " << mk_pp(m_subst_map.get(inx), m) << "\n";); SASSERT(m_subst_map.get(inx) == nullptr); - m_subst_map[inx] = r; m_subst.update_inv_binding_at(inx, r); + m_subst_map[inx] = std::move(r); } } @@ -470,7 +470,7 @@ namespace eq { m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } else if (!m.is_value(m_map[idx])) { // check if the new definition is simpler @@ -482,7 +482,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer ground else if (is_app(t) && to_app(t)->is_ground() && @@ -492,7 +492,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } // -- prefer constants else if (is_uninterp_const(t) @@ -501,7 +501,7 @@ namespace eq { m_pos2var[i] = idx; m_var2pos[idx] = i; m_map[idx] = t; - m_new_exprs.push_back(t); + m_new_exprs.push_back(std::move(t)); } TRACE ("qe_def", tout << "Replacing definition of VAR " << idx << " from " diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 5cf1206a3..e9ec3d4b7 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -200,7 +200,8 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - out << get_id() << ": " << m_expr << " - "; + out << get_id() << ": " << m_expr + << (is_root() ? " R" : "") << " - "; term const* r = &this->get_next(); while (r != this) { out << r->get_id() << " "; @@ -371,20 +372,20 @@ namespace qe { } void term_graph::merge(term &t1, term &t2) { - // -- merge might invalidate term2app cache - m_term2app.reset(); - m_pinned.reset(); - term *a = &t1.get_root(); term *b = &t2.get_root(); if (a == b) return; + // -- merge might invalidate term2app cache + m_term2app.reset(); + m_pinned.reset(); + if (a->get_class_size() > b->get_class_size()) { std::swap(a, b); } - // Remove parents of it from the cg table. + // Remove parents of b from the cg table. for (term* p : term::parents(b)) { if (!p->is_marked()) { p->set_mark(true); @@ -401,7 +402,7 @@ namespace qe { a->merge_eq_class(*b); // Insert parents of b's old equilvalence class into the cg table - for (term* p : term::parents(a)) { + for (term* p : term::parents(b)) { if (p->is_marked()) { term* p_old = m_cg_table.insert_if_not_there(p); p->set_mark(false); @@ -412,6 +413,7 @@ namespace qe { } } } + SASSERT(marks_are_clear()); } expr* term_graph::mk_app_core (expr *e) { @@ -484,10 +486,16 @@ namespace qe { } } + bool term_graph::marks_are_clear() { + for (term * t : m_terms) { + if (t->is_marked()) return false; + } + return true; + } + /// Order of preference for roots of equivalence classes /// XXX This should be factored out to let clients control the preference bool term_graph::term_lt(term const &t1, term const &t2) { - // prefer constants over applications // prefer uninterpreted constants over values // prefer smaller expressions over larger ones @@ -521,6 +529,7 @@ namespace qe { /// Choose better roots for equivalence classes void term_graph::pick_roots() { + SASSERT(marks_are_clear()); for (term* t : m_terms) { if (!t->is_marked() && t->is_root()) pick_root(*t); @@ -589,7 +598,7 @@ namespace qe { // prefer a node that resembles current child, // otherwise, pick a root representative, if present. if (m_term2app.find(ch->get_id(), e)) - kids.push_back(e); + kids.push_back(e); else if (m_root2rep.find(ch->get_root().get_id(), e)) kids.push_back(e); else diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 2ab234a96..0c66f4193 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -75,6 +75,7 @@ namespace qe { void pick_roots(); void reset_marks(); + bool marks_are_clear(); expr* mk_app_core(expr* a); expr_ref mk_app(term const &t); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index e2a9cbed4..978a1a8e1 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2000,7 +2000,8 @@ namespace smt { if (t->filter_candidates()) { for (enode* app : t->get_candidates()) { if (!app->is_marked() && app->is_cgr()) { - execute_core(t, app); + if (m_context.resource_limits_exceeded() || !execute_core(t, app)) + return; app->set_mark(); } } @@ -2014,14 +2015,15 @@ namespace smt { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (app->is_cgr()) { TRACE("trigger_bug", tout << "is_cgr\n";); - execute_core(t, app); + if (m_context.resource_limits_exceeded() || !execute_core(t, app)) + return; } } } } // init(t) must be invoked before execute_core - void execute_core(code_tree * t, enode * n); + bool execute_core(code_tree * t, enode * n); // Return the min, max generation of the enodes in m_pattern_instances. @@ -2250,7 +2252,7 @@ namespace smt { display_instr_input_reg(out, m_pc); } - void interpreter::execute_core(code_tree * t, enode * n) { + bool interpreter::execute_core(code_tree * t, enode * n) { TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";); unsigned since_last_check = 0; @@ -2494,7 +2496,7 @@ namespace smt { #define ON_MATCH(NUM) \ m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \ if (m_context.get_cancel_flag()) { \ - return; \ + return false; \ } \ m_mam.on_match(static_cast(m_pc)->m_qa, \ static_cast(m_pc)->m_pat, \ @@ -2647,7 +2649,7 @@ namespace smt { #ifdef _PROFILE_MAM t->get_watch().stop(); #endif - return; // no more alternatives + return true; // no more alternatives } backtrack_point & bp = m_backtrack_stack[m_top - 1]; m_max_generation = bp.m_old_max_generation; @@ -2675,7 +2677,7 @@ namespace smt { #ifdef _PROFILE_MAM t->get_watch().stop(); #endif - return; + return false; } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index fd9b27069..73a3c27bd 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1594,7 +1594,7 @@ namespace smt { for (literal lit : m_assigned_literals) { expr_ref e(m_manager); literal2expr(lit, e); - assignments.push_back(e); + assignments.push_back(std::move(e)); } } @@ -4180,7 +4180,7 @@ namespace smt { SASSERT(get_justification(guess.var()).get_kind() == b_justification::AXIOM); expr_ref lit(m_manager); literal2expr(guess, lit); - result.push_back(lit); + result.push_back(std::move(lit)); } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 48b689bd7..4f7c8073e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1115,8 +1115,6 @@ namespace smt { void internalize_assertions(); - void assert_assumption(expr * a); - bool validate_assumptions(expr_ref_vector const& asms); void init_assumptions(expr_ref_vector const& asms); @@ -1129,8 +1127,6 @@ namespace smt { void reset_assumptions(); - void reset_clause(); - void add_theory_assumptions(expr_ref_vector & theory_assumptions); lbool mk_unsat_core(lbool result); @@ -1585,8 +1581,6 @@ namespace smt { //proof * const * get_asserted_formula_proofs() const { return m_asserted_formulas.get_formula_proofs(); } - void get_assumptions_core(ptr_vector & result); - void get_assertions(ptr_vector & result) { m_asserted_formulas.get_assertions(result); } void display(std::ostream & out) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 19247c1d9..29c624bb2 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -409,11 +409,11 @@ namespace smt { for (unsigned i = 0; i < num_antecedents; i++) { literal l = antecedents[i]; literal2expr(l, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (consequent != false_literal) { literal2expr(~consequent, n); - fmls.push_back(n); + fmls.push_back(std::move(n)); } if (logic != symbol::null) out << "(set-logic " << logic << ")\n"; visitor.collect(fmls); diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 4ac176a2b..fc9307792 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -281,7 +281,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { expr_ref l(m); ctx.literal2expr(m_literals[i], l); - lits.push_back(l); + lits.push_back(std::move(l)); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); @@ -407,12 +407,7 @@ namespace smt { for (unsigned i = 0; i < m_num_literals; i++) { bool sign = GET_TAG(m_literals[i]) != 0; expr * v = UNTAG(expr*, m_literals[i]); - expr_ref l(m); - if (sign) - l = m.mk_not(v); - else - l = v; - lits.push_back(l); + lits.push_back(sign ? m.mk_not(v) : v); } if (lits.size() == 1) return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.c_ptr()); diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 9dacfb5ce..598bb6c02 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -101,9 +101,11 @@ public: proof * get_proof() override { scoped_watch _t_(m_pool.m_proof_watch); if (!m_proof.get()) { - elim_aux_assertions pc(m_pred); m_proof = m_base->get_proof(); - pc(m, m_proof, m_proof); + if (m_proof) { + elim_aux_assertions pc(m_pred); + pc(m, m_proof, m_proof); + } } return m_proof; } diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 3bd28ad6d..a4e169856 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -62,7 +62,7 @@ public: TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n");); // running implementation - expr_ref_vector flas(m); + ptr_vector flas; const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); scoped_ptr uffree_solver = setup_sat(); diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h index f340d8886..1e6525a06 100644 --- a/src/util/ref_vector.h +++ b/src/util/ref_vector.h @@ -99,6 +99,13 @@ public: return *this; } + template + ref_vector_core& push_back(obj_ref && n) { + m_nodes.push_back(n.get()); + n.steal(); + return *this; + } + void pop_back() { SASSERT(!m_nodes.empty()); T * n = m_nodes.back(); @@ -253,6 +260,13 @@ public: return *this; } + template + element_ref & operator=(obj_ref && n) { + m_manager.dec_ref(m_ref); + m_ref = n.steal(); + return *this; + } + T * get() const { return m_ref; } @@ -288,9 +302,8 @@ public: return *this; } -private: // prevent abuse: - ref_vector & operator=(ref_vector const & other); + ref_vector & operator=(ref_vector const & other) = delete; }; template