mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
Merge pull request #1906 from NikolajBjorner/csp
integrate native support for recursive definitions
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
eef2ac0ff5
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
=============
|
||||
|
||||
|
|
|
|||
93
doc/design_recfuns.md
Normal file
93
doc/design_recfuns.md
Normal file
|
|
@ -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)
|
||||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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'])
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -715,6 +715,4 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/*++
|
||||
Copyright (c) Microsoft Corporation, Arive Gurfinkel 2017
|
||||
Copyright (c) Microsoft Corporation, Arie Gurfinkel 2017
|
||||
|
||||
Module Name:
|
||||
|
||||
|
|
|
|||
|
|
@ -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<Z3_sort> 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<Z3_ast> 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);
|
||||
|
|
|
|||
|
|
@ -532,6 +532,34 @@ namespace Microsoft.Z3
|
|||
return new FuncDecl(this, MkSymbol(name), domain, range);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Creates a new recursive function declaration.
|
||||
/// </summary>
|
||||
public FuncDecl MkRecFuncDecl(string name, Sort[] domain, Sort range)
|
||||
{
|
||||
Debug.Assert(range != null);
|
||||
Debug.Assert(domain.All(d => d != null));
|
||||
|
||||
CheckContextMatch<Sort>(domain);
|
||||
CheckContextMatch(range);
|
||||
return new FuncDecl(this, MkSymbol(name), domain, range, true);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// 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.
|
||||
/// </summary>
|
||||
public void AddRecDef(FuncDecl f, Expr[] args, Expr body)
|
||||
{
|
||||
CheckContextMatch(f);
|
||||
CheckContextMatch<Expr>(args);
|
||||
CheckContextMatch(body);
|
||||
IntPtr[] argsNative = AST.ArrayToNative(args);
|
||||
Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Creates a new function declaration.
|
||||
/// </summary>
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 */
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -16,8 +16,8 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<sstream>
|
||||
#include<cstring>
|
||||
#include <sstream>
|
||||
#include <cstring>
|
||||
#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()) {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -32,5 +32,27 @@ struct mk_pp : public mk_ismt2_pp {
|
|||
}
|
||||
};
|
||||
|
||||
//<! print vector of ASTs
|
||||
class mk_pp_vec {
|
||||
ast_manager & m;
|
||||
ast_ref_vector vec;
|
||||
public:
|
||||
mk_pp_vec(unsigned len, ast ** vec0, ast_manager & m) : m(m), vec(m) {
|
||||
for (unsigned i=0; i<len; ++i) vec.push_back(vec0[i]);
|
||||
}
|
||||
void display(std::ostream & out) const {
|
||||
bool first = true;
|
||||
for (ast* e : vec) {
|
||||
if (first) { first = false; } else { out << " "; }
|
||||
out << mk_pp(e, m);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
|
||||
pp.display(out);
|
||||
return out;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include "ast/ast_pp_util.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_smt_pp.h"
|
||||
#include "ast/recfun_decl_plugin.h"
|
||||
|
||||
void ast_pp_util::collect(expr* e) {
|
||||
coll.visit(e);
|
||||
|
|
@ -49,7 +50,14 @@ void ast_pp_util::display_decls(std::ostream& out) {
|
|||
ast_smt2_pp(out, f, m_env) << "\n";
|
||||
}
|
||||
}
|
||||
SASSERT(coll.get_num_preds() == 0);
|
||||
vector<std::pair<func_decl*, expr*>> 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) {
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -1163,6 +1163,33 @@ public:
|
|||
unregister_var_names(f->get_arity());
|
||||
}
|
||||
|
||||
// format set of mutually recursive definitions
|
||||
void operator()(vector<std::pair<func_decl*, expr*>> 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<format**, f2f>(m(), args, args+3, f2f(), ""));
|
||||
process(e, r);
|
||||
bodies.push_back(r);
|
||||
unregister_var_names(f->get_arity());
|
||||
}
|
||||
r1 = mk_seq1<format*const*, f2f>(m(), decls.begin(), decls.end(), f2f(), "");
|
||||
r2 = mk_seq1<format*const*, f2f>(m(), bodies.begin(), bodies.end(), f2f(), "");
|
||||
format * args[2];
|
||||
args[0] = r1;
|
||||
args[1] = r2;
|
||||
r = mk_seq1<format**, f2f>(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<std::pair<func_decl*, expr*>> 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),
|
||||
|
|
|
|||
|
|
@ -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<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
|
||||
|
||||
|
||||
/**
|
||||
\brief Internal wrapper (for debugging purposes only)
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
374
src/ast/csp_decl_plugin.cpp
Normal file
374
src/ast/csp_decl_plugin.cpp
Normal file
|
|
@ -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<js_sort_kind>(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<js_op_kind>(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<builtin_name> & 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<builtin_name> & 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<csp_decl_plugin*>(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<symbol>& 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<symbol>& 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<symbol>& 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;
|
||||
}
|
||||
|
||||
|
||||
162
src/ast/csp_decl_plugin.h
Normal file
162
src/ast/csp_decl_plugin.h
Normal file
|
|
@ -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<builtin_name> & op_names, symbol const & logic) override;
|
||||
void get_sort_names(svector<builtin_name> & 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<symbol>& properites);
|
||||
bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector<symbol>& 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<symbol>& 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);
|
||||
|
||||
};
|
||||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -26,10 +26,8 @@ Revision History:
|
|||
|
||||
class decl_collector {
|
||||
ast_manager & m_manager;
|
||||
bool m_sep_preds;
|
||||
ptr_vector<sort> m_sorts;
|
||||
ptr_vector<func_decl> m_decls;
|
||||
ptr_vector<func_decl> 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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
428
src/ast/recfun_decl_plugin.cpp
Normal file
428
src/ast/recfun_decl_plugin.cpp
Normal file
|
|
@ -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 <functional>
|
||||
#include <sstream>
|
||||
#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<branch> 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};
|
||||
}
|
||||
};
|
||||
|
||||
//<! build a substitution and a list of conditions from a path
|
||||
static void convert_path(ast_manager & m,
|
||||
choice_lst const * choices,
|
||||
expr_ref_vector & conditions /* out */,
|
||||
expr_substitution & subst /* out */)
|
||||
{
|
||||
for (; choices != nullptr; choices = choices->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<expr> 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<decl::plugin*>(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;
|
||||
}
|
||||
}
|
||||
}
|
||||
249
src/ast/recfun_decl_plugin.h
Normal file
249
src/ast/recfun_decl_plugin.h
Normal file
|
|
@ -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; //<! one possible control path of a function
|
||||
class case_pred; //<! a predicate guarding a given control flow path of a function
|
||||
class util; //<! util for other modules
|
||||
class def; //!< definition of a (recursive) function
|
||||
class promise_def; //!< definition to be complete
|
||||
|
||||
enum op_kind {
|
||||
OP_FUN_DEFINED, // defined function with one or more cases, possibly recursive
|
||||
OP_FUN_CASE_PRED, // predicate guarding a given control flow path
|
||||
OP_DEPTH_LIMIT, // predicate enforcing some depth limit
|
||||
};
|
||||
|
||||
/*! A predicate `p(t1...tn)`, that, if true, means `f(t1...tn)` is following
|
||||
a given path of its control flow and can be unrolled.
|
||||
|
||||
For example, `fact n := if n<2 then 1 else n * fact(n-1)` would have two cases,
|
||||
and therefore two case predicates `C_fact_0` and `C_fact_1`, where
|
||||
`C_fact_0(t)=true` means `t<2` (first path) and `C_fact_1(t)=true` means `not (t<2)` (second path).
|
||||
*/
|
||||
|
||||
typedef var_ref_vector vars;
|
||||
|
||||
class case_def {
|
||||
friend class def;
|
||||
func_decl_ref m_pred; //<! predicate used for this case
|
||||
expr_ref_vector m_guards; //<! conjunction that is equivalent to this case
|
||||
expr_ref m_rhs; //<! if guard is true, `f(t1…tn) = rhs` holds
|
||||
def * m_def; //<! definition this is a part of
|
||||
bool m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
|
||||
|
||||
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);
|
||||
|
||||
void add_guard(expr_ref && e) { m_guards.push_back(e); }
|
||||
public:
|
||||
func_decl* get_decl() const { return m_pred; }
|
||||
|
||||
app_ref apply_case_predicate(ptr_vector<expr> 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<case_def> cases;
|
||||
|
||||
ast_manager & m;
|
||||
symbol m_name; //<! name of function
|
||||
sort_ref_vector m_domain; //<! type of arguments
|
||||
sort_ref m_range; //<! return type
|
||||
vars m_vars; //<! variables of the function
|
||||
cases m_cases; //!< possible cases
|
||||
func_decl_ref m_decl; //!< generic declaration
|
||||
expr_ref m_rhs; //!< definition
|
||||
family_id m_fid;
|
||||
|
||||
def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
|
||||
|
||||
// compute cases for a function, given its RHS (possibly containing `ite`).
|
||||
void compute_cases(is_immediate_pred &, th_rewriter & th_rw,
|
||||
unsigned n_vars, var *const * vars, expr* rhs);
|
||||
void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
|
||||
bool contains_ite(expr* e); // expression contains a test?
|
||||
public:
|
||||
symbol const & get_name() const { return m_name; }
|
||||
vars const & get_vars() const { return m_vars; }
|
||||
cases & get_cases() { return m_cases; }
|
||||
unsigned get_arity() const { return m_domain.size(); }
|
||||
sort_ref_vector const & get_domain() const { return m_domain; }
|
||||
sort_ref const & get_range() const { return m_range; }
|
||||
func_decl * get_decl() const { return m_decl.get(); }
|
||||
expr * get_rhs() const { return m_rhs; }
|
||||
|
||||
bool is_fun_macro() const { return m_cases.size() == 1; }
|
||||
bool is_fun_defined() const { return !is_fun_macro(); }
|
||||
|
||||
};
|
||||
|
||||
// definition to be complete (missing RHS)
|
||||
class promise_def {
|
||||
friend class util;
|
||||
util * u;
|
||||
def * d;
|
||||
void set_definition(unsigned n_vars, var * const * vars, expr * rhs); // call only once
|
||||
public:
|
||||
promise_def(util * u, def * d) : u(u), d(d) {}
|
||||
promise_def(promise_def const & from) : u(from.u), d(from.d) {}
|
||||
def * get_def() const { return d; }
|
||||
};
|
||||
|
||||
namespace decl {
|
||||
|
||||
class plugin : public decl_plugin {
|
||||
typedef obj_map<func_decl, def*> def_map;
|
||||
typedef obj_map<func_decl, case_def*> case_def_map;
|
||||
|
||||
mutable scoped_ptr<util> 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; }
|
||||
|
||||
//<! don't use native theory if recursive function declarations are not populated with defs
|
||||
bool has_defs() const { return m_plugin->has_defs(); }
|
||||
|
||||
//<! add a function declaration
|
||||
def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range);
|
||||
|
||||
|
||||
def& get_def(func_decl* f) {
|
||||
SASSERT(m_plugin->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<expr> 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);
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
|
|
@ -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));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -212,6 +212,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
|
|||
return false;
|
||||
}
|
||||
|
||||
|
||||
template<typename Config>
|
||||
template<bool ProofGen>
|
||||
void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
|
||||
|
|
@ -338,15 +339,12 @@ void rewriter_tpl<Config>::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));
|
||||
|
|
|
|||
|
|
@ -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<func_decls>::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<symbol> 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<symbol> 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<symbol> 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 (<symbol> (<sort>*) <sort>) ", 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 (<symbol> (<sort>*) <sort>) ", 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 <symbol> <sort>) to disumbiguate ", s);
|
||||
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) 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<symbol> 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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<symbol> 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<symbol> const& ids, expr* e);
|
||||
void insert_rec_fun_as_axiom(func_decl* f, expr_ref_vector const& binding, svector<symbol> 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;
|
||||
|
|
|
|||
|
|
@ -91,6 +91,11 @@ UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of
|
|||
ctx.regular_stream() << ")" << std::endl;
|
||||
});
|
||||
|
||||
UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "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", "<term>", "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));
|
||||
|
|
|
|||
|
|
@ -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<expr>::const_iterator it = u.begin();
|
||||
ptr_vector<expr>::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_buffer<func_decl
|
|||
func_decl_set deps;
|
||||
bool all_visited = true;
|
||||
collect_func_decls(m, curr_i->get_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<func_decl
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core const & md, unsigned indent) {
|
||||
ast_manager & m = ctx.get_ast_manager();
|
||||
recfun::util recfun_util(m);
|
||||
sbuffer<symbol> var_names;
|
||||
ptr_buffer<format> f_var_names;
|
||||
ptr_buffer<format> 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));
|
||||
|
|
|
|||
|
|
@ -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<symbol, expr*> 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<symbol>& ids) {
|
||||
recfun::promise_def parse_rec_fun_decl(func_decl_ref& f, expr_ref_vector& bindings, svector<symbol>& 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<expr_ref_vector> const& bindings, vector<svector<symbol> >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) {
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -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<uint64_t> m_coeffs;
|
||||
svector<wliteral> 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<bool> m_visited;
|
||||
svector<unsigned> m_visited;
|
||||
unsigned m_visited_ts;
|
||||
vector<svector<constraint*>> 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<wliteral>& 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;
|
||||
|
|
|
|||
|
|
@ -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<literal>(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) {
|
||||
|
|
|
|||
|
|
@ -34,6 +34,7 @@ namespace sat {
|
|||
svector<int> m_left, m_right;
|
||||
literal_vector m_root, m_parent;
|
||||
bool m_learned;
|
||||
bool m_include_cardinality;
|
||||
|
||||
svector<std::pair<literal, literal>> m_del_bin;
|
||||
|
||||
|
|
@ -54,6 +55,9 @@ namespace sat {
|
|||
// static svector<std::pair<literal, literal>> 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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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'),
|
||||
|
|
|
|||
|
|
@ -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); }
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
))
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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<expr_ref_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;
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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<expr> args;
|
||||
expr * result = get_value(n);
|
||||
SASSERT(result);
|
||||
|
|
|
|||
|
|
@ -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<expr> 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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -3302,7 +3302,6 @@ namespace smt {
|
|||
return b && to_expr(b->get_value(), is_int(v), r);
|
||||
}
|
||||
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_lower(enode * n, rational& r, bool& is_strict) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
|
|
|
|||
1070
src/smt/theory_jobscheduler.cpp
Normal file
1070
src/smt/theory_jobscheduler.cpp
Normal file
File diff suppressed because it is too large
Load diff
244
src/smt/theory_jobscheduler.h
Normal file
244
src/smt/theory_jobscheduler.h
Normal file
|
|
@ -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<symbol> 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<job_resource> m_resources; // resources allowed to run job.
|
||||
u_map<unsigned> 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<res_available> 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<time_t>::max()), m_resource(nullptr), m_makespan(nullptr) {}
|
||||
};
|
||||
|
||||
ast_manager& m;
|
||||
csp_util u;
|
||||
arith_util a;
|
||||
vector<job_info> m_jobs;
|
||||
vector<res_info> m_resources;
|
||||
unsigned_vector m_bound_jobs;
|
||||
unsigned m_bound_qhead;
|
||||
struct scope {
|
||||
unsigned m_bound_jobs_lim;
|
||||
unsigned m_bound_qhead;
|
||||
};
|
||||
svector<scope> 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<job_time> & m_starts, &m_ends;
|
||||
unsigned s_idx, e_idx; // index into starts/ends
|
||||
uint_set m_jobs;
|
||||
public:
|
||||
job_overlap(vector<job_time>& starts, vector<job_time>& 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;
|
||||
|
||||
};
|
||||
};
|
||||
|
||||
451
src/smt/theory_recfun.cpp
Normal file
451
src/smt/theory_recfun.cpp
Normal file
|
|
@ -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<recfun::decl::plugin*>(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<expr> 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 << ")";
|
||||
}
|
||||
}
|
||||
163
src/smt/theory_recfun.h
Normal file
163
src/smt/theory_recfun.h
Normal file
|
|
@ -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<expr> 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<expr> 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<expr> & 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<expr, unsigned> m_pred_depth;
|
||||
expr_ref_vector m_preds;
|
||||
unsigned_vector m_preds_lim;
|
||||
unsigned m_max_depth; // for fairness and termination
|
||||
|
||||
ptr_vector<case_expansion> m_q_case_expand;
|
||||
ptr_vector<body_expansion> m_q_body_expand;
|
||||
vector<literal_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<expr> 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
|
||||
|
|
@ -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";
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ public:
|
|||
void reset() { std::for_each(m_vector.begin(), m_vector.end(), delete_proc<T>()); 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<T> & ptr) {
|
||||
SASSERT(!empty());
|
||||
T * tmp = ptr.detach();
|
||||
ptr = m_vector.back();
|
||||
m_vector[m_vector.size()-1] = tmp;
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -143,6 +143,17 @@ public:
|
|||
};
|
||||
|
||||
|
||||
template<typename Ctx, typename M, typename Mgr, typename D>
|
||||
class insert_ref_map : public trail<Ctx> {
|
||||
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<typename Ctx, typename V>
|
||||
class push_back_vector : public trail<Ctx> {
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue