mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
wip: lra
This commit is contained in:
Simon Cruanes
parent
95edfd9aa9
commit
40d47a8d6c
5 changed files with 87 additions and 703 deletions
|
|
@ -144,6 +144,7 @@ let main () =
|
|||
if is_cnf then [] else [
|
||||
Process.th_bool ;
|
||||
Process.th_data;
|
||||
Process.th_lra;
|
||||
]
|
||||
in
|
||||
Process.Solver.create ~store_proof:!check ~theories tst ()
|
||||
|
|
|
|||
|
|
@ -301,5 +301,12 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
|
|||
include Form
|
||||
end)
|
||||
|
||||
module Th_lra = Sidekick_th_lra.Make(struct
|
||||
module S = Solver
|
||||
type term = S.T.Term.t
|
||||
let view_as_lra _ = assert false (* TODO *)
|
||||
end)
|
||||
|
||||
let th_bool : Solver.theory = Th_bool.theory
|
||||
let th_data : Solver.theory = Th_data.theory
|
||||
let th_lra : Solver.theory = Th_lra.theory
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ module Solver
|
|||
|
||||
val th_bool : Solver.theory
|
||||
val th_data : Solver.theory
|
||||
val th_lra : Solver.theory
|
||||
|
||||
type 'a or_error = ('a, string) CCResult.t
|
||||
|
||||
|
|
|
|||
|
|
@ -6,673 +6,6 @@
|
|||
|
||||
open Sidekick_core
|
||||
|
||||
(*
|
||||
open Mc2_core
|
||||
|
||||
module LE = Linexp
|
||||
open LE.Infix
|
||||
|
||||
let name = "lra"
|
||||
|
||||
type num = Q.t
|
||||
|
||||
type ty_view +=
|
||||
| Ty_rat
|
||||
|
||||
type value_view +=
|
||||
| V_rat of num
|
||||
|
||||
(** Boolean operator for predicates *)
|
||||
type op =
|
||||
| Eq0
|
||||
| Leq0
|
||||
| Lt0
|
||||
|
||||
(* a single constraint on a Q-sorted variables *)
|
||||
type constr =
|
||||
| C_leq
|
||||
| C_lt
|
||||
| C_geq
|
||||
| C_gt
|
||||
| C_eq
|
||||
| C_neq
|
||||
|
||||
type bound =
|
||||
| B_some of {strict:bool; num: num; expr: LE.t; reason:atom}
|
||||
| B_none (* no bound *)
|
||||
|
||||
type eq_cstr =
|
||||
| EC_eq of {num:num; reason:atom; expr: LE.t}
|
||||
| EC_neq of {l: (num * LE.t * atom) list} (* forbidden values *)
|
||||
| EC_none
|
||||
|
||||
(* state for a single Q-sorted variable *)
|
||||
type decide_state +=
|
||||
| State of {
|
||||
mutable last_val: num; (* phase saving *)
|
||||
mutable low: bound;
|
||||
mutable up: bound;
|
||||
mutable eq: eq_cstr;
|
||||
}
|
||||
|
||||
type term_view +=
|
||||
| Const of num
|
||||
| Pred of {
|
||||
op: op;
|
||||
expr: LE.t;
|
||||
mutable watches: Term.Watch2.t; (* can sometimes propagate *)
|
||||
} (** Arithmetic constraint *)
|
||||
|
||||
type lemma_view +=
|
||||
| Lemma_lra
|
||||
|
||||
let k_rat = Service.Key.makef "%s.rat" name
|
||||
let k_make_const = Service.Key.makef "%s.make_const" name
|
||||
let k_make_pred = Service.Key.makef "%s.make_pred" name
|
||||
|
||||
let[@inline] equal_op a b =
|
||||
begin match a, b with
|
||||
| Eq0, Eq0
|
||||
| Leq0, Leq0
|
||||
| Lt0, Lt0 -> true
|
||||
| Eq0, _ | Leq0, _ | Lt0, _ -> false
|
||||
end
|
||||
|
||||
let[@inline] hash_op a = match a with
|
||||
| Eq0 -> 0
|
||||
| Leq0 -> 1
|
||||
| Lt0 -> 2
|
||||
|
||||
(* evaluate a linexp into a number *)
|
||||
let[@inline] eval_le (e:LE.t) : (num * term list) option =
|
||||
LE.eval e
|
||||
~f:(fun t -> match Term.value t with
|
||||
| Some (V_value {view=V_rat n;_}) -> Some n
|
||||
| _ -> None)
|
||||
|
||||
let tc_value =
|
||||
let pp out = function
|
||||
| V_rat q -> Q.pp_print out q
|
||||
| _ -> assert false
|
||||
and equal a b = match a, b with
|
||||
| V_rat a, V_rat b -> Q.equal a b
|
||||
| _ -> false
|
||||
and hash = function
|
||||
| V_rat r -> LE.hash_q r
|
||||
| _ -> assert false
|
||||
in
|
||||
Value.TC.make ~pp ~equal ~hash ()
|
||||
|
||||
let[@inline] mk_val (n:num) : value = Value.make tc_value (V_rat n)
|
||||
|
||||
(* evaluate the linear expression
|
||||
precondition: all terms in it are assigned *)
|
||||
let[@inline] eval_le_num_exn (e:LE.t) : num = match eval_le e with
|
||||
| Some (n,_) -> n
|
||||
| None -> assert false
|
||||
|
||||
let pp_ty out = function Ty_rat -> Fmt.fprintf out "@<1>ℚ" | _ -> assert false
|
||||
|
||||
let mk_state _ : decide_state =
|
||||
State {
|
||||
last_val=Q.zero;
|
||||
up=B_none;
|
||||
low=B_none;
|
||||
eq=EC_none;
|
||||
}
|
||||
|
||||
let pp_constr out (e:constr) = match e with
|
||||
| C_leq -> Fmt.string out "≤"
|
||||
| C_lt -> Fmt.string out "<"
|
||||
| C_geq -> Fmt.string out "≥"
|
||||
| C_gt -> Fmt.string out ">"
|
||||
| C_eq -> Fmt.string out "="
|
||||
| C_neq -> Fmt.string out "≠"
|
||||
|
||||
let pp_bound out = function
|
||||
| B_none -> Fmt.string out "ø"
|
||||
| B_some {strict;num;reason;expr} ->
|
||||
let strict_str = if strict then "[strict]" else "" in
|
||||
Fmt.fprintf out "(@[%a%s@ :expr %a@ :reason %a@])"
|
||||
Q.pp_print num strict_str LE.pp expr Atom.debug reason
|
||||
|
||||
let pp_eq out = function
|
||||
| EC_none -> Fmt.string out "ø"
|
||||
| EC_eq {num;reason;expr} ->
|
||||
Fmt.fprintf out "(@[= %a@ :expr %a@ :reason %a@])"
|
||||
Q.pp_print num LE.pp expr Atom.debug reason
|
||||
| EC_neq {l} ->
|
||||
let pp_tuple out (n,e,a) =
|
||||
Fmt.fprintf out "(@[%a@ :expr %a@ :reason %a@])"
|
||||
Q.pp_print n LE.pp e Atom.debug a
|
||||
in
|
||||
Fmt.fprintf out "(@[<hv>!=@ %a@])"
|
||||
(Util.pp_list pp_tuple) l
|
||||
|
||||
let pp_state out = function
|
||||
| State s ->
|
||||
Fmt.fprintf out "(@[<hv>:low %a@ :up %a@ :eq %a@])"
|
||||
pp_bound s.low pp_bound s.up pp_eq s.eq
|
||||
| _ -> assert false
|
||||
|
||||
let[@inline] subterms (t:term_view) : term Iter.t = match t with
|
||||
| Const _ -> Iter.empty
|
||||
| Pred {expr=e;_} -> LE.terms e
|
||||
| _ -> assert false
|
||||
|
||||
let pp_op out = function
|
||||
| Eq0 -> Fmt.string out "= 0"
|
||||
| Leq0 -> Fmt.string out "≤ 0"
|
||||
| Lt0 -> Fmt.string out "< 0"
|
||||
|
||||
let pp_term out = function
|
||||
| Const n -> Q.pp_print out n
|
||||
| Pred {op;expr;_} ->
|
||||
Fmt.fprintf out "(@[%a@ %a@])" LE.pp_no_paren expr pp_op op
|
||||
| _ -> assert false
|
||||
|
||||
(* evaluate [op n] where [n] is a constant *)
|
||||
let[@inline] eval_bool_const op n : bool =
|
||||
begin match Q.sign n, op with
|
||||
| 0, Eq0 -> true
|
||||
| n, Leq0 when n<=0 -> true
|
||||
| n, Lt0 when n<0 -> true
|
||||
| _ -> false
|
||||
end
|
||||
|
||||
(* evaluate an arithmetic boolean expression *)
|
||||
let eval (t:term) = match Term.view t with
|
||||
| Const n -> Eval_into (mk_val n, [])
|
||||
| Pred {op;expr=e;_} ->
|
||||
begin match eval_le e with
|
||||
| None -> Eval_unknown
|
||||
| Some (n,l) -> Eval_into (Value.of_bool @@ eval_bool_const op n, l)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
let tc_lemma : tc_lemma =
|
||||
Lemma.TC.make
|
||||
~pp:(fun out l -> match l with
|
||||
| Lemma_lra -> Fmt.string out "lra"
|
||||
| _ -> assert false)
|
||||
()
|
||||
|
||||
let lemma_lra = Lemma.make Lemma_lra tc_lemma
|
||||
|
||||
(* build plugin *)
|
||||
let build
|
||||
p_id
|
||||
(Plugin.S_cons (_,true_, Plugin.S_cons (_,false_,Plugin.S_nil)))
|
||||
: Plugin.t =
|
||||
let tc_t = Term.TC.lazy_make() in
|
||||
let tc_ty = Type.TC.lazy_make() in
|
||||
let module T = Term.Term_allocator(struct
|
||||
let tc = tc_t
|
||||
let initial_size = 64
|
||||
let p_id = p_id
|
||||
let equal a b = match a, b with
|
||||
| Const n1, Const n2 -> Q.equal n1 n2
|
||||
| Pred p1, Pred p2 -> p1.op = p2.op && LE.equal p1.expr p2.expr
|
||||
| _ -> false
|
||||
let hash = function
|
||||
| Const n -> LE.hash_q n
|
||||
| Pred {op;expr;_} -> CCHash.combine3 10 (hash_op op) (LE.hash expr)
|
||||
| _ -> assert false
|
||||
end)
|
||||
in
|
||||
let module P = struct
|
||||
let id = p_id
|
||||
let name = name
|
||||
|
||||
let gc_all = T.gc_all
|
||||
let iter_terms = T.iter_terms
|
||||
let check_if_sat _ = Sat
|
||||
|
||||
let ty_rat = lazy (
|
||||
let tc = Type.TC.lazy_get tc_ty in
|
||||
Type.make_static Ty_rat tc
|
||||
)
|
||||
|
||||
(* build a predicate on a linear expression *)
|
||||
let mk_pred (op:op) (e:LE.t) : term =
|
||||
begin match LE.as_const e with
|
||||
| Some n ->
|
||||
(* directly evaluate *)
|
||||
if eval_bool_const op n then true_ else false_
|
||||
| None ->
|
||||
(* simplify: if e is [n·x op 0], then rewrite into [sign(n)·x op 0] *)
|
||||
let e = match LE.as_singleton e with
|
||||
| None -> e
|
||||
| Some (n,t) ->
|
||||
let n = if Q.sign n >= 0 then Q.one else Q.minus_one in
|
||||
LE.singleton n t
|
||||
in
|
||||
let view = Pred {op; expr=e; watches=Term.Watch2.dummy} in
|
||||
T.make view Type.bool
|
||||
end
|
||||
|
||||
let mk_const (n:num) : term = T.make (Const n) (Lazy.force ty_rat)
|
||||
|
||||
(* raise a conflict that deduces [expr_up_bound - expr_low_bound op 0] (which must
|
||||
eval to [false]) from [reasons] *)
|
||||
let raise_conflict acts
|
||||
~sign ~op ~pivot ~expr_up_bound ~expr_low_bound ~reasons () : 'a =
|
||||
let expr = LE.diff expr_low_bound expr_up_bound in
|
||||
assert (not (LE.mem_term pivot expr));
|
||||
let concl = mk_pred op expr in
|
||||
let concl = if sign then Term.Bool.pa concl else Term.Bool.na concl in
|
||||
let c = concl :: List.map Atom.neg reasons in
|
||||
Log.debugf 30
|
||||
(fun k->k
|
||||
"(@[<hv>lra.raise_conflict@ :pivot %a@ :expr %a %a@ \
|
||||
:e_up_b %a@ :e_low_b %a@ \
|
||||
:reasons (@[<v>%a@])@ :clause %a@])"
|
||||
Term.debug pivot LE.pp expr pp_op op LE.pp expr_up_bound LE.pp expr_low_bound
|
||||
(Util.pp_list Atom.debug) reasons Clause.debug_atoms c);
|
||||
Actions.raise_conflict acts c lemma_lra
|
||||
|
||||
(* [make op e t ~reason b] turns this unit constraint over [t]
|
||||
(which is true or false according to [b]) into a proper
|
||||
unit constraint *)
|
||||
let constr_of_unit (op:op) (e:LE.t) (t:term) (b:bool) : constr * LE.t * num =
|
||||
let coeff = LE.find_term_exn t e in
|
||||
let is_pos = Q.sign coeff >= 0 in
|
||||
(* [e' = - e / coeff] *)
|
||||
let e' = LE.mult (Q.div Q.minus_one coeff) (LE.remove_term t e) in
|
||||
let num = eval_le_num_exn e' in
|
||||
(* assuming [b=true] and [is_pos],
|
||||
we have that reason is the same in the current model as [op(t + num)] *)
|
||||
begin match op, b, is_pos with
|
||||
| Eq0, true, _ -> C_eq
|
||||
| Eq0, false, _ -> C_neq
|
||||
| Leq0, true, true -> C_leq
|
||||
| Leq0, true, false -> C_geq
|
||||
| Leq0, false, true -> C_gt
|
||||
| Leq0, false, false -> C_lt
|
||||
| Lt0, true, true -> C_lt
|
||||
| Lt0, true, false -> C_gt
|
||||
| Lt0, false, true -> C_geq
|
||||
| Lt0, false, false -> C_leq
|
||||
end, e', num
|
||||
|
||||
(* check that there isn't a conflict of the shape [a <= t <= a, t != a] *)
|
||||
let check_tight_bound acts t : unit = match Term.decide_state_exn t with
|
||||
| State s ->
|
||||
begin match s.low, s.up, s.eq with
|
||||
| B_some low, B_some up, EC_neq {l} when
|
||||
Q.equal low.num up.num &&
|
||||
List.exists (fun (n,_,_) -> Q.equal low.num n) l
|
||||
->
|
||||
assert (not low.strict);
|
||||
assert (not up.strict);
|
||||
let reason_neq, expr_neq =
|
||||
CCList.find_map
|
||||
(fun (n,e,r) -> if Q.equal low.num n then Some (r,e) else None)
|
||||
l |> CCOpt.get_exn
|
||||
in
|
||||
Log.debugf 30
|
||||
(fun k->k
|
||||
"(@[<hv>lra.raise_conflict.tight-bound@ \
|
||||
@[:term %a@]@ @[low: %a@]@ @[up: %a@]@ @[eq: %a@]@ \
|
||||
expr-low %a@ expr-up %a@ expr-neq: %a@])"
|
||||
Term.pp t pp_bound s.low pp_bound s.up pp_eq s.eq
|
||||
LE.pp low.expr LE.pp up.expr LE.pp expr_neq);
|
||||
(* conflict is:
|
||||
[low <= t & t <= up & t != neq ===> (low < neq \/ neq < up)] *)
|
||||
let case1 =
|
||||
mk_pred Lt0 (LE.diff low.expr expr_neq)
|
||||
and case2 =
|
||||
mk_pred Lt0 (LE.diff expr_neq up.expr)
|
||||
in
|
||||
(* conflict should be:
|
||||
[low <= t & t <= up & low=up => t = neq]. *)
|
||||
let c =
|
||||
Term.Bool.pa case1 :: Term.Bool.pa case2 ::
|
||||
List.rev_map Atom.neg [low.reason; up.reason; reason_neq]
|
||||
in
|
||||
Actions.raise_conflict acts c lemma_lra
|
||||
| _ -> ()
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* add upper bound *)
|
||||
let add_up acts ~strict t num ~expr ~reason : unit = match Term.decide_state_exn t with
|
||||
| State s ->
|
||||
(* check consistency *)
|
||||
begin match s.eq, s.low with
|
||||
| EC_eq eq, _ when
|
||||
(strict && Q.compare eq.num num >= 0) ||
|
||||
(not strict && Q.compare eq.num num > 0) ->
|
||||
raise_conflict acts
|
||||
~sign:true ~op:(if strict then Lt0 else Leq0) ~pivot:t
|
||||
~expr_up_bound:expr ~expr_low_bound:eq.expr ~reasons:[reason; eq.reason] ()
|
||||
| _, B_some b when
|
||||
((strict || b.strict) && Q.compare b.num num >= 0) ||
|
||||
(Q.compare b.num num > 0) ->
|
||||
raise_conflict acts
|
||||
~sign:true ~op:(if strict || b.strict then Lt0 else Leq0) ~pivot:t
|
||||
~expr_up_bound:expr ~expr_low_bound:b.expr ~reasons:[reason; b.reason] ()
|
||||
| _ -> ()
|
||||
end;
|
||||
(* update *)
|
||||
let old_b = s.up in
|
||||
Actions.on_backtrack acts (fun () -> s.up <- old_b);
|
||||
begin match s.up with
|
||||
| B_none ->
|
||||
s.up <- B_some {strict;num;reason;expr};
|
||||
check_tight_bound acts t;
|
||||
| B_some b ->
|
||||
(* only replace if more tight *)
|
||||
if Q.compare b.num num > 0 ||
|
||||
(strict && not b.strict && Q.equal b.num num) then (
|
||||
s.up <- B_some {strict;num;reason;expr};
|
||||
check_tight_bound acts t;
|
||||
)
|
||||
end;
|
||||
| _ -> assert false
|
||||
|
||||
(* add lower bound *)
|
||||
let add_low acts ~strict t num ~expr ~reason : unit = match Term.decide_state_exn t with
|
||||
| State s ->
|
||||
(* check consistency *)
|
||||
begin match s.eq, s.up with
|
||||
| EC_eq eq, _ when
|
||||
(strict && Q.compare eq.num num <= 0) ||
|
||||
(not strict && Q.compare eq.num num < 0) ->
|
||||
raise_conflict acts
|
||||
~sign:true ~op:(if strict then Lt0 else Leq0) ~pivot:t
|
||||
~expr_low_bound:expr ~expr_up_bound:eq.expr ~reasons:[reason; eq.reason] ()
|
||||
| _, B_some b when
|
||||
((strict || b.strict) && Q.compare b.num num <= 0) ||
|
||||
(Q.compare b.num num < 0) ->
|
||||
raise_conflict acts
|
||||
~sign:true ~op:(if strict || b.strict then Lt0 else Leq0) ~pivot:t
|
||||
~expr_low_bound:expr ~expr_up_bound:b.expr ~reasons:[reason; b.reason] ()
|
||||
| _ -> ()
|
||||
end;
|
||||
(* update state *)
|
||||
let old_b = s.low in
|
||||
Actions.on_backtrack acts (fun () -> s.low <- old_b);
|
||||
begin match s.low with
|
||||
| B_none ->
|
||||
s.low <- B_some {strict;num;reason;expr};
|
||||
check_tight_bound acts t;
|
||||
| B_some b ->
|
||||
(* only replace if more tight *)
|
||||
if Q.compare b.num num < 0 ||
|
||||
(strict && not b.strict && Q.equal b.num num) then (
|
||||
s.low <- B_some {strict;num;reason;expr};
|
||||
check_tight_bound acts t;
|
||||
)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* add exact bound *)
|
||||
let add_eq acts t num ~expr ~reason : unit = match Term.decide_state_exn t with
|
||||
| State s ->
|
||||
(* check compatibility with bounds *)
|
||||
begin match s.low, s.up with
|
||||
| B_some b, _ when
|
||||
(b.strict && Q.compare b.num num >= 0) ||
|
||||
(not b.strict && Q.compare b.num num > 0) ->
|
||||
raise_conflict acts ~op:(if b.strict then Lt0 else Leq0)
|
||||
~sign:true ~pivot:t ~expr_up_bound:expr ~expr_low_bound:b.expr
|
||||
~reasons:[reason; b.reason] ()
|
||||
| _, B_some b when
|
||||
(b.strict && Q.compare b.num num <= 0) ||
|
||||
(not b.strict && Q.compare b.num num < 0) ->
|
||||
raise_conflict acts ~op:(if b.strict then Lt0 else Leq0)
|
||||
~sign:true ~pivot:t ~expr_low_bound:expr ~expr_up_bound:b.expr
|
||||
~reasons:[reason; b.reason] ()
|
||||
| _ -> ()
|
||||
end;
|
||||
(* check other equality constraints, and update *)
|
||||
let old_b = s.eq in
|
||||
Actions.on_backtrack acts (fun () -> s.eq <- old_b);
|
||||
begin match s.eq with
|
||||
| EC_none -> s.eq <- EC_eq {num;reason;expr}
|
||||
| EC_neq {l;_} ->
|
||||
(* check if compatible *)
|
||||
List.iter
|
||||
(fun (n2, expr2, reason_neq) ->
|
||||
if Q.equal num n2 then (
|
||||
(* conflict *)
|
||||
assert (Atom.is_true reason_neq);
|
||||
raise_conflict acts ~pivot:t ~op:Eq0 ~sign:false
|
||||
~expr_up_bound:expr ~expr_low_bound:expr2 ~reasons:[reason_neq; reason] ()
|
||||
))
|
||||
l;
|
||||
(* erase *)
|
||||
s.eq <- EC_eq {num;reason;expr}
|
||||
| EC_eq eq ->
|
||||
if Q.equal eq.num num then (
|
||||
() (* do nothing *)
|
||||
) else (
|
||||
(* conflict *)
|
||||
raise_conflict acts ~sign:true
|
||||
~pivot:t ~expr_up_bound:expr ~expr_low_bound:eq.expr ~op:Eq0
|
||||
~reasons:[reason;eq.reason] ()
|
||||
)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* add forbidden value *)
|
||||
let add_neq acts t num ~expr ~reason : unit = match Term.decide_state_exn t with
|
||||
| State s ->
|
||||
let old_b = s.eq in
|
||||
Actions.on_backtrack acts (fun () -> s.eq <- old_b);
|
||||
begin match s.eq with
|
||||
| EC_none ->
|
||||
s.eq <- EC_neq {l=[num,expr,reason]};
|
||||
check_tight_bound acts t;
|
||||
| EC_neq neq ->
|
||||
(* just add constraint, if not redundant *)
|
||||
if not (List.exists (fun (n,_,_) -> Q.equal n num) neq.l) then (
|
||||
s.eq <- EC_neq {l=(num,expr,reason) :: neq.l};
|
||||
check_tight_bound acts t;
|
||||
)
|
||||
| EC_eq eq ->
|
||||
(* check if compatible *)
|
||||
if Q.equal eq.num num then (
|
||||
(* conflict *)
|
||||
raise_conflict acts
|
||||
~pivot:t ~sign:false ~op:Eq0
|
||||
~expr_up_bound:expr ~expr_low_bound:eq.expr
|
||||
~reasons:[eq.reason;reason] ()
|
||||
)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* add a unit constraint to [t]. The constraint is [reason],
|
||||
which is valued to [b] *)
|
||||
let add_unit_constr acts op expr (t:term) ~(reason:atom) (b:bool) : unit =
|
||||
assert (t != Atom.term reason);
|
||||
let constr, expr, num = constr_of_unit op expr t b in
|
||||
(* look into existing constraints *)
|
||||
Log.debugf 10
|
||||
(fun k->k"(@[<hv>lra.add_unit_constr@ :term %a@ :constr @[%a %a@] \
|
||||
@ :reason %a@ :expr %a@ :cur-state %a@])"
|
||||
Term.debug t pp_constr constr Q.pp_print num Atom.debug reason
|
||||
LE.pp expr pp_state (Term.decide_state_exn t));
|
||||
(* update, depending on the kind of constraint [reason] is *)
|
||||
begin match constr with
|
||||
| C_leq -> add_up acts ~strict:false t num ~expr ~reason
|
||||
| C_lt -> add_up acts ~strict:true t num ~expr ~reason
|
||||
| C_geq -> add_low acts ~strict:false t num ~expr ~reason
|
||||
| C_gt -> add_low acts ~strict:true t num ~expr ~reason
|
||||
| C_eq -> add_eq acts t num ~expr ~reason
|
||||
| C_neq -> add_neq acts t num ~expr ~reason
|
||||
end
|
||||
|
||||
(* [t] should evaluate or propagate. Add constraint to its state or
|
||||
propagate *)
|
||||
let check_consistent _acts (t:term) : unit = match Term.view t with
|
||||
| Const _ -> ()
|
||||
| Pred _ ->
|
||||
(* check consistency *)
|
||||
begin match eval t, Term.value t with
|
||||
| Eval_into (V_true,_), Some V_true
|
||||
| Eval_into (V_false,_), Some V_false -> ()
|
||||
| Eval_into (V_false,subs), Some V_true
|
||||
| Eval_into (V_true,subs), Some V_false ->
|
||||
Util.errorf "inconsistency in lra: %a@ :subs (@[%a@])"
|
||||
Term.debug t (Util.pp_list Term.debug) subs
|
||||
| Eval_unknown, _ ->
|
||||
Util.errorf "inconsistency in lra: %a@ does-not-eval"
|
||||
Term.debug t
|
||||
| Eval_into _, _ -> assert false (* non boolean! *)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* [u] is [t] or one of its subterms. All the other watches are up-to-date,
|
||||
so we can add a constraint or even propagate [t] *)
|
||||
let check_or_propagate acts (t:term) ~(u:term) : unit = match Term.view t with
|
||||
| Const _ -> ()
|
||||
| Pred p ->
|
||||
begin match Term.value t with
|
||||
| None ->
|
||||
(* term not assigned, means all subterms are. We can evaluate *)
|
||||
assert (t == u);
|
||||
assert (LE.terms p.expr |> Iter.for_all Term.has_some_value);
|
||||
begin match eval_le p.expr with
|
||||
| None -> assert false
|
||||
| Some (n,subs) ->
|
||||
let v = eval_bool_const p.op n in
|
||||
Actions.propagate_bool_eval acts t v ~subs
|
||||
end
|
||||
| Some V_true ->
|
||||
assert (t != u);
|
||||
add_unit_constr acts p.op p.expr u ~reason:(Term.Bool.pa t) true
|
||||
| Some V_false ->
|
||||
assert (t != u);
|
||||
add_unit_constr acts p.op p.expr u ~reason:(Term.Bool.na t) false
|
||||
| Some _ -> assert false
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
let init acts t : unit = match Term.view t with
|
||||
| Const _ -> ()
|
||||
| Pred p ->
|
||||
let watches = Term.Watch2.make (t :: LE.terms_l p.expr) in
|
||||
p.watches <- watches;
|
||||
Term.Watch2.init p.watches t
|
||||
~on_unit:(fun u -> check_or_propagate acts t ~u)
|
||||
~on_all_set:(fun () -> check_consistent acts t)
|
||||
| _ -> assert false
|
||||
|
||||
let update_watches acts t ~watch : watch_res = match Term.view t with
|
||||
| Pred p ->
|
||||
Term.Watch2.update p.watches t ~watch
|
||||
~on_unit:(fun u -> check_or_propagate acts t ~u)
|
||||
~on_all_set:(fun () -> check_consistent acts t)
|
||||
| Const _ -> assert false
|
||||
| _ -> assert false
|
||||
|
||||
let mk_eq t u = mk_pred Eq0 (LE.singleton1 t -.. LE.singleton1 u)
|
||||
|
||||
(* can [t] be equal to [v] consistently with unit constraints? *)
|
||||
let can_be_eq (t:term) (n:num) : bool = match Term.decide_state_exn t with
|
||||
| State r ->
|
||||
begin match r.eq with
|
||||
| EC_none -> true
|
||||
| EC_eq {num;_} -> Q.equal num n
|
||||
| EC_neq {l} ->
|
||||
List.for_all (fun (num,_,_) -> not (Q.equal num n)) l
|
||||
end
|
||||
&&
|
||||
begin match r.low with
|
||||
| B_none -> true
|
||||
| B_some {num;strict;_} ->
|
||||
(strict && Q.compare num n < 0) ||
|
||||
(not strict && Q.compare num n <= 0)
|
||||
end
|
||||
&&
|
||||
begin match r.up with
|
||||
| B_none -> true
|
||||
| B_some {num;strict;_} ->
|
||||
(strict && Q.compare num n > 0) ||
|
||||
(not strict && Q.compare num n >= 0)
|
||||
end
|
||||
| _ -> assert false
|
||||
|
||||
(* find a feasible value for [t] *)
|
||||
let find_val (t:term) : num =
|
||||
let sufficiently_large ~n forbid =
|
||||
List.fold_left Q.max n forbid |> Q.add Q.one
|
||||
and sufficiently_small ~n forbid =
|
||||
List.fold_left Q.min n forbid |> Q.add Q.minus_one
|
||||
in
|
||||
(* find an element of [)a,b(] that doesn't belong in [forbid] *)
|
||||
let rec find_between a b forbid =
|
||||
(* (a+b)/2 *)
|
||||
let mid = Q.div_2exp (Q.add a b) 1 in
|
||||
if CCList.mem ~eq:Q.equal mid forbid
|
||||
then find_between a mid forbid
|
||||
else mid
|
||||
in
|
||||
begin match Term.decide_state_exn t with
|
||||
| State r ->
|
||||
begin match r.eq with
|
||||
| EC_eq {num;_} -> num
|
||||
| _ ->
|
||||
let forbid = match r.eq with
|
||||
| EC_eq _ -> assert false
|
||||
| EC_neq {l;_} -> List.map (fun (n,_,_) -> n) l
|
||||
| EC_none -> []
|
||||
in
|
||||
begin match r.low, r.up with
|
||||
| B_none, B_none -> sufficiently_large ~n:Q.zero forbid
|
||||
| B_some {num;_}, B_none -> sufficiently_large ~n:num forbid
|
||||
| B_none, B_some {num;_} -> sufficiently_small ~n:num forbid
|
||||
| B_some low, B_some up when Q.equal low.num up.num ->
|
||||
(* tight bounds, [n ≤ t ≤ n] *)
|
||||
assert (not low.strict && not up.strict);
|
||||
assert (not (CCList.mem ~eq:Q.equal low.num forbid));
|
||||
low.num
|
||||
| B_some low, B_some up ->
|
||||
assert (Q.compare low.num up.num < 0);
|
||||
find_between low.num up.num forbid
|
||||
end
|
||||
end
|
||||
| _ -> assert false
|
||||
end
|
||||
|
||||
(* decision, according to current constraints *)
|
||||
let decide _ (t:term) : value = match Term.decide_state_exn t with
|
||||
| State r as st ->
|
||||
let n =
|
||||
if can_be_eq t r.last_val then r.last_val
|
||||
else find_val t
|
||||
in
|
||||
Log.debugf 30
|
||||
(fun k->k"(@[<hv>lra.decide@ %a := %a@ :state %a@])"
|
||||
Term.debug t Q.pp_print n pp_state st);
|
||||
assert (can_be_eq t n);
|
||||
r.last_val <- n; (* save *)
|
||||
mk_val n
|
||||
| _ -> assert false
|
||||
|
||||
let () =
|
||||
Term.TC.lazy_complete tc_t
|
||||
~init ~update_watches ~subterms ~eval ~pp:pp_term;
|
||||
Type.TC.lazy_complete tc_ty
|
||||
~pp:pp_ty ~decide ~eq:mk_eq ~mk_state;
|
||||
()
|
||||
|
||||
let provided_services = [
|
||||
Service.Any (k_rat, Lazy.force ty_rat);
|
||||
Service.Any (k_make_const, mk_const);
|
||||
Service.Any (k_make_pred, mk_pred);
|
||||
]
|
||||
end in
|
||||
(module P)
|
||||
|
||||
let plugin : Plugin.Factory.t =
|
||||
Plugin.Factory.make ~priority:12 ~name ~build
|
||||
~requires:Plugin.(K_cons (Builtins.k_true, K_cons (Builtins.k_false,K_nil)))
|
||||
()
|
||||
*)
|
||||
|
||||
type pred = Lt | Leq | Eq | Neq | Geq | Gt
|
||||
type op = Plus | Minus
|
||||
|
||||
|
|
@ -680,6 +13,7 @@ type 'a lra_view =
|
|||
| LRA_pred of pred * 'a * 'a
|
||||
| LRA_op of op * 'a * 'a
|
||||
| LRA_const of Q.t
|
||||
| LRA_other of 'a
|
||||
|
||||
module type ARG = sig
|
||||
module S : Sidekick_core.SOLVER
|
||||
|
|
@ -689,7 +23,7 @@ module type ARG = sig
|
|||
val view_as_lra : term -> term lra_view
|
||||
(** Project the term into the theory view *)
|
||||
|
||||
val mk_bool : S.T.Term.state -> term lra_view -> term
|
||||
val mk_lra : S.T.Term.state -> term lra_view -> term
|
||||
(** Make a term from the given theory view *)
|
||||
|
||||
module Gensym : sig
|
||||
|
|
@ -719,24 +53,31 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
module Lit = A.S.Solver_internal.Lit
|
||||
module SI = A.S.Solver_internal
|
||||
|
||||
module Simplex = Funarith_zarith.Simplex.Make_full(struct
|
||||
type t =
|
||||
| Fresh of int
|
||||
| T of T.t
|
||||
let compare a b =
|
||||
match a, b with
|
||||
| Fresh i, Fresh j -> CCInt.compare i j
|
||||
| Fresh _, T _ -> -1
|
||||
| T _, Fresh _ -> 1
|
||||
| T t1, T t2 -> T.compare t1 t2
|
||||
let pp out = function
|
||||
| Fresh i -> Fmt.fprintf out "$fresh_%d" i
|
||||
| T t -> T.pp out t
|
||||
module Fresh = struct
|
||||
include A.Gensym
|
||||
let fresh = fresh_term
|
||||
end
|
||||
end)
|
||||
type simp_var =
|
||||
| V_fresh of int
|
||||
| V_t of T.t
|
||||
|
||||
(** Simplex variables *)
|
||||
module Simp_vars = struct
|
||||
type t = simp_var
|
||||
let compare a b =
|
||||
match a, b with
|
||||
| V_fresh i, V_fresh j -> CCInt.compare i j
|
||||
| V_fresh _, V_t _ -> -1
|
||||
| V_t _, V_fresh _ -> 1
|
||||
| V_t t1, V_t t2 -> T.compare t1 t2
|
||||
let pp out = function
|
||||
| V_fresh i -> Fmt.fprintf out "$fresh_%d" i
|
||||
| V_t t -> T.pp out t
|
||||
module Fresh = struct
|
||||
type t = int ref
|
||||
let create() : t = ref 0
|
||||
let fresh n = V_fresh (CCRef.get_then_incr n)
|
||||
end
|
||||
end
|
||||
|
||||
module Simplex = Funarith_zarith.Simplex.Make_full(Simp_vars)
|
||||
module LE = Simplex.L.Expr
|
||||
|
||||
type state = {
|
||||
tst: T.state;
|
||||
|
|
@ -750,7 +91,7 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
gensym=A.Gensym.create tst;
|
||||
simplex=Simplex.create();
|
||||
}
|
||||
|
||||
|
||||
(* FIXME
|
||||
let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
|
||||
let tst = self.tst in
|
||||
|
|
@ -800,18 +141,53 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
let t = fresh_term ~pre self Ty.bool in
|
||||
mk_lit t
|
||||
|
||||
(* preprocess "ite" away *)
|
||||
let preproc_ite self _si ~mk_lit ~add_clause (t:T.t) : T.t option =
|
||||
match A.view_as_bool t with
|
||||
(* turn the term into a linear expression *)
|
||||
let rec as_linexp (t:T.t) : LE.t =
|
||||
let open LE.Infix in
|
||||
match A.view_as_lra t with
|
||||
| LRA_other _ -> LE.of_list Q.zero [Q.one, V_t t]
|
||||
| LRA_pred _ ->
|
||||
Error.errorf "type error: in linexp, LRA predicate %a" T.pp t
|
||||
| LRA_op (op, t1, t2) ->
|
||||
let t1 = as_linexp t1 in
|
||||
let t2 = as_linexp t2 in
|
||||
begin match op with
|
||||
| Plus -> t1 + t2
|
||||
| Minus -> t1 - t2
|
||||
end
|
||||
| LRA_const q -> LE.of_const q
|
||||
|
||||
(* preprocess linear expressions away *)
|
||||
let preproc_lra self si ~mk_lit ~add_clause (t:T.t) : T.t option =
|
||||
let tst = SI.tst si in
|
||||
match A.view_as_lra t with
|
||||
| LRA_pred (_pre, _t1, _t2) ->
|
||||
assert false (* TODO: define a bool variable *)
|
||||
| LRA_op _ | LRA_const _ ->
|
||||
let le = as_linexp t in
|
||||
let proxy = fresh_term self ~pre:"lra" (T.ty t) in
|
||||
Simplex.add_eq self.simplex (V_t proxy, []); (* TODO add LE *)
|
||||
(* TODO: useless?
|
||||
add_clause [
|
||||
mk_lit
|
||||
(A.mk_lra tst
|
||||
(LRA_pred (Eq, le, Simplex.L.Comb.monomial1 (V_t proxy))))
|
||||
];
|
||||
*)
|
||||
Some proxy
|
||||
(*
|
||||
| B_ite (a,b,c) ->
|
||||
let t_a = fresh_term self ~pre:"ite" (T.ty b) in
|
||||
let lit_a = mk_lit a in
|
||||
add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
|
||||
add_clause [lit_a; mk_lit (eq self.tst t_a c)];
|
||||
Some t_a
|
||||
| _ -> None
|
||||
*)
|
||||
| LRA_const _ ->
|
||||
assert false (* TODO: turn into linexp *)
|
||||
| LRA_other _ -> None
|
||||
|
||||
(* TODO: polarity? *)
|
||||
(* TODO: remove
|
||||
let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
|
||||
let rec get_lit (t:T.t) : Lit.t =
|
||||
let t_abs, t_sign = T.abs self.tst t in
|
||||
|
|
@ -872,6 +248,7 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
(* put sign back as a "not" *)
|
||||
let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
|
||||
if T.equal u t then None else Some u
|
||||
*)
|
||||
|
||||
(* check if new terms were added to the congruence closure, that can be turned
|
||||
into clauses *)
|
||||
|
|
@ -893,7 +270,7 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
| None -> ()
|
||||
| Some u ->
|
||||
Log.debugf 5
|
||||
(fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
|
||||
(fun k->k "(@[th-lra.final-check.cnf@ %a@ :yields %a@])"
|
||||
T.pp t T.pp u);
|
||||
SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
|
||||
());
|
||||
|
|
@ -901,20 +278,17 @@ module Make(A : ARG) : S with module A = A = struct
|
|||
()
|
||||
|
||||
let create_and_setup si =
|
||||
Log.debug 2 "(th-bool.setup)";
|
||||
Log.debug 2 "(th-lra.setup)";
|
||||
let st = create (SI.tst si) in
|
||||
SI.add_simplifier si (simplify st);
|
||||
SI.add_preprocess si (preproc_ite st);
|
||||
SI.add_preprocess si (cnf st);
|
||||
if A.check_congruence_classes then (
|
||||
Log.debug 5 "(th-bool.add-final-check)";
|
||||
SI.on_final_check si (check_new_terms st);
|
||||
);
|
||||
(* TODO SI.add_simplifier si (simplify st); *)
|
||||
SI.add_preprocess si (preproc_lra st);
|
||||
(* SI.add_preprocess si (cnf st); *)
|
||||
(* TODO: theory combination *)
|
||||
st
|
||||
|
||||
let theory =
|
||||
A.S.mk_theory
|
||||
~name:"th-bool"
|
||||
~name:"th-lra"
|
||||
~create_and_setup
|
||||
()
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
|
||||
(library
|
||||
(name sidekick_lra)
|
||||
(public_name sidekick.lra)
|
||||
(public_name sidekick.th-lra)
|
||||
(optional) ; only if deps present
|
||||
(flags :standard -open Sidekick_util)
|
||||
(libraries containers sidekick.core zarith funarith.zarith funarith))
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue