diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b73f7a7a8..411fdd1e1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -455,7 +455,7 @@ def display_help(exit_code): print(" -v, --vsproj generate Visual Studio Project Files.") if IS_WINDOWS: print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") - print(" -j, --java generate Java bindinds.") + print(" -j, --java generate Java bindings.") print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") @@ -587,7 +587,7 @@ def set_z3py_dir(p): raise MKException("Python bindings directory '%s' does not exist" % full) Z3PY_SRC_DIR = full if VERBOSE: - print("Python bindinds directory was detected.") + print("Python bindings directory was detected.") _UNIQ_ID = 0 @@ -1151,7 +1151,11 @@ class DotNetDLLComponent(Component): out.write(' ') out.write(cs_file) out.write('\n') - out.write(' csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name)) + out.write(' csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name)) + if DEBUG_MODE: + out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-') + else: + out.write(' /optimize+') if VS_X64: out.write(' /platform:x64') else: @@ -1174,6 +1178,13 @@ class DotNetDLLComponent(Component): mk_dir(os.path.join(dist_path, 'bin')) shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name), '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name)) + shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name), + '%s.xml' % os.path.join(dist_path, 'bin', self.dll_name)) + if DEBUG_MODE: + shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name), + '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name)) + + def mk_unix_dist(self, build_path, dist_path): # Do nothing @@ -2511,7 +2522,11 @@ def mk_vs_proj(name, components): f.write(' \n') f.write(' Disabled\n') f.write(' WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') - f.write(' true\n') + if VS_PAR: + f.write(' false\n') + f.write(' true\n') + else: + f.write(' true\n') f.write(' EnableFastChecks\n') f.write(' Level3\n') f.write(' MultiThreadedDebugDLL\n') @@ -2545,7 +2560,11 @@ def mk_vs_proj(name, components): f.write(' \n') f.write(' Disabled\n') f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') - f.write(' true\n') + if VS_PAR: + f.write(' false\n') + f.write(' true\n') + else: + f.write(' true\n') f.write(' EnableFastChecks\n') f.write(' Level3\n') f.write(' MultiThreadedDLL\n') diff --git a/scripts/update_api.py b/scripts/update_api.py index 6b5a14092..21f238ae9 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -420,7 +420,7 @@ def mk_dotnet(): NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] -Unwrapped = [ 'Z3_del_context' ] +Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ] def mk_dotnet_wrappers(): global Type2Str diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 8c89740ad..b8470839f 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -129,6 +129,7 @@ namespace api { for (unsigned i = 0; i < m_replay_stack.size(); ++i) { dealloc(m_replay_stack[i]); } + m_ast_trail.reset(); } reset_parser(); dealloc(m_solver); @@ -343,24 +344,21 @@ namespace api { void context::push() { get_smt_kernel().push(); - if (!m_user_ref_count) { - m_ast_lim.push_back(m_ast_trail.size()); - m_replay_stack.push_back(0); - } + m_ast_lim.push_back(m_ast_trail.size()); + m_replay_stack.push_back(0); } void context::pop(unsigned num_scopes) { for (unsigned i = 0; i < num_scopes; ++i) { - if (!m_user_ref_count) { - unsigned sz = m_ast_lim.back(); - m_ast_lim.pop_back(); - dealloc(m_replay_stack.back()); - m_replay_stack.pop_back(); - while (m_ast_trail.size() > sz) { - m_ast_trail.pop_back(); - } + unsigned sz = m_ast_lim.back(); + m_ast_lim.pop_back(); + dealloc(m_replay_stack.back()); + m_replay_stack.pop_back(); + while (m_ast_trail.size() > sz) { + m_ast_trail.pop_back(); } } + SASSERT(num_scopes <= get_smt_kernel().get_scope_level()); get_smt_kernel().pop(num_scopes); } diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 48e13d571..e06ad5192 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -38,6 +38,7 @@ Revision History: #include"iz3hash.h" #include"iz3pp.h" #include"iz3checker.h" +#include"scoped_proof.h" using namespace stl_ext; @@ -290,6 +291,99 @@ extern "C" { opts->map[name] = value; } + Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){ + Z3_TRY; + LOG_Z3_get_interpolant(c, pf, pat, p); + RESET_ERROR_CODE(); + + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); + mk_c(c)->save_object(v); + + ast *_pf = to_ast(pf); + ast *_pat = to_ast(pat); + + ptr_vector interp; + ptr_vector cnsts; // to throw away + + ast_manager &_m = mk_c(c)->m(); + + iz3interpolate(_m, + _pf, + cnsts, + _pat, + interp, + (interpolation_options_struct *) 0 // ignore params for now + ); + + // copy result back + for(unsigned i = 0; i < interp.size(); i++){ + v->m_ast_vector.push_back(interp[i]); + _m.dec_ref(interp[i]); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + + Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){ + Z3_TRY; + LOG_Z3_compute_interpolant(c, pat, p, out_interp, model); + RESET_ERROR_CODE(); + + + // params_ref &_p = to_params(p)->m_params; + params_ref _p; + _p.set_bool("proof", true); // this is currently useless + + scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE); + scoped_ptr sf = mk_smt_solver_factory(); + scoped_ptr m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null)); + m_solver.get()->updt_params(_p); // why do we have to do this? + + ast *_pat = to_ast(pat); + + ptr_vector interp; + ptr_vector cnsts; // to throw away + + ast_manager &_m = mk_c(c)->m(); + + model_ref m; + lbool _status = iz3interpolate(_m, + *(m_solver.get()), + _pat, + cnsts, + interp, + m, + 0 // ignore params for now + ); + + Z3_lbool status = of_lbool(_status); + + Z3_ast_vector_ref *v = 0; + *model = 0; + + if(_status == l_false){ + // copy result back + v = alloc(Z3_ast_vector_ref, mk_c(c)->m()); + mk_c(c)->save_object(v); + for(unsigned i = 0; i < interp.size(); i++){ + v->m_ast_vector.push_back(interp[i]); + _m.dec_ref(interp[i]); + } + } + else { + model_ref _m; + m_solver.get()->get_model(_m); + Z3_model_ref *crap = alloc(Z3_model_ref); + crap->m_model = _m.get(); + mk_c(c)->save_object(crap); + *model = of_model(crap); + } + + *out_interp = of_ast_vector(v); + + return status; + Z3_CATCH_RETURN(Z3_L_UNDEF); + } }; @@ -317,7 +411,7 @@ static void get_file_params(const char *filename, hash_mapm_params; mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); + s->m_solver->updt_params(p); } static void init_solver(Z3_context c, Z3_solver s) { diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index e0533fbd9..b81fb2f2c 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -40,7 +40,7 @@ extern "C" { LOG_Z3_pop(c, num_scopes); RESET_ERROR_CODE(); CHECK_SEARCHING(c); - if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) { + if (num_scopes > mk_c(c)->get_num_scopes()) { SET_ERROR_CODE(Z3_IOB); return; } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index fcbba1ff6..6fc59351a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3565,7 +3565,7 @@ namespace Microsoft.Z3 /// /// /// The list of all configuration parameters can be obtained using the Z3 executable: - /// z3.exe -ini? + /// z3.exe -p /// Only a few configuration parameters are mutable once the context is created. /// An exception is thrown when trying to modify an immutable parameter. /// @@ -3691,7 +3691,7 @@ namespace Microsoft.Z3 internal Optimize.DecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Optimize_DRQ; } } - internal uint refCount = 0; + internal long refCount = 0; /// /// Finalizer. diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index e8654ce21..8e474041a 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -19,6 +19,7 @@ Notes: using System; using System.Diagnostics.Contracts; +using System.Threading; namespace Microsoft.Z3 { @@ -50,8 +51,7 @@ namespace Microsoft.Z3 if (m_ctx != null) { - m_ctx.refCount--; - if (m_ctx.refCount == 0) + if (Interlocked.Decrement(ref m_ctx.refCount) == 0) GC.ReRegisterForFinalize(m_ctx); m_ctx = null; } @@ -77,7 +77,7 @@ namespace Microsoft.Z3 { Contract.Requires(ctx != null); - ctx.refCount++; + Interlocked.Increment(ref ctx.refCount); m_ctx = ctx; } @@ -85,7 +85,7 @@ namespace Microsoft.Z3 { Contract.Requires(ctx != null); - ctx.refCount++; + Interlocked.Increment(ref ctx.refCount); m_ctx = ctx; IncRef(obj); m_n_obj = obj; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3504170fd..afd61dba1 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -7117,7 +7117,7 @@ def substitute(t, *m): if isinstance(m, tuple): m1 = _get_args(m) if isinstance(m1, list): - m = _get_args(m1) + m = m1 if __debug__: _z3_assert(is_expr(t), "Z3 expression expected") _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") @@ -7410,3 +7410,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None): dsz, dnames, ddecls = _dict2darray(decls, ctx) return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx) +def Interp(a,ctx=None): + """Create an interpolation operator. + + The argument is an interpolation pattern (see tree_interpolant). + + >>> x = Int('x') + >>> print Interp(x>0) + interp(x > 0) + """ + ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) + s = BoolSort(ctx) + a = s.cast(a) + return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx) + +def tree_interpolant(pat,p=None,ctx=None): + """Compute interpolant for a tree of formulas. + + The input is an interpolation pattern over a set of formulas C. + The pattern pat is a formula combining the formulas in C using + logical conjunction and the "interp" operator (see Interp). This + interp operator is logically the identity operator. It marks the + sub-formulas of the pattern for which interpolants should be + computed. The interpolant is a map sigma from marked subformulas + to formulas, such that, for each marked subformula phi of pat + (where phi sigma is phi with sigma(psi) substituted for each + subformula psi of phi such that psi in dom(sigma)): + + 1) phi sigma implies sigma(phi), and + + 2) sigma(phi) is in the common uninterpreted vocabulary between + the formulas of C occurring in phi and those not occurring in + phi + + and moreover pat sigma implies false. In the simplest case + an interpolant for the pattern "(and (interp A) B)" maps A + to an interpolant for A /\ B. + + The return value is a vector of formulas representing sigma. This + vector contains sigma(phi) for each marked subformula of pat, in + pre-order traversal. This means that subformulas of phi occur before phi + in the vector. Also, subformulas that occur multiply in pat will + occur multiply in the result vector. + + If pat is satisfiable, raises an object of class ModelRef + that represents a model of pat. + + If parameters p are supplied, these are used in creating the + solver that determines satisfiability. + + >>> x = Int('x') + >>> y = Int('y') + >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y)) + [Not(x >= 0), Not(y <= 2)] + + >>> g = And(Interp(x<0),x<2) + >>> try: + ... print tree_interpolant(g).sexpr() + ... except ModelRef as m: + ... print m.sexpr() + (define-fun x () Int + (- 1)) + """ + f = pat + ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) + ptr = (AstVectorObj * 1)() + mptr = (Model * 1)() + if p == None: + p = ParamsRef(ctx) + res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) + if res == Z3_L_FALSE: + return AstVector(ptr[0],ctx) + raise ModelRef(mptr[0], ctx) + +def binary_interpolant(a,b,p=None,ctx=None): + """Compute an interpolant for a binary conjunction. + + If a & b is unsatisfiable, returns an interpolant for a & b. + This is a formula phi such that + + 1) a implies phi + 2) b implies not phi + 3) All the uninterpreted symbols of phi occur in both a and b. + + If a & b is satisfiable, raises an object of class ModelRef + that represents a model of a &b. + + If parameters p are supplied, these are used in creating the + solver that determines satisfiability. + + x = Int('x') + print binary_interpolant(x<0,x>2) + Not(x >= 0) + """ + f = And(Interp(a),b) + return tree_interpolant(f,p,ctx)[0] + +def sequence_interpolant(v,p=None,ctx=None): + """Compute interpolant for a sequence of formulas. + + If len(v) == N, and if the conjunction of the formulas in v is + unsatisfiable, the interpolant is a sequence of formulas w + such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1: + + 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N) + 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i] + and v[i+1]..v[n] + + Requires len(v) >= 1. + + If a & b is satisfiable, raises an object of class ModelRef + that represents a model of a & b. + + If parameters p are supplied, these are used in creating the + solver that determines satisfiability. + + >>> x = Int('x') + >>> y = Int('y') + >>> print sequence_interpolant([x < 0, y == x , y > 2]) + [Not(x >= 0), Not(y >= 0)] + """ + f = v[0] + for i in range(1,len(v)): + f = And(Interp(f),v[i]) + return tree_interpolant(f,p,ctx) + diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index a9e6d6f7e..22da27e03 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3types.py @@ -113,3 +113,4 @@ class FuncEntryObj(ctypes.c_void_p): class RCFNumObj(ctypes.c_void_p): def __init__(self, e): self._as_parameter_ = e def from_param(obj): return obj + diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ebaa44339..57e4d3ec1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1392,6 +1392,16 @@ extern "C" { although some parameters can be changed using #Z3_update_param_value. All main interaction with Z3 happens in the context of a \c Z3_context. + In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects + are determined by the scope level of #Z3_push and #Z3_pop. + In other words, a Z3_ast object remains valid until there is a + call to Z3_pop that takes the current scope below the level where + the object was created. + + Note that all other reference counted objects, including Z3_model, + Z3_solver, Z3_func_interp have to be managed by the caller. + Their reference counts are not handled by the context. + \conly \sa Z3_del_context \conly \deprecated Use #Z3_mk_context_rc @@ -6841,6 +6851,13 @@ END_MLAPI_EXCLUDE /** \brief Create a new (incremental) solver. + The function #Z3_solver_get_model retrieves a model if the + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + The function #Z3_solver_get_model can also be used even + if the result is \c Z3_L_UNDEF, but the returned model + is not guaranteed to satisfy quantified assertions. + def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),)) */ Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c); @@ -6978,8 +6995,11 @@ END_MLAPI_EXCLUDE \brief Check whether the assertions in a given solver are consistent or not. The function #Z3_solver_get_model retrieves a model if the - assertions are not unsatisfiable (i.e., the result is not \c - Z3_L_FALSE) and model construction is enabled. + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + Note that if the call returns Z3_L_UNDEF, Z3 does not + ensure that calls to #Z3_solver_get_model succeed and any models + produced in this case are not guaranteed to satisfy the assertions. The function #Z3_solver_get_proof retrieves a proof if proof generation was enabled when the context was created, and the @@ -7290,7 +7310,7 @@ END_MLAPI_EXCLUDE \mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly \conly The caller is responsible for deleting the model using the function #Z3_del_model. - \conly \remark In constrast with the rest of the Z3 API, the reference counter of the + \conly \remark In contrast with the rest of the Z3 API, the reference counter of the \conly model is incremented. This is to guarantee backward compatibility. In previous \conly versions, models did not support reference counting. @@ -7403,6 +7423,11 @@ END_MLAPI_EXCLUDE \brief Delete a model object. \sa Z3_check_and_get_model + + \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model. + \conly The expected usage is that models created by that method are deleted using Z3_del_model. + \conly This is for backwards compatibility and in contrast to the rest of the API where + \conly callers are responsible for managing reference counts. \deprecated Subsumed by Z3_solver API @@ -7930,6 +7955,108 @@ END_MLAPI_EXCLUDE Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg); + /** Compute an interpolant from a refutation. This takes a proof of + "false" from a set of formulas C, and an interpolation + pattern. The pattern pat is a formula combining the formulas in C + using logical conjunction and the "interp" operator (see + #Z3_mk_interp). This interp operator is logically the identity + operator. It marks the sub-formulas of the pattern for which interpolants should + be computed. The interpolant is a map sigma from marked subformulas to + formulas, such that, for each marked subformula phi of pat (where phi sigma + is phi with sigma(psi) substituted for each subformula psi of phi such that + psi in dom(sigma)): + + 1) phi sigma implies sigma(phi), and + + 2) sigma(phi) is in the common uninterpreted vocabulary between + the formulas of C occurring in phi and those not occurring in + phi + + and moreover pat sigma implies false. In the simplest case + an interpolant for the pattern "(and (interp A) B)" maps A + to an interpolant for A /\ B. + + The return value is a vector of formulas representing sigma. The + vector contains sigma(phi) for each marked subformula of pat, in + pre-order traversal. This means that subformulas of phi occur before phi + in the vector. Also, subformulas that occur multiply in pat will + occur multiply in the result vector. + + In particular, calling Z3_get_interpolant on a pattern of the + form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will + result in a sequence interpolant for A_1, A_2,... A_N. + + Neglecting interp markers, the pattern must be a conjunction of + formulas in C, the set of premises of the proof. Otherwise an + error is flagged. + + Any premises of the proof not present in the pattern are + treated as "background theory". Predicate and function symbols + occurring in the background theory are treated as interpreted and + thus always allowed in the interpolant. + + Interpolant may not necessarily be computable from all + proofs. To be sure an interpolant can be computed, the proof + must be generated by an SMT solver for which interpoaltion is + supported, and the premises must be expressed using only + theories and operators for which interpolation is supported. + + Currently, the only SMT solver that is supported is the legacy + SMT solver. Such a solver is available as the default solver in + #Z3_context objects produced by #Z3_mk_interpolation_context. + Currently, the theories supported are equality with + uninterpreted functions, linear integer arithmetic, and the + theory of arrays (in SMT-LIB terms, this is AUFLIA). + Quantifiers are allowed. Use of any other operators (including + "labels") may result in failure to compute an interpolant from a + proof. + + Parameters: + + \param c logical context. + \param pf a refutation from premises (assertions) C + \param pat an interpolation pattern over C + \param p parameters + + def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS))) + */ + + Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p); + + /* Compute an interpolant for an unsatisfiable conjunction of formulas. + + This takes as an argument an interpolation pattern as in + #Z3_get_interpolant. This is a conjunction, some subformulas of + which are marked with the "interp" operator (see #Z3_mk_interp). + + The conjunction is first checked for unsatisfiability. The result + of this check is returned in the out parameter "status". If the result + is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant + and returned as a vector of formulas. Otherwise the return value is + an empty formula. + + See #Z3_get_interpolant for a discussion of supported theories. + + The advantage of this function over #Z3_get_interpolant is that + it is not necessary to create a suitable SMT solver and generate + a proof. The disadvantage is that it is not possible to use the + solver incrementally. + + Parameters: + + \param c logical context. + \param pat an interpolation pattern + \param p parameters for solver creation + \param status returns the status of the sat check + \param model returns model if satisfiable + + Return value: status of SAT check + + def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL))) + */ + + Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model); + /** Constant reprepresenting a root of a formula tree for tree interpolation */ #define IZ3_ROOT SHRT_MAX diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 527230e16..836ade9ce 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -547,6 +547,9 @@ public: } }; +#define STRINGIZE(x) #x +#define STRINGIZE_VALUE_OF(x) STRINGIZE(x) + class get_info_cmd : public cmd { symbol m_error_behavior; symbol m_name; @@ -584,7 +587,11 @@ public: ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl; } else if (opt == m_version) { - ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl; + ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER +#ifdef Z3GITHASH + << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH) +#endif + << "\")" << std::endl; } else if (opt == m_status) { ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1acdb047e..42497ef5a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -347,8 +347,14 @@ cmd_context::~cmd_context() { } void cmd_context::set_cancel(bool f) { - if (m_solver) - m_solver->set_cancel(f); + if (m_solver) { + if (f) { + m_solver->cancel(); + } + else { + m_solver->reset_cancel(); + } + } if (has_manager()) m().set_cancel(f); } diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 7fd44c088..cb83b52f6 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -33,6 +33,7 @@ Notes: #include"iz3checker.h" #include"iz3profiling.h" #include"interp_params.hpp" +#include"scoped_proof.h" static void show_interpolant_and_maybe_check(cmd_context & ctx, ptr_vector &cnsts, @@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par ast_manager &_m = ctx.m(); // TODO: the following is a HACK to enable proofs in the old smt solver // When we stop using that solver, this hack can be removed - _m.toggle_proof_mode(PGM_FINE); + scoped_proof_mode spm(_m,PGM_FINE); ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled); p.set_bool("proof", true); scoped_ptr sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic()); diff --git a/src/duality/duality.h b/src/duality/duality.h index c315c5431..c1c9797f3 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -1152,6 +1152,13 @@ protected: virtual void LearnFrom(Solver *old_solver) = 0; + /** Return true if the solution be incorrect due to recursion bounding. + That is, the returned "solution" might contain all derivable facts up to the + given recursion bound, but not be actually a fixed point. + */ + + virtual bool IsResultRecursionBounded() = 0; + virtual ~Solver(){} static Solver *Create(const std::string &solver_class, RPFP *rpfp); diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 59611c814..681582415 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -768,6 +768,29 @@ namespace Duality { annot.Simplify(); } + bool recursionBounded; + + /** See if the solution might be bounded. */ + void TestRecursionBounded(){ + recursionBounded = false; + if(RecursionBound == -1) + return; + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &insts = insts_of_node[node]; + for(unsigned j = 0; j < insts.size(); j++) + if(indset->Contains(insts[j])) + if(NodePastRecursionBound(insts[j])){ + recursionBounded = true; + return; + } + } + } + + bool IsResultRecursionBounded(){ + return recursionBounded; + } + /** Generate a proposed solution of the input RPFP from the unwinding, by unioning the instances of each node. */ void GenSolutionFromIndSet(bool with_markers = false){ @@ -1026,6 +1049,7 @@ namespace Duality { timer_stop("ProduceCandidatesForExtension"); if(candidates.empty()){ GenSolutionFromIndSet(); + TestRecursionBounded(); return true; } Candidate cand = candidates.front(); diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index bed93a56f..0d394090f 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -41,6 +41,7 @@ Revision History: #include "iz3hash.h" #include "iz3interp.h" +#include"scoped_proof.h" using namespace stl_ext; @@ -347,8 +348,10 @@ public: // get the interps for the tree positions std::vector _interps = interps; interps.resize(pos_map.size()); - for(unsigned i = 0; i < pos_map.size(); i++) - interps[i] = i < _interps.size() ? _interps[i] : mk_false(); + for(unsigned i = 0; i < pos_map.size(); i++){ + unsigned j = pos_map[i]; + interps[i] = j < _interps.size() ? _interps[j] : mk_false(); + } } bool has_interp(hash_map &memo, const ast &t){ @@ -501,6 +504,8 @@ lbool iz3interpolate(ast_manager &_m_manager, return res; } + + void interpolation_options_struct::apply(iz3base &b){ for(stl_ext::hash_map::iterator it = map.begin(), en = map.end(); it != en; diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 52aa716c3..1c6f9513e 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager, ptr_vector &interps, interpolation_options_struct * options); + /* Compute an interpolant from an ast representing an interpolation problem, if unsat, else return a model (if enabled). Uses the given solver to produce the proof/model. Also returns a vector @@ -90,4 +91,5 @@ lbool iz3interpolate(ast_manager &_m_manager, model_ref &m, interpolation_options_struct * options); + #endif diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index f79a65705..748d2cf0e 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -211,7 +211,7 @@ namespace datalog { m_var_subst(m), m_rule_manager(*this), m_contains_p(*this), - m_check_pred(m_contains_p, m), + m_rule_properties(m, m_rule_manager, *this, m_contains_p), m_transf(*this), m_trail(*this), m_pinned(m), @@ -278,6 +278,7 @@ namespace datalog { symbol context::default_table() const { return m_params->datalog_default_table(); } symbol context::default_relation() const { return m_default_relation; } void context::set_default_relation(symbol const& s) { m_default_relation = s; } + symbol context::print_aig() const { return m_params->print_aig(); } symbol context::check_relation() const { return m_params->datalog_check_relation(); } symbol context::default_table_checker() const { return m_params->datalog_default_table_checker(); } bool context::default_table_checked() const { return m_params->datalog_default_table_checked(); } @@ -294,8 +295,9 @@ namespace datalog { bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); } bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } - - bool context::bit_blast() const { return m_params->xform_bit_blast(); } + symbol context::tab_selection() const { return m_params->tab_selection(); } + bool context::xform_slice() const { return m_params->xform_slice(); } + bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } bool context::karr() const { return m_params->xform_karr(); } bool context::scale() const { return m_params->xform_scale(); } bool context::magic() const { return m_params->xform_magic(); } @@ -324,7 +326,7 @@ namespace datalog { m_bind_variables.add_var(m.mk_const(var)); } - expr_ref context::bind_variables(expr* fml, bool is_forall) { + expr_ref context::bind_vars(expr* fml, bool is_forall) { return m_bind_variables(fml, is_forall); } @@ -452,10 +454,7 @@ namespace datalog { rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]); ++m_rule_fmls_head; } - rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); - for (; it != end; ++it) { - check_rule(*(*it)); - } + check_rules(m_rule_set); } // @@ -541,138 +540,49 @@ namespace datalog { m_engine->add_cover(level, pred, property); } - void context::check_uninterpreted_free(rule& r) { - func_decl* f = 0; - if (get_rule_manager().has_uninterpreted_non_predicates(r, f)) { - std::stringstream stm; - stm << "Uninterpreted '" - << f->get_name() - << "' in "; - r.display(*this, stm); - throw default_exception(stm.str()); - } - } - - void context::check_quantifier_free(rule& r) { - if (get_rule_manager().has_quantifiers(r)) { - std::stringstream stm; - stm << "cannot process quantifiers in rule "; - r.display(*this, stm); - throw default_exception(stm.str()); - } - } - - - void context::check_existential_tail(rule& r) { - unsigned ut_size = r.get_uninterpreted_tail_size(); - unsigned t_size = r.get_tail_size(); - - TRACE("dl", get_rule_manager().display_smt2(r, tout); tout << "\n";); - for (unsigned i = ut_size; i < t_size; ++i) { - app* t = r.get_tail(i); - TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";); - if (m_check_pred(t)) { - std::ostringstream out; - out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate"; - throw default_exception(out.str()); - } - } - } - - void context::check_positive_predicates(rule& r) { - ast_mark visited; - ptr_vector todo, tocheck; - unsigned ut_size = r.get_uninterpreted_tail_size(); - unsigned t_size = r.get_tail_size(); - for (unsigned i = 0; i < ut_size; ++i) { - if (r.is_neg_tail(i)) { - tocheck.push_back(r.get_tail(i)); - } - } - ast_manager& m = get_manager(); - contains_pred contains_p(*this); - check_pred check_pred(contains_p, get_manager()); - - for (unsigned i = ut_size; i < t_size; ++i) { - todo.push_back(r.get_tail(i)); - } - while (!todo.empty()) { - expr* e = todo.back(), *e1, *e2; - todo.pop_back(); - if (visited.is_marked(e)) { - continue; - } - visited.mark(e, true); - if (is_predicate(e)) { - } - else if (m.is_and(e) || m.is_or(e)) { - todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - } - else if (m.is_implies(e, e1, e2)) { - tocheck.push_back(e1); - todo.push_back(e2); - } - else if (is_quantifier(e)) { - todo.push_back(to_quantifier(e)->get_expr()); - } - else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && - m.is_true(e1)) { - todo.push_back(e2); - } - else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && - m.is_true(e2)) { - todo.push_back(e1); - } - else { - tocheck.push_back(e); - } - } - for (unsigned i = 0; i < tocheck.size(); ++i) { - expr* e = tocheck[i]; - if (check_pred(e)) { - std::ostringstream out; - out << "recursive predicate " << mk_ismt2_pp(e, get_manager()) << " occurs nested in body"; - r.display(*this, out << "\n"); - throw default_exception(out.str()); - - } - } - } - - void context::check_rule(rule& r) { + void context::check_rules(rule_set& r) { + m_rule_properties.set_generate_proof(generate_proof_trace()); switch(get_engine()) { - case DATALOG_ENGINE: - check_quantifier_free(r); - check_uninterpreted_free(r); - check_existential_tail(r); + case DATALOG_ENGINE: + m_rule_properties.collect(r); + m_rule_properties.check_quantifier_free(); + m_rule_properties.check_uninterpreted_free(); + m_rule_properties.check_nested_free(); break; case PDR_ENGINE: - check_existential_tail(r); - check_positive_predicates(r); - check_uninterpreted_free(r); + m_rule_properties.collect(r); + m_rule_properties.check_existential_tail(); + m_rule_properties.check_for_negated_predicates(); + m_rule_properties.check_uninterpreted_free(); break; case QPDR_ENGINE: - check_positive_predicates(r); - check_uninterpreted_free(r); + m_rule_properties.collect(r); + m_rule_properties.check_for_negated_predicates(); + m_rule_properties.check_uninterpreted_free(); break; case BMC_ENGINE: - check_positive_predicates(r); + m_rule_properties.collect(r); + m_rule_properties.check_for_negated_predicates(); break; case QBMC_ENGINE: - check_existential_tail(r); - check_positive_predicates(r); + m_rule_properties.collect(r); + m_rule_properties.check_existential_tail(); + m_rule_properties.check_for_negated_predicates(); break; case TAB_ENGINE: - check_existential_tail(r); - check_positive_predicates(r); + m_rule_properties.collect(r); + m_rule_properties.check_existential_tail(); + m_rule_properties.check_for_negated_predicates(); break; case DUALITY_ENGINE: - check_existential_tail(r); - check_positive_predicates(r); + m_rule_properties.collect(r); + m_rule_properties.check_existential_tail(); + m_rule_properties.check_for_negated_predicates(); break; case CLP_ENGINE: - check_existential_tail(r); - check_positive_predicates(r); + m_rule_properties.collect(r); + m_rule_properties.check_existential_tail(); + m_rule_properties.check_for_negated_predicates(); break; case DDNF_ENGINE: break; @@ -681,9 +591,6 @@ namespace datalog { UNREACHABLE(); break; } - if (generate_proof_trace() && !r.get_proof()) { - m_rule_manager.mk_rule_asserted_proof(r); - } } void context::add_rule(rule_ref& r) { @@ -934,11 +841,7 @@ namespace datalog { // TODO: what? if(get_engine() != DUALITY_ENGINE) { new_query(); - rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); - rule_ref r(m_rule_manager); - for (; it != end; ++it) { - check_rule(*(*it)); - } + check_rules(m_rule_set); } #endif m_mc = mk_skip_model_converter(); @@ -1078,10 +981,10 @@ namespace datalog { void context::get_raw_rule_formulas(expr_ref_vector& rules, svector& names){ for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - expr_ref r = bind_variables(m_rule_fmls[i].get(), true); - rules.push_back(r.get()); - // rules.push_back(m_rule_fmls[i].get()); - names.push_back(m_rule_names[i]); + expr_ref r = bind_vars(m_rule_fmls[i].get(), true); + rules.push_back(r.get()); + // rules.push_back(m_rule_fmls[i].get()); + names.push_back(m_rule_names[i]); } } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 85d4b7c0e..cfd4dfc3b 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -42,6 +42,7 @@ Revision History: #include"expr_functors.h" #include"dl_engine_base.h" #include"bind_variables.h" +#include"rule_properties.h" struct fixedpoint_params; @@ -53,6 +54,7 @@ namespace datalog { MEMOUT, INPUT_ERROR, APPROX, + BOUNDED, CANCELED }; @@ -141,6 +143,17 @@ namespace datalog { SK_UINT64, SK_SYMBOL }; + class contains_pred : public i_expr_pred { + context const& ctx; + public: + contains_pred(context& ctx): ctx(ctx) {} + virtual ~contains_pred() {} + + virtual bool operator()(expr* e) { + return ctx.is_predicate(e); + } + }; + private: class sort_domain; @@ -154,32 +167,21 @@ namespace datalog { typedef obj_map > pred2syms; typedef obj_map sort_domain_map; - class contains_pred : public i_expr_pred { - context const& ctx; - public: - contains_pred(context& ctx): ctx(ctx) {} - virtual ~contains_pred() {} - - virtual bool operator()(expr* e) { - return ctx.is_predicate(e); - } - }; - ast_manager & m; register_engine_base& m_register_engine; smt_params & m_fparams; params_ref m_params_ref; fixedpoint_params* m_params; - bool m_generate_proof_trace; - bool m_unbound_compressor; - symbol m_default_relation; + bool m_generate_proof_trace; // cached configuration parameter + bool m_unbound_compressor; // cached configuration parameter + symbol m_default_relation; // cached configuration parameter dl_decl_util m_decl_util; th_rewriter m_rewriter; var_subst m_var_subst; rule_manager m_rule_manager; contains_pred m_contains_p; - check_pred m_check_pred; + rule_properties m_rule_properties; rule_transformer m_transf; trail_stack m_trail; ast_ref_vector m_pinned; @@ -259,18 +261,21 @@ namespace datalog { bool unbound_compressor() const; void set_unbound_compressor(bool f); bool similarity_compressor() const; + symbol print_aig() const; + symbol tab_selection() const; unsigned similarity_compressor_threshold() const; unsigned soft_timeout() const; unsigned initial_restart_timeout() const; bool generate_explanations() const; bool explanations_on_relation_level() const; bool magic_sets_for_queries() const; - bool bit_blast() const; bool karr() const; bool scale() const; bool magic() const; bool quantify_arrays() const; bool instantiate_quantifiers() const; + bool xform_bit_blast() const; + bool xform_slice() const; void register_finite_sort(sort * s, sort_kind k); @@ -287,7 +292,7 @@ namespace datalog { universal (if is_forall is true) or existential quantifier. */ - expr_ref bind_variables(expr* fml, bool is_forall); + expr_ref bind_vars(expr* fml, bool is_forall); /** Register datalog relation. @@ -307,6 +312,8 @@ namespace datalog { \brief Retrieve predicates */ func_decl_set const& get_predicates() const { return m_preds; } + ast_ref_vector const &get_pinned() const {return m_pinned; } + bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); } bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); } @@ -419,7 +426,7 @@ namespace datalog { /** \brief Check if rule is well-formed according to engine. */ - void check_rule(rule& r); + void check_rules(rule_set& r); /** \brief Return true if facts to \c pred can be added using the \c add_table_fact() function. @@ -565,11 +572,6 @@ namespace datalog { void ensure_engine(); - void check_quantifier_free(rule& r); - void check_uninterpreted_free(rule& r); - void check_existential_tail(rule& r); - void check_positive_predicates(rule& r); - // auxilary functions for SMT2 pretty-printer. void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out); diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index 2015d4eea..b846bc06a 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -252,17 +252,16 @@ namespace datalog { unsigned rule_manager::extract_horn(expr* fml, app_ref_vector& body, app_ref& head) { expr* e1, *e2; - unsigned index = m_counter.get_next_var(fml); if (::is_forall(fml)) { - index += to_quantifier(fml)->get_num_decls(); fml = to_quantifier(fml)->get_expr(); } + unsigned index = m_counter.get_next_var(fml); if (m.is_implies(fml, e1, e2)) { - expr_ref_vector es(m); + m_args.reset(); head = ensure_app(e2); - qe::flatten_and(e1, es); - for (unsigned i = 0; i < es.size(); ++i) { - body.push_back(ensure_app(es[i].get())); + qe::flatten_and(e1, m_args); + for (unsigned i = 0; i < m_args.size(); ++i) { + body.push_back(ensure_app(m_args[i].get())); } } else { @@ -370,7 +369,7 @@ namespace datalog { } void rule_manager::bind_variables(expr* fml, bool is_forall, expr_ref& result) { - result = m_ctx.bind_variables(fml, is_forall); + result = m_ctx.bind_vars(fml, is_forall); } void rule_manager::flatten_body(app_ref_vector& body) { diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp new file mode 100644 index 000000000..7f019c74e --- /dev/null +++ b/src/muz/base/rule_properties.cpp @@ -0,0 +1,189 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + rule_properties.cpp + +Abstract: + + Collect properties of rules. + +Author: + + Nikolaj Bjorner (nbjorner) 9-25-2014 + +Notes: + + +--*/ + +#include"expr_functors.h" +#include"rule_properties.h" +#include"dl_rule_set.h" +#include"for_each_expr.h" +#include"dl_context.h" + +using namespace datalog; +rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): + m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {} + +rule_properties::~rule_properties() {} + +void rule_properties::collect(rule_set const& rules) { + reset(); + rule_set::iterator it = rules.begin(), end = rules.end(); + expr_sparse_mark visited; + for (; it != end; ++it) { + rule* r = *it; + m_rule = r; + unsigned ut_size = r->get_uninterpreted_tail_size(); + unsigned t_size = r->get_tail_size(); + if (r->has_negation()) { + m_negative_rules.push_back(r); + } + for (unsigned i = ut_size; i < t_size; ++i) { + for_each_expr_core(*this, visited, r->get_tail(i)); + } + if (m_generate_proof && !r->get_proof()) { + rm.mk_rule_asserted_proof(*r); + } + } +} + +void rule_properties::check_quantifier_free() { + if (!m_quantifiers.empty()) { + quantifier* q = m_quantifiers.begin()->m_key; + rule* r = m_quantifiers.begin()->m_value; + std::stringstream stm; + stm << "cannot process quantifier in rule "; + r->display(m_ctx, stm); + throw default_exception(stm.str()); + } +} + +void rule_properties::check_for_negated_predicates() { + if (!m_negative_rules.empty()) { + rule* r = m_negative_rules[0]; + std::stringstream stm; + stm << "Rule contains negative predicate "; + r->display(m_ctx, stm); + throw default_exception(stm.str()); + } +} + + +void rule_properties::check_uninterpreted_free() { + if (!m_uninterp_funs.empty()) { + func_decl* f = m_uninterp_funs.begin()->m_key; + rule* r = m_uninterp_funs.begin()->m_value; + std::stringstream stm; + stm << "Uninterpreted '" + << f->get_name() + << "' in "; + r->display(m_ctx, stm); + throw default_exception(stm.str()); + } +} + +void rule_properties::check_nested_free() { + if (!m_interp_pred.empty()) { + std::stringstream stm; + rule* r = m_interp_pred[0]; + stm << "Rule contains nested predicates "; + r->display(m_ctx, stm); + throw default_exception(stm.str()); + + } +} + +void rule_properties::check_existential_tail() { + ast_mark visited; + ptr_vector todo, tocheck; + for (unsigned i = 0; i < m_interp_pred.size(); ++i) { + rule& r = *m_interp_pred[i]; + unsigned ut_size = r.get_uninterpreted_tail_size(); + unsigned t_size = r.get_tail_size(); + for (unsigned i = ut_size; i < t_size; ++i) { + todo.push_back(r.get_tail(i)); + } + } + context::contains_pred contains_p(m_ctx); + check_pred check_pred(contains_p, m); + + while (!todo.empty()) { + expr* e = todo.back(), *e1, *e2; + todo.pop_back(); + if (visited.is_marked(e)) { + continue; + } + visited.mark(e, true); + if (m_is_predicate(e)) { + } + else if (m.is_and(e) || m.is_or(e)) { + todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else if (m.is_implies(e, e1, e2)) { + tocheck.push_back(e1); + todo.push_back(e2); + } + else if (is_quantifier(e)) { + todo.push_back(to_quantifier(e)->get_expr()); + } + else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && + m.is_true(e1)) { + todo.push_back(e2); + } + else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && + m.is_true(e2)) { + todo.push_back(e1); + } + else { + tocheck.push_back(e); + } + } + for (unsigned i = 0; i < tocheck.size(); ++i) { + expr* e = tocheck[i]; + if (check_pred(e)) { + std::ostringstream out; + out << "recursive predicate " << mk_ismt2_pp(e, m) << " occurs nested in the body of a rule"; + throw default_exception(out.str()); + } + } +} + + +void rule_properties::insert(ptr_vector& rules, rule* r) { + if (rules.empty() || rules.back() != r) { + rules.push_back(r); + } +} + +void rule_properties::operator()(var* n) { } + +void rule_properties::operator()(quantifier* n) { + m_quantifiers.insert(n, m_rule); +} +void rule_properties::operator()(app* n) { + if (m_is_predicate(n)) { + insert(m_interp_pred, m_rule); + } + else if (is_uninterp(n)) { + m_uninterp_funs.insert(n->get_decl(), m_rule); + } + else if (m_dt.is_accessor(n)) { + sort* s = m.get_sort(n->get_arg(0)); + SASSERT(m_dt.is_datatype(s)); + if (m_dt.get_datatype_constructors(s)->size() > 1) { + m_uninterp_funs.insert(n->get_decl(), m_rule); + } + } +} + +void rule_properties::reset() { + m_quantifiers.reset(); + m_uninterp_funs.reset(); + m_interp_pred.reset(); + m_negative_rules.reset(); +} + diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h new file mode 100644 index 000000000..bfff8cbe4 --- /dev/null +++ b/src/muz/base/rule_properties.h @@ -0,0 +1,60 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + rule_properties.h + +Abstract: + + Collect properties of rules. + +Author: + + Nikolaj Bjorner (nbjorner) 9-25-2014 + +Notes: + + +--*/ + +#ifndef _RULE_PROPERTIES_H_ +#define _RULE_PROPERTIES_H_ + +#include"ast.h" +#include"datatype_decl_plugin.h" +#include"dl_rule.h" + +namespace datalog { + class rule_properties { + ast_manager& m; + rule_manager& rm; + context& m_ctx; + i_expr_pred& m_is_predicate; + datatype_util m_dt; + bool m_generate_proof; + rule* m_rule; + obj_map m_quantifiers; + obj_map m_uninterp_funs; + ptr_vector m_interp_pred; + ptr_vector m_negative_rules; + + void insert(ptr_vector& rules, rule* r); + public: + rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate); + ~rule_properties(); + void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; } + void collect(rule_set const& r); + void check_quantifier_free(); + void check_uninterpreted_free(); + void check_existential_tail(); + void check_for_negated_predicates(); + void check_nested_free(); + void operator()(var* n); + void operator()(quantifier* n); + void operator()(app* n); + void reset(); + }; +} + +#endif /* _RULE_PROPERTIES_H_ */ diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 2b970e4fa..57e4ba8cb 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -32,7 +32,6 @@ Revision History: #include "dl_transforms.h" #include "dl_mk_rule_inliner.h" #include "scoped_proof.h" -#include"fixedpoint_params.hpp" namespace datalog { @@ -1444,7 +1443,7 @@ namespace datalog { expr_ref bg_assertion = m_ctx.get_background_assertion(); apply_default_transformation(m_ctx); - if (m_ctx.get_params().xform_slice()) { + if (m_ctx.xform_slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 3f035b453..a633939b6 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -36,6 +36,7 @@ Revision History: #include "model_v2_pp.h" #include "fixedpoint_params.hpp" #include "used_vars.h" +#include "func_decl_dependencies.h" // template class symbol_table; @@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) { _d->rpfp->AssertAxiom(e); } + // make sure each predicate is the head of at least one clause + func_decl_set heads; + for(unsigned i = 0; i < clauses.size(); i++){ + expr cl = clauses[i]; + + while(true){ + if(cl.is_app()){ + decl_kind k = cl.decl().get_decl_kind(); + if(k == Implies) + cl = cl.arg(1); + else { + heads.insert(cl.decl()); + break; + } + } + else if(cl.is_quantifier()) + cl = cl.body(); + else break; + } + } + ast_ref_vector const &pinned = m_ctx.get_pinned(); + for(unsigned i = 0; i < pinned.size(); i++){ + ::ast *fa = pinned[i]; + if(is_func_decl(fa)){ + ::func_decl *fd = to_func_decl(fa); + if(m_ctx.is_predicate(fd)) { + func_decl f(_d->ctx,fd); + if(!heads.contains(fd)){ + int arity = f.arity(); + std::vector args; + for(int j = 0; j < arity; j++) + args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))()); + expr c = implies(_d->ctx.bool_val(false),f(args)); + c = _d->ctx.make_quant(Forall,args,c); + clauses.push_back(c); + } + } + } + } + // creates 1-1 map between clauses and rpfp edges _d->rpfp->FromClauses(clauses); @@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) { // dealloc(rs); this is now owned by data // true means the RPFP problem is SAT, so the query is UNSAT - return ans ? l_false : l_true; + // but we return undef if the UNSAT result is bounded + if(ans){ + if(rs->IsResultRecursionBounded()){ +#if 0 + m_ctx.set_status(datalog::BOUNDED); + return l_undef; +#else + return l_false; +#endif + } + return l_false; + } + return l_true; } expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) { diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 9807cec4a..221d17d57 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -103,7 +103,7 @@ struct dl_context { void add_rule(expr * rule, symbol const& name) { init(); if (m_collected_cmds) { - expr_ref rl = m_context->bind_variables(rule, true); + expr_ref rl = m_context->bind_vars(rule, true); m_collected_cmds->m_rules.push_back(rl); m_collected_cmds->m_names.push_back(name); m_trail.push(push_back_vector(m_collected_cmds->m_rules)); @@ -116,7 +116,7 @@ struct dl_context { bool collect_query(expr* q) { if (m_collected_cmds) { - expr_ref qr = m_context->bind_variables(q, false); + expr_ref qr = m_context->bind_vars(q, false); m_collected_cmds->m_queries.push_back(qr); m_trail.push(push_back_vector(m_collected_cmds->m_queries)); return true; @@ -253,6 +253,11 @@ public: print_certificate(ctx); break; case l_undef: + if(dlctx.get_status() == datalog::BOUNDED){ + ctx.regular_stream() << "bounded\n"; + print_certificate(ctx); + break; + } ctx.regular_stream() << "unknown\n"; switch(dlctx.get_status()) { case datalog::INPUT_ERROR: diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index a1c556baf..6032b3f02 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -190,7 +190,7 @@ class horn_tactic : public tactic { bool produce_proofs = g->proofs_enabled(); if (produce_proofs) { - if (!m_ctx.get_params().generate_proof_trace()) { + if (!m_ctx.generate_proof_trace()) { params_ref params = m_ctx.get_params().p; params.set_bool("generate_proof_trace", true); updt_params(params); @@ -316,7 +316,7 @@ class horn_tactic : public tactic { m_ctx.get_rules(); // flush adding rules. apply_default_transformation(m_ctx); - if (m_ctx.get_params().xform_slice()) { + if (m_ctx.xform_slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 722661e38..ea8eca6f4 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -80,7 +80,7 @@ namespace pdr { pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), - m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), + m_sig(m), m_solver(pm, ctx.get_params().pdr_try_minimize_core(), head->get_name()), m_invariants(m), m_transition(m), m_initial_state(m), m_reachable(pm, (datalog::PDR_CACHE_MODE)ctx.get_params().pdr_cache_mode()) {} diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 63adfa1f6..ddfe85484 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -251,7 +251,6 @@ namespace pdr { model_node* m_root; std::deque m_leaves; vector > m_cache; - obj_map& cache(model_node const& n); void erase_children(model_node& n, bool backtrack); void erase_leaf(model_node& n); diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 06f858608..a7d0a02bf 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -30,7 +30,6 @@ Revision History: #include "pdr_farkas_learner.h" #include "ast_smt2_pp.h" #include "expr_replacer.h" -#include "fixedpoint_params.hpp" // // Auxiliary structure to introduce propositional names for assumptions that are not @@ -226,12 +225,12 @@ namespace pdr { }; - prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& name) : + prop_solver::prop_solver(manager& pm, bool try_minimize_core, symbol const& name) : m_fparams(pm.get_fparams()), m(pm.get_manager()), m_pm(pm), m_name(name), - m_try_minimize_core(p.pdr_try_minimize_core()), + m_try_minimize_core(try_minimize_core), m_ctx(pm.mk_fresh()), m_pos_level_atoms(m), m_neg_level_atoms(m), diff --git a/src/muz/pdr/pdr_prop_solver.h b/src/muz/pdr/pdr_prop_solver.h index a63ec2bf4..d7f13a603 100644 --- a/src/muz/pdr/pdr_prop_solver.h +++ b/src/muz/pdr/pdr_prop_solver.h @@ -31,7 +31,6 @@ Revision History: #include "pdr_manager.h" #include "pdr_smt_context_manager.h" -struct fixedpoint_params; namespace pdr { class prop_solver { @@ -75,7 +74,7 @@ namespace pdr { public: - prop_solver(pdr::manager& pm, fixedpoint_params const& p, symbol const& name); + prop_solver(pdr::manager& pm, bool try_minimize_core, symbol const& name); /** return true is s is a symbol introduced by prop_solver */ bool is_aux_symbol(func_decl * s) const { diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 705644340..c512598a0 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -590,7 +590,7 @@ namespace datalog { } // enforce interpreted tail predicates - unsigned ut_len=r->get_uninterpreted_tail_size(); + unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index fc8ceadce..bf2f09d56 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -346,7 +346,7 @@ namespace datalog { print_container(m_controls, out); } virtual void display_body_impl(rel_context_base const & ctx, std::ostream & out, std::string indentation) const { - // m_body->display_indented(ctx, out, indentation+" "); + m_body->display_indented(ctx, out, indentation+" "); } }; diff --git a/src/muz/rel/dl_vector_relation.h b/src/muz/rel/dl_vector_relation.h index 6c55e7b6d..c349c6e19 100644 --- a/src/muz/rel/dl_vector_relation.h +++ b/src/muz/rel/dl_vector_relation.h @@ -60,8 +60,6 @@ namespace datalog { dealloc(m_elems); } - virtual bool can_swap() const { return true; } - virtual void swap(relation_base& other) { vector_relation& o = dynamic_cast(other); if (&o == this) return; diff --git a/src/muz/rel/product_set.h b/src/muz/rel/product_set.h index ebfe339fe..238a33d8a 100644 --- a/src/muz/rel/product_set.h +++ b/src/muz/rel/product_set.h @@ -248,7 +248,6 @@ namespace datalog { class product_set_factory { - friend class product_set_factory; unsigned char m_data[0]; public: enum initial_t { diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 36ba98781..4b099c9b4 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -51,7 +51,6 @@ Revision History: #include"dl_mk_interp_tail_simplifier.h" #include"dl_mk_bit_blast.h" #include"dl_mk_separate_negated_tails.h" -#include"fixedpoint_params.hpp" namespace datalog { @@ -159,8 +158,8 @@ namespace datalog { TRACE("dl", m_context.display(tout);); //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); - if (m_context.get_params().print_aig().size()) { - const char *filename = static_cast(m_context.get_params().print_aig().c_ptr()); + if (m_context.print_aig().size()) { + const char *filename = static_cast(m_context.print_aig().c_ptr()); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); std::ofstream strm(filename, std::ios_base::binary); aig(strm); @@ -300,7 +299,7 @@ namespace datalog { transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); - if (m_context.get_params().xform_bit_blast()) { + if (m_context.xform_bit_blast()) { transf.register_plugin(alloc(mk_bit_blast, m_context, 22000)); transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context, 21000)); } @@ -541,7 +540,7 @@ namespace datalog { void rel_context::add_fact(func_decl* pred, relation_fact const& fact) { get_rmanager().reset_saturated_marks(); get_relation(pred).add_fact(fact); - if (m_context.get_params().print_aig().size()) { + if (m_context.print_aig().size()) { m_table_facts.push_back(std::make_pair(pred, fact)); } } diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 75fb03c9e..51e4c33af 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1,3 +1,67 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + udoc_relation.cpp + +Abstract: + + Relation based on union of DOCs. + +Author: + + Nuno Lopes (a-nlopes) 2013-03-01 + Nikolaj Bjorner (nbjorner) 2014-09-15 + +Revision History: + + Revised version of dl_hassel_diff facilities. + +Notes: + + Current pending items: + - Fix the incomplete non-emptiness check in doc.cpp + It can fall back to a sat_solver call in the worst case. + The sat_solver.h interface gives a way to add clauses to a sat solver + and check for satisfiability. It can be used from scratch each time. + - Profile and fix bottlnecks: + - Potential bottleneck in projection exercised in some benchmarks. + Projection is asymptotically very expensive. We are here interested in + handling common/cheap cases efficiently. + - Simplification of udoc and utbv (from negated tails) after operations such as join and union. + - The current simplification is between cheap and expensive. Some low-cost simplification + based on sorting + coallescing and detecting empty docs could be used. + - There are several places where code copies a sequence of bits from one vector to another. + Any such places in udoc_relation should be shifted down to 'doc_manager'. Loops in 'doc_manager' + should be shifted down to 'tbv_manager' and loops there should be moved to 'fixed_bitvector_manager'. + Finally, more efficient and general implementations of non-aligned copies are useful where such + bottlnecks show up on the radar. + - Fix filter_by_negated. + Current implementation seems incorrect. The fast path seems right, but the slow path does not. + Recall the semantics: + filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, + corresponding columns in neg: d1,...,dN): + tgt := {x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) } + We are given tgt, and neg as two udocs. + The fast pass removes doc's t from tgt where we can establish + that for every x in t there is a n in neg and a y in n, + such that projections(x) = projections(y). + This is claimed to be the case if projections(n) contains projections(t). + + The slow pass uses the projection to create a doc n' from each n that has the same signature as tgt. + It then subtracts each n'. The way n' is created is by copying bits from n. + This seems wrong, for example if the projection contains overlapping regions. + Here is a possible corrected version: + define join_project(tgt, neg, c1, .., cN, d1, .. , dN) as + exists y : y \in neg & x in tgt & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) + return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN) + We have most of the facilities required for a join project operation. + For example, the filter_project function uses both equalities and deleted columns. + - Lipstick service: + - filter_proj_fn uses both a bit_vector and a svector for representing removed bits. + This is due to underlying routines using different types for the same purpose. +--*/ #include "udoc_relation.h" #include "dl_relation_manager.h" #include "qe_util.h" @@ -63,7 +127,7 @@ namespace datalog { m_elems.push_back(fact2doc(f)); } bool udoc_relation::empty() const { - if (get_signature().empty()) return false; + if (m_elems.is_empty()) return true; // TBD: make this a complete check for (unsigned i = 0; i < m_elems.size(); ++i) { if (!dm.is_empty(m_elems[i])) return false; @@ -1156,17 +1220,15 @@ namespace datalog { m_original_condition(condition, m), m_reduced_condition(m), m_equalities(union_ctx) { - t.expand_column_vector(m_removed_cols); unsigned num_bits = t.get_num_bits(); - m_col_list.resize(num_bits, false); + t.expand_column_vector(m_removed_cols); + m_col_list.resize(num_bits, false); + m_to_delete.resize(num_bits, false); for (unsigned i = 0; i < num_bits; ++i) { m_equalities.mk_var(); } for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_col_list.set(m_removed_cols[i], true); - } - m_to_delete.resize(t.get_num_bits(), false); - for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_to_delete[m_removed_cols[i]] = true; } expr_ref guard(m), non_eq_cond(condition, m); diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index d75ebe20e..3175d1622 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -765,7 +765,7 @@ namespace tb { m_weight_multiply(1.0), m_update_frequency(20), m_next_update(20) { - set_strategy(ctx.get_params().tab_selection()); + set_strategy(ctx.tab_selection()); } void init(rules const& rs) { diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index fcd20d78f..8f4c840eb 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -262,7 +262,7 @@ namespace datalog { rule_set * operator()(rule_set const & source) { // TODO pc - if (!m_context.bit_blast()) { + if (!m_context.xform_bit_blast()) { return 0; } rule_manager& rm = m_context.get_rule_manager(); diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 8ec385f9d..a4ec5f380 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -124,7 +124,7 @@ public: virtual void set_cancel(bool f) { m_goal2sat.set_cancel(f); m_solver.set_cancel(f); - m_preprocess->set_cancel(f); + if (f) m_preprocess->cancel(); else m_preprocess->reset_cancel(); } virtual void push() { m_solver.user_push(); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index d12fabfa7..24c82feb0 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -299,6 +299,7 @@ namespace opt { void maxsmt::set_cancel(bool f) { m_cancel = f; + if (m_msolver) { m_msolver->set_cancel(f); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 4c0d8d825..3bef5bebe 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -78,7 +78,7 @@ namespace opt { virtual rational get_lower() const { return m_lower; } virtual rational get_upper() const { return m_upper; } virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } - virtual void set_cancel(bool f) { m_cancel = f; s().set_cancel(f); } + virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); } virtual void collect_statistics(statistics& st) const { } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } void set_model() { s().get_model(m_model); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 9b48707bd..9c720ad97 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1011,13 +1011,13 @@ namespace opt { #pragma omp critical (opt_context) { if (m_solver) { - m_solver->set_cancel(f); + if (f) m_solver->cancel(); else m_solver->reset_cancel(); } if (m_pareto) { m_pareto->set_cancel(f); } if (m_simplify) { - m_simplify->set_cancel(f); + if (f) m_simplify->cancel(); else m_solver->reset_cancel(); } map_t::iterator it = m_maxsmts.begin(), end = m_maxsmts.end(); for (; it != end; ++it) { diff --git a/src/opt/opt_pareto.h b/src/opt/opt_pareto.h index 8a2378ae9..84e0702aa 100644 --- a/src/opt/opt_pareto.h +++ b/src/opt/opt_pareto.h @@ -64,7 +64,10 @@ namespace opt { m_solver->collect_statistics(st); } virtual void set_cancel(bool f) { - m_solver->set_cancel(f); + if (f) + m_solver->cancel(); + else + m_solver->reset_cancel(); m_cancel = f; } virtual void display(std::ostream & out) const { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 526447f9f..7053d63ec 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -136,9 +136,8 @@ namespace smt { if (cex == 0) return false; // no model available. unsigned num_decls = q->get_num_decls(); - unsigned num_sks = sks.size(); // Remark: sks were created for the flat version of q. - SASSERT(num_sks >= num_decls); + SASSERT(sks.size() >= num_decls); expr_ref_buffer bindings(m_manager); bindings.resize(num_decls); unsigned max_generation = 0; diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index cd043c8a7..e007539aa 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -413,6 +413,7 @@ namespace smt { atoms m_atoms; // set of theory atoms ptr_vector m_asserted_bounds; // set of asserted bounds unsigned m_asserted_qhead; + ptr_vector m_new_atoms; // new bound atoms that have yet to be internalized. svector m_nl_monomials; // non linear monomials svector m_nl_propagated; // non linear monomials that became linear v_dependency_manager m_dep_manager; // for tracking bounds during non-linear reasoning @@ -575,7 +576,6 @@ namespace smt { void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params); void mk_bound_axioms(atom * a); void mk_bound_axiom(atom* a1, atom* a2); - ptr_vector m_new_atoms; void flush_bound_axioms(); typename atoms::iterator next_sup(atom* a1, atom_kind kind, typename atoms::iterator it, diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 9dae2d0c4..7414eda83 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -874,9 +874,6 @@ namespace smt { parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) }; - //std::cout << "v" << v << " " << ((kind1==A_LOWER)?"<= ":">= ") << k1 << "\t "; - //std::cout << "v" << v << " " << ((kind2==A_LOWER)?"<= ":">= ") << k2 << "\n"; - if (kind1 == A_LOWER) { if (kind2 == A_LOWER) { if (k2 <= k1) { @@ -958,16 +955,13 @@ namespace smt { typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1; typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2; bool flo_inf, fhi_inf, flo_sup, fhi_sup; - // std::cout << atoms.size() << "\n"; - ptr_addr_hashtable visited; + ptr_addr_hashtable visited; for (unsigned i = 0; i < atoms.size(); ++i) { atom* a1 = atoms[i]; lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf); hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf); lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup); hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup); -// std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n"; - // std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n"; if (lo_inf1 != end) lo_inf = lo_inf1; if (lo_sup1 != end) lo_sup = lo_sup1; if (hi_inf1 != end) hi_inf = hi_inf1; diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index bab921ed2..d02c9e540 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -654,6 +654,7 @@ namespace smt { } return get_value(v, computed_epsilon) == val; } + /** \brief Return true if for every monomial x_1 * ... * x_n, @@ -2309,8 +2310,9 @@ namespace smt { if (m_nl_monomials.empty()) return FC_DONE; - if (check_monomial_assignments()) + if (check_monomial_assignments()) { return FC_DONE; + } if (!m_params.m_nl_arith) return FC_GIVEUP; @@ -2338,9 +2340,10 @@ namespace smt { if (!max_min_nl_vars()) return FC_CONTINUE; - if (check_monomial_assignments()) + if (check_monomial_assignments()) { return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE; - + } + svector vars; get_non_linear_cluster(vars); @@ -2391,8 +2394,9 @@ namespace smt { } while (m_nl_strategy_idx != old_idx); - if (check_monomial_assignments()) + if (check_monomial_assignments()) { return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE; + } TRACE("non_linear", display(tout);); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index a98e5be49..dfbb62f65 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -218,8 +218,14 @@ public: } virtual void set_cancel(bool f) { - m_solver1->set_cancel(f); - m_solver2->set_cancel(f); + if (f) { + m_solver1->cancel(); + m_solver2->cancel(); + } + else { + m_solver1->reset_cancel(); + m_solver2->reset_cancel(); + } } virtual void set_progress_callback(progress_callback * callback) { diff --git a/src/solver/solver.h b/src/solver/solver.h index e0d3d30e2..1e310a484 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -99,7 +99,6 @@ public: */ virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0; - virtual void set_cancel(bool f) {} /** \brief Interrupt this solver. */ @@ -130,7 +129,6 @@ public: \brief Display the content of this solver. */ virtual void display(std::ostream & out) const; - class scoped_push { solver& s; bool m_nopop; @@ -139,6 +137,8 @@ public: ~scoped_push() { if (!m_nopop) s.pop(1); } void disable_pop() { m_nopop = true; } }; +protected: + virtual void set_cancel(bool f) = 0; }; diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 9889b5872..01c45ee44 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) { } void solver_na2as::restore_assumptions(unsigned old_sz) { - SASSERT(old_sz == 0); + // SASSERT(old_sz == 0); for (unsigned i = old_sz; i < m_assumptions.size(); i++) { m_manager.dec_ref(m_assumptions[i]); } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 5b8e8e107..375f35ed1 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -175,8 +175,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass } void tactic2solver::set_cancel(bool f) { - if (m_tactic.get()) - m_tactic->set_cancel(f); + if (m_tactic.get()) { + if (f) + m_tactic->cancel(); + else + m_tactic->reset_cancel(); + } } void tactic2solver::collect_statistics(statistics & st) const { diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h index c8befd9b2..291bfbcf3 100644 --- a/src/tactic/aig/aig.h +++ b/src/tactic/aig/aig.h @@ -73,8 +73,6 @@ public: void display(std::ostream & out, aig_ref const & r) const; void display_smt2(std::ostream & out, aig_ref const & r) const; unsigned get_num_aigs() const; - void cancel() { set_cancel(true); } - void reset_cancel() { set_cancel(false); } void set_cancel(bool f); }; diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index d396359a3..9bf967be3 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -172,18 +172,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index a1aa0bdc8..e8fb72be4 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -319,18 +319,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index b534c8295..1a33bf4f2 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -398,20 +398,13 @@ public: } virtual void cleanup() { - unsigned num_conflicts = m_imp->m_num_conflicts; - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); + d->m_num_conflicts = m_imp->m_num_conflicts; #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_conflicts = num_conflicts; } protected: diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 4eec83037..dc17a4f87 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -333,18 +333,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index d2e3ebf1f..693066ee1 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -338,18 +338,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index c4b7cbaf3..c180029ae 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1682,18 +1682,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void operator()(goal_ref const & in, diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 9ee8f6728..33d5f138e 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -345,18 +345,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index a62b311b5..323903f6c 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -191,17 +191,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 89195a9d5..643195b05 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1002,17 +1002,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index 12954005f..d7e4f30d2 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) { } void propagate_ineqs_tactic::cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 3b1a86345..3d222cf56 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -425,18 +425,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 7c7eca33b..5dbfc4ebd 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -144,18 +144,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned get_num_steps() const { diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 8dcaf2112..5f20015ca 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -465,18 +465,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned get_num_steps() const { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index d3fdb6e56..e149afc75 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) { } void bv_size_reduction_tactic::cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index f60487d60..56b18dd8d 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -311,18 +311,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m(), m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 1f560ef62..aca6d9084 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const } cofactor_elim_term_ite::~cofactor_elim_term_ite() { - imp * d = m_imp; - #pragma omp critical (cofactor_elim_term_ite) - { - m_imp = 0; - } - dealloc(d); + dealloc(m_imp); } void cofactor_elim_term_ite::updt_params(params_ref const & p) { @@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) { } void cofactor_elim_term_ite::set_cancel(bool f) { - #pragma omp critical (cofactor_elim_term_ite) - { - if (m_imp) - m_imp->set_cancel(f); - } + if (m_imp) + m_imp->set_cancel(f); } void cofactor_elim_term_ite::cleanup() { - ast_manager & m = m_imp->m; - #pragma omp critical (cofactor_elim_term_ite) + ast_manager & m = m_imp->m; + imp * d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) { - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + std::swap(d, m_imp); } + dealloc(d); } diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h index ce2f31ea0..e734fcad6 100644 --- a/src/tactic/core/cofactor_elim_term_ite.h +++ b/src/tactic/core/cofactor_elim_term_ite.h @@ -37,8 +37,9 @@ public: void cancel() { set_cancel(true); } void reset_cancel() { set_cancel(false); } - void set_cancel(bool f); void cleanup(); + void set_cancel(bool f); + }; #endif diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 71f4771a9..bb38d28ce 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) { void ctx_simplify_tactic::cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index c2245b409..2277c3fa8 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -90,17 +90,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 456bad5e0..e49884004 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -174,17 +174,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 4d64bf061..6d7bcb2f2 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -1036,18 +1036,13 @@ public: virtual void cleanup() { unsigned num_elim_apps = get_num_elim_apps(); - ast_manager & m = m_imp->m_manager; - imp * d = m_imp; + ast_manager & m = m_imp->m_manager; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } m_imp->m_num_elim_apps = num_elim_apps; } diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index f8f6174b9..9b974ae19 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -225,18 +225,12 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m_imp->m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 1e358177f..5873efd61 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -255,17 +255,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 59ed2dcd3..99375e6e8 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -541,17 +541,12 @@ void reduce_args_tactic::set_cancel(bool f) { } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; + ast_manager & m = m_imp->m(); + imp * d = alloc(imp, m); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 32f3fd7f7..80be97b0b 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -118,17 +118,12 @@ void simplify_tactic::set_cancel(bool f) { void simplify_tactic::cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } unsigned simplify_tactic::get_num_steps() const { diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index fc9cb393c..1ba5a6da8 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -43,9 +43,11 @@ public: virtual void cleanup(); unsigned get_num_steps() const; - virtual void set_cancel(bool f); virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); } +protected: + virtual void set_cancel(bool f); + }; tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 995940406..3b0a57d20 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -749,23 +749,19 @@ public: virtual void cleanup() { unsigned num_elim_vars = m_imp->m_num_eliminated_vars; ast_manager & m = m_imp->m(); - imp * d = m_imp; expr_replacer * r = m_imp->m_r; if (r) r->set_substitution(0); bool owner = m_imp->m_r_owner; m_imp->m_r_owner = false; // stole replacer + + imp * d = alloc(imp, m, m_params, r, owner); + d->m_num_eliminated_vars = num_elim_vars; #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params, r, owner); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_eliminated_vars = num_elim_vars; } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index b6c4b0655..c5be7ab1f 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -898,20 +898,14 @@ public: } virtual void cleanup() { - unsigned num_aux_vars = m_imp->m_num_aux_vars; ast_manager & m = m_imp->m; - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); + d->m_num_aux_vars = m_imp->m_num_aux_vars; #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - m_imp->m_num_aux_vars = num_aux_vars; } virtual void set_cancel(bool f) { diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 3a6b7ea45..4a3a01b6f 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -138,19 +138,13 @@ public: (*m_imp)(in, result, mc, pc, core); } - virtual void cleanup() { - ast_manager & m = m_imp->m; - imp * d = m_imp; + virtual void cleanup() { + imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { - d = m_imp; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } protected: diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 619e56ef2..de8769c07 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -79,17 +79,12 @@ public: } virtual void cleanup() { - sls_engine * d = m_engine; + sls_engine * d = alloc(sls_engine, m, m_params); #pragma omp critical (tactic_cancel) { - d = m_engine; + std::swap(d, m_engine); } dealloc(d); - d = alloc(sls_engine, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_engine = d; - } } virtual void collect_statistics(statistics & st) const { diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 80de1bcd0..8b4f9f576 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -47,7 +47,6 @@ public: void cancel(); void reset_cancel(); - virtual void set_cancel(bool f) {} /** \brief Apply tactic to goal \c in. @@ -96,6 +95,13 @@ public: // translate tactic to the given manager virtual tactic * translate(ast_manager & m) = 0; +private: + friend class nary_tactical; + friend class binary_tactical; + friend class unary_tactical; + + virtual void set_cancel(bool f) {} + }; typedef ref tactic_ref; diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 893047397..cfb4ec194 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -102,11 +102,8 @@ protected: \brief Reset cancel flag of t if this was not canceled. */ void parent_reset_cancel(tactic & t) { - #pragma omp critical (tactic_cancel) - { - if (!m_cancel) { - t.set_cancel(false); - } + if (!m_cancel) { + t.reset_cancel(); } } @@ -393,11 +390,8 @@ protected: \brief Reset cancel flag of st if this was not canceled. */ void parent_reset_cancel(tactic & t) { - #pragma omp critical (tactic_cancel) - { - if (!m_cancel) { - t.set_cancel(false); - } + if (!m_cancel) { + t.reset_cancel(); } } @@ -988,7 +982,7 @@ protected: virtual void set_cancel(bool f) { m_cancel = f; if (m_t) - m_t->set_cancel(f); + m_t->set_cancel(f); } template diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 14a42ec51..2f0262fc8 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -144,17 +144,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 393a40603..cea8f2cfc 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -151,17 +151,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index 0705c627c..efecb38ba 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -119,17 +119,12 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m(); - imp * d = m_imp; + imp * d = alloc(imp, m, m_params); #pragma omp critical (tactic_cancel) { - m_imp = 0; + std::swap(d, m_imp); } dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } } virtual void set_cancel(bool f) { diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index bb991c65f..39ea06959 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -58,8 +58,12 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params, ctx_q.updt_params(params); { parser* p = parser::create(ctx_q,m); - TRUSTME( p->parse_file(problem_file) ); + bool ok = p->parse_file(problem_file); dealloc(p); + if (!ok) { + std::cout << "Could not parse: " << problem_file << "\n"; + return; + } } relation_manager & rel_mgr_q = ctx_b.get_rel_context()->get_rmanager(); @@ -143,8 +147,12 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) { ctx.updt_params(params); { wpa_parser* p = wpa_parser::create(ctx, m); - TRUSTME( p->parse_directory(problem_dir) ); + bool ok = p->parse_directory(problem_dir); dealloc(p); + if (!ok) { + std::cout << "Could not parse: " << problem_dir << "\n"; + return; + } } const unsigned attempts = 10; @@ -213,8 +221,12 @@ void tst_dl_query() { ctx_base.updt_params(params); { parser* p = parser::create(ctx_base,m); - TRUSTME( p->parse_file(problem_file) ); + bool ok = p->parse_file(problem_file); dealloc(p); + if (!ok) { + std::cout << "Could not parse: " << problem_file << "\n"; + return; + } } ctx_base.get_rel_context()->saturate(); diff --git a/src/util/debug.h b/src/util/debug.h index 9e519982f..a36743f73 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -73,7 +73,7 @@ bool is_debug_enabled(const char * tag); UNREACHABLE(); \ } #else -#define VERIFY(_x_) (_x_) +#define VERIFY(_x_) (void)(_x_) #endif #define MAKE_NAME2(LINE) zofty_ ## LINE diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 3f2e224d9..45088d5d4 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -35,6 +35,7 @@ static long long g_memory_max_used_size = 0; static long long g_memory_watermark = 0; static bool g_exit_when_out_of_memory = false; static char const * g_out_of_memory_msg = "ERROR: out of memory"; +static volatile bool g_memory_fully_initialized = false; void memory::exit_when_out_of_memory(bool flag, char const * msg) { g_exit_when_out_of_memory = flag; @@ -83,10 +84,18 @@ void memory::initialize(size_t max_size) { initialize = true; } } - if (!initialize) - return; - g_memory_out_of_memory = false; - mem_initialize(); + if (initialize) { + g_memory_out_of_memory = false; + mem_initialize(); + g_memory_fully_initialized = true; + } + else { + // Delay the current thread until the DLL is fully initialized + // Without this, multiple threads can start to call API functions + // before memory::initialize(...) finishes. + while (!g_memory_fully_initialized) + /* wait */ ; + } } bool memory::is_out_of_memory() { @@ -98,9 +107,9 @@ bool memory::is_out_of_memory() { return r; } -void memory::set_high_watermark(size_t watermak) { +void memory::set_high_watermark(size_t watermark) { // This method is only safe to invoke at initialization time, that is, before the threads are created. - g_memory_watermark = watermak; + g_memory_watermark = watermark; } bool memory::above_high_watermark() { diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 603898af8..8ff5f8e8f 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -165,6 +165,14 @@ public: SASSERT(e); return e->get_data().m_value; } + + value const & operator[](key * k) const { + return find(k); + } + + value & operator[](key * k) { + return find(k); + } iterator find_iterator(Key * k) const { return m_table.find(key_data(k)); diff --git a/src/util/util.h b/src/util/util.h index 0aa8f881d..eb24ece13 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -24,6 +24,9 @@ Revision History: #include #include #include +#ifdef _MSC_VER +#include +#endif #ifndef SIZE_MAX #define SIZE_MAX std::numeric_limits::max() @@ -95,7 +98,12 @@ unsigned uint64_log2(uint64 v); COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); // Return the number of 1 bits in v. -inline unsigned get_num_1bits(unsigned v) { +static inline unsigned get_num_1bits(unsigned v) { +#ifdef _MSC_VER + return __popcnt(v); +#elif defined(__GNUC__) + return __builtin_popcount(v); +#else #ifdef Z3DEBUG unsigned c; unsigned v1 = v; @@ -108,15 +116,16 @@ inline unsigned get_num_1bits(unsigned v) { unsigned r = (((v + (v >> 4)) & 0xF0F0F0F) * 0x1010101) >> 24; SASSERT(c == r); return r; +#endif } // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64. // So, I'm using the following two definitions to fix the problem -inline uint64 shift_right(uint64 x, uint64 y) { +static inline uint64 shift_right(uint64 x, uint64 y) { return y < 64ull ? (x >> y) : 0ull; } -inline uint64 shift_left(uint64 x, uint64 y) { +static inline uint64 shift_left(uint64 x, uint64 y) { return y < 64ull ? (x << y) : 0ull; } @@ -255,10 +264,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair const & p return out; } -#ifndef _WINDOWS -#define __forceinline inline -#endif - template bool has_duplicates(const IT & begin, const IT & end) { for (IT it1 = begin; it1 != end; ++it1) {