[LRA] Add fourier-moskin algorithm for comparisons

  - deduce only contradiction

src_colibri2/core/datastructure.ml

@@ -224,3 +224,27 @@ module Queue = struct
 
 
 end
+
+module Ref = struct
+
+  type 'a t = 'a Context.Ref.t Env.Unsaved.t
+
+  let create : type a. a Colibri2_popop_lib.Pp.pp -> _ -> a -> a t = fun pp name v ->
+    let module M = struct
+      type t = a Context.Ref.t
+      let name = name end
+    in
+    let key = Env.Unsaved.create_key (module M) in
+    let init d = Context.Ref.create d v in
+    let pp = Context.Ref.pp pp in
+    Env.Unsaved.register ~init ~pp key;
+    key
+
+  let get t d = Context.Ref.get (Egraph.get_unsaved_env d t)
+  let set t d v = Context.Ref.set (Egraph.get_unsaved_env d t) v
+
+  module Ro = struct
+    let get t d = Context.Ref.get (Egraph.Ro.get_unsaved_env d t)
+    let set t d v = Context.Ref.set (Egraph.Ro.get_unsaved_env d t) v
+  end
+end

src_colibri2/core/datastructure.mli

@@ -69,3 +69,14 @@ module Queue: sig
   val fold: f:('acc -> 'a -> 'acc) ->  init:'acc -> 'a t -> Egraph.t -> 'acc
 
 end
+
+module Ref: sig
+  type 'a t
+  val create: 'a Fmt.t -> string -> 'a -> 'a t
+  val get: 'a t -> Egraph.t -> 'a
+  val set: 'a t -> Egraph.t -> 'a -> unit
+  module Ro: sig
+    val get: 'a t -> Egraph.Ro.t -> 'a
+    val set: 'a t -> Egraph.Ro.t -> 'a -> unit
+  end
+end

src_colibri2/tests/solve/smt_lra/sat/dune.inc

@@ -43,6 +43,10 @@
 (rule (alias runtest) (action (diff oracle attach_only_when_dom_present.smt2.res)))
 (rule (action (with-stdout-to init_not_repr.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:init_not_repr.smt2}))))
 (rule (alias runtest) (action (diff oracle init_not_repr.smt2.res)))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:le.smt2}))))
+(rule (alias runtest) (action (diff oracle le.smt2.res)))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:le2.smt2}))))
+(rule (alias runtest) (action (diff oracle le2.smt2.res)))
 (rule (action (with-stdout-to mul.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:mul.smt2}))))
 (rule (alias runtest) (action (diff oracle mul.smt2.res)))
 (rule (action (with-stdout-to sem_invariant_in_learnt_dec.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:sem_invariant_in_learnt_dec.smt2}))))

src_colibri2/tests/solve/smt_lra/sat/le.smt2

+(set-logic ALL)
+
+(declare-fun a () Int)
+
+(assert (<= a (+ a 1)))
+
+(check-sat)

src_colibri2/tests/solve/smt_lra/sat/le2.smt2

+(set-logic ALL)
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (<= a b))
+(assert (<= b a))
+
+(check-sat)

src_colibri2/tests/solve/smt_lra/unsat/dune.inc

@@ -3,6 +3,10 @@
 (rule (alias runtest) (action (diff oracle arith_ExpMult_by_zero.smt2.res)))
 (rule (action (with-stdout-to arith_merge_case2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:arith_merge_case2.smt2}))))
 (rule (alias runtest) (action (diff oracle arith_merge_case2.smt2.res)))
+(rule (action (with-stdout-to le.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:le.smt2}))))
+(rule (alias runtest) (action (diff oracle le.smt2.res)))
+(rule (action (with-stdout-to le2.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:le2.smt2}))))
+(rule (alias runtest) (action (diff oracle le2.smt2.res)))
 (rule (action (with-stdout-to solver_merge_itself_repr_empty.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_merge_itself_repr_empty.smt2}))))
 (rule (alias runtest) (action (diff oracle solver_merge_itself_repr_empty.smt2.res)))
 (rule (action (with-stdout-to solver_set_sem_merge_sign.smt2.res (run %{bin:colibri2} --max-step 1000 %{dep:solver_set_sem_merge_sign.smt2}))))

src_colibri2/tests/solve/smt_lra/unsat/le.smt2

+(set-logic ALL)
+
+(declare-fun a () Int)
+
+(assert (<= (+ a 1) a))
+
+(check-sat)

src_colibri2/tests/solve/smt_lra/unsat/le2.smt2

+(set-logic ALL)
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+(assert (<= a b))
+(assert (< b a))
+
+(check-sat)

src_colibri2/theories/LRA/LRA.ml

@@ -59,7 +59,9 @@ module RealValue = RealValue
 let th_register env =
   Dom_interval.init env;
   Dom_polynome.init env;
-  RealValue.init env
+  RealValue.init env;
+  Fourier.init env;
+  ()
 
 let () = Egraph.add_default_theory th_register
 

src_colibri2/theories/LRA/fourier.ml

+open Colibri2_popop_lib
+open Colibri2_core
+
+let comparisons = Datastructure.Queue.create Ground.pp "LRA.fourier.comparisons"
+let scheduled = Datastructure.Ref.create Bool.pp "LRA.fourier.scheduled" false
+
+let debug = Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
+
+type eq = { p: Polynome.t; bound: Interval.Bound.t }
+(** p <= 0 or p < 0 *)
+
+let add_eq d eqs p bound =
+  match Polynome.is_cst p, bound with
+  | None, _ -> { p; bound }::eqs
+  | Some p, Interval.Bound.Large when Q.sign p <= 0 -> eqs
+  | Some p, Interval.Bound.Strict when Q.sign p < 0 -> eqs
+  | _ -> Egraph.contradiction d
+
+let mk_eq d bound truth a b =
+  let (!) n =
+    match Egraph.get_dom d Dom_polynome.dom_poly n with
+    | None -> Polynome.monome Q.one n
+    | Some p -> p in
+  let bound = if truth then bound else match bound with | Interval.Bound.Large -> Strict | Strict -> Large in
+  let a,b = if truth then a,b else b,a in
+  Polynome.sub (!a) (!b), bound
+
+let fm (d:Egraph.t) =
+  Debug.dprintf0 debug "[Fourier]";
+  Datastructure.Ref.set scheduled d false;
+  let eqs, vars = Datastructure.Queue.fold comparisons d
+      ~f:(fun (eqs,vars) g ->
+          match Boolean.is d (Ground.node g) with
+          | None -> (eqs,vars)
+          | Some truth ->
+          let p,bound =
+            match Ground.sem g with
+            | { app = {builtin = Expr.Lt}; tyargs = []; args = [a;b]; _ } ->
+              mk_eq d Strict truth a b
+            | { app = {builtin = Expr.Leq}; tyargs = []; args = [a;b]; _ } ->
+              mk_eq d Large truth a b
+            | { app = {builtin = Expr.Geq}; tyargs = []; args = [a;b]; _ } ->
+              mk_eq d Large truth b a
+            | { app = {builtin = Expr.Gt}; tyargs = []; args = [a;b]; _ } ->
+              mk_eq d Strict truth b a
+            | _ -> assert false
+          in
+          (add_eq d eqs p bound,Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly)
+        ) ~init:([],Node.S.empty)
+  in
+  let rec split n positive negative absent = function
+    | [] -> (positive,negative,absent)
+    | eq::l ->
+      match Node.M.find_opt n eq.p.poly with
+      | None -> split n positive negative (eq::absent) l
+      | Some q ->
+        if Q.sign q > 0 then
+          split n ((q,eq)::positive) negative absent l
+        else split n positive ((q,eq)::negative) absent l
+  in
+  let rec aux eqs vars =
+    match Node.S.choose vars with
+    | exception Not_found -> ()
+    | n ->
+      let vars = Node.S.remove n vars in
+      let positive, negative, absent = split n [] [] [] eqs in
+      match positive, negative with
+      | [], _ | _ , [] -> aux absent vars
+      | _, _ ->
+        let eqs =
+          Lists.fold_product (fun eqs (pq,peq) (nq,neq) ->
+              let q = Q.div pq (Q.abs nq) in
+              let p = Polynome.cx_p_cy Q.one peq.p q neq.p in
+              let bound =
+                match peq.bound, neq.bound with
+                | Large, Large -> Interval.Bound.Large
+                | _ -> Interval.Bound.Strict in
+              add_eq d eqs p bound
+            ) absent positive negative
+        in
+        aux eqs vars
+  in
+  aux eqs vars
+
+module Daemon = struct
+  type event = unit
+
+  let print_event = Unit.pp
+
+  let enqueue d _ =
+    if Datastructure.Ref.Ro.get scheduled d
+    then Events.Wait.EnqAlready
+    else begin
+      Datastructure.Ref.Ro.set scheduled d true;
+      Events.Wait.EnqRun ()
+    end
+
+  let key =
+    Events.Dem.create_key
+      ( module struct
+        type d = unit
+        type t = unit
+        let name = "LRA.fourier"
+      end )
+
+  let delay = Events.Delayed_by 64
+
+  type runable = unit
+
+  let print_runable = Unit.pp
+
+  let run d () = fm d; None
+end
+
+let () = Egraph.Wait.register_dem (module Daemon)
+
+
+(** {2 Initialization} *)
+let converter d (f:Ground.t) =
+  match Ground.sem f with
+  | { app = {builtin = (Expr.Lt|Expr.Leq|Expr.Geq|Expr.Gt)}; tyargs = []; args } ->
+    let attach n = Egraph.attach_dom d n Dom_polynome.dom_poly Daemon.key () in
+    List.iter attach args;
+    Egraph.attach_value d (Ground.node f) RealValue.key Daemon.key ();
+    Datastructure.Queue.push comparisons d f;
+    Egraph.register_delayed_event d Daemon.key ()
+  | _ -> ()
+
+let init env =
+  Ground.register_converter env converter

src_colibri2/theories/LRA/fourier.mli

+val init: Egraph.t -> unit