diff --git a/CMakeLists.txt b/CMakeLists.txt index 28ff64568..cd9c14435 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,7 @@ endif() ################################################################################ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 8) -set(Z3_VERSION_PATCH 2) +set(Z3_VERSION_PATCH 3) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/RELEASE_NOTES b/RELEASE_NOTES index acdb627d8..dcb8fc093 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -1,5 +1,19 @@ RELEASE NOTES +Version 4.8.3 +============= +- New features + - native handling of recursive function definitions + - PB rounding based option for conflict resolution when reasoning about PB constraints. + +Version 4.8.2 +============= +- Post-Release. + +Version 4.8.1 +============= +- Release. Bug-fix for 4.8.0 + Version 4.8.0 ============= diff --git a/doc/design_recfuns.md b/doc/design_recfuns.md new file mode 100644 index 000000000..89980931e --- /dev/null +++ b/doc/design_recfuns.md @@ -0,0 +1,93 @@ +# Design for handling recursive functions + +Main source of inspiration is [Sutter, Köksal & Kuncak 2011], +as implemented in Leon, but the main +differences is that we should unroll function definitions directly from the +inside of Z3, in a backtracking way. Termination and fairness are ensured by +iterative-deepening on the maximum number of unrollings in a given branch. + +## Unfolding + +The idea is that every function definition `f(x1…xn) := rhs[x1…xn]` is +compiled into: + +- a list of cases `A_f_i[x1…xn] => f(x1…xn) = rhs_i[x1…xn]`. + When `A_f_i[t1…tn]` becomes true in the model, `f(t1…tn)` is said to be + *unfolded* and the clause `A_f_i[t1…tn] => f(t1…tn) = rhs_i[t1…tn]` + is added as an auxiliary clause. +- a list of constraints `Γ_f_i[x1…xn] <=> A_f_i[x1…xn]` + that states when `A_f_i[x1…xn]` should be true, depending on inputs `x1…xn`. + For every term `f(t1…tn)` present in congruence closure, we + immediately add all the `Γ_f_i[t1…tn] <=> A_f_i[t1…tn]` as auxiliary clauses + (maybe during internalization of `f(t1…tn)`?). + +where each `A_f_i[x1…xn]` is a special new predicate representing the +given case of `f`, and `rhs_i` does not contain any `ite`. +We assume pattern matching has been compiled to `ite` beforehand. + +For example, `fact(n) := if n<2 then 1 else n * fact(n-1)` is compiled into: + +- `A_fact_0[n] => fact(n) = 1` +- `A_fact_1[n] => fact(n) = n * fact(n-1)` +- `A_fact_0[n] <=> n < 2` +- `A_fact_1[n] <=> ¬(n < 2)` + +The 2 first clauses are only added when `A_fact_0[t]` is true +(respectively `A_fact_1[t]` is true). +The 2 other clauses are added as soon as `fact(t)` is internalized. + +## Termination + +To ensure termination, we define variables: + +- `unfold_depth: int` +- `current_max_unfold_depth: int` +- `global_max_unfold_depth: int` + +and a special literal `[max_depth=$n]` for each `n:int`. +Solving is done under the local assumption +`[max_depth=$current_max_unfold_depth]` (this should be handled in some outer +loop, e.g. in a custom tactic). + +Whenever `A_f_i[t1…tn]` becomes true (for any `f`), we increment +`unfold_depth`. If `unfold_depth > current_max_unfold_depth`, then +the conflict clause `[max_depth=$current_max_unfold_depth] => Γ => false` +where `Γ` is the conjunction of all `A_f_i[t1…tn]` true in the trail. + +For non-recursive functions, we don't have to increment `unfold_depth`. Some other functions that are known + +If the solver answers "SAT", we have a model. +Otherwise, if `[max_depth=$current_max_unfold_depth]` is part of the +unsat-core, then we increase `current_max_unfold_depth`. +If `current_max_unfold_depth == global_max_unfold_depth` then +we report "UNKNOWN" (reached global depth limit), otherwise we can +try to `solve()` again with the new assumption (higher depth limit). + +## Tactic + +there should be a parametrized tactic `funrec(t, n)` where `t` is the tactic +used to solve (under assumption that depth is limited to `current_max_unfold_depth`) +and `n` is an integer that is assigned to `global_max_unfold_depth`. + +This way, to try and find models for a problem with recursive functions + LIA, +one could use something like `(funrec (then simplify dl smt) 100)`. + +## Expected benefits + +This addition to Z3 would bring many benefits compared to current alternatives (Leon, quantifiers, …) + +- should be very fast and lightweight + (compared to Leon or quantifiers). + In particular, every function call is very lightweight even compared to Leon (no need for full model building, followed by unsat core extraction) +- possibility of answering "SAT" for any `QF_*` fragment + + recursive functions +- makes `define-funs-rec` a first-class citizen of the language, usable to model user-defined theories or to analyze functional + programs directly + +## Optimizations + +- maybe `C_f_i` literals should never be decided on + (they can always be propagated). + Even stronger: they should not be part of conflicts? + (i.e. tune conflict resolution to always resolve + these literals away, disregarding their level) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 3089f5e2b..ab9c73209 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1190,6 +1190,20 @@ void mk_model_example() { std::cout << m.eval(a + b < 2)<< std::endl; } +void recfun_example() { + std::cout << "recfun example\n"; + context c; + expr x = c.int_const("x"); + expr y = c.int_const("y"); + expr b = c.bool_const("b"); + sort I = c.int_sort(); + sort B = c.bool_sort(); + func_decl f = recfun("f", I, B, I); + expr_vector args(c); + args.push_back(x); args.push_back(b); + c.recdef(f, args, ite(b, x, f(x + 1, !b))); + prove(f(x,c.bool_val(false)) > x); +} int main() { @@ -1239,6 +1253,7 @@ int main() { consequence_example(); std::cout << "\n"; parse_example(); std::cout << "\n"; mk_model_example(); std::cout << "\n"; + recfun_example(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 18d57e729..5bd96c0fc 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 8, 2, 0) + set_version(4, 8, 3, 0) add_lib('util', [], includes2install = ['z3_version.h']) add_lib('polynomial', ['util'], 'math/polynomial') add_lib('sat', ['util']) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index a28315cda..cbe365c6c 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -38,6 +38,8 @@ Revision History: #include "util/cancel_eh.h" #include "util/scoped_timer.h" #include "ast/pp_params.hpp" +#include "ast/expr_abstract.h" + extern bool is_numeral_sort(Z3_context c, Z3_sort ty); @@ -110,6 +112,54 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const* domain, + Z3_sort range) { + Z3_TRY; + LOG_Z3_mk_rec_func_decl(c, s, domain_size, domain, range); + RESET_ERROR_CODE(); + // + recfun::promise_def def = + mk_c(c)->recfun().get_plugin().mk_def(to_symbol(s), + domain_size, + to_sorts(domain), + to_sort(range)); + func_decl* d = def.get_def()->get_decl(); + mk_c(c)->save_ast_trail(d); + RETURN_Z3(of_func_decl(d)); + Z3_CATCH_RETURN(nullptr); + } + + void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body) { + Z3_TRY; + LOG_Z3_add_rec_def(c, f, n, args, body); + func_decl* d = to_func_decl(f); + ast_manager& m = mk_c(c)->m(); + recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin(); + expr_ref abs_body(m); + expr_ref_vector _args(m); + var_ref_vector _vars(m); + for (unsigned i = 0; i < n; ++i) { + _args.push_back(to_expr(args[i])); + _vars.push_back(m.mk_var(n - i - 1, m.get_sort(_args.back()))); + if (m.get_sort(_args.back()) != d->get_domain(i)) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + return; + } + } + expr_abstract(m, 0, n, _args.c_ptr(), to_expr(body), abs_body); + recfun::promise_def pd = p.get_promise_def(d); + if (!pd.get_def()) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + return; + } + if (m.get_sort(abs_body) != d->get_range()) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + return; + } + p.set_definition(pd, n, _vars.c_ptr(), abs_body); + Z3_CATCH; + } + Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const * args) { Z3_TRY; LOG_Z3_mk_app(c, d, num_args, args); diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index c236ba3e8..9fe13a15f 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -79,6 +79,7 @@ namespace api { m_datalog_util(m()), m_fpa_util(m()), m_sutil(m()), + m_recfun(m()), m_last_result(m()), m_ast_trail(m()), m_pmanager(m_limit) { diff --git a/src/api/api_context.h b/src/api/api_context.h index a6f55d1aa..a6b8600d6 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -29,6 +29,7 @@ Revision History: #include "ast/datatype_decl_plugin.h" #include "ast/dl_decl_plugin.h" #include "ast/fpa_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "util/event_handler.h" @@ -62,6 +63,7 @@ namespace api { datalog::dl_decl_util m_datalog_util; fpa_util m_fpa_util; seq_util m_sutil; + recfun::util m_recfun; // Support for old solver API smt_params m_fparams; @@ -128,6 +130,7 @@ namespace api { fpa_util & fpautil() { return m_fpa_util; } datatype_util& dtutil() { return m_dt_plugin->u(); } seq_util& sutil() { return m_sutil; } + recfun::util& recfun() { return m_recfun; } family_id get_basic_fid() const { return m_basic_fid; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return m_arith_fid; } diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 06207cee6..ae21885a9 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -715,6 +715,4 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - - }; diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 10ba9faa0..0b0c694d7 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) Microsoft Corporation, Arive Gurfinkel 2017 +Copyright (c) Microsoft Corporation, Arie Gurfinkel 2017 Module Name: diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 07056746d..d360b6153 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -311,6 +311,13 @@ namespace z3 { func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range); func_decl function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range); + func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range); + func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range); + func_decl recfun(char const * name, sort const & domain, sort const & range); + func_decl recfun(char const * name, sort const & d1, sort const & d2, sort const & range); + + void recdef(func_decl, expr_vector const& args, expr const& body); + expr constant(symbol const & name, sort const & s); expr constant(char const * name, sort const & s); expr bool_const(char const * name); @@ -2815,6 +2822,37 @@ namespace z3 { return func_decl(*this, f); } + inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) { + array args(arity); + for (unsigned i = 0; i < arity; i++) { + check_context(domain[i], range); + args[i] = domain[i]; + } + Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range); + check_error(); + return func_decl(*this, f); + + } + + inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) { + return recfun(str_symbol(name), arity, domain, range); + } + + inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) { + return recfun(str_symbol(name), 1, &d1, range); + } + + inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) { + sort dom[2] = { d1, d2 }; + return recfun(str_symbol(name), 2, dom, range); + } + + void context::recdef(func_decl f, expr_vector const& args, expr const& body) { + check_context(f, args); check_context(f, body); + array vars(args); + Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body); + } + inline expr context::constant(symbol const & name, sort const & s) { Z3_ast r = Z3_mk_const(m_ctx, name, s); check_error(); @@ -2976,6 +3014,19 @@ namespace z3 { return range.ctx().function(name.c_str(), domain, range); } + inline func_decl recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) { + return range.ctx().recfun(name, arity, domain, range); + } + inline func_decl recfun(char const * name, unsigned arity, sort const * domain, sort const & range) { + return range.ctx().recfun(name, arity, domain, range); + } + inline func_decl recfun(char const * name, sort const& d1, sort const & range) { + return range.ctx().recfun(name, d1, range); + } + inline func_decl recfun(char const * name, sort const& d1, sort const& d2, sort const & range) { + return range.ctx().recfun(name, d1, d2, range); + } + inline expr select(expr const & a, expr const & i) { check_context(a, i); Z3_ast r = Z3_mk_select(a.ctx(), a, i); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 97541e31f..ac11022c1 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -532,6 +532,34 @@ namespace Microsoft.Z3 return new FuncDecl(this, MkSymbol(name), domain, range); } + /// + /// Creates a new recursive function declaration. + /// + public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range) + { + Debug.Assert(range != null); + Debug.Assert(domain.All(d => d != null)); + + CheckContextMatch(domain); + CheckContextMatch(range); + return new FuncDecl(this, MkSymbol(name), domain, range, true); + } + + /// + /// Bind a definition to a recursive function declaration. + /// The function must have previously been created using + /// MkRecFuncDecl. The body may contain recursive uses of the function or + /// other mutually recursive functions. + /// + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + { + CheckContextMatch(f); + CheckContextMatch(args); + CheckContextMatch(body); + IntPtr[] argsNative = AST.ArrayToNative(args); + Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); + } + /// /// Creates a new function declaration. /// diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 24ae456d8..30ed790db 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -302,6 +302,15 @@ namespace Microsoft.Z3 Debug.Assert(range != null); } + internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range, bool is_rec) + : base(ctx, Native.Z3_mk_rec_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject)) + { + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(range != null); + } + + #if DEBUG internal override void CheckNativeObject(IntPtr obj) { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d466d2e77..f68b908e2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1,4 +1,5 @@ + ############################################ # Copyright (c) 2012 Microsoft Corporation # @@ -799,6 +800,49 @@ def Function(name, *sig): def _to_func_decl_ref(a, ctx): return FuncDeclRef(a, ctx) +def RecFunction(name, *sig): + """Create a new Z3 recursive with the given sorts.""" + sig = _get_args(sig) + if __debug__: + _z3_assert(len(sig) > 0, "At least two arguments expected") + arity = len(sig) - 1 + rng = sig[arity] + if __debug__: + _z3_assert(is_sort(rng), "Z3 sort expected") + dom = (Sort * arity)() + for i in range(arity): + if __debug__: + _z3_assert(is_sort(sig[i]), "Z3 sort expected") + dom[i] = sig[i].ast + ctx = rng.ctx + return FuncDeclRef(Z3_mk_rec_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx) + +def RecAddDefinition(f, args, body): + """Set the body of a recursive function. + Recursive definitions are only unfolded during search. + >>> ctx = Context() + >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) + >>> n = Int('n', ctx) + >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) + >>> simplify(fac(5)) + fac(5) + >>> s = Solver(ctx=ctx) + >>> s.add(fac(n) < 3) + >>> s.check() + sat + >>> s.model().eval(fac(5)) + 120 + """ + if is_app(args): + args = [args] + ctx = body.ctx + args = _get_args(args) + n = len(args) + _args = (Ast * n)() + for i in range(n): + _args[i] = args[i].ast + Z3_add_rec_def(ctx.ref(), f.ast, n, _args, body.ast) + ######################################### # # Expressions @@ -6511,8 +6555,8 @@ class Solver(Z3PPObject): >>> s.add(x > 0, x < 2) >>> s.check() sat - >>> s.model() - [x = 1] + >>> s.model().eval(x) + 1 >>> s.add(x < 1) >>> s.check() unsat diff --git a/src/api/z3_api.h b/src/api/z3_api.h index de446d9a8..a776bbe8e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2081,6 +2081,7 @@ extern "C" { Z3_sort range); + /** \brief Create a constant or function application. @@ -2140,6 +2141,48 @@ extern "C" { def_API('Z3_mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT))) */ Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty); + + + /** + \brief Declare a recursive function + + \param c logical context. + \param s name of the function. + \param domain_size number of arguments. It should be greater than 0. + \param domain array containing the sort of each argument. The array must contain domain_size elements. + \param range sort of the constant or the return sort of the function. + + After declaring recursive function, it should be associated with a recursive definition #Z3_mk_rec_def. + The function #Z3_mk_app can be used to create a constant or function + application. + + \sa Z3_mk_app + \sa Z3_mk_rec_def + + def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) + */ + Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, + unsigned domain_size, Z3_sort const domain[], + Z3_sort range); + + /** + \brief Define the body of a recursive function. + + \param c logical context. + \param f function declaration. + \param n number of arguments to the function + \param args constants that are used as arguments to the recursive function in the definition. + \param body body of the recursive function + + After declaring a recursive function or a collection of mutually recursive functions, use + this function to provide the definition for the recursive function. + + \sa Z3_mk_rec_func_decl + + def_API('Z3_add_rec_def', VOID, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST), _in(AST))) + */ + void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body); + /*@}*/ /** @name Propositional Logic and Equality */ diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 80543bb05..ce2817b58 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(ast ast_translation.cpp ast_util.cpp bv_decl_plugin.cpp + csp_decl_plugin.cpp datatype_decl_plugin.cpp decl_collector.cpp dl_decl_plugin.cpp @@ -35,6 +36,7 @@ z3_add_component(ast occurs.cpp pb_decl_plugin.cpp pp.cpp + recfun_decl_plugin.cpp reg_decl_plugins.cpp seq_decl_plugin.cpp shared_occs.cpp diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 09f082522..aea8863af 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -361,6 +361,9 @@ public: app * mk_int(int i) { return mk_numeral(rational(i), true); } + app * mk_int(rational const& r) { + return mk_numeral(r, true); + } app * mk_real(int i) { return mk_numeral(rational(i), false); } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 99e861b16..9a5e1de9c 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -16,8 +16,8 @@ Author: Revision History: --*/ -#include -#include +#include +#include #include "ast/ast.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" @@ -1360,7 +1360,8 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs): m_proof_mode(disable_proofs ? PGM_DISABLED : src.m_proof_mode), m_trace_stream(src.m_trace_stream), m_trace_stream_owner(false), - m_rec_fun(":rec-fun") { + m_rec_fun(":rec-fun"), + m_lambda_def(":lambda-def") { SASSERT(!src.is_format_manager()); m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true); init(); @@ -1541,6 +1542,10 @@ void ast_manager::raise_exception(char const * msg) { throw ast_exception(msg); } +void ast_manager::raise_exception(std::string const& msg) { + throw ast_exception(msg.c_str()); +} + std::ostream& ast_manager::display(std::ostream& out, parameter const& p) { switch (p.get_kind()) { diff --git a/src/ast/ast.h b/src/ast/ast.h index ee39f4032..4054b32dc 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -707,6 +707,10 @@ public: func_decl * get_decl() const { return m_decl; } family_id get_family_id() const { return get_decl()->get_family_id(); } decl_kind get_decl_kind() const { return get_decl()->get_decl_kind(); } + symbol const& get_name() const { return get_decl()->get_name(); } + unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); } + parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); } + parameter const* get_parameters() const { return get_decl()->get_parameters(); } bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; } unsigned get_num_args() const { return m_num_args; } expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; } @@ -1558,7 +1562,7 @@ public: // Equivalent to throw ast_exception(msg) Z3_NORETURN void raise_exception(char const * msg); - Z3_NORETURN void raise_exception(std::string const& msg) { raise_exception(msg.c_str()); } + Z3_NORETURN void raise_exception(std::string const& s); std::ostream& display(std::ostream& out, parameter const& p); @@ -1632,7 +1636,7 @@ public: bool are_distinct(expr * a, expr * b) const; bool contains(ast * a) const { return m_ast_table.contains(a); } - + bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; } bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; } func_decl* get_rec_fun_decl(quantifier* q) const; @@ -2497,6 +2501,7 @@ public: void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); } }; + typedef ast_ref_fast_mark<1> ast_ref_fast_mark1; typedef ast_ref_fast_mark<2> ast_ref_fast_mark2; typedef ast_ref_fast_mark1 expr_ref_fast_mark1; diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h index 5629f847a..bfb92c920 100644 --- a/src/ast/ast_pp.h +++ b/src/ast/ast_pp.h @@ -32,5 +32,27 @@ struct mk_pp : public mk_ismt2_pp { } }; +//> recfuns; + recfun::util u(m); + func_decl_ref_vector funs = u.get_rec_funs(); + if (funs.empty()) return; + for (func_decl * f : funs) { + recfuns.push_back(std::make_pair(f, u.get_def(f).get_rhs())); + } + ast_smt2_pp_recdefs(out, recfuns, m_env); } void ast_pp_util::remove_decl(func_decl* f) { diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h index c3b8aa601..e70880672 100644 --- a/src/ast/ast_pp_util.h +++ b/src/ast/ast_pp_util.h @@ -31,7 +31,7 @@ class ast_pp_util { decl_collector coll; - ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m, false) {} + ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m) {} void collect(expr* e); diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 3a55bbb0b..5f2d36279 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1163,6 +1163,33 @@ public: unregister_var_names(f->get_arity()); } + // format set of mutually recursive definitions + void operator()(vector> const& funs, format_ref & r) { + format_ref_vector decls(m()), bodies(m()); + format_ref r1(m()), r2(m()); + + for (auto const& p : funs) { + unsigned len; + func_decl* f = p.first; + expr* e = p.second; + format * fname = m_env.pp_fdecl_name(f, len); + register_var_names(f->get_arity()); + format * args[3]; + args[0] = fname; + args[1] = pp_var_args(f->get_arity(), f->get_domain()); + args[2] = m_env.pp_sort(f->get_range()); + decls.push_back(mk_seq1(m(), args, args+3, f2f(), "")); + process(e, r); + bodies.push_back(r); + unregister_var_names(f->get_arity()); + } + r1 = mk_seq1(m(), decls.begin(), decls.end(), f2f(), ""); + r2 = mk_seq1(m(), bodies.begin(), bodies.end(), f2f(), ""); + format * args[2]; + args[0] = r1; + args[1] = r2; + r = mk_seq1(m(), args, args+2, f2f(), "define-rec-funs"); + } }; @@ -1275,6 +1302,16 @@ std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, return out; } +std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector> const& funs, smt2_pp_environment & env, params_ref const & p) { + ast_manager & m = env.get_manager(); + format_ref r(fm(m)); + smt2_printer pr(env, p); + pr(funs, r); + pp(out, r.get(), m, p); + return out; +} + + mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix): m_ast(t), m_manager(m), diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index 13093f138..dc306c6df 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -105,6 +105,8 @@ std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & e std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun"); std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun"); std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref()); +std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref()); + /** \brief Internal wrapper (for debugging purposes only) diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 5e2828adf..227e00419 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -980,14 +980,6 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { } } - for (unsigned i = 0; i < decls.get_num_preds(); ++i) { - func_decl* d = decls.get_pred_decls()[i]; - if (!(*m_is_declared)(d)) { - smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); - p(d); - strm << "\n"; - } - } #endif for (expr* a : m_assumptions) { diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp new file mode 100644 index 000000000..21cd798b2 --- /dev/null +++ b/src/ast/csp_decl_plugin.cpp @@ -0,0 +1,374 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + csp_decl_plugin.h + +Abstract: + + Declarations used for a job-shop scheduling domain. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-8-9 + +Revision History: + + +--*/ +#include "ast/csp_decl_plugin.h" +#include "ast/arith_decl_plugin.h" + +void csp_decl_plugin::set_manager(ast_manager* m, family_id fid) { + decl_plugin::set_manager(m, fid); + m_int_sort = m_manager->mk_sort(m_manager->mk_family_id("arith"), INT_SORT); + m_alist_sort = m_manager->mk_sort(symbol("AList"), sort_info(m_family_id, ALIST_SORT)); + m_job_sort = m_manager->mk_sort(symbol("Job"), sort_info(m_family_id, JOB_SORT)); + m_resource_sort = m_manager->mk_sort(symbol("Resource"), sort_info(m_family_id, RESOURCE_SORT)); + m_manager->inc_ref(m_int_sort); + m_manager->inc_ref(m_resource_sort); + m_manager->inc_ref(m_job_sort); + m_manager->inc_ref(m_alist_sort); +} + +void csp_decl_plugin::finalize() { + m_manager->dec_ref(m_alist_sort); + m_manager->dec_ref(m_job_sort); + m_manager->dec_ref(m_resource_sort); + m_manager->dec_ref(m_int_sort); +} + +sort * csp_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { + if (num_parameters != 0) { + m_manager->raise_exception("no parameters expected with job-shop sort"); + } + switch (static_cast(k)) { + case JOB_SORT: return m_job_sort; + case RESOURCE_SORT: return m_resource_sort; + case ALIST_SORT: return m_alist_sort; + default: UNREACHABLE(); return nullptr; + } +} + +func_decl * csp_decl_plugin::mk_func_decl( + decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) { + symbol name; + sort* rng = nullptr; + switch (static_cast(k)) { + case OP_JS_JOB: + check_arity(arity); + check_index1(num_parameters, parameters); + name = symbol("job"); + rng = m_job_sort; + break; + case OP_JS_RESOURCE: + check_arity(arity); + check_index1(num_parameters, parameters); + name = symbol("resource"); + rng = m_resource_sort; + break; + case OP_JS_RESOURCE_MAKESPAN: + if (arity != 1 || domain[0] != m_resource_sort) m_manager->raise_exception("makespan expects a resource argument"); + name = symbol("makespan"); + rng = m_int_sort; + break; + case OP_JS_START: + if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("start expects a job argument"); + if (num_parameters > 0) m_manager->raise_exception("no parameters"); + name = symbol("job-start"); + rng = m_int_sort; + break; + case OP_JS_END: + if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("resource expects a job argument"); + if (num_parameters > 0) m_manager->raise_exception("no parameters"); + name = symbol("job-end"); + rng = m_int_sort; + break; + case OP_JS_JOB2RESOURCE: + if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("job2resource expects a job argument"); + if (num_parameters > 0) m_manager->raise_exception("no parameters"); + name = symbol("job2resource"); + rng = m_resource_sort; + break; + case OP_JS_MODEL: + // has no parameters + // all arguments are of sort alist + name = symbol("js-model"); + rng = m_manager->mk_bool_sort(); + break; + case OP_JS_JOB_RESOURCE: + if (arity != 6) m_manager->raise_exception("add-job-resource expects 6 arguments"); + if (domain[0] != m_job_sort) m_manager->raise_exception("first argument of add-job-resource expects should be a job"); + if (domain[1] != m_resource_sort) m_manager->raise_exception("second argument of add-job-resource expects should be a resource"); + if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer"); + if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer"); + if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer"); + if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties"); + name = symbol("add-job-resource"); + rng = m_alist_sort; + break; + case OP_JS_RESOURCE_AVAILABLE: + if (arity != 6) m_manager->raise_exception("add-resource-available expects 6 arguments"); + if (domain[0] != m_resource_sort) m_manager->raise_exception("first argument of add-resource-available expects should be a resource"); + if (domain[2] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer"); + if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer"); + if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer"); + if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer"); + if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be an a list of properties"); + name = symbol("add-resource-available"); + rng = m_alist_sort; + break; + case OP_JS_JOB_PREEMPTABLE: + if (arity != 1 || domain[0] != m_job_sort) + m_manager->raise_exception("set-preemptable expects one argument, which is a job"); + name = symbol("set-preemptable"); + rng = m_alist_sort; + break; + case OP_JS_PROPERTIES: + if (arity != 0) m_manager->raise_exception("js-properties takes no arguments"); + for (unsigned i = 0; i < num_parameters; ++i) { + if (!parameters[i].is_symbol()) m_manager->raise_exception("js-properties expects a list of keyword parameters"); + } + name = symbol("js-properties"); + rng = m_alist_sort; + break; + case OP_JS_JOB_GOAL: + if (arity != 1 || domain[0] != m_job_sort) + m_manager->raise_exception("add-job-goal expects one argument, which is a job"); + if (num_parameters != 2 || !parameters[0].is_symbol() || !parameters[1].is_int()) + m_manager->raise_exception("add-job-goal expects one symbol and one integer parameter"); + name = symbol("add-job-goal"); + rng = m_alist_sort; + break; + case OP_JS_OBJECTIVE: + if (arity != 0) + m_manager->raise_exception("add-optimization-objective expects no arguments"); + if (num_parameters != 1 || !parameters[0].is_symbol()) + m_manager->raise_exception("add-optimization-objective expects one symbol parameter"); + name = symbol("add-optimization-objective"); + rng = m_alist_sort; + break; + default: + UNREACHABLE(); + return nullptr; + } + return m_manager->mk_func_decl(name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + +} + +void csp_decl_plugin::check_arity(unsigned arity) { + if (arity > 0) + m_manager->raise_exception("csp variables use parameters only and take no arguments"); +} + +void csp_decl_plugin::check_index1(unsigned num_parameters, parameter const* ps) { + if (num_parameters != 1 || !ps[0].is_int()) + m_manager->raise_exception("csp variable expects a single integer parameter"); +} + +void csp_decl_plugin::check_index2(unsigned num_parameters, parameter const* ps) { + if (num_parameters != 2 || !ps[0].is_int() || !ps[1].is_int()) + m_manager->raise_exception("csp variable expects two integer parameters"); +} + + +bool csp_decl_plugin::is_value(app * e) const { + return is_app_of(e, m_family_id, OP_JS_JOB) || is_app_of(e, m_family_id, OP_JS_RESOURCE); +} + +void csp_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol("CSP")) { + op_names.push_back(builtin_name("job", OP_JS_JOB)); + op_names.push_back(builtin_name("resource", OP_JS_RESOURCE)); + op_names.push_back(builtin_name("makespan", OP_JS_RESOURCE_MAKESPAN)); + op_names.push_back(builtin_name("job-start", OP_JS_START)); + op_names.push_back(builtin_name("job-end", OP_JS_END)); + op_names.push_back(builtin_name("job2resource", OP_JS_JOB2RESOURCE)); + op_names.push_back(builtin_name("js-model", OP_JS_MODEL)); + op_names.push_back(builtin_name("add-job-resource", OP_JS_JOB_RESOURCE)); + op_names.push_back(builtin_name("add-resource-available", OP_JS_RESOURCE_AVAILABLE)); + op_names.push_back(builtin_name("set-preemptable", OP_JS_JOB_PREEMPTABLE)); + op_names.push_back(builtin_name("js-properties", OP_JS_PROPERTIES)); + op_names.push_back(builtin_name("add-job-goal", OP_JS_JOB_GOAL)); + op_names.push_back(builtin_name("add-optimization-objective", OP_JS_OBJECTIVE)); + } +} + +void csp_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { + if (logic == symbol("CSP")) { + sort_names.push_back(builtin_name("Job", JOB_SORT)); + sort_names.push_back(builtin_name("Resource", RESOURCE_SORT)); + } +} + +expr * csp_decl_plugin::get_some_value(sort * s) { + parameter p(0); + if (is_sort_of(s, m_family_id, JOB_SORT)) + return m_manager->mk_const(mk_func_decl(OP_JS_JOB, 1, &p, 0, nullptr, nullptr)); + if (is_sort_of(s, m_family_id, RESOURCE_SORT)) + return m_manager->mk_const(mk_func_decl(OP_JS_RESOURCE, 1, &p, 0, nullptr, nullptr)); + UNREACHABLE(); + return nullptr; +} + + +csp_util::csp_util(ast_manager& m): m(m) { + m_fid = m.mk_family_id("csp"); + m_plugin = static_cast(m.get_plugin(m_fid)); +} + +sort* csp_util::mk_job_sort() { + return m_plugin->mk_job_sort(); +} + +sort* csp_util::mk_resource_sort() { + return m_plugin->mk_resource_sort(); +} + +app* csp_util::mk_job(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_JOB, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +unsigned csp_util::job2id(expr* j) { + if (is_app_of(j, m_fid, OP_JS_JOB)) { + return to_app(j)->get_decl()->get_parameter(0).get_int(); + } + SASSERT(is_app_of(j, m_fid, OP_JS_START) || + is_app_of(j, m_fid, OP_JS_END) || + is_app_of(j, m_fid, OP_JS_JOB2RESOURCE)); + return job2id(to_app(j)->get_arg(0)); +} + +app* csp_util::mk_resource(unsigned r) { + parameter p(r); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_RESOURCE, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +unsigned csp_util::resource2id(expr* r) { + SASSERT(is_app_of(r, m_fid, OP_JS_RESOURCE)); + return to_app(r)->get_decl()->get_parameter(0).get_int(); +} + +app* csp_util::mk_start(unsigned j) { + app_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_START, 0, nullptr, 1, &js, nullptr), job); +} + +app* csp_util::mk_end(unsigned j) { + app_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_END, 0, nullptr, 1, &js, nullptr), job); +} + +app* csp_util::mk_job2resource(unsigned j) { + app_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 0, nullptr, 1, &js, nullptr), job); +} + +app* csp_util::mk_makespan(unsigned r) { + app_ref resource(mk_resource(r), m); + sort* rs = m.get_sort(resource); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_RESOURCE_MAKESPAN, 0, nullptr, 1, &rs, nullptr), resource); +} + +bool csp_util::is_resource(expr* e, unsigned& r) { + return is_app_of(e, m_fid, OP_JS_RESOURCE) && (r = resource2id(e), true); +} + +bool csp_util::is_makespan(expr * e, unsigned& r) { + return is_app_of(e, m_fid, OP_JS_RESOURCE_MAKESPAN) && is_resource(to_app(e)->get_arg(0), r); +} + +bool csp_util::is_job(expr* e, unsigned& j) { + return is_app_of(e, m_fid, OP_JS_JOB) && (j = job2id(e), true); +} + +bool csp_util::is_job2resource(expr* e, unsigned& j) { + return is_app_of(e, m_fid, OP_JS_JOB2RESOURCE) && (j = job2id(e), true); +} + +bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, unsigned& cap_time, uint64_t& start, uint64_t& end, svector& properties) { + if (!is_app_of(e, m_fid, OP_JS_RESOURCE_AVAILABLE)) return false; + res = to_app(e)->get_arg(0); + arith_util a(m); + rational r; + if (!a.is_numeral(to_app(e)->get_arg(1), r) || !r.is_unsigned()) return false; + loadpct = r.get_unsigned(); + if (!a.is_numeral(to_app(e)->get_arg(2), r) || !r.is_unsigned()) return false; + cap_time = r.get_unsigned(); + if (!a.is_numeral(to_app(e)->get_arg(3), r) || !r.is_uint64()) return false; + start = r.get_uint64(); + if (!a.is_numeral(to_app(e)->get_arg(4), r) || !r.is_uint64()) return false; + end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(5), properties)) return false; + return true; +} + +bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properties) { + if (!is_app_of(e, m_fid, OP_JS_JOB_RESOURCE)) return false; + job = to_app(e)->get_arg(0); + res = to_app(e)->get_arg(1); + arith_util a(m); + rational r; + if (!a.is_numeral(to_app(e)->get_arg(2), r) || !r.is_unsigned()) return false; + loadpct = r.get_unsigned(); + if (!a.is_numeral(to_app(e)->get_arg(3), r) || !r.is_uint64()) return false; + capacity = r.get_uint64(); + if (!a.is_numeral(to_app(e)->get_arg(4), r) || !r.is_uint64()) return false; + end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(5), properties)) return false; + return true; +} + +bool csp_util::is_set_preemptable(expr* e, expr *& job) { + if (!is_app_of(e, m_fid, OP_JS_JOB_PREEMPTABLE)) return false; + job = to_app(e)->get_arg(0); + return true; +} + +bool csp_util::is_js_properties(expr* e, svector& properties) { + if (!is_app_of(e, m_fid, OP_JS_PROPERTIES)) + return false; + unsigned sz = to_app(e)->get_decl()->get_num_parameters(); + for (unsigned i = 0; i < sz; ++i) { + properties.push_back(to_app(e)->get_decl()->get_parameter(i).get_symbol()); + } + return true; +} + +bool csp_util::is_job_goal(expr* e, js_job_goal& goal, unsigned& level, expr*& job) { + if (!is_app_of(e, m_fid, OP_JS_JOB_GOAL)) + return false; + SASSERT(2 == to_app(e)->get_decl()->get_num_parameters()); + SASSERT(1 == to_app(e)->get_num_args()); + symbol g = to_app(e)->get_decl()->get_parameter(0).get_symbol(); + level = to_app(e)->get_decl()->get_parameter(1).get_int(); + if (g == ":earliest-end-time" || g == "earliest-end-time") + goal = JS_JOB_GOAL_EARLIEST_END_TIME; + else if (g == ":latest-start-time" || g == "latest-start-time") + goal = JS_JOB_GOAL_LATEST_START_TIME; + else + return false; + job = to_app(e)->get_arg(0); + return true; +} + +bool csp_util::is_objective(expr* e, js_optimization_objective& objective) { + if (!is_app_of(e, m_fid, OP_JS_OBJECTIVE)) + return false; + SASSERT(1 == to_app(e)->get_decl()->get_num_parameters()); + symbol obj = to_app(e)->get_decl()->get_parameter(0).get_symbol(); + if (obj == ":duration" || obj == "duration") + objective = JS_OBJECTIVE_DURATION; + else if (obj == ":priority" || obj == "priority") + objective = JS_OBJECTIVE_PRIORITY; + else + return false; + return true; +} + + diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h new file mode 100644 index 000000000..f6f15d70a --- /dev/null +++ b/src/ast/csp_decl_plugin.h @@ -0,0 +1,162 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + csp_decl_plugin.h + +Abstract: + + Declarations used for a job-shop scheduling domain. + + The job-shop domain comprises of constants job(j), resource(r) + + It finds values to variables: + - start(j), end(j), job2resource(j) + + It assumes a background of: + - resources : Job -> Resource -> Int * LoadPct - time to run job j on resource r assuming LoadPct + - runtime : Job -> Int - time to run job j if not associated with any resource + - capacity : Resource -> Int -> LoadPct - capacity of resource r at time t, given as sequence of time intervals + // assume each job has at least one resource associated with it. + // introduce a dummy resource if needed. + + // Theory: + end(j) - start(j) = time-to-execute(j) + time-to-execute(j) := time-to-execute(j, resource(j)) otherwise + + time-to-execute(j, r) := (T - start(j)) + where capacity(j,r) = sum_{t = start(j)}^{T} load(loadpct(j,r), r, t) + + capacity(j, r) := cap where (cap, loadpct) = resources j r + loadpct(j, r) := loadpct where (cap, loadpct) = resources j r + + load(loadpct, r, t) := min(capacity r t, loadpct) / loadpct + + capacity(r, t) >= sum_{j | job-on-resource(j, r, t) } min(capacity r t, loadpct(j, r)) + + // Macros: + job-on-resource(j, r) := r = resource(j); + job-on-resource(j, r, t) := (job-on-resource(j, r) & start(j) <= t <= end(j)); + start_min(j, t) := start(j) >= t; + end_max(j, t) := end(j) <= t; + job_link(j1, j2, startstart, hard) := start(j1) = start(j2); + job_link(j1, j2, startstart, soft) := start(j1) <= start(j2); + job_link(j1, j2, endend, hard) := end(j1) = end(j2); + job_link(j1, j2, endend, soft) := end(j2) <= end(j1); + job_link(j1, j2, endstart, hard) := end(j1) = start(j2); + job_link(j1, j2, endstart, soft) := end(j2) <= start(j1); + job_link(j1, j2, startend, hard) := end(j2) = start(j1); + job_link(j1, j2, startend, soft) := end(j1) <= start(j2); + job_delay(j1, j2, t) := end(j1) + t <= end(j2); + job_on_same_resource(j1, j2) := resource(j1) = resource(j2); + job_not_on_same_resource(j1, j2) := resource(j1) != resource(j2); + job_time_intersect(j1, j2) := start(j1) <= end(j2) <= end(j1) || start(j2) <= end(j1) <= end(j2); + + job-on-resource(j, r, t) => job-property(j) = null or job_property(j) in working_time_property(r, t); + +Author: + + Nikolaj Bjorner (nbjorner) 2018-8-9 + +Revision History: + + +--*/ +#pragma once; +#include "ast/ast.h" + +enum js_sort_kind { + JOB_SORT, + RESOURCE_SORT, + ALIST_SORT +}; + +enum js_op_kind { + OP_JS_JOB, // value of type job + OP_JS_RESOURCE, // value of type resource + OP_JS_RESOURCE_MAKESPAN, // makespan of resource: the minimal resource time required for assigned jobs. + OP_JS_START, // start time of a job + OP_JS_END, // end time of a job + OP_JS_JOB2RESOURCE, // resource associated with job + OP_JS_MODEL, // jobscheduler model + OP_JS_JOB_RESOURCE, // model declaration for job assignment to resource + OP_JS_JOB_PREEMPTABLE, // model declaration for whether job is pre-emptable + OP_JS_RESOURCE_AVAILABLE, // model declaration for availability intervals of resource + OP_JS_PROPERTIES, // model declaration of a set of properties. Each property is a keyword. + OP_JS_JOB_GOAL, // job goal objective :earliest-end-time or :latest-start-time + OP_JS_OBJECTIVE // duration or completion-time +}; + +enum js_job_goal { + JS_JOB_GOAL_EARLIEST_END_TIME, + JS_JOB_GOAL_LATEST_START_TIME +}; + +enum js_optimization_objective { + JS_OBJECTIVE_DURATION, + JS_OBJECTIVE_PRIORITY +}; + +class csp_decl_plugin : public decl_plugin { +public: + csp_decl_plugin() {} + ~csp_decl_plugin() override {} + void finalize() override; + void set_manager(ast_manager* m, family_id fid) override; + decl_plugin * mk_fresh() override { return alloc(csp_decl_plugin); } + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override; + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + bool is_value(app * e) const override; + bool is_unique_value(app * e) const override { return is_value(e); } + void get_op_names(svector & op_names, symbol const & logic) override; + void get_sort_names(svector & sort_names, symbol const & logic) override; + expr * get_some_value(sort * s) override; + sort * mk_job_sort() const { return m_job_sort; } + sort * mk_resource_sort() const { return m_resource_sort; } + sort * mk_alist_sort() const { return m_alist_sort; } +private: + sort* m_job_sort; + sort* m_resource_sort; + sort* m_alist_sort; + sort* m_int_sort; + + void check_arity(unsigned arity); + void check_index1(unsigned n, parameter const* ps); + void check_index2(unsigned n, parameter const* ps); +}; + +class csp_util { + ast_manager& m; + family_id m_fid; + csp_decl_plugin* m_plugin; +public: + csp_util(ast_manager& m); + sort* mk_job_sort(); + sort* mk_resource_sort(); + + app* mk_job(unsigned j); + app* mk_resource(unsigned r); + app* mk_start(unsigned j); + app* mk_end(unsigned j); + app* mk_job2resource(unsigned j); + app* mk_makespan(unsigned r); + + bool is_job(expr* e, unsigned& j); + bool is_job2resource(expr* e, unsigned& j); + bool is_resource(expr* e, unsigned& r); + bool is_makespan(expr* e, unsigned& r); + bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, unsigned& cap_time, uint64_t& start, uint64_t& end, svector& properites); + bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properites); + bool is_set_preemptable(expr* e, expr *& job); + bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); } + bool is_js_properties(expr* e, svector& properties); + bool is_job_goal(expr* e, js_job_goal& goal, unsigned& level, expr*& job); + bool is_objective(expr* e, js_optimization_objective& objective); + +private: + unsigned job2id(expr* j); + unsigned resource2id(expr* r); + +}; diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index bec60e61c..bc415c461 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -50,18 +50,14 @@ void decl_collector::visit_func(func_decl * n) { if (!m_visited.is_marked(n)) { family_id fid = n->get_family_id(); if (fid == null_family_id) { - if (m_sep_preds && is_bool(n->get_range())) - m_preds.push_back(n); - else - m_decls.push_back(n); + m_decls.push_back(n); } m_visited.mark(n, true); } } -decl_collector::decl_collector(ast_manager & m, bool preds): +decl_collector::decl_collector(ast_manager & m): m_manager(m), - m_sep_preds(preds), m_dt_util(m) { m_basic_fid = m_manager.get_basic_family_id(); m_dt_fid = m_dt_util.get_family_id(); diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 07539dbd8..8945c0bec 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -26,10 +26,8 @@ Revision History: class decl_collector { ast_manager & m_manager; - bool m_sep_preds; ptr_vector m_sorts; ptr_vector m_decls; - ptr_vector m_preds; ast_mark m_visited; family_id m_basic_fid; family_id m_dt_fid; @@ -46,8 +44,7 @@ class decl_collector { public: - // if preds == true, then predicates are stored in a separate collection. - decl_collector(ast_manager & m, bool preds = true); + decl_collector(ast_manager & m); ast_manager & m() { return m_manager; } void visit_func(func_decl* n); @@ -59,11 +56,9 @@ public: unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); } - unsigned get_num_preds() const { return m_preds.size(); } sort * const * get_sorts() const { return m_sorts.c_ptr(); } func_decl * const * get_func_decls() const { return m_decls.c_ptr(); } - func_decl * const * get_pred_decls() const { return m_preds.c_ptr(); } }; #endif diff --git a/src/ast/expr_functors.cpp b/src/ast/expr_functors.cpp index cada71ac9..6a2138106 100644 --- a/src/ast/expr_functors.cpp +++ b/src/ast/expr_functors.cpp @@ -69,7 +69,11 @@ void check_pred::visit(expr* e) { case AST_QUANTIFIER: { quantifier* q = to_quantifier(e); expr* arg = q->get_expr(); - if (m_visited.is_marked(arg)) { + if (!m_check_quantifiers) { + todo.pop_back(); + m_visited.mark(e, true); + } + else if (m_visited.is_marked(arg)) { todo.pop_back(); if (m_pred_holds.is_marked(arg)) { m_pred_holds.mark(e, true); diff --git a/src/ast/expr_functors.h b/src/ast/expr_functors.h index 5a4cac477..5825bea73 100644 --- a/src/ast/expr_functors.h +++ b/src/ast/expr_functors.h @@ -53,8 +53,10 @@ class check_pred { ast_mark m_pred_holds; ast_mark m_visited; expr_ref_vector m_refs; + bool m_check_quantifiers; public: - check_pred(i_expr_pred& p, ast_manager& m) : m_pred(p), m_refs(m) {} + check_pred(i_expr_pred& p, ast_manager& m, bool check_quantifiers = true) : + m_pred(p), m_refs(m), m_check_quantifiers(check_quantifiers) {} bool operator()(expr* e); diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp new file mode 100644 index 000000000..7fe7ae00b --- /dev/null +++ b/src/ast/recfun_decl_plugin.cpp @@ -0,0 +1,428 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation, Simon Cruanes + +Module Name: + + recfun_decl_plugin.cpp + +Abstract: + + Declaration and definition of (potentially recursive) functions + +Author: + + Simon Cruanes 2017-11 + +Revision History: + +--*/ + + +#include +#include +#include "ast/expr_functors.h" +#include "ast/expr_substitution.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/ast_pp.h" +#include "util/scoped_ptr_vector.h" + +#define TRACEFN(x) TRACE("recfun", tout << x << '\n';) +#define VALIDATE_PARAM(m, _pred_) if (!(_pred_)) m.raise_exception("invalid parameter to recfun " #_pred_); + +namespace recfun { + + + case_def::case_def( + ast_manager &m, + family_id fid, + def * d, + std::string & name, + unsigned case_index, + sort_ref_vector const & arg_sorts, + expr_ref_vector const& guards, + expr* rhs) + : m_pred(m), + m_guards(guards), + m_rhs(expr_ref(rhs,m)), + m_def(d) { + parameter p(case_index); + func_decl_info info(fid, OP_FUN_CASE_PRED, 1, &p); + m_pred = m.mk_func_decl(symbol(name.c_str()), arg_sorts.size(), arg_sorts.c_ptr(), m.mk_bool_sort(), info); + } + + def::def(ast_manager &m, family_id fid, symbol const & s, + unsigned arity, sort* const * domain, sort* range) + : m(m), m_name(s), + m_domain(m, arity, domain), + m_range(range, m), m_vars(m), m_cases(), + m_decl(m), + m_rhs(m), + m_fid(fid) + { + SASSERT(arity == get_arity()); + func_decl_info info(fid, OP_FUN_DEFINED); + m_decl = m.mk_func_decl(s, arity, domain, range, info); + } + + // does `e` contain any `ite` construct? + bool def::contains_ite(expr * e) { + struct ite_find_p : public i_expr_pred { + ast_manager & m; + ite_find_p(ast_manager & m) : m(m) {} + virtual bool operator()(expr * e) { return m.is_ite(e); } + }; + // ignore ites under quantifiers. + // this is redundant as the code + // that unfolds ites uses quantifier-free portion. + ite_find_p p(m); + check_pred cp(p, m, false); + return cp(e); + } + + /* + * compilation of functions to a list of cases. + * + * We use a backtracking algorithm in a relatively functional style, + * where the multiple states (corresponding to alternatives) are stored in + * a region, and deallocated at the end + */ + + // immutable list of choices of `ite` terms (mapping each one's condition to true/false) + struct choice_lst { + app * ite; + bool sign; + choice_lst const * next; // or null for the last one + choice_lst(app * ite, bool sign, choice_lst const * next) : ite(ite), sign(sign), next(next) {} + }; + + struct ite_lst { + app * ite; // invariant: `is_ite(e)` + ite_lst const * next; + ite_lst(app * ite, ite_lst const * next) : ite(ite), next(next) {} + }; + + // immutable stack of expressions to unfold + struct unfold_lst { + expr * e; + unfold_lst const * next; // or null for last one + }; + + // main state for one branch of the search tree. + struct branch { + choice_lst const * path; // choices made so far + ite_lst const * to_split; // `ite` terms to make a choice on + unfold_lst const * to_unfold; // terms yet to unfold + + branch(unfold_lst const * to_unfold): + path(nullptr), to_split(nullptr), to_unfold(to_unfold) {} + branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : + path(path), to_split(to_split), to_unfold(to_unfold) {} + branch(branch const & from) : + path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {} + }; + + // state for computing cases from the RHS of a functions' definition + class case_state { + region m_reg; + vector m_branches; + + public: + case_state() : m_reg(), m_branches() {} + + bool empty() const { return m_branches.empty(); } + + branch pop_branch() { + branch res = m_branches.back(); + m_branches.pop_back(); + return res; + } + + void push_branch(branch const & b) { m_branches.push_back(b); } + + unfold_lst const * cons_unfold(expr * e, unfold_lst const * next) { + return new (m_reg) unfold_lst{e, next}; + } + unfold_lst const * cons_unfold(expr * e1, expr * e2, unfold_lst const * next) { + return cons_unfold(e1, cons_unfold(e2, next)); + } + unfold_lst const * mk_unfold_lst(expr * e) { + return cons_unfold(e, nullptr); + } + + ite_lst const * cons_ite(app * ite, ite_lst const * next) { + return new (m_reg) ite_lst{ite, next}; + } + + choice_lst const * cons_choice(app * ite, bool sign, choice_lst const * next) { + return new (m_reg) choice_lst{ite, sign, next}; + } + }; + + //next) { + app * ite = choices->ite; + expr* c = nullptr, *th = nullptr, *el = nullptr; + VERIFY(m.is_ite(ite, c, th, el)); + + // condition to add to the guard + conditions.push_back(choices->sign ? c : m.mk_not(c)); + + // binding to add to the substitution + subst.insert(ite, choices->sign ? th : el); + } + } + + // substitute `subst` in `e` + static expr_ref replace_subst(th_rewriter & th_rw, ast_manager & m, + expr_substitution & subst, expr * e) { + th_rw.reset(); + th_rw.set_substitution(&subst); + expr_ref res(m); + th_rw(e, res); + return res; + } + + void def::add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr * rhs, bool is_imm) { + case_def c(m, m_fid, this, name, case_index, get_domain(), conditions, rhs); + c.set_is_immediate(is_imm); + TRACEFN("add_case " << name << " " << mk_pp(rhs, m) + << " :is_imm " << is_imm + << " :guards " << conditions); + m_cases.push_back(c); + } + + + // Compute a set of cases, given the RHS + void def::compute_cases(is_immediate_pred & is_i, th_rewriter & th_rw, + unsigned n_vars, var *const * vars, expr* rhs) + { + VERIFY(m_cases.empty() && "cases cannot already be computed"); + SASSERT(n_vars == m_domain.size()); + + TRACEFN("compute cases " << mk_pp(rhs, m)); + + unsigned case_idx = 0; + + std::string name("case-"); + name.append(m_name.bare_str()); + + m_vars.append(n_vars, vars); + m_rhs = rhs; + + expr_ref_vector conditions(m); + + // is the function a macro (unconditional body)? + if (n_vars == 0 || !contains_ite(rhs)) { + // constant function or trivial control flow, only one (dummy) case + add_case(name, 0, conditions, rhs); + return; + } + + // analyze control flow of `rhs`, accumulating guards and + // rebuilding a `ite`-free RHS on the fly for each path in `rhs`. + // Each such `ite`-free term is converted into a case_def and added to definition. + + case_state st; + + st.push_branch(branch(st.mk_unfold_lst(rhs))); + + while (! st.empty()) { + TRACEFN("main loop iter"); + + branch b = st.pop_branch(); + + // first: unfold expressions, stopping when we meet subterms that are `ite` + while (b.to_unfold != nullptr) { + + ptr_vector stack; + stack.push_back(b.to_unfold->e); + + b.to_unfold = b.to_unfold->next; + + while (! stack.empty()) { + expr * e = stack.back(); + stack.pop_back(); + + if (m.is_ite(e)) { + // need to do a case split on `e`, forking the search space + b.to_split = st.cons_ite(to_app(e), b.to_split); + } + else if (is_app(e)) { + // explore arguments + for (expr * arg : *to_app(e)) { + if (contains_ite(arg)) { + stack.push_back(arg); + } + } + } + } + } + + if (b.to_split != nullptr) { + // split one `ite`, which will lead to distinct (sets of) cases + app * ite = b.to_split->ite; + expr* c = nullptr, *th = nullptr, *el = nullptr; + VERIFY(m.is_ite(ite, c, th, el)); + + /* explore both positive choice and negative choice. + * each contains a longer path, with `ite` mapping to `true` (resp. `false), + * and must unfold the `then` (resp. `else`) branch. + * We must also unfold the test itself, for it could contain + * tests. + */ + + branch b_pos(st.cons_choice(ite, true, b.path), + b.to_split->next, + st.cons_unfold(c, th, b.to_unfold)); + + branch b_neg(st.cons_choice(ite, false, b.path), + b.to_split->next, + st.cons_unfold(c, el, b.to_unfold)); + + st.push_branch(b_neg); + st.push_branch(b_pos); + } + else { + // leaf of the search tree + + conditions.reset(); + expr_substitution subst(m); + convert_path(m, b.path, conditions, subst); + + // substitute, to get rid of `ite` terms + expr_ref case_rhs = replace_subst(th_rw, m, subst, rhs); + for (unsigned i = 0; i < conditions.size(); ++i) { + conditions[i] = replace_subst(th_rw, m, subst, conditions.get(i)); + } + + // yield new case + bool is_imm = is_i(case_rhs); + add_case(name, case_idx++, conditions, case_rhs, is_imm); + } + } + + TRACEFN("done analyzing " << get_name()); + } + + /* + * Main manager for defined functions + */ + + util::util(ast_manager & m) + : m_manager(m), m_fid(m.get_family_id("recfun")), m_th_rw(m), + m_plugin(dynamic_cast(m.get_plugin(m_fid))) { + } + + util::~util() { + } + + def * util::decl_fun(symbol const& name, unsigned n, sort *const * domain, sort * range) { + return alloc(def, m(), m_fid, name, n, domain, range); + } + + void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { + d.set_definition(n_vars, vars, rhs); + } + + app_ref util::mk_depth_limit_pred(unsigned d) { + parameter p(d); + func_decl_info info(m_fid, OP_DEPTH_LIMIT, 1, &p); + func_decl* decl = m().mk_const_decl(symbol("recfun-depth-limit"), m().mk_bool_sort(), info); + return app_ref(m().mk_const(decl), m()); + } + + // used to know which `app` are from this theory + struct is_imm_pred : is_immediate_pred { + util & u; + is_imm_pred(util & u) : u(u) {} + bool operator()(expr * rhs) { + // find an `app` that is an application of a defined function + struct find : public i_expr_pred { + util & u; + find(util & u) : u(u) {} + bool operator()(expr * e) override { + //return is_app(e) ? u.owns_app(to_app(e)) : false; + if (! is_app(e)) return false; + + app * a = to_app(e); + return u.is_defined(a); + } + }; + find f(u); + check_pred cp(f, u.m()); + bool contains_defined_fun = cp(rhs); + return ! contains_defined_fun; + } + }; + + // set definition + void promise_def::set_definition(unsigned n_vars, var * const * vars, expr * rhs) { + SASSERT(n_vars == d->get_arity()); + + is_imm_pred is_i(*u); + d->compute_cases(is_i, u->get_th_rewriter(), n_vars, vars, rhs); + } + + namespace decl { + plugin::plugin() : decl_plugin(), m_defs(), m_case_defs() {} + plugin::~plugin() { finalize(); } + + void plugin::finalize() { + for (auto& kv : m_defs) { + dealloc(kv.m_value); + } + m_defs.reset(); + // m_case_defs does not own its data, no need to deallocate + m_case_defs.reset(); + m_util = nullptr; // force deletion + } + + util & plugin::u() const { + SASSERT(m_manager); + SASSERT(m_family_id != null_family_id); + if (!m_util.get()) { + m_util = alloc(util, *m_manager); + } + return *(m_util.get()); + } + + promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) { + def* d = u().decl_fun(name, n, params, range); + SASSERT(! m_defs.contains(d->get_decl())); + m_defs.insert(d->get_decl(), d); + return promise_def(&u(), d); + } + + void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { + u().set_definition(d, n_vars, vars, rhs); + for (case_def & c : d.get_def()->get_cases()) { + m_case_defs.insert(c.get_decl(), &c); + } + } + + bool plugin::has_defs() const { + return !m_case_defs.empty(); + } + + def* plugin::mk_def(symbol const& name, unsigned n, sort ** params, sort * range, + unsigned n_vars, var ** vars, expr * rhs) { + promise_def d = mk_def(name, n, params, range); + SASSERT(! m_defs.contains(d.get_def()->get_decl())); + set_definition(d, n_vars, vars, rhs); + return d.get_def(); + } + + // generic declaration of symbols + func_decl * plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) + { + UNREACHABLE(); + return nullptr; + } + } +} diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h new file mode 100644 index 000000000..347689a37 --- /dev/null +++ b/src/ast/recfun_decl_plugin.h @@ -0,0 +1,249 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation, Simon Cruanes + +Module Name: + + recfun_decl_plugin.h + +Abstract: + + Declaration and definition of (potentially recursive) functions + +Author: + + Simon Cruanes 2017-11 + +Revision History: + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "ast/rewriter/th_rewriter.h" +#include "util/obj_hashtable.h" + +namespace recfun { + class case_def; // const & args) const { + ast_manager& m = m_pred.get_manager(); + return app_ref(m.mk_app(m_pred, args.size(), args.c_ptr()), m); + } + + def * get_def() const { return m_def; } + expr_ref_vector const & get_guards() const { return m_guards; } + expr * get_guards_c_ptr() const { return *m_guards.c_ptr(); } + expr * get_guard(unsigned i) const { return m_guards[i]; } + expr * get_rhs() const { return m_rhs; } + unsigned num_guards() const { return m_guards.size(); } + bool is_immediate() const { return m_immediate; }; + void set_is_immediate(bool b) { m_immediate = b; } + }; + + // closure for computing whether a `rhs` expression is immediate + struct is_immediate_pred { + virtual bool operator()(expr * rhs) = 0; + }; + + class def { + friend class util; + friend class promise_def; + typedef vector cases; + + ast_manager & m; + symbol m_name; // def_map; + typedef obj_map case_def_map; + + mutable scoped_ptr m_util; + def_map m_defs; // function->def + case_def_map m_case_defs; // case_pred->def + + ast_manager & m() { return *m_manager; } + public: + plugin(); + ~plugin() override; + void finalize() override; + + util & u() const; // build or return util + + bool is_fully_interp(sort * s) const override { return false; } // might depend on unin sorts + + decl_plugin * mk_fresh() override { return alloc(plugin); } + + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { + UNREACHABLE(); return nullptr; + } + + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + + promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range); + + void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + + def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); + + bool has_def(func_decl* f) const { return m_defs.contains(f); } + bool has_defs() const; + def const& get_def(func_decl* f) const { return *(m_defs[f]); } + promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); } + def& get_def(func_decl* f) { return *(m_defs[f]); } + bool has_case_def(func_decl* f) const { return m_case_defs.contains(f); } + case_def& get_case_def(func_decl* f) { SASSERT(has_case_def(f)); return *(m_case_defs[f]); } + + func_decl_ref_vector get_rec_funs() { + func_decl_ref_vector result(m()); + for (auto& kv : m_defs) result.push_back(kv.m_key); + return result; + } + }; + } + + // Varus utils for recursive functions + class util { + friend class decl::plugin; + + ast_manager & m_manager; + family_id m_fid; + th_rewriter m_th_rw; + decl::plugin * m_plugin; + + bool compute_is_immediate(expr * rhs); + void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + + public: + util(ast_manager &m); + ~util(); + + ast_manager & m() { return m_manager; } + th_rewriter & get_th_rewriter() { return m_th_rw; } + decl::plugin& get_plugin() { return *m_plugin; } + + bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); } + bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); } + bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); } + bool is_depth_limit(expr * e) const { return is_app_of(e, m_fid, OP_DEPTH_LIMIT); } + bool owns_app(app * e) const { return e->get_family_id() == m_fid; } + + //has_defs(); } + + //has_def(f)); + return m_plugin->get_def(f); + } + + case_def& get_case_def(expr* e) { + SASSERT(is_case_pred(e)); + return m_plugin->get_case_def(to_app(e)->get_decl()); + } + + app* mk_fun_defined(def const & d, unsigned n_args, expr * const * args) { + return m().mk_app(d.get_decl(), n_args, args); + } + + app* mk_fun_defined(def const & d, ptr_vector const & args) { + return mk_fun_defined(d, args.size(), args.c_ptr()); + } + + func_decl_ref_vector get_rec_funs() { + return m_plugin->get_rec_funs(); + } + + app_ref mk_depth_limit_pred(unsigned d); + + }; +} + diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 985ecee9e..7e121eb7f 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -22,6 +22,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/datatype_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/dl_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/pb_decl_plugin.h" @@ -40,6 +41,9 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("datatype")))) { m.register_plugin(symbol("datatype"), alloc(datatype_decl_plugin)); } + if (!m.get_plugin(m.mk_family_id(symbol("recfun")))) { + m.register_plugin(symbol("recfun"), alloc(recfun::decl::plugin)); + } if (!m.get_plugin(m.mk_family_id(symbol("datalog_relation")))) { m.register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin)); } diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 84fef488f..4195e7de6 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -279,8 +279,9 @@ protected: return false; } - bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { - return m_cfg.get_macro(f, def, q, def_pr); + bool get_macro(func_decl * f, expr * & def, proof * & def_pr) { + quantifier* q = nullptr; + return m_cfg.get_macro(f, def, q, def_pr); } void push_frame(expr * t, bool mcache, unsigned max_depth) { diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index ebe52f52a..3ee1e4caf 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -212,6 +212,7 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { return false; } + template template void rewriter_tpl::process_app(app * t, frame & fr) { @@ -338,15 +339,12 @@ void rewriter_tpl::process_app(app * t, frame & fr) { // TODO: add rewrite rules support expr * def = nullptr; proof * def_pr = nullptr; - quantifier * def_q = nullptr; // When get_macro succeeds, then // we know that: // forall X. f(X) = def[X] // and def_pr is a proof for this quantifier. // - // Remark: def_q is only used for proof generation. - // It is the quantifier forall X. f(X) = def[X] - if (get_macro(f, def, def_q, def_pr)) { + if (get_macro(f, def, def_pr)) { SASSERT(!f->is_associative() || !flat_assoc(f)); SASSERT(new_num_args == t->get_num_args()); SASSERT(m().get_sort(def) == m().get_sort(t)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7b7f81561..db0164445 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -30,6 +30,7 @@ Notes: #include "ast/seq_decl_plugin.h" #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" +#include "ast/csp_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/pp.h" @@ -474,7 +475,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_manager(m), m_own_manager(m == nullptr), m_manager_initialized(false), - m_rec_fun_declared(false), m_pmanager(nullptr), m_sexpr_manager(nullptr), m_regular("stdout", std::cout), @@ -679,6 +679,8 @@ bool cmd_context::logic_has_datatype() const { return !has_logic() || smt_logics::logic_has_datatype(m_logic); } +bool cmd_context::logic_has_recfun() const { return true; } + void cmd_context::init_manager_core(bool new_manager) { SASSERT(m_manager != 0); SASSERT(m_pmanager != 0); @@ -691,10 +693,12 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv()); register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); + register_plugin(symbol("recfun"), alloc(recfun::decl::plugin), logic_has_recfun()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb()); register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); + register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic)); } else { // the manager was created by an external module @@ -706,9 +710,11 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("bv"), logic_has_bv(), fids); load_plugin(symbol("array"), logic_has_array(), fids); load_plugin(symbol("datatype"), logic_has_datatype(), fids); + load_plugin(symbol("recfun"), logic_has_recfun(), fids); load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); + load_plugin(symbol("csp"), smt_logics::logic_is_csp(m_logic), fids); for (family_id fid : fids) { decl_plugin * p = m_manager->get_plugin(fid); if (p) { @@ -790,9 +796,11 @@ void cmd_context::insert(symbol const & s, func_decl * f) { if (contains_macro(s, f)) { throw cmd_exception("invalid declaration, named expression already defined with this name ", s); } +#if 0 if (m_builtin_decls.contains(s)) { throw cmd_exception("invalid declaration, builtin symbol ", s); } +#endif dictionary::entry * e = m_func_decls.insert_if_not_there2(s, func_decls()); func_decls & fs = e->get_data().m_value; if (!fs.insert(m(), f)) { @@ -827,9 +835,11 @@ void cmd_context::insert(symbol const & s, psort_decl * p) { void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, expr * t) { expr_ref _t(t, m()); +#if 0 if (m_builtin_decls.contains(s)) { throw cmd_exception("invalid macro/named expression, builtin symbol ", s); } +#endif if (contains_macro(s, arity, domain)) { throw cmd_exception("named expression already defined"); } @@ -888,7 +898,20 @@ void cmd_context::model_del(func_decl* f) { m_mc0->hide(f); } -void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e) { + +recfun::decl::plugin& cmd_context::get_recfun_plugin() { + recfun::util u(get_ast_manager()); + return u.get_plugin(); +} + + +recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) { + SASSERT(logic_has_recfun()); + return get_recfun_plugin().mk_def(name, arity, domain, range); +} + +// insert a recursive function as a regular quantified axiom +void cmd_context::insert_rec_fun_as_axiom(func_decl *f, expr_ref_vector const& binding, svector const &ids, expr* e) { expr_ref eq(m()); app_ref lhs(m()); lhs = m().mk_app(f, binding.size(), binding.c_ptr()); @@ -907,19 +930,42 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats); } - // - // disable warning given the current way they are used - // (Z3 will here silently assume and not check the definitions to be well founded, - // and please use HSF for everything else). - // - if (false && !ids.empty() && !m_rec_fun_declared) { - warning_msg("recursive function definitions are assumed well-founded"); - m_rec_fun_declared = true; - } assert_expr(eq); } + +void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* rhs) { + + if (gparams::get_value("smt.recfun.native") != "true") { + // just use an axiom + insert_rec_fun_as_axiom(f, binding, ids, rhs); + return; + } + + TRACE("recfun", tout<< "define recfun " << f->get_name() << " = " << mk_pp(rhs, m()) << "\n";); + + recfun::decl::plugin& p = get_recfun_plugin(); + + var_ref_vector vars(m()); + for (expr* b : binding) { + SASSERT(is_var(b)); + vars.push_back(to_var(b)); + } + + recfun::promise_def d = p.get_promise_def(f); + p.set_definition(d, vars.size(), vars.c_ptr(), rhs); +} + func_decl * cmd_context::find_func_decl(symbol const & s) const { + if (contains_macro(s)) { + throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); + } + func_decls fs; + if (m_func_decls.find(s, fs)) { + if (fs.more_than_one()) + throw cmd_exception("ambiguous function declaration reference, provide full signature to disumbiguate ( (*) ) ", s); + return fs.first(); + } builtin_decl d; if (m_builtin_decls.find(s, d)) { try { @@ -933,15 +979,6 @@ func_decl * cmd_context::find_func_decl(symbol const & s) const { } throw cmd_exception("invalid function declaration reference, must provide signature for builtin symbol ", s); } - if (contains_macro(s)) { - throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); - } - func_decls fs; - if (m_func_decls.find(s, fs)) { - if (fs.more_than_one()) - throw cmd_exception("ambiguous function declaration reference, provide full signature to disumbiguate ( (*) ) ", s); - return fs.first(); - } throw cmd_exception("invalid function declaration reference, unknown function ", s); return nullptr; } @@ -966,6 +1003,18 @@ static builtin_decl const & peek_builtin_decl(builtin_decl const & first, family func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range) const { + + if (domain && contains_macro(s, arity, domain)) + throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); + + func_decl * f = nullptr; + func_decls fs; + if (num_indices == 0 && m_func_decls.find(s, fs)) { + f = fs.find(arity, domain, range); + } + if (f) { + return f; + } builtin_decl d; if (domain && m_builtin_decls.find(s, d)) { family_id fid = d.m_fid; @@ -990,21 +1039,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, invalid builtin reference ", s); return f; } - - if (domain && contains_macro(s, arity, domain)) - throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); - - if (num_indices > 0) - throw cmd_exception("invalid indexed function declaration reference, unknown builtin function ", s); - - func_decl * f = nullptr; - func_decls fs; - if (m_func_decls.find(s, fs)) { - f = fs.find(arity, domain, range); - } - if (f == nullptr) - throw cmd_exception("invalid function declaration reference, unknown function ", s); - return f; + throw cmd_exception("invalid function declaration reference, unknown function ", s); } psort_decl * cmd_context::find_psort_decl(symbol const & s) const { @@ -1041,29 +1076,6 @@ void cmd_context::mk_const(symbol const & s, expr_ref & result) const { void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, sort * range, expr_ref & result) const { - builtin_decl d; - if (m_builtin_decls.find(s, d)) { - family_id fid = d.m_fid; - decl_kind k = d.m_decl; - // Hack: if d.m_next != 0, we use the sort of args[0] (if available) to decide which plugin we use. - if (d.m_decl != 0 && num_args > 0) { - builtin_decl const & d2 = peek_builtin_decl(d, m().get_sort(args[0])->get_family_id()); - fid = d2.m_fid; - k = d2.m_decl; - } - if (num_indices == 0) { - result = m().mk_app(fid, k, 0, nullptr, num_args, args, range); - } - else { - result = m().mk_app(fid, k, num_indices, indices, num_args, args, range); - } - if (result.get() == nullptr) - throw cmd_exception("invalid builtin application ", s); - CHECK_SORT(result.get()); - return; - } - if (num_indices > 0) - throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s); expr* _t; if (macros_find(s, num_args, args, _t)) { TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n"; @@ -1079,6 +1091,31 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg func_decls fs; if (!m_func_decls.find(s, fs)) { + + builtin_decl d; + if (m_builtin_decls.find(s, d)) { + family_id fid = d.m_fid; + decl_kind k = d.m_decl; + // Hack: if d.m_next != 0, we use the sort of args[0] (if available) to decide which plugin we use. + if (d.m_decl != 0 && num_args > 0) { + builtin_decl const & d2 = peek_builtin_decl(d, m().get_sort(args[0])->get_family_id()); + fid = d2.m_fid; + k = d2.m_decl; + } + if (num_indices == 0) { + result = m().mk_app(fid, k, 0, nullptr, num_args, args, range); + } + else { + result = m().mk_app(fid, k, num_indices, indices, num_args, args, range); + } + if (result.get() == nullptr) + throw cmd_exception("invalid builtin application ", s); + CHECK_SORT(result.get()); + return; + } + if (num_indices > 0) + throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s); + if (num_args == 0) { throw cmd_exception("unknown constant ", s); } @@ -1088,14 +1125,17 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg if (num_args == 0 && range == nullptr) { if (fs.more_than_one()) - throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as ) to disumbiguate ", s); + throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as ) to disambiguate ", s); func_decl * f = fs.first(); if (f == nullptr) { throw cmd_exception("unknown constant ", s); } - if (f->get_arity() != 0) - throw cmd_exception("invalid function application, missing arguments ", s); - result = m().mk_const(f); + if (f->get_arity() != 0) { + result = array_util(m()).mk_as_array(f); + } + else { + result = m().mk_const(f); + } } else { func_decl * f = fs.find(m(), num_args, args, range); @@ -2000,7 +2040,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr if (logic != symbol::null) out << "(set-logic " << logic << ")" << std::endl; // collect uninterpreted function declarations - decl_collector decls(m(), false); + decl_collector decls(m()); for (unsigned i = 0; i < num; i++) { decls.visit(assertions[i]); } @@ -2031,8 +2071,8 @@ void cmd_context::slow_progress_sample() { svector labels; m_solver->get_labels(labels); regular_stream() << "(labels"; - for (unsigned i = 0; i < labels.size(); i++) { - regular_stream() << " " << labels[i]; + for (symbol const& s : labels) { + regular_stream() << " " << s; } regular_stream() << "))" << std::endl; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index cb49d1825..b2ed1e5cb 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -32,6 +32,7 @@ Notes: #include "ast/ast.h" #include "ast/ast_printer.h" #include "ast/datatype_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "tactic/generic_model_converter.h" #include "solver/solver.h" #include "solver/progress_callback.h" @@ -199,7 +200,6 @@ protected: ast_manager * m_manager; bool m_own_manager; bool m_manager_initialized; - bool m_rec_fun_declared; pdecl_manager * m_pmanager; sexpr_manager * m_sexpr_manager; check_logic m_check_logic; @@ -291,6 +291,7 @@ protected: bool logic_has_array() const; bool logic_has_datatype() const; bool logic_has_fpa() const; + bool logic_has_recfun() const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;} @@ -306,6 +307,7 @@ protected: void erase_macro(symbol const& s); bool macros_find(symbol const& s, unsigned n, expr*const* args, expr*& t) const; + recfun::decl::plugin& get_recfun_plugin(); public: cmd_context(bool main_ctx = true, ast_manager * m = nullptr, symbol const & l = symbol::null); @@ -384,12 +386,14 @@ public: void insert(probe_info * p) { tactic_manager::insert(p); } void insert_user_tactic(symbol const & s, sexpr * d); void insert_aux_pdecl(pdecl * p); - void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e); void model_add(symbol const & s, unsigned arity, sort *const* domain, expr * t); void model_del(func_decl* f); + void insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e); + void insert_rec_fun_as_axiom(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* e); func_decl * find_func_decl(symbol const & s) const; func_decl * find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range) const; + recfun::promise_def decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range); psort_decl * find_psort_decl(symbol const & s) const; cmd * find_cmd(symbol const & s) const; sexpr * find_user_tactic(symbol const & s) const; diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 235576735..bdd2c8b97 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -91,6 +91,11 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "", "display shared subterms of ctx.regular_stream() << ")" << std::endl; }); +UNARY_CMD(assert_not_cmd, "assert-not", "", "assert negation", CPK_EXPR, expr *, { + expr_ref ne(ctx.m().mk_not(arg), ctx.m()); + ctx.assert_expr(ne); +}); + UNARY_CMD(num_shared_cmd, "dbg-num-shared", "", "return the number of shared subterms", CPK_EXPR, expr *, { shared_occs s(ctx.m()); s(arg); @@ -537,6 +542,7 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(shift_vars_cmd)); ctx.insert(alloc(pp_shared_cmd)); ctx.insert(alloc(num_shared_cmd)); + ctx.insert(alloc(assert_not_cmd)); ctx.insert(alloc(size_cmd)); ctx.insert(alloc(subst_cmd)); ctx.insert(alloc(bool_rewriter_cmd)); diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index 807e2b4e7..b2a4f02aa 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -21,6 +21,7 @@ Revision History: #include "model/model_smt2_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/func_decl_dependencies.h" +#include "ast/recfun_decl_plugin.h" #include "ast/pp.h" using namespace format_ns; @@ -60,11 +61,9 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod ctx.display(buffer, s, 13); buffer << ":\n"; pp_indent(buffer, TAB_SZ); - ptr_vector::const_iterator it = u.begin(); - ptr_vector::const_iterator end = u.end(); - for (; it != end; ++it) { - SASSERT(is_app(*it)); - app * c = to_app(*it); + for (expr* e : u) { + SASSERT(is_app(e)); + app * c = to_app(e); pp_symbol(buffer, c->get_decl()->get_name()); buffer << " "; } @@ -87,9 +86,8 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod out << "\n"; pp_indent(out, indent); out << ";; definitions for universe elements:\n"; - it = u.begin(); - for (; it != end; ++it) { - app * c = to_app(*it); + for (expr * e : u) { + app * c = to_app(e); pp_indent(out, indent); out << "(declare-fun "; unsigned len = pp_symbol(out, c->get_decl()->get_name()); @@ -101,9 +99,8 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod out << ";; cardinality constraint:\n"; f_conds.reset(); format * var = mk_string(m, "x"); - it = u.begin(); - for (; it != end; ++it) { - app * c = to_app(*it); + for (expr* e : u) { + app * c = to_app(e); symbol csym = c->get_decl()->get_name(); std::string cname; if (is_smt2_quoted_symbol(csym)) @@ -170,10 +167,7 @@ void sort_fun_decls(ast_manager & m, model_core const & md, ptr_bufferget_else(), deps); - func_decl_set::iterator it2 = deps.begin(); - func_decl_set::iterator end2 = deps.end(); - for (; it2 != end2; ++it2) { - func_decl * d = *it2; + for (func_decl * d : deps) { if (d->get_arity() > 0 && md.has_interpretation(d) && !visited.contains(d)) { todo.push_back(d); visited.insert(d); @@ -189,8 +183,10 @@ void sort_fun_decls(ast_manager & m, model_core const & md, ptr_buffer var_names; ptr_buffer f_var_names; ptr_buffer f_arg_decls; @@ -200,6 +196,9 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co sort_fun_decls(m, md, func_decls); for (unsigned i = 0; i < func_decls.size(); i++) { func_decl * f = func_decls[i]; + if (recfun_util.is_defined(f)) { + continue; + } func_interp * f_i = md.get_func_interp(f); SASSERT(f->get_arity() == f_i->get_arity()); format_ref body(fm(m)); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 0662cacb5..106a77c0e 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -114,6 +114,7 @@ namespace smt2 { symbol m_define_fun_rec; symbol m_define_funs_rec; symbol m_match; + symbol m_case; symbol m_underscore; typedef std::pair named_expr; @@ -382,7 +383,9 @@ namespace smt2 { next(); return; } - throw parser_exception(msg); + std::ostringstream str; + str << msg << " got " << curr_id(); + throw parser_exception(str.str()); } symbol const & curr_id() const { return m_scanner.get_id(); } @@ -406,6 +409,7 @@ namespace smt2 { bool curr_id_is_underscore() const { SASSERT(curr_is_identifier()); return curr_id() == m_underscore; } bool curr_id_is_as() const { SASSERT(curr_is_identifier()); return curr_id() == m_as; } bool curr_id_is_match() const { SASSERT(curr_is_identifier()); return curr_id() == m_match; } + bool curr_id_is_case() const { return curr_id() == m_case; } bool curr_id_is_forall() const { SASSERT(curr_is_identifier()); return curr_id() == m_forall; } bool curr_id_is_exists() const { SASSERT(curr_is_identifier()); return curr_id() == m_exists; } bool curr_id_is_lambda() const { SASSERT(curr_is_identifier()); return curr_id() == m_lambda; } @@ -625,8 +629,6 @@ namespace smt2 { args.push_back(u); next(); } - if (args.empty()) - throw parser_exception("invalid indexed sort, index expected"); sort * r = d->instantiate(pm(), args.size(), args.c_ptr()); if (r == nullptr) throw parser_exception("invalid sort application"); @@ -1321,7 +1323,13 @@ namespace smt2 { /** * SMT-LIB 2.6 pattern matches are of the form - * (match t ((p1 t1) ... (pm+1 tm+1))) + * + * (match t ((p1 t1) ... (pm+1 tm+1))) + * + * precursor form is + * + * (match t (case p1 t1) (case p2 t2) ... ) + * */ void push_match_frame() { SASSERT(curr_is_identifier()); @@ -1338,21 +1346,42 @@ namespace smt2 { sort* srt = m().get_sort(t); check_lparen_next("pattern bindings should be enclosed in a parenthesis"); - while (!curr_is_rparen()) { - m_env.begin_scope(); - unsigned num_bindings = m_num_bindings; - check_lparen_next("invalid pattern binding, '(' expected"); - parse_match_pattern(srt); - patterns.push_back(expr_stack().back()); - expr_stack().pop_back(); - parse_expr(); - cases.push_back(expr_stack().back()); - expr_stack().pop_back(); - m_num_bindings = num_bindings; - m_env.end_scope(); - check_rparen_next("invalid pattern binding, ')' expected"); + if (curr_id_is_case()) { + while (curr_id_is_case()) { + next(); + m_env.begin_scope(); + unsigned num_bindings = m_num_bindings; + parse_match_pattern(srt); + patterns.push_back(expr_stack().back()); + expr_stack().pop_back(); + parse_expr(); + cases.push_back(expr_stack().back()); + expr_stack().pop_back(); + m_num_bindings = num_bindings; + m_env.end_scope(); + check_rparen_next("invalid pattern binding, ')' expected"); + if (curr_is_lparen()) { + next(); + } + } + } + else { + while (!curr_is_rparen()) { + m_env.begin_scope(); + unsigned num_bindings = m_num_bindings; + parse_match_pattern(srt); + patterns.push_back(expr_stack().back()); + expr_stack().pop_back(); + check_lparen_next("invalid pattern binding, '(' expected"); + parse_expr(); + cases.push_back(expr_stack().back()); + expr_stack().pop_back(); + m_num_bindings = num_bindings; + m_env.end_scope(); + check_rparen_next("invalid pattern binding, ')' expected"); + } + next(); } - next(); m_num_expr_frames = num_frames + 1; expr_stack().push_back(compile_patterns(t, patterns, cases)); } @@ -1410,6 +1439,12 @@ namespace smt2 { // compute match condition and substitution // t is shifted by size of subst. expr_ref bind_match(expr* t, expr* pattern, expr_ref_vector& subst) { + if (m().get_sort(t) != m().get_sort(pattern)) { + std::ostringstream str; + str << "sorts of pattern " << expr_ref(pattern, m()) << " and term " + << expr_ref(t, m()) << " are not aligned"; + throw parser_exception(str.str()); + } expr_ref tsh(m()); if (is_var(pattern)) { shifter()(t, 1, tsh); @@ -1520,11 +1555,22 @@ namespace smt2 { check_identifier("invalid indexed identifier, symbol expected"); symbol r = curr_id(); next(); - unsigned num_indices = 0; while (!curr_is_rparen()) { if (curr_is_int()) { - unsigned u = curr_unsigned(); - m_param_stack.push_back(parameter(u)); + if (!curr_numeral().is_unsigned()) { + m_param_stack.push_back(parameter(curr_numeral())); + } + else { + m_param_stack.push_back(parameter(curr_unsigned())); + } + next(); + } + else if (curr_is_float()) { + m_param_stack.push_back(parameter(curr_numeral())); + next(); + } + else if (curr_is_keyword()) { + m_param_stack.push_back(parameter(curr_id())); next(); } else if (curr_is_identifier() || curr_is_lparen()) { @@ -1533,10 +1579,7 @@ namespace smt2 { else { throw parser_exception("invalid indexed identifier, integer, identifier or '(' expected"); } - num_indices++; } - if (num_indices == 0) - throw parser_exception("invalid indexed identifier, index expected"); next(); return r; } @@ -1857,13 +1900,31 @@ namespace smt2 { unsigned num_args = expr_stack().size() - fr->m_expr_spos; unsigned num_indices = m_param_stack.size() - fr->m_param_spos; expr_ref t_ref(m()); - m_ctx.mk_app(fr->m_f, - num_args, - expr_stack().c_ptr() + fr->m_expr_spos, - num_indices, - m_param_stack.c_ptr() + fr->m_param_spos, - fr->m_as_sort ? sort_stack().back() : nullptr, - t_ref); + local l; + if (m_env.find(fr->m_f, l)) { + push_local(l); + t_ref = expr_stack().back(); + for (unsigned i = 0; i < num_args; ++i) { + expr* arg = expr_stack().get(fr->m_expr_spos + i); + expr* args[2] = { t_ref.get(), arg }; + m_ctx.mk_app(symbol("select"), + 2, + args, + 0, + nullptr, + nullptr, + t_ref); + } + } + else { + m_ctx.mk_app(fr->m_f, + num_args, + expr_stack().c_ptr() + fr->m_expr_spos, + num_indices, + m_param_stack.c_ptr() + fr->m_param_spos, + fr->m_as_sort ? sort_stack().back() : nullptr, + t_ref); + } expr_stack().shrink(fr->m_expr_spos); m_param_stack.shrink(fr->m_param_spos); if (fr->m_as_sort) @@ -2216,10 +2277,14 @@ namespace smt2 { parse_expr(); if (m().get_sort(expr_stack().back()) != sort_stack().back()) throw parser_exception("invalid function/constant definition, sort mismatch"); - if (is_fun) - m_ctx.insert(id, num_vars, sort_stack().c_ptr() + sort_spos, expr_stack().back()); - else - m_ctx.model_add(id, num_vars, sort_stack().c_ptr() + sort_spos, expr_stack().back()); + sort* const* sorts = sort_stack().c_ptr() + sort_spos; + expr* t = expr_stack().back(); + if (is_fun) { + m_ctx.insert(id, num_vars, sorts, t); + } + else { + m_ctx.model_add(id, num_vars, sorts, t); + } check_rparen("invalid function/constant definition, ')' expected"); // restore stacks & env symbol_stack().shrink(sym_spos); @@ -2311,7 +2376,7 @@ namespace smt2 { next(); } - void parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector& ids) { + recfun::promise_def parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector& ids) { SASSERT(m_num_bindings == 0); check_identifier("invalid function/constant definition, symbol expected"); symbol id = curr_id(); @@ -2322,7 +2387,8 @@ namespace smt2 { unsigned num_vars = parse_sorted_vars(); SASSERT(num_vars == m_num_bindings); parse_sort("Invalid recursive function definition"); - f = m().mk_func_decl(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back()); + recfun::promise_def pdef = m_ctx.decl_rec_fun(id, num_vars, sort_stack().c_ptr() + sort_spos, sort_stack().back()); + f = pdef.get_def()->get_decl(); bindings.append(num_vars, expr_stack().c_ptr() + expr_spos); ids.append(num_vars, symbol_stack().c_ptr() + sym_spos); symbol_stack().shrink(sym_spos); @@ -2330,6 +2396,7 @@ namespace smt2 { expr_stack().shrink(expr_spos); m_env.end_scope(); m_num_bindings = 0; + return pdef; } void parse_rec_fun_bodies(func_decl_ref_vector const& decls, vector const& bindings, vector >const & ids) { @@ -3005,6 +3072,7 @@ namespace smt2 { m_define_fun_rec("define-fun-rec"), m_define_funs_rec("define-funs-rec"), m_match("match"), + m_case("case"), m_underscore("_"), m_num_open_paren(0), m_current_file(filename) { diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 01d627115..e939072e1 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -49,6 +49,11 @@ namespace sat { return static_cast(*this); } + ba_solver::pb_base const& ba_solver::constraint::to_pb_base() const{ + SASSERT(is_pb() || is_card()); + return static_cast(*this); + } + ba_solver::xr& ba_solver::constraint::to_xr() { SASSERT(is_xr()); return static_cast(*this); @@ -1009,27 +1014,13 @@ namespace sat { // --------------------------- // conflict resolution - void ba_solver::normalize_active_coeffs() { - reset_active_var_set(); - unsigned i = 0, j = 0, sz = m_active_vars.size(); - for (; i < sz; ++i) { - bool_var v = m_active_vars[i]; - if (!m_active_var_set.contains(v) && get_coeff(v) != 0) { - m_active_var_set.insert(v); - if (j != i) { - m_active_vars[j] = m_active_vars[i]; - } - ++j; - } - } - m_active_vars.shrink(j); - } void ba_solver::inc_coeff(literal l, unsigned offset) { SASSERT(offset > 0); bool_var v = l.var(); SASSERT(v != null_bool_var); m_coeffs.reserve(v + 1, 0); + TRACE("ba_verbose", tout << l << " " << offset << "\n";); int64_t coeff0 = m_coeffs[v]; if (coeff0 == 0) { @@ -1066,59 +1057,114 @@ namespace sat { return m_coeffs.get(v, 0); } + uint64_t ba_solver::get_coeff(literal lit) const { + int64_t c1 = get_coeff(lit.var()); + SASSERT(c1 < 0 == lit.sign()); + uint64_t c = static_cast(std::abs(c1)); + m_overflow |= c != c1; + return c; + } + + ba_solver::wliteral ba_solver::get_wliteral(bool_var v) { + int64_t c1 = get_coeff(v); + literal l = literal(v, c1 < 0); + c1 = std::abs(c1); + unsigned c = static_cast(c1); + // TRACE("ba", tout << l << " " << c << "\n";); + m_overflow |= c != c1; + return wliteral(c, l); + } + unsigned ba_solver::get_abs_coeff(bool_var v) const { - int64_t c = get_coeff(v); - if (c < INT_MIN+1 || c > UINT_MAX) { - m_overflow = true; - return UINT_MAX; - } - return static_cast(std::abs(c)); + int64_t c1 = std::abs(get_coeff(v)); + unsigned c = static_cast(c1); + m_overflow |= c != c1; + return c; } int ba_solver::get_int_coeff(bool_var v) const { - int64_t c = m_coeffs.get(v, 0); - if (c < INT_MIN || c > INT_MAX) { - m_overflow = true; - return 0; - } - return static_cast(c); + int64_t c1 = m_coeffs.get(v, 0); + int c = static_cast(c1); + m_overflow |= c != c1; + return c; } void ba_solver::inc_bound(int64_t i) { - if (i < INT_MIN || i > INT_MAX) { - m_overflow = true; - return; - } int64_t new_bound = m_bound; new_bound += i; - if (new_bound < 0) { - m_overflow = true; - } - else if (new_bound > UINT_MAX) { - m_overflow = true; - } - else { - m_bound = static_cast(new_bound); - } + unsigned nb = static_cast(new_bound); + m_overflow |= new_bound < 0 || nb != new_bound; + m_bound = nb; } void ba_solver::reset_coeffs() { - for (unsigned i = 0; i < m_active_vars.size(); ++i) { + for (unsigned i = m_active_vars.size(); i-- > 0; ) { m_coeffs[m_active_vars[i]] = 0; } m_active_vars.reset(); } + void ba_solver::init_visited() { + m_visited_ts++; + if (m_visited_ts == 0) { + m_visited_ts = 1; + m_visited.reset(); + } + while (m_visited.size() < 2*s().num_vars()) { + m_visited.push_back(0); + } + } + static bool _debug_conflict = false; static literal _debug_consequent = null_literal; static unsigned_vector _debug_var2position; // #define DEBUG_CODE(_x_) _x_ - lbool ba_solver::resolve_conflict() { + void ba_solver::bail_resolve_conflict(unsigned idx) { + literal_vector const& lits = s().m_trail; + while (m_num_marks > 0) { + bool_var v = lits[idx].var(); + if (s().is_marked(v)) { + s().reset_mark(v); + --m_num_marks; + } + if (idx == 0 && !_debug_conflict) { + _debug_conflict = true; + _debug_var2position.reserve(s().num_vars()); + for (unsigned i = 0; i < lits.size(); ++i) { + _debug_var2position[lits[i].var()] = i; + } + IF_VERBOSE(0, + active2pb(m_A); + uint64_t c = 0; + for (wliteral l : m_A.m_wlits) c += l.first; + verbose_stream() << "sum of coefficients: " << c << "\n"; + display(verbose_stream(), m_A, true); + verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";); + + for (literal l : lits) { + if (s().is_marked(l.var())) { + IF_VERBOSE(0, verbose_stream() << "missing mark: " << l << "\n";); + s().reset_mark(l.var()); + } + } + m_num_marks = 0; + resolve_conflict(); + } + --idx; + } + } + + lbool ba_solver::resolve_conflict() { if (0 == m_num_propagations_since_pop) { return l_undef; } + + if (s().m_config.m_pb_resolve == PB_ROUNDING) { + return resolve_conflict_rs(); + } + m_overflow = false; reset_coeffs(); m_num_marks = 0; @@ -1127,6 +1173,9 @@ namespace sat { justification js = s().m_conflict; TRACE("ba", tout << consequent << " " << js << "\n";); m_conflict_lvl = s().get_max_lvl(consequent, js); + if (m_conflict_lvl == 0) { + return l_undef; + } if (consequent != null_literal) { consequent.neg(); process_antecedent(consequent, 1); @@ -1256,7 +1305,6 @@ namespace sat { process_next_resolvent: // find the next marked variable in the assignment stack - // bool_var v; while (true) { consequent = lits[idx]; @@ -1290,77 +1338,354 @@ namespace sat { DEBUG_CODE(for (bool_var i = 0; i < static_cast(s().num_vars()); ++i) SASSERT(!s().is_marked(i));); SASSERT(validate_lemma()); - normalize_active_coeffs(); - if (!create_asserting_lemma()) { goto bail_out; } + active2lemma(); + DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); - TRACE("ba", tout << m_lemma << "\n";); - - if (get_config().m_drat) { - svector ps; // TBD fill in - drat_add(m_lemma, ps); - } - - s().m_lemma.reset(); - s().m_lemma.append(m_lemma); - for (unsigned i = 1; i < m_lemma.size(); ++i) { - CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); - s().mark(m_lemma[i].var()); - } - return l_true; bail_out: + if (m_overflow) { + ++m_stats.m_num_overflow; + m_overflow = false; + } + bail_resolve_conflict(idx); + return l_undef; + } - m_overflow = false; + unsigned ba_solver::ineq::bv_coeff(bool_var v) const { + for (unsigned i = size(); i-- > 0; ) { + if (lit(i).var() == v) return coeff(i); + } + UNREACHABLE(); + return 0; + } + + void ba_solver::ineq::divide(unsigned c) { + if (c == 1) return; + for (unsigned i = size(); i-- > 0; ) { + m_wlits[i].first = (coeff(i) + c - 1) / c; + } + m_k = (m_k + c - 1) / c; + } + + /** + * Remove literal at position i, subtract coefficient from bound. + */ + void ba_solver::ineq::weaken(unsigned i) { + unsigned ci = coeff(i); + SASSERT(m_k >= ci); + m_k -= ci; + m_wlits[i] = m_wlits.back(); + m_wlits.pop_back(); + } + + /** + * Round coefficient of inequality to 1. + */ + void ba_solver::round_to_one(ineq& ineq, bool_var v) { + unsigned c = ineq.bv_coeff(v); + if (c == 1) return; + unsigned sz = ineq.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned ci = ineq.coeff(i); + unsigned q = ci % c; + if (q != 0 && !is_false(ineq.lit(i))) { + if (q == ci) { + ineq.weaken(i); + --i; + --sz; + } + else { + ineq.m_wlits[i].first -= q; + ineq.m_k -= q; + } + } + } + ineq.divide(c); + TRACE("ba", display(tout << "var: " << v << " " << c << ": ", ineq, true);); + } + + void ba_solver::round_to_one(bool_var w) { + unsigned c = get_abs_coeff(w); + if (c == 1 || c == 0) return; + for (bool_var v : m_active_vars) { + wliteral wl = get_wliteral(v); + unsigned q = wl.first % c; + if (q != 0 && !is_false(wl.second)) { + m_coeffs[v] = wl.first - q; + m_bound -= q; + SASSERT(m_bound > 0); + } + } + SASSERT(validate_lemma()); + divide(c); + SASSERT(validate_lemma()); + TRACE("ba", active2pb(m_B); display(tout, m_B, true);); + } + + void ba_solver::divide(unsigned c) { + SASSERT(c != 0); + if (c == 1) return; + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + int ci = get_int_coeff(v); + if (!test_and_set_active(v) || ci == 0) continue; + if (ci > 0) { + m_coeffs[v] = (ci + c - 1) / c; + } + else { + m_coeffs[v] = -static_cast((-ci + c - 1) / c); + } + m_active_vars[j++] = v; + } + m_active_vars.shrink(j); + m_bound = static_cast((m_bound + c - 1) / c); + } + + void ba_solver::resolve_on(literal consequent) { + round_to_one(consequent.var()); + m_coeffs[consequent.var()] = 0; + } + + void ba_solver::resolve_with(ineq const& ineq) { + TRACE("ba", display(tout, ineq, true);); + inc_bound(ineq.m_k); + TRACE("ba", tout << "bound: " << m_bound << "\n";); + + for (unsigned i = ineq.size(); i-- > 0; ) { + literal l = ineq.lit(i); + inc_coeff(l, static_cast(ineq.coeff(i))); + TRACE("ba", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";); + } + } + + void ba_solver::reset_marks(unsigned idx) { while (m_num_marks > 0) { - bool_var v = lits[idx].var(); + SASSERT(idx > 0); + bool_var v = s().m_trail[idx].var(); if (s().is_marked(v)) { s().reset_mark(v); --m_num_marks; } - if (idx == 0 && !_debug_conflict) { - _debug_conflict = true; - _debug_var2position.reserve(s().num_vars()); - for (unsigned i = 0; i < lits.size(); ++i) { - _debug_var2position[lits[i].var()] = i; - } - IF_VERBOSE(0, - active2pb(m_A); - uint64_t c = 0; - for (uint64_t c1 : m_A.m_coeffs) c += c1; - verbose_stream() << "sum of coefficients: " << c << "\n"; - display(verbose_stream(), m_A, true); - verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";); + --idx; + } + } + + /** + * \brief mark variables that are on the assignment stack but + * below the current processing level. + */ + void ba_solver::mark_variables(ineq const& ineq) { + for (wliteral wl : ineq.m_wlits) { + literal l = wl.second; + if (!is_false(l)) continue; + bool_var v = l.var(); + unsigned level = lvl(v); + if (!s().is_marked(v) && !is_visited(v) && level == m_conflict_lvl) { + s().mark(v); + ++m_num_marks; + } + } + } - for (literal l : lits) { - if (s().is_marked(l.var())) { - IF_VERBOSE(0, verbose_stream() << "missing mark: " << l << "\n";); - s().reset_mark(l.var()); + lbool ba_solver::resolve_conflict_rs() { + if (0 == m_num_propagations_since_pop) { + return l_undef; + } + m_overflow = false; + reset_coeffs(); + init_visited(); + m_num_marks = 0; + m_bound = 0; + literal consequent = s().m_not_l; + justification js = s().m_conflict; + m_conflict_lvl = s().get_max_lvl(consequent, js); + if (m_conflict_lvl == 0) { + return l_undef; + } + if (consequent != null_literal) { + consequent.neg(); + process_antecedent(consequent, 1); + } + TRACE("ba", tout << consequent << " " << js << "\n";); + unsigned idx = s().m_trail.size() - 1; + + do { + TRACE("ba", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n"; + if (consequent != null_literal) { active2pb(m_A); display(tout, m_A, true); } + ); + + switch (js.get_kind()) { + case justification::NONE: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + break; + case justification::BINARY: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + process_antecedent(js.get_literal()); + break; + case justification::TERNARY: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + process_antecedent(js.get_literal1()); + process_antecedent(js.get_literal2()); + break; + case justification::CLAUSE: { + clause & c = s().get_clause(js); + unsigned i = 0; + if (consequent != null_literal) { + round_to_one(consequent.var()); + inc_coeff(consequent, 1); + if (c[0] == consequent) { + i = 1; + } + else { + SASSERT(c[1] == consequent); + process_antecedent(c[0]); + i = 2; } } - m_num_marks = 0; - resolve_conflict(); + inc_bound(1); + unsigned sz = c.size(); + for (; i < sz; i++) + process_antecedent(c[i]); + break; } + case justification::EXT_JUSTIFICATION: { + ++m_stats.m_num_resolves; + ext_justification_idx index = js.get_ext_justification_idx(); + constraint& cnstr = index2constraint(index); + SASSERT(!cnstr.was_removed()); + switch (cnstr.tag()) { + case card_t: + case pb_t: { + pb_base const& p = cnstr.to_pb_base(); + unsigned k = p.k(), sz = p.size(); + m_A.reset(0); + for (unsigned i = 0; i < sz; ++i) { + literal l = p.get_lit(i); + unsigned c = p.get_coeff(i); + if (l == consequent || !is_visited(l.var())) { + m_A.push(l, c); + } + else { + SASSERT(k > c); + TRACE("ba", tout << "visited: " << l << "\n";); + k -= c; + } + } + SASSERT(k > 0); + if (p.lit() != null_literal) m_A.push(~p.lit(), k); + m_A.m_k = k; + break; + } + default: + constraint2pb(cnstr, consequent, 1, m_A); + break; + } + mark_variables(m_A); + if (consequent == null_literal) { + SASSERT(validate_ineq(m_A)); + m_bound = static_cast(m_A.m_k); + for (wliteral wl : m_A.m_wlits) { + process_antecedent(wl.second, wl.first); + } + } + else { + round_to_one(consequent.var()); + if (cnstr.is_pb()) round_to_one(m_A, consequent.var()); + SASSERT(validate_ineq(m_A)); + resolve_with(m_A); + } + break; + } + default: + UNREACHABLE(); + break; + } + + SASSERT(validate_lemma()); + cut(); + + // find the next marked variable in the assignment stack + bool_var v; + while (true) { + consequent = s().m_trail[idx]; + v = consequent.var(); + mark_visited(v); + if (s().is_marked(v)) { + int64_t c = get_coeff(v); + if (c == 0 || (c < 0 == consequent.sign())) { + s().reset_mark(v); + --m_num_marks; + } + else { + break; + } + } + if (idx == 0) { + TRACE("ba", tout << "there is no consequent\n";); + goto bail_out; + } + --idx; + } + + SASSERT(lvl(v) == m_conflict_lvl); + s().reset_mark(v); --idx; + --m_num_marks; + js = s().m_justification[v]; + } + while (m_num_marks > 0 && !m_overflow); + TRACE("ba", active2pb(m_A); display(tout, m_A, true);); + + // TBD: check if this is useful + if (!m_overflow && consequent != null_literal) { + round_to_one(consequent.var()); + } + if (!m_overflow && create_asserting_lemma()) { + active2lemma(); + return l_true; + } + + bail_out: + TRACE("ba", tout << "bail " << m_overflow << "\n";); + if (m_overflow) { + ++m_stats.m_num_overflow; + m_overflow = false; } return l_undef; } - bool ba_solver::create_asserting_lemma() { - bool adjusted = false; - adjust_conflict_level: + bool ba_solver::create_asserting_lemma() { int64_t bound64 = m_bound; int64_t slack = -bound64; - for (bool_var v : m_active_vars) { - slack += get_abs_coeff(v); + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + unsigned c = get_abs_coeff(v); + if (!test_and_set_active(v) || c == 0) continue; + slack += c; + m_active_vars[j++] = v; } + m_active_vars.shrink(j); m_lemma.reset(); m_lemma.push_back(null_literal); unsigned num_skipped = 0; @@ -1395,29 +1720,34 @@ namespace sat { } } if (slack >= 0) { + TRACE("ba", tout << "slack is non-negative\n";); IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); return false; } if (m_overflow) { + TRACE("ba", tout << "overflow\n";); return false; } if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { s().set_conflict(justification()); - return false; } + TRACE("ba", tout << "no asserting literal\n";); return false; - unsigned old_level = m_conflict_lvl; - m_conflict_lvl = 0; - for (unsigned i = 1; i < m_lemma.size(); ++i) { - m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i])); - } - IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); - adjusted = true; - goto adjust_conflict_level; } - if (!adjusted) { - active2card(); + + TRACE("ba", tout << m_lemma << "\n";); + + if (get_config().m_drat) { + svector ps; // TBD fill in + drat_add(m_lemma, ps); + } + + s().m_lemma.reset(); + s().m_lemma.append(m_lemma); + for (unsigned i = 1; i < m_lemma.size(); ++i) { + CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); + s().mark(m_lemma[i].var()); } return true; } @@ -1461,10 +1791,16 @@ namespace sat { } if (g >= 2) { - normalize_active_coeffs(); - for (bool_var v : m_active_vars) { + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + int64_t c = m_coeffs[v]; + if (!test_and_set_active(v) || c == 0) continue; m_coeffs[v] /= static_cast(g); + m_active_vars[j++] = v; } + m_active_vars.shrink(j); m_bound = (m_bound + g - 1) / g; ++m_stats.m_num_cut; } @@ -1500,9 +1836,8 @@ namespace sat { bool_var v = l.var(); unsigned level = lvl(v); - if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) { + if (!s().is_marked(v) && level == m_conflict_lvl) { s().mark(v); - TRACE("sat_verbose", tout << "Mark: v" << v << "\n";); ++m_num_marks; if (_debug_conflict && _debug_consequent != null_literal && _debug_var2position[_debug_consequent.var()] < _debug_var2position[l.var()]) { IF_VERBOSE(0, verbose_stream() << "antecedent " << l << " is above consequent in stack\n";); @@ -1527,7 +1862,9 @@ namespace sat { return p; } - ba_solver::ba_solver(): m_solver(nullptr), m_lookahead(nullptr), m_unit_walk(nullptr), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { + ba_solver::ba_solver() + : m_solver(nullptr), m_lookahead(nullptr), m_unit_walk(nullptr), + m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); m_num_propagations_since_pop = 0; } @@ -2325,7 +2662,8 @@ namespace sat { } void ba_solver::gc() { - if (m_learned.size() >= 2 * m_constraints.size()) { + if (m_learned.size() >= 2 * m_constraints.size() && + (s().at_search_lvl() || s().at_base_lvl())) { for (auto & c : m_learned) update_psm(*c); std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt()); gc_half("glue-psm"); @@ -2342,8 +2680,12 @@ namespace sat { constraint* c = m_learned[i]; if (!m_constraint_to_reinit.contains(c)) { remove_constraint(*c, "gc"); + m_allocator.deallocate(c->obj_size(), c); ++removed; } + else { + m_learned[new_sz++] = c; + } } m_stats.m_num_gc += removed; m_learned.shrink(new_sz); @@ -2493,7 +2835,8 @@ namespace sat { set_non_external(); if (get_config().m_elim_vars) elim_pure(); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); + unit_strengthen(); cleanup_clauses(); cleanup_constraints(); update_pure(); @@ -2939,9 +3282,10 @@ namespace sat { bool found_dup = false; bool found_root = false; + init_visited(); for (unsigned i = 0; i < c.size(); ++i) { literal l = c.get_lit(i); - if (is_marked(l)) { + if (is_visited(l)) { found_dup = true; break; } @@ -2951,10 +3295,7 @@ namespace sat { } } for (unsigned i = 0; i < c.size(); ++i) { - literal l = c.get_lit(i); - unmark_visited(l); - unmark_visited(~l); - found_root |= l.var() == root.var(); + found_root |= c.get_lit(i).var() == root.var(); } if (found_root) { @@ -3111,6 +3452,98 @@ namespace sat { return pure_literals; } + /** + * Strengthen inequalities using binary implication information. + * + * x -> ~y, x -> ~z, y + z + u >= 2 + * ---------------------------------- + * y + z + u + ~x >= 3 + * + * for c : constraints + * for l : c: + * slack <- of c under root(~l) + * if slack < 0: + * add ~root(~l) to c, k <- k + 1 + */ + void ba_solver::unit_strengthen() { + big big(s().m_rand); + big.init(s(), true); + for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) + unit_strengthen(big, *m_constraints[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) + unit_strengthen(big, *m_learned[i]); + } + + void ba_solver::unit_strengthen(big& big, constraint& c) { + if (c.was_removed()) return; + switch (c.tag()) { + case card_t: + unit_strengthen(big, c.to_card()); + break; + case pb_t: + unit_strengthen(big, c.to_pb()); + break; + default: + break; + } + } + + void ba_solver::unit_strengthen(big& big, pb_base& p) { + if (p.lit() != null_literal) return; + unsigned sz = p.size(); + for (unsigned i = 0; i < sz; ++i) { + literal u = p.get_lit(i); + literal r = big.get_root(u); + if (r == u) continue; + unsigned k = p.k(), b = 0; + for (unsigned j = 0; j < sz; ++j) { + literal v = p.get_lit(j); + if (r == big.get_root(v)) { + b += p.get_coeff(j); + } + } + if (b > k) { + r.neg(); + unsigned coeff = b - k; + + svector wlits; + // add coeff * r to p + wlits.push_back(wliteral(coeff, r)); + for (unsigned j = 0; j < sz; ++j) { + u = p.get_lit(j); + unsigned c = p.get_coeff(j); + if (r == u) { + wlits[0].first += c; + } + else if (~r == u) { + if (coeff == c) { + wlits[0] = wlits.back(); + wlits.pop_back(); + b -= c; + } + else if (coeff < c) { + wlits[0].first = c - coeff; + wlits[0].second.neg(); + b -= coeff; + } + else { + // coeff > c + wlits[0].first = coeff - c; + b -= c; + } + } + else { + wlits.push_back(wliteral(c, u)); + } + } + ++m_stats.m_num_big_strengthenings; + p.set_removed(); + constraint* c = add_pb_ge(null_literal, wlits, b, p.learned()); + return; + } + } + } + void ba_solver::subsumption(constraint& cnstr) { if (cnstr.was_removed()) return; switch (cnstr.tag()) { @@ -3199,10 +3632,10 @@ namespace sat { unsigned common = 0; comp.reset(); for (literal l : c2) { - if (is_marked(l)) { + if (is_visited(l)) { ++common; } - else if (is_marked(~l)) { + else if (is_visited(~l)) { comp.push_back(l); } else { @@ -3224,10 +3657,10 @@ namespace sat { self = false; for (literal l : c2) { - if (is_marked(l)) { + if (is_visited(l)) { ++common; } - else if (is_marked(~l)) { + else if (is_visited(~l)) { ++complement; } else { @@ -3251,10 +3684,10 @@ namespace sat { unsigned num_sub = 0; for (unsigned i = 0; i < p2.size(); ++i) { literal l = p2.get_lit(i); - if (is_marked(l) && m_weights[l.index()] <= p2.get_coeff(i)) { + if (is_visited(l) && m_weights[l.index()] <= p2.get_coeff(i)) { ++num_sub; } - if (p1.size() + i > p2.size() + num_sub) return false; + if (p1.size() + i > p2.size() + num_sub) return false; } return num_sub == p1.size(); } @@ -3319,7 +3752,7 @@ namespace sat { clear_watch(c2); unsigned j = 0; for (unsigned i = 0; i < c2.size(); ++i) { - if (!is_marked(~c2[i])) { + if (!is_visited(~c2[i])) { c2[j++] = c2[i]; } } @@ -3355,7 +3788,7 @@ namespace sat { void ba_solver::binary_subsumption(card& c1, literal lit) { if (c1.k() + 1 != c1.size()) return; - SASSERT(is_marked(lit)); + SASSERT(is_visited(lit)); SASSERT(!c1.was_removed()); watch_list & wlist = get_wlist(~lit); watch_list::iterator it = wlist.begin(); @@ -3363,7 +3796,7 @@ namespace sat { watch_list::iterator end = wlist.end(); for (; it != end; ++it) { watched w = *it; - if (w.is_binary_clause() && is_marked(w.get_literal())) { + if (w.is_binary_clause() && is_visited(w.get_literal())) { ++m_stats.m_num_bin_subsumes; IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); if (!w.is_learned()) { @@ -3385,6 +3818,7 @@ namespace sat { return; } clause_vector removed_clauses; + init_visited(); for (literal l : c1) mark_visited(l); for (unsigned i = 0; i < std::min(c1.size(), c1.k() + 1); ++i) { literal lit = c1[i]; @@ -3392,7 +3826,6 @@ namespace sat { clause_subsumption(c1, lit, removed_clauses); binary_subsumption(c1, lit); } - for (literal l : c1) unmark_visited(l); m_clause_removed |= !removed_clauses.empty(); for (clause *c : removed_clauses) { c->set_removed(true); @@ -3404,6 +3837,7 @@ namespace sat { if (p1.was_removed() || p1.lit() != null_literal) { return; } + init_visited(); for (wliteral l : p1) { SASSERT(m_weights.size() <= l.second.index() || m_weights[l.second.index()] == 0); m_weights.setx(l.second.index(), l.first, 0); @@ -3415,7 +3849,6 @@ namespace sat { } for (wliteral l : p1) { m_weights[l.second.index()] = 0; - unmark_visited(l.second); } } @@ -3612,10 +4045,11 @@ namespace sat { } } - void ba_solver::display(std::ostream& out, ineq& ineq, bool values) const { - for (unsigned i = 0; i < ineq.m_lits.size(); ++i) { - out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " "; - if (values) out << value(ineq.m_lits[i]) << " "; + void ba_solver::display(std::ostream& out, ineq const& ineq, bool values) const { + for (unsigned i = 0; i < ineq.size(); ++i) { + if (ineq.coeff(i) != 1) out << ineq.coeff(i) << "*"; + out << ineq.lit(i) << " "; + if (values) out << value(ineq.lit(i)) << " "; } out << ">= " << ineq.m_k << "\n"; } @@ -3705,6 +4139,10 @@ namespace sat { st.update("ba resolves", m_stats.m_num_resolves); st.update("ba cuts", m_stats.m_num_cut); st.update("ba gc", m_stats.m_num_gc); + st.update("ba overflow", m_stats.m_num_overflow); + st.update("ba big strengthenings", m_stats.m_num_big_strengthenings); + st.update("ba lemmas", m_stats.m_num_lemmas); + st.update("ba subsumes", m_stats.m_num_bin_subsumes + m_stats.m_num_clause_subsumes + m_stats.m_num_pb_subsumes); } bool ba_solver::validate_unit_propagation(card const& c, literal alit) const { @@ -3799,62 +4237,88 @@ namespace sat { int64_t val = -bound64; reset_active_var_set(); for (bool_var v : m_active_vars) { - if (m_active_var_set.contains(v)) continue; - int64_t coeff = get_coeff(v); - if (coeff == 0) continue; - m_active_var_set.insert(v); - literal lit(v, false); - if (coeff < 0 && value(lit) != l_true) { - val -= coeff; - } - else if (coeff > 0 && value(lit) != l_false) { - val += coeff; + if (!test_and_set_active(v)) continue; + wliteral wl = get_wliteral(v); + if (wl.first == 0) continue; + if (!is_false(wl.second)) { + val += wl.first; } } - CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A);); + CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A, true);); return val < 0; } + /** + * the slack of inequalities on the stack should be non-positive. + */ + bool ba_solver::validate_ineq(ineq const& ineq) const { + int64_t k = -static_cast(ineq.m_k); + for (wliteral wl : ineq.m_wlits) { + if (!is_false(wl.second)) + k += wl.first; + } + CTRACE("ba", k > 0, display(tout, ineq, true);); + return k <= 0; + } + void ba_solver::reset_active_var_set() { while (!m_active_var_set.empty()) m_active_var_set.erase(); } - void ba_solver::active2pb(ineq& p) { - reset_active_var_set(); - p.reset(m_bound); - for (bool_var v : m_active_vars) { - if (m_active_var_set.contains(v)) continue; - int64_t coeff = get_coeff(v); - if (coeff == 0) continue; + bool ba_solver::test_and_set_active(bool_var v) { + if (m_active_var_set.contains(v)) { + return false; + } + else { m_active_var_set.insert(v); - literal lit(v, coeff < 0); - p.m_lits.push_back(lit); - p.m_coeffs.push_back(std::abs(coeff)); + return true; + } + } + + void ba_solver::active2pb(ineq& p) { + p.reset(m_bound); + active2wlits(p.m_wlits); + } + + void ba_solver::active2wlits() { + m_wlits.reset(); + active2wlits(m_wlits); + } + + void ba_solver::active2wlits(svector& wlits) { + uint64_t sum = 0; + reset_active_var_set(); + for (bool_var v : m_active_vars) { + if (!test_and_set_active(v)) continue; + wliteral wl = get_wliteral(v); + if (wl.first == 0) continue; + wlits.push_back(wl); + sum += wl.first; + } + m_overflow |= sum >= UINT_MAX/2; + } + + ba_solver::constraint* ba_solver::active2lemma() { + switch (s().m_config.m_pb_lemma_format) { + case PB_LEMMA_CARDINALITY: + return active2card(); + case PB_LEMMA_PB: + return active2constraint(); + default: + UNREACHABLE(); + return nullptr; } } ba_solver::constraint* ba_solver::active2constraint() { - reset_active_var_set(); - m_wlits.reset(); - uint64_t sum = 0; - if (m_bound == 1) return nullptr; - if (m_overflow) return nullptr; - - for (bool_var v : m_active_vars) { - int coeff = get_int_coeff(v); - if (m_active_var_set.contains(v) || coeff == 0) continue; - m_active_var_set.insert(v); - literal lit(v, coeff < 0); - m_wlits.push_back(wliteral(get_abs_coeff(v), lit)); - sum += get_abs_coeff(v); - } - - if (m_overflow || sum >= UINT_MAX/2) { + active2wlits(); + if (m_overflow) { return nullptr; } - else { - return add_pb_ge(null_literal, m_wlits, m_bound, true); - } + constraint* c = add_pb_ge(null_literal, m_wlits, m_bound, true); + TRACE("ba", if (c) display(tout, *c, true);); + ++m_stats.m_num_lemmas; + return c; } /* @@ -3889,11 +4353,9 @@ namespace sat { ba_solver::constraint* ba_solver::active2card() { - normalize_active_coeffs(); - m_wlits.reset(); - for (bool_var v : m_active_vars) { - int coeff = get_int_coeff(v); - m_wlits.push_back(std::make_pair(get_abs_coeff(v), literal(v, coeff < 0))); + active2wlits(); + if (m_overflow) { + return nullptr; } std::sort(m_wlits.begin(), m_wlits.end(), compare_wlit()); unsigned k = 0; @@ -3928,7 +4390,9 @@ namespace sat { ++num_max_level; } } - if (m_overflow) return nullptr; + if (m_overflow) { + return nullptr; + } if (slack >= k) { #if 0 @@ -3947,8 +4411,9 @@ namespace sat { } constraint* c = add_at_least(null_literal, lits, k, true); + ++m_stats.m_num_lemmas; + if (c) { - // IF_VERBOSE(0, verbose_stream() << *c << "\n";); lits.reset(); for (wliteral wl : m_wlits) { if (value(wl.second) == l_false) lits.push_back(wl.second); @@ -3963,15 +4428,18 @@ namespace sat { void ba_solver::justification2pb(justification const& js, literal lit, unsigned offset, ineq& ineq) { switch (js.get_kind()) { case justification::NONE: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); break; case justification::BINARY: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); ineq.push(js.get_literal(), offset); break; case justification::TERNARY: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); ineq.push(js.get_literal1(), offset); @@ -3986,35 +4454,7 @@ namespace sat { case justification::EXT_JUSTIFICATION: { ext_justification_idx index = js.get_ext_justification_idx(); constraint& cnstr = index2constraint(index); - switch (cnstr.tag()) { - case card_t: { - card& c = cnstr.to_card(); - ineq.reset(offset*c.k()); - for (literal l : c) ineq.push(l, offset); - if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k()); - break; - } - case pb_t: { - pb& p = cnstr.to_pb(); - ineq.reset(p.k()); - for (wliteral wl : p) ineq.push(wl.second, wl.first); - if (p.lit() != null_literal) ineq.push(~p.lit(), p.k()); - break; - } - case xr_t: { - xr& x = cnstr.to_xr(); - literal_vector ls; - get_antecedents(lit, x, ls); - ineq.reset(offset); - for (literal l : ls) ineq.push(~l, offset); - literal lxr = x.lit(); - if (lxr != null_literal) ineq.push(~lxr, offset); - break; - } - default: - UNREACHABLE(); - break; - } + constraint2pb(cnstr, lit, offset, ineq); break; } default: @@ -4023,6 +4463,38 @@ namespace sat { } } + void ba_solver::constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& ineq) { + switch (cnstr.tag()) { + case card_t: { + card& c = cnstr.to_card(); + ineq.reset(offset*c.k()); + for (literal l : c) ineq.push(l, offset); + if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k()); + break; + } + case pb_t: { + pb& p = cnstr.to_pb(); + ineq.reset(offset * p.k()); + for (wliteral wl : p) ineq.push(wl.second, offset * wl.first); + if (p.lit() != null_literal) ineq.push(~p.lit(), offset * p.k()); + break; + } + case xr_t: { + xr& x = cnstr.to_xr(); + literal_vector ls; + SASSERT(lit != null_literal); + get_antecedents(lit, x, ls); + ineq.reset(offset); + for (literal l : ls) ineq.push(~l, offset); + literal lxr = x.lit(); + if (lxr != null_literal) ineq.push(~lxr, offset); + break; + } + default: + UNREACHABLE(); + break; + } + } // validate that m_A & m_B implies m_C @@ -4030,14 +4502,14 @@ namespace sat { return true; u_map coeffs; uint64_t k = m_A.m_k + m_B.m_k; - for (unsigned i = 0; i < m_A.m_lits.size(); ++i) { - uint64_t coeff = m_A.m_coeffs[i]; - SASSERT(!coeffs.contains(m_A.m_lits[i].index())); - coeffs.insert(m_A.m_lits[i].index(), coeff); + for (unsigned i = 0; i < m_A.size(); ++i) { + uint64_t coeff = m_A.coeff(i); + SASSERT(!coeffs.contains(m_A.lit(i).index())); + coeffs.insert(m_A.lit(i).index(), coeff); } - for (unsigned i = 0; i < m_B.m_lits.size(); ++i) { - uint64_t coeff1 = m_B.m_coeffs[i], coeff2; - literal lit = m_B.m_lits[i]; + for (unsigned i = 0; i < m_B.size(); ++i) { + uint64_t coeff1 = m_B.coeff(i), coeff2; + literal lit = m_B.lit(i); if (coeffs.find((~lit).index(), coeff2)) { if (coeff1 == coeff2) { coeffs.remove((~lit).index()); @@ -4062,11 +4534,11 @@ namespace sat { } } // C is above the sum of A and B - for (unsigned i = 0; i < m_C.m_lits.size(); ++i) { - literal lit = m_C.m_lits[i]; + for (unsigned i = 0; i < m_C.size(); ++i) { + literal lit = m_C.lit(i); uint64_t coeff; if (coeffs.find(lit.index(), coeff)) { - if (coeff > m_C.m_coeffs[i] && m_C.m_coeffs[i] < m_C.m_k) { + if (coeff > m_C.coeff(i) && m_C.coeff(i) < m_C.m_k) { goto violated; } coeffs.remove(lit.index()); @@ -4113,15 +4585,15 @@ namespace sat { */ literal ba_solver::translate_to_sat(solver& s, u_map& translation, ineq const& pb) { SASSERT(pb.m_k > 0); - if (pb.m_lits.size() > 1) { + if (pb.size() > 1) { ineq a, b; a.reset(pb.m_k); b.reset(pb.m_k); - for (unsigned i = 0; i < pb.m_lits.size()/2; ++i) { - a.push(pb.m_lits[i], pb.m_coeffs[i]); + for (unsigned i = 0; i < pb.size()/2; ++i) { + a.push(pb.lit(i), pb.coeff(i)); } - for (unsigned i = pb.m_lits.size()/2; i < pb.m_lits.size(); ++i) { - b.push(pb.m_lits[i], pb.m_coeffs[i]); + for (unsigned i = pb.size()/2; i < pb.size(); ++i) { + b.push(pb.lit(i), pb.coeff(i)); } bool_var v = s.mk_var(); literal lit(v, false); @@ -4133,8 +4605,8 @@ namespace sat { s.mk_clause(lits); return lit; } - if (pb.m_coeffs[0] >= pb.m_k) { - return translate_to_sat(s, translation, pb.m_lits[0]); + if (pb.coeff(0) >= pb.m_k) { + return translate_to_sat(s, translation, pb.lit(0)); } else { return null_literal; @@ -4186,9 +4658,9 @@ namespace sat { ba_solver::ineq ba_solver::negate(ineq const& a) const { ineq result; uint64_t sum = 0; - for (unsigned i = 0; i < a.m_lits.size(); ++i) { - result.push(~a.m_lits[i], a.m_coeffs[i]); - sum += a.m_coeffs[i]; + for (unsigned i = 0; i < a.size(); ++i) { + result.push(~a.lit(i), a.coeff(i)); + sum += a.coeff(i); } SASSERT(sum >= a.m_k + 1); result.m_k = sum + 1 - a.m_k; @@ -4207,15 +4679,15 @@ namespace sat { TRACE("ba", tout << "literal " << l << " is not false\n";); return false; } - if (!p.m_lits.contains(l)) { + if (!p.contains(l)) { TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";); return false; } } uint64_t value = 0; - for (unsigned i = 0; i < p.m_lits.size(); ++i) { - uint64_t coeff = p.m_coeffs[i]; - if (!lits.contains(p.m_lits[i])) { + for (unsigned i = 0; i < p.size(); ++i) { + uint64_t coeff = p.coeff(i); + if (!lits.contains(p.lit(i))) { value += coeff; } } diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index 26887e3b1..558b22bf3 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -25,6 +25,7 @@ Revision History: #include "sat/sat_solver.h" #include "sat/sat_lookahead.h" #include "sat/sat_unit_walk.h" +#include "sat/sat_big.h" #include "util/scoped_ptr_vector.h" #include "util/sorting_network.h" @@ -41,8 +42,11 @@ namespace sat { unsigned m_num_bin_subsumes; unsigned m_num_clause_subsumes; unsigned m_num_pb_subsumes; + unsigned m_num_big_strengthenings; unsigned m_num_cut; unsigned m_num_gc; + unsigned m_num_overflow; + unsigned m_num_lemmas; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -57,6 +61,7 @@ namespace sat { class card; class pb; class xr; + class pb_base; class constraint { protected: @@ -104,6 +109,7 @@ namespace sat { card const& to_card() const; pb const& to_pb() const; xr const& to_xr() const; + pb_base const& to_pb_base() const; bool is_card() const { return m_tag == card_t; } bool is_pb() const { return m_tag == pb_t; } bool is_xr() const { return m_tag == xr_t; } @@ -118,7 +124,7 @@ namespace sat { }; friend std::ostream& operator<<(std::ostream& out, constraint const& c); - + // base class for pb and cardinality constraints class pb_base : public constraint { protected: @@ -204,12 +210,18 @@ namespace sat { protected: struct ineq { - literal_vector m_lits; - svector m_coeffs; + svector m_wlits; uint64_t m_k; ineq(): m_k(0) {} - void reset(uint64_t k) { m_lits.reset(); m_coeffs.reset(); m_k = k; } - void push(literal l, uint64_t c) { m_lits.push_back(l); m_coeffs.push_back(c); } + unsigned size() const { return m_wlits.size(); } + literal lit(unsigned i) const { return m_wlits[i].second; } + unsigned coeff(unsigned i) const { return m_wlits[i].first; } + void reset(uint64_t k) { m_wlits.reset(); m_k = k; } + void push(literal l, unsigned c) { m_wlits.push_back(wliteral(c,l)); } + unsigned bv_coeff(bool_var v) const; + void divide(unsigned c); + void weaken(unsigned i); + bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; } }; solver* m_solver; @@ -273,7 +285,8 @@ namespace sat { // simplification routines - svector m_visited; + svector m_visited; + unsigned m_visited_ts; vector> m_cnstr_use_list; use_list m_clause_use_list; bool m_simplify_change; @@ -292,9 +305,11 @@ namespace sat { void binary_subsumption(card& c1, literal lit); void clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses); void card_subsumption(card& c1, literal lit); - void mark_visited(literal l) { m_visited[l.index()] = true; } - void unmark_visited(literal l) { m_visited[l.index()] = false; } - bool is_marked(literal l) const { return m_visited[l.index()] != 0; } + void init_visited(); + void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; } + void mark_visited(bool_var v) { mark_visited(literal(v, false)); } + bool is_visited(bool_var v) const { return is_visited(literal(v, false)); } + bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; } unsigned get_num_unblocked_bin(literal l); literal get_min_occurrence_literal(card const& c); void init_use_lists(); @@ -302,6 +317,9 @@ namespace sat { unsigned set_non_external(); unsigned elim_pure(); bool elim_pure(literal lit); + void unit_strengthen(); + void unit_strengthen(big& big, constraint& cs); + void unit_strengthen(big& big, pb_base& p); void subsumption(constraint& c1); void subsumption(card& c1); void gc_half(char const* _method); @@ -396,10 +414,23 @@ namespace sat { lbool eval(model const& m, pb const& p) const; double get_reward(pb const& p, literal_occs_fun& occs) const; + // RoundingPb conflict resolution + lbool resolve_conflict_rs(); + void round_to_one(ineq& ineq, bool_var v); + void round_to_one(bool_var v); + void divide(unsigned c); + void resolve_on(literal lit); + void resolve_with(ineq const& ineq); + void reset_marks(unsigned idx); + void mark_variables(ineq const& ineq); + + void bail_resolve_conflict(unsigned idx); + // access solver inline lbool value(bool_var v) const { return value(literal(v, false)); } inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; } + inline bool is_false(literal lit) const { return l_false == value(lit); } inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); } inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); } @@ -426,9 +457,11 @@ namespace sat { mutable bool m_overflow; void reset_active_var_set(); - void normalize_active_coeffs(); + bool test_and_set_active(bool_var v); void inc_coeff(literal l, unsigned offset); int64_t get_coeff(bool_var v) const; + uint64_t get_coeff(literal lit) const; + wliteral get_wliteral(bool_var v); unsigned get_abs_coeff(bool_var v) const; int get_int_coeff(bool_var v) const; unsigned get_bound() const; @@ -436,6 +469,7 @@ namespace sat { literal get_asserting_literal(literal conseq); void process_antecedent(literal l, unsigned offset); + void process_antecedent(literal l) { process_antecedent(l, 1); } void process_card(card& c, unsigned offset); void cut(); bool create_asserting_lemma(); @@ -446,6 +480,7 @@ namespace sat { bool validate_conflict(pb const& p) const; bool validate_assign(literal_vector const& lits, literal lit); bool validate_lemma(); + bool validate_ineq(ineq const& ineq) const; bool validate_unit_propagation(card const& c, literal alit) const; bool validate_unit_propagation(pb const& p, literal alit) const; bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const; @@ -464,12 +499,17 @@ namespace sat { ineq m_A, m_B, m_C; void active2pb(ineq& p); + constraint* active2lemma(); constraint* active2constraint(); constraint* active2card(); + void active2wlits(); + void active2wlits(svector& wlits); void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p); + void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p); bool validate_resolvent(); + unsigned get_coeff(ineq const& pb, literal lit); - void display(std::ostream& out, ineq& p, bool values = false) const; + void display(std::ostream& out, ineq const& p, bool values = false) const; void display(std::ostream& out, card const& c, bool values) const; void display(std::ostream& out, pb const& p, bool values) const; void display(std::ostream& out, xr const& c, bool values) const; diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 35898a110..c1eeecd27 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -22,7 +22,8 @@ Revision History: namespace sat { big::big(random_gen& rand): - m_rand(rand) { + m_rand(rand), + m_include_cardinality(false) { } void big::init(solver& s, bool learned) { @@ -42,22 +43,22 @@ namespace sat { m_roots[v.index()] = false; edges.push_back(v); } -#if 0 - if (w.is_ext_constraint() && + if (m_include_cardinality && + w.is_ext_constraint() && s.m_ext && - learned && + learned && // cannot (yet) observe if ext constraints are learned !seen_idx.contains(w.get_ext_constraint_idx()) && s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) { seen_idx.insert(w.get_ext_constraint_idx(), true); - for (unsigned i = 0; i < r.size(); ++i) { - literal u = r[i]; - for (unsigned j = i + 1; j < r.size(); ++j) { - // add ~r[i] -> r[j] - literal v = r[j]; - literal u = ~r[j]; + for (unsigned i = 0; i < std::min(4u, r.size()); ++i) { + shuffle(r.size(), r.c_ptr(), m_rand); + literal u = r[0]; + for (unsigned j = 1; j < r.size(); ++j) { + literal v = ~r[j]; + // add u -> v m_roots[v.index()] = false; m_dag[u.index()].push_back(v); - // add ~r[j] -> r[i] + // add ~v -> ~u v.neg(); u.neg(); m_roots[u.index()] = false; @@ -65,7 +66,6 @@ namespace sat { } } } -#endif } } done_adding_edges(); @@ -268,6 +268,16 @@ namespace sat { return out << v; } + literal big::get_root(literal l) { + literal r = l; + do { + l = r; + r = m_root[l.index()]; + } + while (r != l); + return r; + } + void big::display(std::ostream& out) const { unsigned idx = 0; for (auto& next : m_dag) { diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 898ddd1e8..25093fd60 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -34,6 +34,7 @@ namespace sat { svector m_left, m_right; literal_vector m_root, m_parent; bool m_learned; + bool m_include_cardinality; svector> m_del_bin; @@ -54,6 +55,9 @@ namespace sat { // static svector> s_del_bin; big(random_gen& rand); + + void set_include_cardinality(bool f) { m_include_cardinality = f; } + /** \brief initialize a BIG from a solver. */ @@ -77,7 +81,7 @@ namespace sat { int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } - literal get_root(literal l) const { return m_root[l.index()]; } + literal get_root(literal l); bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); } void display(std::ostream& out) const; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 29221c0e8..423a5f532 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -199,6 +199,22 @@ namespace sat { else throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented"); + s = p.pb_resolve(); + if (s == "cardinality") + m_pb_resolve = PB_CARDINALITY; + else if (s == "rounding") + m_pb_resolve = PB_ROUNDING; + else + throw sat_param_exception("invalid PB resolve: 'cardinality' or 'rounding' expected"); + + s = p.pb_lemma_format(); + if (s == "cardinality") + m_pb_lemma_format = PB_LEMMA_CARDINALITY; + else if (s == "pb") + m_pb_lemma_format = PB_LEMMA_PB; + else + throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected"); + m_card_solver = p.cardinality_solver(); sat_simplifier_params sp(_p); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index ba5c9aaf3..4d33225f0 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -60,6 +60,16 @@ namespace sat { PB_SEGMENTED }; + enum pb_resolve { + PB_CARDINALITY, + PB_ROUNDING + }; + + enum pb_lemma_format { + PB_LEMMA_CARDINALITY, + PB_LEMMA_PB + }; + enum reward_t { ternary_reward, unit_literal_reward, @@ -151,6 +161,8 @@ namespace sat { pb_solver m_pb_solver; bool m_card_solver; + pb_resolve m_pb_resolve; + pb_lemma_format m_pb_lemma_format; // branching heuristic settings. branching_heuristic m_branching_heuristic; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 2aef881ca..acde7e30c 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -43,8 +43,10 @@ def_module_params('sat', ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'), ('cardinality.solver', BOOL, True, 'use cardinality solver'), ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'), - ('xor.solver', BOOL, False, 'use xor solver'), + ('xor.solver', BOOL, False, 'use xor solver'), ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'), + ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'), + ('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index 146bd2366..1ba646992 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -60,7 +60,6 @@ namespace sat { void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); } int get_left(literal l) const { return m_big.get_left(l); } int get_right(literal l) const { return m_big.get_right(l); } - literal get_root(literal l) const { return m_big.get_root(l); } bool connected(literal u, literal v) const { return m_big.connected(u, v); } }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index fea45c07b..f38da472f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -343,12 +343,6 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { -#if 0 - if ((l1.var() == 2039 || l2.var() == 2039) && - (l1.var() == 27042 || l2.var() == 27042)) { - IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n"); - } -#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d42a28ac0..645ef8a3f 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -82,6 +82,7 @@ struct goal2sat::imp { m_is_lemma(false) { updt_params(p); m_true = sat::null_bool_var; + mk_true(); } void updt_params(params_ref const & p) { diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 26b099240..52d3a5943 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -56,9 +56,11 @@ z3_add_component(smt theory_dl.cpp theory_dummy.cpp theory_fpa.cpp + theory_jobscheduler.cpp theory_lra.cpp theory_opt.cpp theory_pb.cpp + theory_recfun.cpp theory_seq.cpp theory_str.cpp theory_utvpi.cpp diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index b8b561e37..6b4aee1c3 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -95,5 +95,7 @@ def_module_params(module_name='smt', ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'), - ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy') + ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), + ('recfun.native', BOOL, True, 'use native rec-fun solver'), + ('recfun.depth', UINT, 2, 'initial depth for maxrec expansion') )) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 41f11dca2..21af24b32 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -37,6 +37,7 @@ Revision History: #include "model/model_pp.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_translation.h" +#include "ast/recfun_decl_plugin.h" namespace smt { @@ -1384,7 +1385,10 @@ namespace smt { SASSERT(m_manager.is_eq(n)); expr * lhs = n->get_arg(0); expr * rhs = n->get_arg(1); - if (val == l_true) { + if (m_manager.is_bool(lhs)) { + // no-op + } + else if (val == l_true) { add_eq(get_enode(lhs), get_enode(rhs), eq_justification(l)); } else { @@ -3207,7 +3211,7 @@ namespace smt { } else { set_conflict(b_justification(tmp_clause.first), null_literal); - } + } VERIFY(!resolve_conflict()); return l_false; next_clause: @@ -3266,6 +3270,18 @@ namespace smt { m_assumptions.reset(); } + bool context::should_research(lbool r) { + if (r != l_false || m_unsat_core.empty()) { + return false; + } + for (theory* th : m_theory_set) { + if (th->should_research(m_unsat_core)) { + return true; + } + } + return false; + } + lbool context::mk_unsat_core(lbool r) { if (r != l_false) return r; SASSERT(inconsistent()); @@ -3353,7 +3369,7 @@ namespace smt { add_theory_assumptions(theory_assumptions); if (!theory_assumptions.empty()) { TRACE("search", tout << "Adding theory assumptions to context" << std::endl;); - return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true); + return check(0, nullptr, reset_cancel); } internalize_assertions(); @@ -3407,19 +3423,24 @@ namespace smt { } } - lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) { + lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) { if (!check_preamble(reset_cancel)) return l_undef; SASSERT(at_base_level()); setup_context(false); - expr_ref_vector asms(m_manager, num_assumptions, assumptions); - if (!already_did_theory_assumptions) add_theory_assumptions(asms); - // introducing proxies: if (!validate_assumptions(asms)) return l_undef; - TRACE("unsat_core_bug", tout << asms << "\n";); - internalize_assertions(); - init_assumptions(asms); - TRACE("before_search", display(tout);); - lbool r = search(); - r = mk_unsat_core(r); + lbool r; + do { + pop_to_base_lvl(); + expr_ref_vector asms(m_manager, num_assumptions, assumptions); + add_theory_assumptions(asms); + // introducing proxies: if (!validate_assumptions(asms)) return l_undef; + TRACE("unsat_core_bug", tout << asms << "\n";); + internalize_assertions(); + init_assumptions(asms); + TRACE("before_search", display(tout);); + r = search(); + r = mk_unsat_core(r); + } + while (should_research(r)); r = check_finalize(r); return r; } @@ -3428,15 +3449,20 @@ namespace smt { if (!check_preamble(true)) return l_undef; TRACE("before_search", display(tout);); setup_context(false); - expr_ref_vector asms(cube); - add_theory_assumptions(asms); - // introducing proxies: if (!validate_assumptions(asms)) return l_undef; - for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; - internalize_assertions(); - init_assumptions(asms); - for (auto const& clause : clauses) init_clause(clause); - lbool r = search(); - r = mk_unsat_core(r); + lbool r; + do { + pop_to_base_lvl(); + expr_ref_vector asms(cube); + add_theory_assumptions(asms); + // introducing proxies: if (!validate_assumptions(asms)) return l_undef; + for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; + internalize_assertions(); + init_assumptions(asms); + for (auto const& clause : clauses) init_clause(clause); + r = search(); + r = mk_unsat_core(r); + } + while (should_research(r)); r = check_finalize(r); return r; } @@ -3770,7 +3796,7 @@ namespace smt { } m_stats.m_num_final_checks++; - TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";); + TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";); final_check_status ok = m_qmanager->final_check_eh(false); if (ok != FC_DONE) @@ -4428,6 +4454,26 @@ namespace smt { m_model->register_decl(f, fi); } } + recfun::util u(m); + recfun::decl::plugin& p = u.get_plugin(); + func_decl_ref_vector recfuns = u.get_rec_funs(); + for (func_decl* f : recfuns) { + auto& def = u.get_def(f); + expr* rhs = def.get_rhs(); + if (!rhs) continue; + func_interp* fi = alloc(func_interp, m, f->get_arity()); + // reverse argument order so that variable 0 starts at the beginning. + expr_ref_vector subst(m); + unsigned idx = 0; + for (unsigned i = 0; i < f->get_arity(); ++i) { + subst.push_back(m.mk_var(i, f->get_domain(i))); + } + var_subst sub(m, true); + expr_ref bodyr = sub(rhs, subst.size(), subst.c_ptr()); + + fi->set_else(bodyr); + m_model->register_decl(f, fi); + } } }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d0c9cc776..6f382a5f6 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -859,6 +859,10 @@ namespace smt { void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr); + void mk_th_axiom(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) { + mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params); + } + /* * Provide a hint to the core solver that the specified literals form a "theory case split". * The core solver will enforce the condition that exactly one of these literals can be @@ -1010,9 +1014,9 @@ namespace smt { void restore_theory_vars(enode * r2, enode * r1); void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { - SASSERT(lhs != rhs); - SASSERT(lhs->get_root() != rhs->get_root()); - m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); + if (lhs->get_root() != rhs->get_root()) { + m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); + } } void push_new_congruence(enode * n1, enode * n2, bool used_commutativity) { @@ -1133,6 +1137,8 @@ namespace smt { void add_theory_assumptions(expr_ref_vector & theory_assumptions); lbool mk_unsat_core(lbool result); + + bool should_research(lbool result); void validate_unsat_core(); @@ -1243,6 +1249,11 @@ namespace smt { public: bool can_propagate() const; + // Retrieve arithmetic values. + bool get_arith_lo(expr* e, rational& lo, bool& strict); + bool get_arith_up(expr* e, rational& up, bool& strict); + bool get_arith_value(expr* e, rational& value); + // ----------------------------------- // // Model checking... (must be improved) @@ -1515,7 +1526,7 @@ namespace smt { void pop(unsigned num_scopes); - lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false); + lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true); lbool check(expr_ref_vector const& cube, vector const& clauses); @@ -1609,6 +1620,34 @@ namespace smt { void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); } }; + struct pp_lit { + context & ctx; + literal lit; + pp_lit(context & ctx, literal lit) : ctx(ctx), lit(lit) {} + }; + + inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) { + return pp.ctx.display_detailed_literal(out, pp.lit); + } + + struct pp_lits { + context & ctx; + literal const *lits; + unsigned len; + pp_lits(context & ctx, unsigned len, literal const *lits) : ctx(ctx), lits(lits), len(len) {} + pp_lits(context & ctx, literal_vector const& ls) : ctx(ctx), lits(ls.c_ptr()), len(ls.size()) {} + }; + + inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) { + out << "{"; + bool first = true; + for (unsigned i = 0; i < pp.len; ++i) { + if (first) { first = false; } else { out << " or\n"; } + pp.ctx.display_detailed_literal(out, pp.lits[i]); + } + return out << "}"; + + } struct enode_eq_pp { context const& ctx; enode_pair const& p; diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index 7f409622b..a6c4f49b4 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -303,7 +303,7 @@ namespace smt { for (bool_var v = 0; v < num; v++) { if (has_enode(v)) { enode * n = bool_var2enode(v); - if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false) { + if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m_manager.is_iff(n->get_owner())) { TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m_manager) << "\n";); enode * lhs = n->get_arg(0)->get_root(); enode * rhs = n->get_arg(1)->get_root(); diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index a4b3029e2..c27845ff6 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -402,7 +402,10 @@ namespace smt { enode * n = m_context->get_enode(t); unsigned num_args = n->get_num_args(); func_decl * f = n->get_decl(); - if (num_args > 0 && n->get_cg() == n && include_func_interp(f)) { + if (num_args == 0 && include_func_interp(f)) { + m_model->register_decl(f, get_value(n)); + } + else if (num_args > 0 && n->get_cg() == n && include_func_interp(f)) { ptr_buffer args; expr * result = get_value(n); SASSERT(result); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 6dcc9448c..2cf0e2651 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -28,6 +28,7 @@ Revision History: #include "smt/theory_array_full.h" #include "smt/theory_bv.h" #include "smt/theory_datatype.h" +#include "smt/theory_recfun.h" #include "smt/theory_dummy.h" #include "smt/theory_dl.h" #include "smt/theory_seq_empty.h" @@ -35,6 +36,7 @@ Revision History: #include "smt/theory_pb.h" #include "smt/theory_fpa.h" #include "smt/theory_str.h" +#include "smt/theory_jobscheduler.h" namespace smt { @@ -119,6 +121,8 @@ namespace smt { setup_UFLRA(); else if (m_logic == "LRA") setup_LRA(); + else if (m_logic == "CSP") + setup_CSP(); else if (m_logic == "QF_FP") setup_QF_FP(); else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP") @@ -196,6 +200,8 @@ namespace smt { setup_QF_DT(); else if (m_logic == "LRA") setup_LRA(); + else if (m_logic == "CSP") + setup_CSP(); else setup_unknown(st); } @@ -217,6 +223,7 @@ namespace smt { void setup::setup_QF_DT() { setup_QF_UF(); setup_datatypes(); + setup_recfuns(); } void setup::setup_QF_BVRE() { @@ -873,6 +880,12 @@ namespace smt { m_context.register_plugin(alloc(theory_datatype, m_manager, m_params)); } + void setup::setup_recfuns() { + TRACE("recfun", tout << "registering theory recfun...\n";); + theory_recfun * th = alloc(theory_recfun, m_manager); + m_context.register_plugin(th); + } + void setup::setup_dl() { m_context.register_plugin(mk_theory_dl(m_manager)); } @@ -916,6 +929,11 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_seq, m_manager, m_params)); } + void setup::setup_CSP() { + setup_unknown(); + m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager)); + } + void setup::setup_unknown() { static_features st(m_manager); ptr_vector fmls; @@ -926,6 +944,7 @@ namespace smt { setup_arrays(); setup_bv(); setup_datatypes(); + setup_recfuns(); setup_dl(); setup_seq_str(st); setup_card(); @@ -945,6 +964,7 @@ namespace smt { setup_seq_str(st); setup_card(); setup_fpa(); + setup_recfuns(); return; } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index ed0ab066d..01a143301 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -81,6 +81,7 @@ namespace smt { void setup_QF_FPBV(); void setup_QF_S(); void setup_LRA(); + void setup_CSP(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); void setup_AUFLIRA(bool simple_array = true); @@ -93,6 +94,7 @@ namespace smt { void setup_unknown(static_features & st); void setup_arrays(); void setup_datatypes(); + void setup_recfuns(); void setup_bv(); void setup_arith(); void setup_dl(); diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index f65ffe922..66bb3e14b 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -194,6 +194,15 @@ namespace smt { return l_false; } + /** + \brief This method is called from the smt_context when an unsat core is generated. + The theory may tell the solver to perform iterative deepening by invalidating + this unsat core and increasing some resource constraints. + */ + virtual bool should_research(expr_ref_vector & unsat_core) { + return false; + } + /** \brief This method is invoked before the search starts. */ @@ -294,6 +303,8 @@ namespace smt { SASSERT(m_context); return *m_context; } + + context & ctx() const { return get_context(); } ast_manager & get_manager() const { SASSERT(m_manager); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3da78e8ee..4ca4928d0 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3302,7 +3302,6 @@ namespace smt { return b && to_expr(b->get_value(), is_int(v), r); } - template bool theory_arith::get_lower(enode * n, rational& r, bool& is_strict) { theory_var v = n->get_th_var(get_id()); diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp new file mode 100644 index 000000000..880d75d24 --- /dev/null +++ b/src/smt/theory_jobscheduler.cpp @@ -0,0 +1,1070 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_jobscheduler.cpp + +Abstract: + + +Author: + + Nikolaj Bjorner (nbjorner) 2018-09-08. + +Revision History: + +TODO: + +- arithmetic interface + +- propagation queue: + - register bounds on start times to propagate energy constraints + - more general registration mechanism for arithmetic theory. +- interact with opt +- jobs without resources + - complain or add dummy resource? At which level. + +Features: +- properties +- priority + - try mss based from outside +- job-goal + - try optimization based on arithmetic solver. + - earliest start, latest start +- constraint level + - add constraints gradually +- resource groups + - resource groups like a resource + - resources bound to resource groups within time intervals + - job can require to use K resources from a resource group simultaneously. + +--*/ + +#include "ast/ast_pp.h" +#include "smt/theory_jobscheduler.h" +#include "smt/smt_context.h" +#include "smt/smt_arith_value.h" +#include "smt/smt_model_generator.h" + +namespace smt { + + theory_var theory_jobscheduler::mk_var(enode * n) { + theory_var v = theory::mk_var(n); + return v; + } + + bool theory_jobscheduler::internalize_term(app * term) { + context & ctx = get_context(); + if (ctx.e_internalized(term)) + return true; + for (expr* arg : *term) { + if (!ctx.e_internalized(arg)) + ctx.internalize(arg, false); + } + enode* e = ctx.mk_enode(term, false, false, true); + theory_var v = mk_var(e); + ctx.attach_th_var(e, this, v); + ctx.mark_as_relevant(e); + return true; + } + + bool theory_jobscheduler::internalize_atom(app * atom, bool gate_ctx) { + TRACE("csp", tout << mk_pp(atom, m) << "\n";); + context & ctx = get_context(); + SASSERT(u.is_model(atom)); + for (expr* arg : *atom) { + if (!ctx.e_internalized(arg)) ctx.internalize(arg, false); + internalize_cmd(arg); + } + add_done(); + bool_var bv = ctx.mk_bool_var(atom); + ctx.set_var_theory(bv, get_id()); + return true; + } + + struct symbol_cmp { + bool operator()(symbol const& s1, symbol const& s2) const { + return lt(s1, s2); + } + }; + + // TBD: stronger parameter validation + void theory_jobscheduler::internalize_cmd(expr* cmd) { + symbol key, val; + rational r; + expr* job, *resource; + unsigned j = 0, res = 0, cap = 0, loadpct = 100, level = 0; + time_t start = 0, end = std::numeric_limits::max(), capacity = 0; + js_job_goal goal; + js_optimization_objective obj; + properties ps; + if (u.is_set_preemptable(cmd, job) && u.is_job(job, j)) { + set_preemptable(j, true); + } + else if (u.is_add_resource_available(cmd, resource, loadpct, cap, start, end, ps) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); + (void) cap; // TBD + add_resource_available(res, loadpct, start, end, ps); + } + else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end, ps) && u.is_job(job, j) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); + add_job_resource(j, res, loadpct, capacity, end, ps); + } + else if (u.is_job_goal(cmd, goal, level, job) && u.is_job(job, j)) { + // skip + } + else if (u.is_objective(cmd, obj)) { + // skip + } + else { + invalid_argument("command not recognized ", cmd); + } + } + + void theory_jobscheduler::invalid_argument(char const* msg, expr* arg) { + std::ostringstream strm; + strm << msg << mk_pp(arg, m); + throw default_exception(strm.str()); + } + + void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) { + enode* e1 = get_enode(v1); + enode* e2 = get_enode(v2); + enode* root = e1->get_root(); + unsigned r; + if (u.is_resource(root->get_owner(), r)) { + enode* next = e1; + do { + unsigned j; + if (u.is_job2resource(next->get_owner(), j) && !m_jobs[j].m_is_bound) { + m_bound_jobs.push_back(j); + m_jobs[j].m_is_bound = true; + } + next = next->get_next(); + } + while (e1 != next); + } + } + + + void theory_jobscheduler::new_diseq_eh(theory_var v1, theory_var v2) { + + } + + void theory_jobscheduler::push_scope_eh() { + scope s; + s.m_bound_jobs_lim = m_bound_jobs.size(); + s.m_bound_qhead = m_bound_qhead; + m_scopes.push_back(s); + } + + void theory_jobscheduler::pop_scope_eh(unsigned num_scopes) { + unsigned new_lvl = m_scopes.size() - num_scopes; + scope const& s = m_scopes[new_lvl]; + for (unsigned i = s.m_bound_jobs_lim; i < m_bound_jobs.size(); ++i) { + unsigned j = m_bound_jobs[i]; + m_jobs[j].m_is_bound = false; + } + m_bound_jobs.shrink(s.m_bound_jobs_lim); + m_bound_qhead = s.m_bound_qhead; + m_scopes.shrink(new_lvl); + } + + final_check_status theory_jobscheduler::final_check_eh() { + TRACE("csp", tout << "\n";); + bool blocked = false; + for (unsigned j = 0; j < m_jobs.size(); ++j) { + if (split_job2resource(j)) { + return FC_CONTINUE; + } + } + for (unsigned r = 0; r < m_resources.size(); ++r) { + if (constrain_resource_energy(r)) { + blocked = true; + } + } + for (unsigned j = 0; j < m_jobs.size(); ++j) { + if (constrain_end_time_interval(j, resource(j))) { + blocked = true; + } + } + + if (blocked) return FC_CONTINUE; + return FC_DONE; + } + + bool theory_jobscheduler::can_propagate() { + return m_bound_qhead < m_bound_jobs.size(); + } + + literal theory_jobscheduler::mk_literal(expr * e) { + expr_ref _e(e, m); + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + ctx.mark_as_relevant(ctx.get_enode(e)); + return ctx.get_literal(e); + } + + literal theory_jobscheduler::mk_ge(expr* e, time_t t) { + return mk_literal(mk_ge_expr(e, t)); + } + + expr* theory_jobscheduler::mk_ge_expr(expr* e, time_t t) { + return a.mk_ge(e, a.mk_int(rational(t, rational::ui64()))); + } + + literal theory_jobscheduler::mk_ge(enode* e, time_t t) { + return mk_ge(e->get_owner(), t); + } + + literal theory_jobscheduler::mk_le(expr* e, time_t t) { + return mk_literal(mk_le_expr(e, t)); + } + + expr* theory_jobscheduler::mk_le_expr(expr* e, time_t t) { + return a.mk_le(e, a.mk_int(rational(t, rational::ui64()))); + } + + literal theory_jobscheduler::mk_le(enode* l, enode* r) { + context& ctx = get_context(); + expr_ref le(a.mk_le(l->get_owner(), r->get_owner()), m); + ctx.get_rewriter()(le); + return mk_literal(le); + } + + literal theory_jobscheduler::mk_le(enode* e, time_t t) { + return mk_le(e->get_owner(), t); + } + + literal theory_jobscheduler::mk_eq_lit(expr * l, expr * r) { + literal lit = mk_eq(l, r, false); + get_context().mark_as_relevant(lit); + return lit; + } + + + /** + * iterator of job overlaps. + */ + theory_jobscheduler::job_overlap::job_overlap(vector& starts, vector& ends): + m_start(0), m_starts(starts), m_ends(ends), s_idx(0), e_idx(0) { + job_time::compare cmp; + std::sort(starts.begin(), starts.end(), cmp); + std::sort(ends.begin(), ends.end(), cmp); + } + + bool theory_jobscheduler::job_overlap::next() { + if (s_idx == m_starts.size()) { + return false; + } + do { + m_start = std::max(m_start, m_starts[s_idx].m_time); + + // add jobs that start before or at m_start + while (s_idx < m_starts.size() && m_starts[s_idx].m_time <= m_start) { + m_jobs.insert(m_starts[s_idx].m_job); + ++s_idx; + } + // remove jobs that end before m_start. + while (e_idx < m_ends.size() && m_ends[e_idx].m_time < m_start) { + m_jobs.remove(m_ends[e_idx].m_job); + ++e_idx; + } + } + // as long as set of jobs increments, add to m_start + while (s_idx < m_starts.size() && e_idx < m_ends.size() && + m_starts[s_idx].m_time <= m_ends[e_idx].m_time); + + return true; + } + + + /** + * r = resource(j) & start(j) >= slb => end(j) >= ect(j, r, slb) + * + * note: not used so far + * note: subsumed by constrain_end_time_interval used in final-check + */ + void theory_jobscheduler::propagate_end_time(unsigned j, unsigned r) { + time_t slb = est(j); + time_t clb = ect(j, r, slb); + context& ctx = get_context(); + + if (clb > end(j)) { + job_info const& ji = m_jobs[j]; + literal start_ge_lo = mk_ge(ji.m_start, slb); + if (ctx.get_assignment(start_ge_lo) != l_true) { + return; + } + enode_pair eq(ji.m_job2resource, m_resources[r].m_resource); + if (eq.first->get_root() != eq.second->get_root()) { + return; + } + + literal end_ge_lo = mk_ge(ji.m_end, clb); + // Initialization ensures that satisfiable states have completion time below end. + VERIFY(clb <= get_job_resource(j, r).m_end); + region& r = ctx.get_region(); + ctx.assign(end_ge_lo, + ctx.mk_justification( + ext_theory_propagation_justification(get_id(), r, 1, &start_ge_lo, 1, &eq, end_ge_lo, 0, nullptr))); + } + } + + /** + * For time interval [t0, t1] the end-time can be computed as a function + * of start time based on reource load availability. + * + * r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0 + */ + bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) { + unsigned idx1 = 0, idx2 = 0; + time_t s = start(j); + job_resource const& jr = get_job_resource(j, r); + TRACE("csp", tout << "job: " << j << " resource: " << r << " start: " << s << "\n";); + vector& available = m_resources[r].m_available; + if (!resource_available(r, s, idx1)) return false; + if (!resource_available(jr, available[idx1])) return false; + time_t e = ect(j, r, s); + TRACE("csp", tout << "job: " << j << " resource: " << r << " ect: " << e << "\n";); + if (!resource_available(r, e, idx2)) return false; // infeasible.. + if (!resource_available(jr, available[idx2])) return false; + time_t start1 = available[idx1].m_start; + time_t end1 = available[idx1].m_end; + unsigned cap1 = available[idx1].m_loadpct; + time_t start2 = available[idx2].m_start; + time_t end2 = available[idx2].m_end; + unsigned cap2 = available[idx2].m_loadpct; + // calculate minimal start1 <= t0 <= s, such that ect(j, r, t0) >= start2 + // calculate maximal s <= t1 <= end1, such that ect(j, r, t1) <= end2 + time_t delta1 = (s - start1)*cap1; + time_t delta2 = (e - start2)*cap2; + time_t t0, t1; + if (delta1 <= delta2) { + t0 = start1; + } + else { + // solve for t0: + // (s - t0)*cap1 = (e - start2)*cap2; + t0 = s - (delta2 / cap1); + } + delta1 = (end1 - s)*cap1; + delta2 = (end2 - e)*cap2; + if (delta1 <= delta2) { + t1 = end1; + } + else { + // solve for t1: + // (t1 - s)*cap1 = (end2 - e)*cap2 + t1 = s + (delta2 / cap1); + } + + time_t delta = ect(j, r, t0) - t0; + if (end(j) == start(j) + delta) { + return false; + } + TRACE("csp", tout << "job: " << j << " resource " << r << " t0: " << t0 << " t1: " << t1 << " delta: " << delta << "\n";); + literal_vector lits; + enode* start_e = m_jobs[j].m_start; + enode* end_e = m_jobs[j].m_end; + lits.push_back(~mk_eq_lit(m_jobs[j].m_job2resource, m_resources[r].m_resource)); + lits.push_back(~mk_ge(start_e, t0)); + lits.push_back(~mk_le(start_e, t1)); + expr_ref rhs(a.mk_add(start_e->get_owner(), a.mk_int(rational(delta, rational::ui64()))), m); + lits.push_back(mk_eq_lit(end_e->get_owner(), rhs)); + context& ctx = get_context(); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + return true; + } + + + /** + * Ensure that job overlaps don't exceed available energy + */ + bool theory_jobscheduler::constrain_resource_energy(unsigned r) { + bool blocked = false; + vector starts, ends; + res_info const& ri = m_resources[r]; + for (unsigned j : ri.m_jobs) { + if (resource(j) == r) { + starts.push_back(job_time(j, start(j))); + ends.push_back(job_time(j, end(j))); + } + } + job_overlap overlap(starts, ends); + while (overlap.next()) { + unsigned cap = 0; + auto const& jobs = overlap.jobs(); + for (auto j : jobs) { + cap += get_job_resource(j, r).m_loadpct; + if (cap > 100) { + block_job_overlap(r, jobs, j); + blocked = true; + goto try_next_overlap; + } + } + try_next_overlap: + ; + } + return blocked; + } + + void theory_jobscheduler::block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job) { + // + // block the following case: + // each job is assigned to r. + // max { start(j) | j0..last_job } <= min { end(j) | j0..last_job } + // joint capacity of jobs exceeds availability of resource. + // + time_t max_start = 0; + unsigned max_j = last_job; + for (auto j : jobs) { + if (max_start < start(j)) { + max_start = start(j); + max_j = j; + } + if (j == last_job) break; + } + literal_vector lits; + for (auto j : jobs) { + // create literals for: + // resource(j) == r + // m_jobs[j].m_start <= m_jobs[max_j].m_start; + // m_jobs[max_j].m_start <= m_jobs[j].m_end; + lits.push_back(~mk_eq_lit(m_jobs[j].m_job2resource, m_resources[r].m_resource)); + if (j != max_j) { + lits.push_back(~mk_le(m_jobs[j].m_start, m_jobs[max_j].m_start)); + lits.push_back(~mk_le(m_jobs[max_j].m_start, m_jobs[j].m_end)); + } + if (j == last_job) break; + } + context& ctx = get_context(); + ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + } + + void theory_jobscheduler::propagate() { + while (m_bound_qhead < m_bound_jobs.size()) { + unsigned j = m_bound_jobs[m_bound_qhead++]; + unsigned r = 0; + job_info const& ji = m_jobs[j]; + VERIFY(u.is_resource(ji.m_job2resource->get_root()->get_owner(), r)); + TRACE("csp", tout << "job: " << j << " resource: " << r << "\n";); + propagate_job2resource(j, r); + } + } + + void theory_jobscheduler::propagate_job2resource(unsigned j, unsigned r) { + job_info const& ji = m_jobs[j]; + res_info const& ri = m_resources[r]; + job_resource const& jr = get_job_resource(j, r); + literal eq = mk_eq_lit(ji.m_job2resource, ri.m_resource); + assert_last_end_time(j, r, jr, eq); + assert_last_start_time(j, r, eq); + assert_first_start_time(j, r, eq); + vector const& available = ri.m_available; + // TBD: needs to take properties into account + + unsigned i = 0; + if (!first_available(jr, ri, i)) return; + while (true) { + unsigned next = i + 1; + if (!first_available(jr, ri, next)) return; + SASSERT(available[i].m_end < available[next].m_start); + assert_job_not_in_gap(j, r, i, next, eq); + if (!ji.m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) { + assert_job_non_preemptable(j, r, i, next, eq); + } + i = next; + } + } + + theory_jobscheduler::theory_jobscheduler(ast_manager& m): + theory(m.get_family_id("csp")), + m(m), + u(m), + a(m), + m_bound_qhead(0) { + } + + std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { + return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end; + for (auto const& s : jr.m_properties) out << " " << s; out << "\n"; + } + + std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const { + for (job_resource const& jr : j.m_resources) { + display(out << " ", jr) << "\n"; + } + return out; + } + + std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const { + return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%"; + for (auto const& s : r.m_properties) out << " " << s; out << "\n"; + } + + std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const { + for (res_available const& ra : r.m_available) { + display(out << " ", ra); + } + return out; + } + + void theory_jobscheduler::display(std::ostream & out) const { + out << "jobscheduler:\n"; + for (unsigned j = 0; j < m_jobs.size(); ++j) { + display(out << "job " << j << ":\n", m_jobs[j]) << "\n"; + } + for (unsigned r = 0; r < m_resources.size(); ++r) { + display(out << "resource " << r << ":\n", m_resources[r]) << "\n"; + } + } + + void theory_jobscheduler::collect_statistics(::statistics & st) const { + + } + + bool theory_jobscheduler::include_func_interp(func_decl* f) { + return + f->get_decl_kind() == OP_JS_START || + f->get_decl_kind() == OP_JS_END || + f->get_decl_kind() == OP_JS_JOB2RESOURCE; + } + + void theory_jobscheduler::init_model(model_generator & m) { + + } + + model_value_proc * theory_jobscheduler::mk_value(enode * n, model_generator & mg) { + return alloc(expr_wrapper_proc, n->get_root()->get_owner()); + } + + bool theory_jobscheduler::get_value(enode * n, expr_ref & r) { + std::cout << mk_pp(n->get_owner(), m) << "\n"; + return false; + } + + theory * theory_jobscheduler::mk_fresh(context * new_ctx) { + return alloc(theory_jobscheduler, new_ctx->get_manager()); + } + + time_t theory_jobscheduler::get_lo(expr* e) { + arith_value av(get_context()); + rational val; + bool is_strict; + if (av.get_lo(e, val, is_strict) && !is_strict && val.is_uint64()) { + return val.get_uint64(); + } + return 0; + } + + time_t theory_jobscheduler::get_up(expr* e) { + arith_value av(get_context()); + rational val; + bool is_strict; + if (av.get_up(e, val, is_strict) && !is_strict && val.is_uint64()) { + return val.get_uint64(); + } + return std::numeric_limits::max(); + } + + time_t theory_jobscheduler::get_value(expr* e) { + arith_value av(get_context()); + rational val; + if (av.get_value(e, val) && val.is_uint64()) { + return val.get_uint64(); + } + return 0; + } + + time_t theory_jobscheduler::est(unsigned j) { + return get_lo(m_jobs[j].m_start->get_owner()); + } + + time_t theory_jobscheduler::lst(unsigned j) { + return get_up(m_jobs[j].m_start->get_owner()); + } + + time_t theory_jobscheduler::ect(unsigned j) { + return get_lo(m_jobs[j].m_end->get_owner()); + } + + time_t theory_jobscheduler::lct(unsigned j) { + return get_up(m_jobs[j].m_end->get_owner()); + } + + time_t theory_jobscheduler::start(unsigned j) { + return get_value(m_jobs[j].m_start->get_owner()); + } + + time_t theory_jobscheduler::end(unsigned j) { + return get_value(m_jobs[j].m_end->get_owner()); + } + + unsigned theory_jobscheduler::resource(unsigned j) { + unsigned r; + enode* next = m_jobs[j].m_job2resource, *n = next; + do { + if (u.is_resource(next->get_owner(), r)) { + return r; + } + next = next->get_next(); + } + while (next != n); + return 0; + } + + void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) { + m_jobs.reserve(j + 1); + m_jobs[j].m_is_preemptable = is_preemptable; + } + + void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned loadpct, uint64_t cap, time_t end, properties const& ps) { + SASSERT(get_context().at_base_level()); + SASSERT(0 <= loadpct && loadpct <= 100); + SASSERT(0 <= cap); + m_jobs.reserve(j + 1); + m_resources.reserve(r + 1); + job_info& ji = m_jobs[j]; + if (ji.m_resource2index.contains(r)) { + throw default_exception("resource already bound to job"); + } + if (!ji.m_start) { + context& ctx = get_context(); + app_ref job(u.mk_job(j), m); + app_ref start(u.mk_start(j), m); + app_ref end(u.mk_end(j), m); + app_ref res(u.mk_job2resource(j), m); + if (!ctx.e_internalized(job)) ctx.internalize(job, false); + if (!ctx.e_internalized(start)) ctx.internalize(start, false); + if (!ctx.e_internalized(end)) ctx.internalize(end, false); + if (!ctx.e_internalized(res)) ctx.internalize(res, false); + ji.m_job = ctx.get_enode(job); + ji.m_start = ctx.get_enode(start); + ji.m_end = ctx.get_enode(end); + ji.m_job2resource = ctx.get_enode(res); + } + ji.m_resource2index.insert(r, ji.m_resources.size()); + ji.m_resources.push_back(job_resource(r, cap, loadpct, end, ps)); + SASSERT(!m_resources[r].m_jobs.contains(j)); + m_resources[r].m_jobs.push_back(j); + } + + + void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps) { + SASSERT(get_context().at_base_level()); + SASSERT(1 <= max_loadpct && max_loadpct <= 100); + SASSERT(start <= end); + m_resources.reserve(r + 1); + res_info& ri = m_resources[r]; + if (!ri.m_resource) { + context& ctx = get_context(); + app_ref res(u.mk_resource(r), m); + if (!ctx.e_internalized(res)) ctx.internalize(res, false); + ri.m_resource = ctx.get_enode(res); + app_ref ms(u.mk_makespan(r), m); + if (!ctx.e_internalized(ms)) ctx.internalize(ms, false); + ri.m_makespan = ctx.get_enode(ms); + } + ri.m_available.push_back(res_available(max_loadpct, start, end, ps)); + } + + /* + * Initialze the state based on the set of jobs and resources added. + * Ensure that the availability slots for each resource is sorted by time. + * + * For each resource j: + * est(j) <= start(j) <= end(j) <= lct(j) + * + * possible strengthenings: + * - start(j) <= lst(j) + * - start(j) + min_completion_time(j) <= end(j) + * - start(j) + max_completion_time(j) >= end(j) + * + * makespan constraints? + * + */ + void theory_jobscheduler::add_done() { + TRACE("csp", tout << "add-done begin\n";); + context & ctx = get_context(); + + // sort availability intervals + for (res_info& ri : m_resources) { + vector& available = ri.m_available; + res_available::compare cmp; + std::sort(available.begin(), available.end(), cmp); + } + + literal lit; + unsigned job_id = 0; + + for (job_info const& ji : m_jobs) { + if (ji.m_resources.empty()) { + throw default_exception("every job should be associated with at least one resource"); + } + + // start(j) <= end(j) + lit = mk_le(ji.m_start, ji.m_end); + ctx.mk_th_axiom(get_id(), 1, &lit); + + time_t start_lb = std::numeric_limits::max(); + time_t runtime_lb = std::numeric_limits::max(); + time_t end_ub = 0, runtime_ub = 0; + for (job_resource const& jr : ji.m_resources) { + unsigned r = jr.m_resource_id; + res_info const& ri = m_resources[r]; + if (ri.m_available.empty()) continue; + unsigned idx = 0; + if (first_available(jr, ri, idx)) { + start_lb = std::min(start_lb, ri.m_available[idx].m_start); + } + idx = ri.m_available.size(); + if (last_available(jr, ri, idx)) { + end_ub = std::max(end_ub, ri.m_available[idx].m_end); + } + runtime_lb = std::min(runtime_lb, jr.m_capacity); + // TBD: more accurate estimates for runtime_lb based on gaps + // TBD: correct estimate of runtime_ub taking gaps into account. + } + CTRACE("csp", (start_lb > end_ub), tout << "there is no associated resource working time\n";); + if (start_lb > end_ub) { + warning_msg("Job %d has no associated resource working time", job_id); + } + + // start(j) >= start_lb + lit = mk_ge(ji.m_start, start_lb); + ctx.mk_th_axiom(get_id(), 1, &lit); + + // end(j) <= end_ub + lit = mk_le(ji.m_end, end_ub); + ctx.mk_th_axiom(get_id(), 1, &lit); + + // start(j) + runtime_lb <= end(j) + // end(j) <= start(j) + runtime_ub + + ++job_id; + } + + TRACE("csp", tout << "add-done end\n";); + } + + // resource(j) = r => end(j) <= end(j, r) + void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) { + job_info const& ji = m_jobs[j]; + literal l2 = mk_le(ji.m_end, jr.m_end); + get_context().mk_th_axiom(get_id(), ~eq, l2); + } + + // resource(j) = r => start(j) <= lst(j, r, end(j, r)) + void theory_jobscheduler::assert_last_start_time(unsigned j, unsigned r, literal eq) { + context& ctx = get_context(); + time_t t; + if (lst(j, r, t)) { + ctx.mk_th_axiom(get_id(), ~eq, mk_le(m_jobs[j].m_start, t)); + } + else { + eq.neg(); + ctx.mk_th_axiom(get_id(), 1, &eq); + } + } + + // resource(j) = r => start(j) >= available[0].m_start + void theory_jobscheduler::assert_first_start_time(unsigned j, unsigned r, literal eq) { + job_resource const& jr = get_job_resource(j, r); + unsigned idx = 0; + if (!first_available(jr, m_resources[r], idx)) return; + vector& available = m_resources[r].m_available; + literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start); + get_context().mk_th_axiom(get_id(), ~eq, l2); + } + + // resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j); + void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { + job_resource const& jr = get_job_resource(j, r); + vector& available = m_resources[r].m_available; + SASSERT(resource_available(jr, available[idx])); + literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); + literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end); + get_context().mk_th_axiom(get_id(), ~eq, l2, l3); + } + + // resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j); + void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { + vector& available = m_resources[r].m_available; + job_resource const& jr = get_job_resource(j, r); + SASSERT(resource_available(jr, available[idx])); + literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end); + literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); + get_context().mk_th_axiom(get_id(), ~eq, l2, l3); + } + + /** + * bind a job to one of the resources it can run on. + */ + bool theory_jobscheduler::split_job2resource(unsigned j) { + job_info const& ji = m_jobs[j]; + context& ctx = get_context(); + if (ji.m_is_bound) return false; + auto const& jrs = ji.m_resources; + for (job_resource const& jr : jrs) { + unsigned r = jr.m_resource_id; + res_info const& ri = m_resources[r]; + enode* e1 = ji.m_job2resource; + enode* e2 = ri.m_resource; + if (ctx.is_diseq(e1, e2)) + continue; + literal eq = mk_eq_lit(e1, e2); + if (ctx.get_assignment(eq) != l_false) { + ctx.mark_as_relevant(eq); + if (assume_eq(e1, e2)) { + return true; + } + } + } + literal_vector lits; + for (job_resource const& jr : jrs) { + unsigned r = jr.m_resource_id; + res_info const& ri = m_resources[r]; + enode* e1 = ji.m_job2resource; + enode* e2 = ri.m_resource; + lits.push_back(mk_eq_lit(e1, e2)); + } + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + return true; + } + + /** + * check that each job is run on some resource according to + * requested capacity. + * + * Check that the sum of jobs run in each time instance + * does not exceed capacity. + */ + void theory_jobscheduler::validate_assignment() { + vector> start_times, end_times; + start_times.reserve(m_resources.size()); + end_times.reserve(m_resources.size()); + for (unsigned j = 0; j < m_jobs.size(); ++j) { + unsigned r = resource(j); + start_times[r].push_back(job_time(j, start(j))); + end_times[r].push_back(job_time(j, end(j))); + if (ect(j, r, start(j)) > end(j)) { + throw default_exception("job not assigned full capacity"); + } + unsigned idx; + if (!resource_available(r, start(j), idx)) { + throw default_exception("resource is not available at job start time"); + } + } + for (unsigned r = 0; r < m_resources.size(); ++r) { + // order jobs running on r by start, end-time intervals + // then consume ordered list to find jobs in scope. + job_overlap overlap(start_times[r], end_times[r]); + while (overlap.next()) { + // check that sum of job loads does not exceed 100% + unsigned cap = 0; + for (auto j : overlap.jobs()) { + cap += get_job_resource(j, r).m_loadpct; + } + if (cap > 100) { + throw default_exception("capacity on resource exceeded"); + } + } + } + } + + theory_jobscheduler::job_resource const& theory_jobscheduler::get_job_resource(unsigned j, unsigned r) const { + job_info const& ji = m_jobs[j]; + return ji.m_resources[ji.m_resource2index[r]]; + } + + /** + * find idx, if any, such that t is within the time interval of available[idx] + */ + bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& idx) { + vector& available = m_resources[r].m_available; + unsigned lo = 0, hi = available.size(), mid = hi / 2; + while (lo < hi) { + SASSERT(lo <= mid && mid < hi); + res_available const& ra = available[mid]; + if (ra.m_start <= t && t <= ra.m_end) { + idx = mid; + return true; + } + else if (ra.m_start > t && mid > 0) { + hi = mid; + mid = lo + (mid - lo) / 2; + } + else if (ra.m_end < t) { + lo = mid + 1; + mid += (hi - mid) / 2; + } + else { + break; + } + } + return false; + } + + /** + * compute earliest completion time for job j on resource r starting at time start. + */ + time_t theory_jobscheduler::ect(unsigned j, unsigned r, time_t start) { + job_resource const& jr = get_job_resource(j, r); + vector& available = m_resources[r].m_available; + + unsigned j_load_pct = jr.m_loadpct; + time_t cap = jr.m_capacity; + unsigned idx = 0; + if (!resource_available(r, start, idx)) { + TRACE("csp", tout << "resource is not available for " << j << " " << r << "\n";); + return std::numeric_limits::max(); + } + SASSERT(cap > 0); + + for (; idx < available.size(); ++idx) { + if (!resource_available(jr, available[idx])) continue; + start = std::max(start, available[idx].m_start); + time_t end = available[idx].m_end; + unsigned load_pct = available[idx].m_loadpct; + time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end); + TRACE("csp", tout << "delta: " << delta << " capacity: " << cap << " load " + << load_pct << " jload: " << j_load_pct << " start: " << start << " end " << end << "\n";); + if (delta > cap) { + end = solve_for_end(load_pct, j_load_pct, start, cap); + cap = 0; + } + else { + cap -= delta; + } + if (cap == 0) { + return end; + } + } + return std::numeric_limits::max(); + } + + /** + * find end, such that cap = (load / job_load_pct) * (end - start + 1) + */ + time_t theory_jobscheduler::solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap) { + SASSERT(load_pct > 0); + SASSERT(job_load_pct > 0); + // cap = (load / job_load_pct) * (end - start + 1) + // <=> + // end - start + 1 = (cap * job_load_pct) / load + // <=> + // end = start - 1 + (cap * job_load_pct) / load + // <=> + // end = (load * (start - 1) + cap * job_load_pct) / load + unsigned load = std::min(load_pct, job_load_pct); + return (load * (start - 1) + cap * job_load_pct) / load; + } + + /** + * find start, such that cap = (load / job_load_pct) * (end - start + 1) + */ + time_t theory_jobscheduler::solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap) { + SASSERT(load_pct > 0); + SASSERT(job_load_pct > 0); + // cap = (load / job_load_pct) * (end - start + 1) + // <=> + // end - start + 1 = (cap * job_load_pct) / load + // <=> + // start = end + 1 - (cap * job_load_pct) / load + // <=> + // start = (load * (end + 1) - cap * job_load_pct) / load + unsigned load = std::min(load_pct, job_load_pct); + return (load * (end + 1) - cap * job_load_pct) / load; + } + + /** + * find cap, such that cap = (load / job_load_pct) * (end - start + 1) + */ + time_t theory_jobscheduler::solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end) { + SASSERT(job_load_pct > 0); + unsigned load = std::min(load_pct, job_load_pct); + return (load * (end - start + 1)) / job_load_pct; + } + + /** + * Compute last start time for job on resource r. + */ + bool theory_jobscheduler::lst(unsigned j, unsigned r, time_t& start) { + start = 0; + job_resource const& jr = get_job_resource(j, r); + vector& available = m_resources[r].m_available; + unsigned j_load_pct = jr.m_loadpct; + time_t cap = jr.m_capacity; + for (unsigned idx = available.size(); idx-- > 0; ) { + if (!resource_available(jr, available[idx])) continue; + start = available[idx].m_start; + time_t end = available[idx].m_end; + unsigned load_pct = available[idx].m_loadpct; + time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end); + if (delta > cap) { + start = solve_for_start(load_pct, j_load_pct, end, cap); + cap = 0; + } + else { + cap -= delta; + } + if (cap == 0) { + return true; + } + } + return false; + } + + /** + * \brief check that job properties is a subset of resource properties. + * It assumes that both vectors are sorted. + */ + + bool theory_jobscheduler::resource_available(job_resource const& jr, res_available const& ra) const { + auto const& jps = jr.m_properties; + auto const& rps = ra.m_properties; + if (jps.size() > rps.size()) return false; + unsigned j = 0, i = 0; + for (; i < jps.size() && j < rps.size(); ) { + if (jps[i] == rps[j]) { + ++i; ++j; + } + else if (lt(rps[j], jps[i])) { + ++j; + } + else { + break; + } + } + return i == jps.size(); + } + + /** + * \brief minimal current resource available for job resource, includes idx. + */ + bool theory_jobscheduler::first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + for (; idx < ri.m_available.size(); ++idx) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + + /** + * \brief maximal previous resource available for job resource, excludes idx. + */ + bool theory_jobscheduler::last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + while (idx-- > 0) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + + +}; + diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h new file mode 100644 index 000000000..59c3b975d --- /dev/null +++ b/src/smt/theory_jobscheduler.h @@ -0,0 +1,244 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_jobscheduling.h + +Abstract: + + Propagation solver for jobscheduling problems. + It relies on an external module to tighten bounds of + job variables. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-09-08. + +Revision History: + +--*/ +#pragma once; + +#include "util/uint_set.h" +#include "ast/csp_decl_plugin.h" +#include "ast/arith_decl_plugin.h" +#include "smt/smt_theory.h" + +namespace smt { + + typedef uint64_t time_t; + + class theory_jobscheduler : public theory { + public: + typedef svector properties; + protected: + + struct job_resource { + unsigned m_resource_id; // id of resource + time_t m_capacity; // amount of resource to use + unsigned m_loadpct; // assuming loadpct + time_t m_end; // must run before + properties m_properties; + job_resource(unsigned r, time_t cap, unsigned loadpct, time_t end, properties const& ps): + m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end), m_properties(ps) {} + }; + + struct job_time { + unsigned m_job; + time_t m_time; + job_time(unsigned j, time_t time): m_job(j), m_time(time) {} + + struct compare { + bool operator()(job_time const& jt1, job_time const& jt2) const { + return jt1.m_time < jt2.m_time; + } + }; + }; + + struct job_info { + bool m_is_preemptable; // can job be pre-empted + vector m_resources; // resources allowed to run job. + u_map m_resource2index; // resource to index into vector + enode* m_job; + enode* m_start; + enode* m_end; + enode* m_job2resource; + bool m_is_bound; + job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr), m_is_bound(false) {} + }; + + struct res_available { + unsigned m_loadpct; + time_t m_start; + time_t m_end; + properties m_properties; + res_available(unsigned load_pct, time_t start, time_t end, properties const& ps): + m_loadpct(load_pct), + m_start(start), + m_end(end), + m_properties(ps) + {} + struct compare { + bool operator()(res_available const& ra1, res_available const& ra2) const { + return ra1.m_start < ra2.m_start; + } + }; + }; + + struct res_info { + unsigned_vector m_jobs; // jobs allocated to run on resource + vector m_available; // time intervals where resource is available + time_t m_end; // can't run after + enode* m_resource; + enode* m_makespan; + res_info(): m_end(std::numeric_limits::max()), m_resource(nullptr), m_makespan(nullptr) {} + }; + + ast_manager& m; + csp_util u; + arith_util a; + vector m_jobs; + vector m_resources; + unsigned_vector m_bound_jobs; + unsigned m_bound_qhead; + struct scope { + unsigned m_bound_jobs_lim; + unsigned m_bound_qhead; + }; + svector m_scopes; + + protected: + + theory_var mk_var(enode * n) override; + + bool internalize_atom(app * atom, bool gate_ctx) override; + + bool internalize_term(app * term) override; + + void assign_eh(bool_var v, bool is_true) override {} + + void new_eq_eh(theory_var v1, theory_var v2) override; + + void new_diseq_eh(theory_var v1, theory_var v2) override; + + void push_scope_eh() override; + + void pop_scope_eh(unsigned num_scopes) override; + + final_check_status final_check_eh() override; + + bool can_propagate() override; + + void propagate() override; + + public: + + theory_jobscheduler(ast_manager& m); + + ~theory_jobscheduler() override {} + + void display(std::ostream & out) const override; + + void collect_statistics(::statistics & st) const override; + + bool include_func_interp(func_decl* f) override; + + void init_model(model_generator & m) override; + + model_value_proc * mk_value(enode * n, model_generator & mg) override; + + bool get_value(enode * n, expr_ref & r) override; + + theory * mk_fresh(context * new_ctx) override; + + public: + // set up job/resource global constraints + void set_preemptable(unsigned j, bool is_preemptable); + void add_job_resource(unsigned j, unsigned r, unsigned loadpct, time_t cap, time_t end, properties const& ps); + void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps); + void add_done(); + + // assignments + time_t est(unsigned j); // earliest start time of job j + time_t lst(unsigned j); // last start time + time_t ect(unsigned j); // earliest completion time + time_t lct(unsigned j); // last completion time + time_t start(unsigned j); // start time of job j + time_t end(unsigned j); // end time of job j + time_t get_lo(expr* e); + time_t get_up(expr* e); + time_t get_value(expr* e); + unsigned resource(unsigned j); // resource of job j + + // derived bounds + time_t ect(unsigned j, unsigned r, time_t start); + bool lst(unsigned j, unsigned r, time_t& t); + + bool resource_available(job_resource const& jr, res_available const& ra) const; + bool first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + bool last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + + time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap); + time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap); + time_t solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end); + + // validate assignment + void validate_assignment(); + bool resource_available(unsigned r, time_t t, unsigned& idx); // load available on resource r at time t. + time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end); // capacity used between start and end + + job_resource const& get_job_resource(unsigned j, unsigned r) const; + + // propagation + void propagate_end_time(unsigned j, unsigned r); + void propagate_job2resource(unsigned j, unsigned r); + + // final check constraints + bool constrain_end_time_interval(unsigned j, unsigned r); + bool constrain_resource_energy(unsigned r); + bool split_job2resource(unsigned j); + + void assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq); + void assert_last_start_time(unsigned j, unsigned r, literal eq); + void assert_first_start_time(unsigned j, unsigned r, literal eq); + void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); + void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); + + void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job); + + class job_overlap { + time_t m_start; + vector & m_starts, &m_ends; + unsigned s_idx, e_idx; // index into starts/ends + uint_set m_jobs; + public: + job_overlap(vector& starts, vector& ends); + bool next(); + uint_set const& jobs() const { return m_jobs; } + }; + + // term builders + literal mk_ge(expr* e, time_t t); + expr* mk_ge_expr(expr* e, time_t t); + literal mk_ge(enode* e, time_t t); + literal mk_le(expr* e, time_t t); + expr* mk_le_expr(expr* e, time_t t); + literal mk_le(enode* e, time_t t); + literal mk_le(enode* l, enode* r); + literal mk_literal(expr* e); + literal mk_eq_lit(enode * l, enode * r) { return mk_eq_lit(l->get_owner(), r->get_owner()); } + literal mk_eq_lit(expr * l, expr * r); + + void internalize_cmd(expr* cmd); + void unrecognized_argument(expr* arg) { invalid_argument("unrecognized argument ", arg); } + void invalid_argument(char const* msg, expr* arg); + + std::ostream& display(std::ostream & out, res_info const& r) const; + std::ostream& display(std::ostream & out, res_available const& r) const; + std::ostream& display(std::ostream & out, job_info const& r) const; + std::ostream& display(std::ostream & out, job_resource const& r) const; + + }; +}; + diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp new file mode 100644 index 000000000..c3e7c997e --- /dev/null +++ b/src/smt/theory_recfun.cpp @@ -0,0 +1,451 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation, Simon Cuares + +Module Name: + + theory_recfun.cpp + +Abstract: + + Theory responsible for unrolling recursive functions + +Author: + + Simon Cuares December 2017 + +Revision History: + +--*/ + +#include "util/stats.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "smt/theory_recfun.h" +#include "smt/params/smt_params_helper.hpp" + + +#define TRACEFN(x) TRACE("recfun", tout << x << '\n';) + +namespace smt { + + theory_recfun::theory_recfun(ast_manager & m) + : theory(m.mk_family_id("recfun")), + m(m), + m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))), + m_util(m_plugin.u()), + m_preds(m), + m_max_depth(0), + m_q_case_expand(), + m_q_body_expand() + { + } + + theory_recfun::~theory_recfun() { + reset_queues(); + } + + char const * theory_recfun::get_name() const { return "recfun"; } + + theory* theory_recfun::mk_fresh(context* new_ctx) { + return alloc(theory_recfun, new_ctx->get_manager()); + } + + void theory_recfun::init(context* ctx) { + theory::init(ctx); + smt_params_helper p(ctx->get_params()); + m_max_depth = p.recfun_depth(); + if (m_max_depth < 2) m_max_depth = 2; + } + + void theory_recfun::init_search_eh() { + } + + bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) { + TRACEFN(mk_pp(atom, m)); + if (!u().has_defs()) { + return false; + } + for (expr * arg : *atom) { + ctx().internalize(arg, false); + } + if (!ctx().e_internalized(atom)) { + ctx().mk_enode(atom, false, true, false); + } + if (!ctx().b_internalized(atom)) { + bool_var v = ctx().mk_bool_var(atom); + ctx().set_var_theory(v, get_id()); + } + return true; + } + + bool theory_recfun::internalize_term(app * term) { + if (!u().has_defs()) { + return false; + } + for (expr* e : *term) { + ctx().internalize(e, false); + } + // the internalization of the arguments may have triggered the internalization of term. + if (!ctx().e_internalized(term)) { + ctx().mk_enode(term, false, false, true); + } + return true; + } + + void theory_recfun::reset_queues() { + for (auto* e : m_q_case_expand) { + dealloc(e); + } + m_q_case_expand.reset(); + for (auto* e : m_q_body_expand) { + dealloc(e); + } + m_q_body_expand.reset(); + m_q_clauses.clear(); + } + + void theory_recfun::reset_eh() { + reset_queues(); + m_stats.reset(); + theory::reset_eh(); + } + + /* + * when `n` becomes relevant, if it's `f(t1...tn)` with `f` defined, + * then case-expand `n`. If it's a macro we can also immediately + * body-expand it. + */ + void theory_recfun::relevant_eh(app * n) { + SASSERT(ctx().relevancy()); + if (u().is_defined(n) && u().has_defs()) { + TRACEFN("relevant_eh: (defined) " << mk_pp(n, m)); + push_case_expand(alloc(case_expansion, u(), n)); + } + } + + void theory_recfun::push_scope_eh() { + theory::push_scope_eh(); + m_preds_lim.push_back(m_preds.size()); + } + + void theory_recfun::pop_scope_eh(unsigned num_scopes) { + theory::pop_scope_eh(num_scopes); + reset_queues(); + + // restore depth book-keeping + unsigned new_lim = m_preds_lim.size()-num_scopes; +#if 0 + // depth tracking of recursive unfolding is + // turned off when enabling this code: + unsigned start = m_preds_lim[new_lim]; + for (unsigned i = start; i < m_preds.size(); ++i) { + m_pred_depth.remove(m_preds.get(i)); + } + m_preds.resize(start); +#endif + m_preds_lim.shrink(new_lim); + } + + void theory_recfun::restart_eh() { + TRACEFN("restart"); + reset_queues(); + theory::restart_eh(); + } + + bool theory_recfun::can_propagate() { + return ! (m_q_case_expand.empty() && + m_q_body_expand.empty() && + m_q_clauses.empty()); + } + + void theory_recfun::propagate() { + + for (literal_vector & c : m_q_clauses) { + TRACEFN("add axiom " << pp_lits(ctx(), c)); + ctx().mk_th_axiom(get_id(), c); + } + m_q_clauses.clear(); + + for (unsigned i = 0; i < m_q_case_expand.size(); ++i) { + case_expansion* e = m_q_case_expand[i]; + if (e->m_def->is_fun_macro()) { + // body expand immediately + assert_macro_axiom(*e); + } + else { + // case expand + SASSERT(e->m_def->is_fun_defined()); + assert_case_axioms(*e); + } + dealloc(e); + m_q_case_expand[i] = nullptr; + } + m_stats.m_case_expansions += m_q_case_expand.size(); + m_q_case_expand.reset(); + + for (unsigned i = 0; i < m_q_body_expand.size(); ++i) { + assert_body_axiom(*m_q_body_expand[i]); + dealloc(m_q_body_expand[i]); + m_q_body_expand[i] = nullptr; + } + m_stats.m_body_expansions += m_q_body_expand.size(); + m_q_body_expand.reset(); + } + + /** + * make clause `depth_limit => ~guard` + * the guard appears at a depth below the current cutoff. + */ + void theory_recfun::assert_max_depth_limit(expr* guard) { + literal_vector c; + app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth); + c.push_back(~mk_literal(dlimit)); + c.push_back(~mk_literal(guard)); + TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c)); + m_q_clauses.push_back(std::move(c)); + } + + /** + * retrieve depth associated with predicate or expression. + */ + unsigned theory_recfun::get_depth(expr* e) { + SASSERT(u().is_defined(e) || u().is_case_pred(e)); + unsigned d = 0; + m_pred_depth.find(e, d); + TRACEFN("depth " << d << " " << mk_pp(e, m)); + return d; + } + + /** + * Update depth of subterms of e with respect to d. + */ + void theory_recfun::set_depth_rec(unsigned d, expr* e) { + struct insert_c { + theory_recfun& th; + unsigned m_depth; + insert_c(theory_recfun& th, unsigned d): th(th), m_depth(d) {} + void operator()(app* e) { th.set_depth(m_depth, e); } + void operator()(quantifier*) {} + void operator()(var*) {} + }; + insert_c proc(*this, d); + for_each_expr(proc, e); + } + + void theory_recfun::set_depth(unsigned depth, expr* e) { + if ((u().is_defined(e) || u().is_case_pred(e)) && !m_pred_depth.contains(e)) { + m_pred_depth.insert(e, depth); + m_preds.push_back(e); + TRACEFN("depth " << depth << " : " << mk_pp(e, m)); + } + } + + /** + * if `is_true` and `v = C_f_i(t1...tn)`, + * then body-expand i-th case of `f(t1...tn)` + */ + void theory_recfun::assign_eh(bool_var v, bool is_true) { + expr* e = ctx().bool_var2expr(v); + if (is_true && u().is_case_pred(e)) { + TRACEFN("assign_case_pred_true " << mk_pp(e, m)); + // body-expand + push_body_expand(alloc(body_expansion, u(), to_app(e))); + } + } + + // replace `vars` by `args` in `e` + expr_ref theory_recfun::apply_args( + unsigned depth, + recfun::vars const & vars, + ptr_vector const & args, + expr * e) { + SASSERT(is_standard_order(vars)); + var_subst subst(m, true); + expr_ref new_body(m); + new_body = subst(e, args.size(), args.c_ptr()); + ctx().get_rewriter()(new_body); // simplify + set_depth_rec(depth + 1, new_body); + return new_body; + } + + literal theory_recfun::mk_literal(expr* e) { + ctx().internalize(e, false); + literal lit = ctx().get_literal(e); + ctx().mark_as_relevant(lit); + return lit; + } + + literal theory_recfun::mk_eq_lit(expr* l, expr* r) { + literal lit; + if (m.is_true(r) || m.is_false(r)) { + std::swap(l, r); + } + if (m.is_true(l)) { + lit = mk_literal(r); + } + else if (m.is_false(l)) { + lit = ~mk_literal(r); + } + else { + lit = mk_eq(l, r, false); + } + ctx().mark_as_relevant(lit); + return lit; + } + + /** + * For functions f(args) that are given as macros f(vs) = rhs + * + * 1. substitute `e.args` for `vs` into the macro rhs + * 2. add unit clause `f(args) = rhs` + */ + void theory_recfun::assert_macro_axiom(case_expansion & e) { + m_stats.m_macro_expansions++; + TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n"); + SASSERT(e.m_def->is_fun_macro()); + auto & vars = e.m_def->get_vars(); + expr_ref lhs(e.m_lhs, m); + unsigned depth = get_depth(e.m_lhs); + expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); + literal lit = mk_eq_lit(lhs, rhs); + ctx().mk_th_axiom(get_id(), 1, &lit); + TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" << + "literal " << pp_lit(ctx(), lit)); + } + + /** + * Add case axioms for every case expansion path. + * + * assert `p(args) <=> And(guards)` (with CNF on the fly) + * + * also body-expand paths that do not depend on any defined fun + */ + void theory_recfun::assert_case_axioms(case_expansion & e) { + TRACEFN("assert_case_axioms "<< pp_case_expansion(e,m) + << " with " << e.m_def->get_cases().size() << " cases"); + SASSERT(e.m_def->is_fun_defined()); + // add case-axioms for all case-paths + auto & vars = e.m_def->get_vars(); + literal_vector preds; + for (recfun::case_def const & c : e.m_def->get_cases()) { + // applied predicate to `args` + app_ref pred_applied = c.apply_case_predicate(e.m_args); + + // cut off cases below max-depth + unsigned depth = get_depth(e.m_lhs); + set_depth(depth, pred_applied); + SASSERT(u().owns_app(pred_applied)); + literal concl = mk_literal(pred_applied); + preds.push_back(concl); + + if (depth >= m_max_depth) { + assert_max_depth_limit(pred_applied); + continue; + } + + literal_vector guards; + guards.push_back(concl); + for (auto & g : c.get_guards()) { + expr_ref ga = apply_args(depth, vars, e.m_args, g); + literal guard = mk_literal(ga); + guards.push_back(~guard); + literal c[2] = {~concl, guard}; + ctx().mk_th_axiom(get_id(), 2, c); + } + ctx().mk_th_axiom(get_id(), guards); + + if (c.is_immediate()) { + body_expansion be(pred_applied, c, e.m_args); + assert_body_axiom(be); + } + } + // the disjunction of branches is asserted + // to close the available cases. + ctx().mk_th_axiom(get_id(), preds); + } + + /** + * For a guarded definition guards => f(vars) = rhs + * and occurrence f(args) + * + * substitute `args` for `vars` in guards, and rhs + * add axiom guards[args/vars] => f(args) = rhs[args/vars] + * + */ + void theory_recfun::assert_body_axiom(body_expansion & e) { + recfun::def & d = *e.m_cdef->get_def(); + auto & vars = d.get_vars(); + auto & args = e.m_args; + SASSERT(is_standard_order(vars)); + unsigned depth = get_depth(e.m_pred); + expr_ref lhs(u().mk_fun_defined(d, args), m); + expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs()); + + literal_vector clause; + for (auto & g : e.m_cdef->get_guards()) { + expr_ref guard = apply_args(depth, vars, args, g); + clause.push_back(~mk_literal(guard)); + if (clause.back() == true_literal) { + return; + } + if (clause.back() == false_literal) { + clause.pop_back(); + } + } + clause.push_back(mk_eq_lit(lhs, rhs)); + ctx().mk_th_axiom(get_id(), clause); + TRACEFN("body " << pp_body_expansion(e,m)); + TRACEFN(pp_lits(ctx(), clause)); + } + + final_check_status theory_recfun::final_check_eh() { + TRACEFN("final\n"); + if (can_propagate()) { + propagate(); + return FC_CONTINUE; + } + return FC_DONE; + } + + void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { + if (u().has_defs()) { + app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth); + TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m)); + assumptions.push_back(dlimit); + } + } + + // if `dlimit` occurs in unsat core, return 'true' + bool theory_recfun::should_research(expr_ref_vector & unsat_core) { + for (auto & e : unsat_core) { + if (u().is_depth_limit(e)) { + m_max_depth = (3 * m_max_depth) / 2; + IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increase-depth " << m_max_depth << ")\n"); + return true; + } + } + return false; + } + + void theory_recfun::display(std::ostream & out) const { + out << "recfun{}"; + } + + void theory_recfun::collect_statistics(::statistics & st) const { + st.update("recfun macro expansion", m_stats.m_macro_expansions); + st.update("recfun case expansion", m_stats.m_case_expansions); + st.update("recfun body expansion", m_stats.m_body_expansions); + } + + std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) { + return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")"; + } + + std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) { + out << "body_exp(" << e.e.m_cdef->get_decl()->get_name(); + for (auto* t : e.e.m_args) { + out << " " << mk_pp(t,e.m); + } + return out << ")"; + } +} diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h new file mode 100644 index 000000000..46392c6d2 --- /dev/null +++ b/src/smt/theory_recfun.h @@ -0,0 +1,163 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_recfun.h + +Abstract: + + Theory responsible for unrolling recursive functions + +Author: + + Simon Cuares December 2017 + +Revision History: + +--*/ +#ifndef THEORY_RECFUN_H_ +#define THEORY_RECFUN_H_ + +#include "smt/smt_theory.h" +#include "smt/smt_context.h" +#include "ast/ast_pp.h" +#include "ast/recfun_decl_plugin.h" + +namespace smt { + + class theory_recfun : public theory { + struct stats { + unsigned m_case_expansions, m_body_expansions, m_macro_expansions; + void reset() { memset(this, 0, sizeof(stats)); } + stats() { reset(); } + }; + + // one case-expansion of `f(t1...tn)` + struct case_expansion { + app * m_lhs; // the term to expand + recfun::def * m_def; + ptr_vector m_args; + case_expansion(recfun::util& u, app * n) : + m_lhs(n), m_def(nullptr), m_args() { + SASSERT(u.is_defined(n)); + func_decl * d = n->get_decl(); + m_def = &u.get_def(d); + m_args.append(n->get_num_args(), n->get_args()); + } + case_expansion(case_expansion const & from) + : m_lhs(from.m_lhs), + m_def(from.m_def), + m_args(from.m_args) {} + case_expansion(case_expansion && from) + : m_lhs(from.m_lhs), + m_def(from.m_def), + m_args(std::move(from.m_args)) {} + }; + + struct pp_case_expansion { + case_expansion & e; + ast_manager & m; + pp_case_expansion(case_expansion & e, ast_manager & m) : e(e), m(m) {} + }; + + friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &); + + // one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)` + struct body_expansion { + app* m_pred; + recfun::case_def const * m_cdef; + ptr_vector m_args; + + body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() { + m_cdef = &u.get_case_def(n); + m_args.append(n->get_num_args(), n->get_args()); + } + body_expansion(app* pred, recfun::case_def const & d, ptr_vector & args) : + m_pred(pred), m_cdef(&d), m_args(args) {} + body_expansion(body_expansion const & from): + m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {} + body_expansion(body_expansion && from) : + m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {} + }; + + struct pp_body_expansion { + body_expansion & e; + ast_manager & m; + pp_body_expansion(body_expansion & e, ast_manager & m) : e(e), m(m) {} + }; + + friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &); + + ast_manager& m; + recfun::decl::plugin& m_plugin; + recfun::util& m_util; + stats m_stats; + + // book-keeping for depth of predicates + obj_map m_pred_depth; + expr_ref_vector m_preds; + unsigned_vector m_preds_lim; + unsigned m_max_depth; // for fairness and termination + + ptr_vector m_q_case_expand; + ptr_vector m_q_body_expand; + vector m_q_clauses; + + recfun::util & u() const { return m_util; } + bool is_defined(app * f) const { return u().is_defined(f); } + bool is_case_pred(app * f) const { return u().is_case_pred(f); } + + bool is_defined(enode * e) const { return is_defined(e->get_owner()); } + bool is_case_pred(enode * e) const { return is_case_pred(e->get_owner()); } + + void reset_queues(); + expr_ref apply_args(unsigned depth, recfun::vars const & vars, ptr_vector const & args, expr * e); //!< substitute variables by args + void assert_macro_axiom(case_expansion & e); + void assert_case_axioms(case_expansion & e); + void assert_body_axiom(body_expansion & e); + literal mk_literal(expr* e); + + void assert_max_depth_limit(expr* guard); + unsigned get_depth(expr* e); + void set_depth(unsigned d, expr* e); + void set_depth_rec(unsigned d, expr* e); + + literal mk_eq_lit(expr* l, expr* r); + bool is_standard_order(recfun::vars const& vars) const { + return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; + } + protected: + void push_case_expand(case_expansion* e) { m_q_case_expand.push_back(e); } + void push_body_expand(body_expansion* e) { m_q_body_expand.push_back(e); } + + bool internalize_atom(app * atom, bool gate_ctx) override; + bool internalize_term(app * term) override; + void reset_eh() override; + void relevant_eh(app * n) override; + char const * get_name() const override; + final_check_status final_check_eh() override; + void assign_eh(bool_var v, bool is_true) override; + void push_scope_eh() override; + void pop_scope_eh(unsigned num_scopes) override; + void restart_eh() override; + bool can_propagate() override; + void propagate() override; + bool should_research(expr_ref_vector &) override; + + void new_eq_eh(theory_var v1, theory_var v2) override {} + void new_diseq_eh(theory_var v1, theory_var v2) override {} + void add_theory_assumptions(expr_ref_vector & assumptions) override; + void init(context* ctx) override; + + public: + theory_recfun(ast_manager & m); + ~theory_recfun() override; + theory * mk_fresh(context * new_ctx) override; + void init_search_eh() override; + void display(std::ostream & out) const override; + void collect_statistics(::statistics & st) const override; + }; +} + +#endif diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 59a9a1562..d0fd8f809 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -22,7 +22,7 @@ Revision History: bool smt_logics::supported_logic(symbol const & s) { - return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || + return logic_has_uf(s) || logic_is_allcsp(s) || logic_has_fd(s) || logic_has_arith(s) || logic_has_bv(s) || logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s); @@ -83,7 +83,7 @@ bool smt_logics::logic_has_arith(symbol const & s) { s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_S" || - s == "ALL" || + logic_is_allcsp(s) || s == "QF_FD" || s == "HORN" || s == "QF_FPLRA"; @@ -102,7 +102,7 @@ bool smt_logics::logic_has_bv(symbol const & s) { s == "QF_BVRE" || s == "QF_FPBV" || s == "QF_BVFP" || - s == "ALL" || + logic_is_allcsp(s) || s == "QF_FD" || s == "HORN"; } @@ -123,22 +123,22 @@ bool smt_logics::logic_has_array(symbol const & s) { s == "AUFNIRA" || s == "AUFBV" || s == "ABV" || - s == "ALL" || + logic_is_allcsp(s) || s == "QF_ABV" || s == "QF_AUFBV" || s == "HORN"; } bool smt_logics::logic_has_seq(symbol const & s) { - return s == "QF_BVRE" || s == "QF_S" || s == "ALL"; + return s == "QF_BVRE" || s == "QF_S" || logic_is_allcsp(s); } bool smt_logics::logic_has_str(symbol const & s) { - return s == "QF_S" || s == "ALL"; + return s == "QF_S" || logic_is_allcsp(s); } bool smt_logics::logic_has_fpa(symbol const & s) { - return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || s == "ALL"; + return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || logic_is_allcsp(s); } bool smt_logics::logic_has_uf(symbol const & s) { @@ -150,9 +150,10 @@ bool smt_logics::logic_has_horn(symbol const& s) { } bool smt_logics::logic_has_pb(symbol const& s) { - return s == "QF_FD" || s == "ALL" || logic_has_horn(s); + return s == "QF_FD" || logic_is_allcsp(s) || logic_has_horn(s); } bool smt_logics::logic_has_datatype(symbol const& s) { - return s == "QF_FD" || s == "ALL" || s == "QF_DT"; + return s == "QF_FD" || logic_is_allcsp(s) || s == "QF_DT"; } + diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h index 702431cdd..4382f575b 100644 --- a/src/solver/smt_logics.h +++ b/src/solver/smt_logics.h @@ -25,6 +25,8 @@ public: static bool supported_logic(symbol const & s); static bool logic_has_reals_only(symbol const& l); static bool logic_is_all(symbol const& s) { return s == "ALL"; } + static bool logic_is_csp(symbol const& s) { return s == "CSP"; } + static bool logic_is_allcsp(symbol const& s) { return logic_is_all(s) || logic_is_csp(s); } static bool logic_has_uf(symbol const& s); static bool logic_has_arith(symbol const & s); static bool logic_has_bv(symbol const & s); diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h index 920ecb2c9..52272389a 100644 --- a/src/util/scoped_ptr_vector.h +++ b/src/util/scoped_ptr_vector.h @@ -31,6 +31,7 @@ public: void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc()); m_vector.reset(); } void push_back(T * ptr) { m_vector.push_back(ptr); } void pop_back() { SASSERT(!empty()); set(size()-1, nullptr); m_vector.pop_back(); } + T * back() const { return m_vector.back(); } T * operator[](unsigned idx) const { return m_vector[idx]; } void set(unsigned idx, T * ptr) { if (m_vector[idx] == ptr) @@ -51,6 +52,13 @@ public: push_back(nullptr); } } + //!< swap last element with given pointer + void swap_back(scoped_ptr & ptr) { + SASSERT(!empty()); + T * tmp = ptr.detach(); + ptr = m_vector.back(); + m_vector[m_vector.size()-1] = tmp; + } }; #endif diff --git a/src/util/trail.h b/src/util/trail.h index b9f4602c7..fadafe724 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -143,6 +143,17 @@ public: }; +template +class insert_ref_map : public trail { + Mgr& m; + M& m_map; + D m_obj; +public: + insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {} + virtual ~insert_ref_map() {} + virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); } +}; + template class push_back_vector : public trail { diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 0f3715cb1..202df1039 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -269,10 +269,10 @@ public: void remove(unsigned v) { if (contains(v)) { m_in_set[v] = false; - unsigned i = 0; - for (i = 0; i < m_set.size() && m_set[i] != v; ++i) + unsigned i = m_set.size(); + for (; i > 0 && m_set[--i] != v; ) ; - SASSERT(i < m_set.size()); + SASSERT(m_set[i] == v); m_set[i] = m_set.back(); m_set.pop_back(); }