From 40d47a8d6cde18d04731195d69dbbececbf9e1ed Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 26 Feb 2020 09:04:38 -0600 Subject: [PATCH] wip: lra --- src/main/main.ml | 1 + src/smtlib/Process.ml | 7 + src/smtlib/Process.mli | 1 + src/th-lra/Sidekick_lra.ml | 778 ++++--------------------------------- src/th-lra/dune | 3 +- 5 files changed, 87 insertions(+), 703 deletions(-) diff --git a/src/main/main.ml b/src/main/main.ml index 12b57e49..001d8330 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -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 () diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 19e2c274..180a55a7 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -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 diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli index ec8a2084..2ffb0392 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Process.mli @@ -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 diff --git a/src/th-lra/Sidekick_lra.ml b/src/th-lra/Sidekick_lra.ml index 656df4a3..f323b4bf 100644 --- a/src/th-lra/Sidekick_lra.ml +++ b/src/th-lra/Sidekick_lra.ml @@ -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 "(@[!=@ %a@])" - (Util.pp_list pp_tuple) l - -let pp_state out = function - | State s -> - Fmt.fprintf out "(@[: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 - "(@[lra.raise_conflict@ :pivot %a@ :expr %a %a@ \ - :e_up_b %a@ :e_low_b %a@ \ - :reasons (@[%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 - "(@[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"(@[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"(@[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 diff --git a/src/th-lra/dune b/src/th-lra/dune index 8c1c7811..ffcbc4c5 100644 --- a/src/th-lra/dune +++ b/src/th-lra/dune @@ -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))