From 9cf9b1f8b9f70ec3a9b0afa4130e530107490e5f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 18 Nov 2021 09:56:42 +0100
Subject: [PATCH] Propagate distances between nodes that are between -1 < . < 1
---
src_colibri2/core/colibri2_core.mli | 6 +-
src_colibri2/core/egraph.ml | 8 +-
src_colibri2/core/ground.ml | 3 +-
src_colibri2/core/interp.ml | 9 +-
src_colibri2/popop_lib/debug.ml | 16 +-
src_colibri2/popop_lib/debug.mli | 5 +-
src_colibri2/popop_lib/exthtbl.ml | 28 +
src_colibri2/popop_lib/exthtbl.mli | 10 +-
src_colibri2/popop_lib/unit.ml | 4 +
src_colibri2/solver/scheduler.ml | 22 +-
.../solve/all/unsat/ordered_is_ordered.psmt2 | 2 +-
src_colibri2/theories/LRA/LRA.ml | 127 +---
src_colibri2/theories/LRA/LRA_build.ml | 144 +++++
src_colibri2/theories/LRA/dom_interval.ml | 2 +-
src_colibri2/theories/LRA/fourier.ml | 27 +-
src_colibri2/theories/LRA/polynome.ml | 53 +-
src_colibri2/theories/LRA/polynome.mli | 4 +
src_colibri2/theories/LRA/simplex.ml | 610 ++++++++++--------
src_colibri2/theories/LRA/stages/bound.ml | 17 +-
.../theories/LRA/stages/stage1/interval.ml | 83 ++-
src_colibri2/theories/bool/equality.ml | 88 ++-
src_colibri2/theories/quantifier/common.ml | 11 +-
22 files changed, 737 insertions(+), 542 deletions(-)
create mode 100644 src_colibri2/theories/LRA/LRA_build.ml
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index bb76702dc..8743ba99b 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -1639,7 +1639,11 @@ module Debug : sig
type 'a stat
- val register_stats_int : name:string -> init:int -> int stat
+ val register_stats_int : string -> int stat
+
+ val register_stats_time : string -> float stat
+
+ val add_time_during : float stat -> (unit -> 'a) -> 'a
val incr : int stat -> unit
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 6b62164f9..a38171f0a 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -35,14 +35,14 @@ let debug_few = Debug.register_info_flag
"Egraph.few"
let print_decision = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
-let print_contradiction = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ contradiction@ found" "contradiction"
+let print_contradiction = Colibri2_popop_lib.Debug.register_info_flag ~desc:"Print@ information@ about@ the@ contradiction@ found" "contradiction"
let stats_set_dom =
- Debug.register_stats_int ~name:"Egraph.set_dom/merge" ~init:0
+ Debug.register_stats_int "Egraph.set_dom/merge"
let stats_set_value =
- Debug.register_stats_int ~name:"Egraph.set_value/merge" ~init:0
+ Debug.register_stats_int "Egraph.set_value/merge"
let stats_register =
- Debug.register_stats_int ~name:"Egraph.register" ~init:0
+ Debug.register_stats_int "Egraph.register"
module DecTag = DInt
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 0207576f9..542493908 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -495,8 +495,7 @@ module Defs = struct
(** Maximum level where the terms can be directly decided *)
let level_dec = 0
- let stats_function_call =
- Debug.register_stats_int ~name:"Ground.function_call" ~init:0
+ let stats_function_call = Debug.register_stats_int "Ground.function_call"
let converter d (v : ThTerm.t) =
let level = Option.value ~default:0 (ThTermH.find_opt levels d v) in
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index 4dffec901..5efc717d7 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -232,9 +232,12 @@ let node d n =
raise exn
| Some th -> (
match Ground.of_thterm th with
- | None ->
- Fmt.epr "@.%a does not have type@." Node.pp n';
- raise exn
+ | None -> (
+ match Ground.ClosedQuantifier.of_thterm th with
+ | None ->
+ Fmt.epr "@.%a does not have type@." Node.pp n';
+ raise exn
+ | Some _ -> ty (Egraph.ro d) Ground.Ty.bool)
| Some g -> ty (Egraph.ro d) (Ground.sem g).ty)
else ty (Egraph.ro d) (Ground.Ty.S.choose (Ground.tys d n'))
in
diff --git a/src_colibri2/popop_lib/debug.ml b/src_colibri2/popop_lib/debug.ml
index 8fb130466..77d4bba8f 100644
--- a/src_colibri2/popop_lib/debug.ml
+++ b/src_colibri2/popop_lib/debug.ml
@@ -299,9 +299,21 @@ let modstats1 r f x =
let modstats2 r f x y =
if test_flag stats then r := f !r x y
-let register_stats_int ~name ~init =
- register_stats ~pp:Format.pp_print_int ~name ~init
+let register_stats_int name =
+ register_stats ~pp:Format.pp_print_int ~name ~init:0
+
+let register_stats_time name =
+ register_stats ~pp:(fun fmt f -> Format.fprintf fmt "%.2fs" f) ~name ~init:0.
let incr r = if test_flag stats then incr r
let decr r = if test_flag stats then decr r
+let add_time_during r f =
+ let gettime () = (Unix.times ()).tms_utime in
+ if test_flag stats then
+ let pre = gettime () in
+ Fun.protect f ~finally:(fun () ->
+ let post = gettime () in
+ r := !r +. (post -. pre)
+ )
+ else f ()
diff --git a/src_colibri2/popop_lib/debug.mli b/src_colibri2/popop_lib/debug.mli
index 54cbd4d25..b709f967f 100644
--- a/src_colibri2/popop_lib/debug.mli
+++ b/src_colibri2/popop_lib/debug.mli
@@ -197,8 +197,11 @@ val modstats0: 'a stat -> ('a -> 'a) -> unit
val modstats1: 'a stat -> ('a -> 'b -> 'a) -> 'b -> unit
val modstats2: 'a stat -> ('a -> 'b -> 'c -> 'a) -> 'b -> 'c -> unit
-val register_stats_int: name:string -> init:int -> int stat
+val register_stats_int: string -> int stat
+val register_stats_time: string -> float stat
val incr: int stat -> unit
val decr: int stat -> unit
+val add_time_during: float stat -> (unit -> 'a) -> 'a
+
val print_stats: unit -> unit
diff --git a/src_colibri2/popop_lib/exthtbl.ml b/src_colibri2/popop_lib/exthtbl.ml
index d6931d37a..79e10417d 100644
--- a/src_colibri2/popop_lib/exthtbl.ml
+++ b/src_colibri2/popop_lib/exthtbl.ml
@@ -90,7 +90,9 @@ module type S =
val find_def : 'a t -> 'a -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_exn : 'a t -> exn -> key -> 'a
+ val choose : 'a t -> (key * 'a) option
val mapi : (key -> 'a -> 'a) -> 'a t -> unit
+ val filter_mapi : (key -> 'a -> 'a option) -> 'a t -> unit
val memo : (key -> 'a) -> 'a t -> key -> 'a
val is_empty : 'a t -> bool
val remove_all: 'a t -> key -> unit
@@ -345,6 +347,18 @@ module MakeSeeded(H: SeededHashedType) =
done;
!accu
+ let choose h =
+ let rec iter d i =
+ if i < 0 then None
+ else
+ match d.(i) with
+ | Empty ->
+ iter d (i-1)
+ | Cons(k, d, _) ->
+ Some (k,d);
+ in
+ let d = h.data in
+ iter d (Array.length d - 1)
let mapi f h =
let rec do_bucket f b =
@@ -357,6 +371,20 @@ module MakeSeeded(H: SeededHashedType) =
d.(i) <- do_bucket f d.(i)
done
+ let filter_mapi f h =
+ let rec do_bucket f b =
+ match b with
+ Empty -> Empty
+ | Cons(k, d, rest) ->
+ (match f k d with
+ | None -> h.size <- h.size - 1; do_bucket f rest
+ | Some v ->
+ Cons(k, v, do_bucket f rest)) in
+ let d = h.data in
+ for i = 0 to Array.length d - 1 do
+ d.(i) <- do_bucket f d.(i)
+ done
+
let length h = h.size
let rec bucket_length accu = function
diff --git a/src_colibri2/popop_lib/exthtbl.mli b/src_colibri2/popop_lib/exthtbl.mli
index 2ef0e7bbc..8f1e3b009 100644
--- a/src_colibri2/popop_lib/exthtbl.mli
+++ b/src_colibri2/popop_lib/exthtbl.mli
@@ -94,9 +94,15 @@ module type S =
val find_exn : 'a t -> exn -> key -> 'a
(** return the first binding or raise the given exception if none found *)
+ val choose : 'a t -> (key * 'a) option
+
val mapi : (key -> 'a -> 'a) -> 'a t -> unit
- (** change the value of all the key,
- don't modify the table during this run *)
+ (** change the value of all the key.
+ The table should not be modified externally during this run *)
+
+ val filter_mapi : (key -> 'a -> 'a option) -> 'a t -> unit
+ (** change the value of all the key.
+ The table should not be modified externally during this run *)
val memo : (key -> 'a) -> 'a t -> key -> 'a
(** convenience function, memoize a function *)
diff --git a/src_colibri2/popop_lib/unit.ml b/src_colibri2/popop_lib/unit.ml
index 10787b6fe..ea297dc29 100644
--- a/src_colibri2/popop_lib/unit.ml
+++ b/src_colibri2/popop_lib/unit.ml
@@ -230,6 +230,10 @@ module H = struct
let create _ = { c = [] }
let memo _ = assert false
let mapi f s = s.c <- List.map (fun e -> f () e) s.c
+ let filter_mapi f s = s.c <- List.filter_map (fun e -> f () e) s.c
+ let choose s = match s.c with
+ | [] -> None
+ | v::_ -> Some ((),v)
let stats _ = assert false
let length _ = assert false
let fold _ = assert false
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 22a4e8e8b..03dd7d332 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -41,22 +41,22 @@ let debug_dotgui =
let var_decay = 1. /. 0.95
-let stats_propa = Debug.register_stats_int ~name:"Scheduler.daemon" ~init:0
+let stats_propa = Debug.register_stats_int "Scheduler.daemon"
-let stats_lasteffort =
- Debug.register_stats_int ~name:"Scheduler.lasteffort" ~init:0
+let stats_lasteffort = Debug.register_stats_int "Scheduler.lasteffort"
let stats_lasteffort_propa =
- Debug.register_stats_int ~name:"Scheduler.lasteffort_propa" ~init:0
+ Debug.register_stats_int "Scheduler.lasteffort_propa"
-let stats_dec = Debug.register_stats_int ~name:"Scheduler.decision" ~init:0
+let stats_dec = Debug.register_stats_int "Scheduler.decision"
-let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
+let stats_con = Debug.register_stats_int "Scheduler.conflict"
-let stats_step = Debug.register_stats_int ~name:"Scheduler.step" ~init:0
+let stats_con_fix = Debug.register_stats_int "Scheduler.conflict_fix_model"
-let stats_fix_model =
- Debug.register_stats_int ~name:"Scheduler.fix_model" ~init:0
+let stats_step = Debug.register_stats_int "Scheduler.step"
+
+let stats_fix_model = Debug.register_stats_int "Scheduler.fix_model"
exception Contradiction
@@ -546,7 +546,9 @@ let rec conflict_analysis t =
Debug.dprintf0 debug "[Scheduler] End of learning";
if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
Backtrackable.draw_graph ~force:true t.solver_state;
- Debug.incr stats_con;
+ (match Context.Ref.get t.solve_step with
+ | FixModel -> Debug.incr stats_con_fix
+ | BacktrackChoice _ | Propagate -> Debug.incr stats_con);
t.var_inc := !(t.var_inc) *. var_decay;
let rec rewind () =
match t.prev_scheduler_state with
diff --git a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2 b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
index b68bf6fca..d3c911337 100644
--- a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
+++ b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
@@ -1,7 +1,7 @@
;; produced by local colibri2.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
-(set-option :max-steps-colibri2 11000)
+(set-option :max-steps-colibri2 14000)
(declare-datatypes ((tuple2 2))
((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 11a6c011f..1ab90f492 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -19,10 +19,6 @@
(*************************************************************************)
open Colibri2_core
-open Colibri2_stdlib.Std
-
-let default_value = Q.zero
-
module RealValue = RealValue
let th_register env =
@@ -36,125 +32,4 @@ let th_register env =
let () = Init.add_default_theory th_register
-(** Helpers to remove *)
-
-let a = Expr.Term.Var.mk "a" Expr.Ty.real
-
-let b = Expr.Term.Var.mk "b" Expr.Ty.real
-
-let ta = Expr.Term.of_var a
-
-let tb = Expr.Term.of_var b
-
-let c = Expr.Term.Var.mk "c" Expr.Ty.real
-
-let d = Expr.Term.Var.mk "d" Expr.Ty.real
-
-let tc = Expr.Term.of_var c
-
-let td = Expr.Term.of_var d
-
-let tadd = Expr.Term.Real.add ta tb
-
-let add d na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst d tadd
-
-let tadd' = Expr.Term.Real.(add (mul tc ta) (mul td tb))
-
-let add' env qa na qb nb =
- let qa = RealValue.cst qa in
- let qb = RealValue.cst qb in
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb); (c, qa); (d, qb) ];
- }
- in
- Ground.convert ~subst env tadd'
-
-let tsub = Expr.Term.Real.sub ta tb
-
-let sub env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tsub
-
-let tmult_cst = Expr.Term.Real.(mul tc ta)
-
-let mult_cst env qa na =
- let qa = RealValue.cst qa in
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (c, qa) ];
- }
- in
- Ground.convert ~subst env tmult_cst
-
-let tmult = Expr.Term.Real.(mul ta tb)
-
-let mult env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tmult
-
-let tgt_zero = Expr.Term.Real.(gt ta tb)
-
-let gt_zero env na =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
- }
- in
- Ground.convert ~subst env tgt_zero
-
-let tge_zero = Expr.Term.Real.(ge ta tb)
-
-let ge_zero env na =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
- }
- in
- Ground.convert ~subst env tge_zero
-
-let cmp tcmp env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tcmp
-
-let tlt = Expr.Term.Real.lt ta tb
-
-let tle = Expr.Term.Real.le ta tb
-
-let tgt = Expr.Term.Real.gt ta tb
-
-let tge = Expr.Term.Real.ge ta tb
-
-let lt env na nb = cmp tlt env na nb
-
-let le env na nb = cmp tle env na nb
-
-let gt env na nb = cmp tgt env na nb
-
-let ge env na nb = cmp tge env na nb
+include LRA_build
diff --git a/src_colibri2/theories/LRA/LRA_build.ml b/src_colibri2/theories/LRA/LRA_build.ml
new file mode 100644
index 000000000..7f0b7e530
--- /dev/null
+++ b/src_colibri2/theories/LRA/LRA_build.ml
@@ -0,0 +1,144 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+open Colibri2_core
+
+(** Helpers to remove *)
+
+let a = Expr.Term.Var.mk "a" Expr.Ty.real
+
+let b = Expr.Term.Var.mk "b" Expr.Ty.real
+
+let ta = Expr.Term.of_var a
+
+let tb = Expr.Term.of_var b
+
+let c = Expr.Term.Var.mk "c" Expr.Ty.real
+
+let d = Expr.Term.Var.mk "d" Expr.Ty.real
+
+let tc = Expr.Term.of_var c
+
+let td = Expr.Term.of_var d
+
+let tadd = Expr.Term.Real.add ta tb
+
+let add d na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst d tadd
+
+let tadd' = Expr.Term.Real.(add (mul tc ta) (mul td tb))
+
+let add' env qa na qb nb =
+ let qa = RealValue.cst qa in
+ let qb = RealValue.cst qb in
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb); (c, qa); (d, qb) ];
+ }
+ in
+ Ground.convert ~subst env tadd'
+
+let tsub = Expr.Term.Real.sub ta tb
+
+let sub env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tsub
+
+let tmult_cst = Expr.Term.Real.(mul tc ta)
+
+let mult_cst env qa na =
+ let qa = RealValue.cst qa in
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (c, qa) ];
+ }
+ in
+ Ground.convert ~subst env tmult_cst
+
+let tmult = Expr.Term.Real.(mul ta tb)
+
+let mult env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tmult
+
+let tgt_zero = Expr.Term.Real.(gt ta tb)
+
+let gt_zero env na =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
+ }
+ in
+ Ground.convert ~subst env tgt_zero
+
+let tge_zero = Expr.Term.Real.(ge ta tb)
+
+let ge_zero env na =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
+ }
+ in
+ Ground.convert ~subst env tge_zero
+
+let cmp tcmp env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tcmp
+
+let tlt = Expr.Term.Real.lt ta tb
+
+let tle = Expr.Term.Real.le ta tb
+
+let tgt = Expr.Term.Real.gt ta tb
+
+let tge = Expr.Term.Real.ge ta tb
+
+let lt env na nb = cmp tlt env na nb
+
+let le env na nb = cmp tle env na nb
+
+let gt env na nb = cmp tgt env na nb
+
+let ge env na nb = cmp tge env na nb
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index 47b52e036..d64a5a9a0 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -242,7 +242,7 @@ let init env =
Daemon.attach_reg_value env RealValue.key (fun d value ->
let v = RealValue.value value in
let s = D.singleton v in
- Egraph.set_dom d dom (RealValue.node value) s);
+ upd_dom d (RealValue.node value) s);
Ground.register_converter env converter;
Interp.Register.node env (fun _ d n ->
match Egraph.get_dom d dom n with
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 78d1d1833..0aa6ae821 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -29,7 +29,9 @@ let scheduled =
let debug =
Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
-let stats_run = Debug.register_stats_int ~name:"Fourier.run" ~init:0
+let stats_run = Debug.register_stats_int "Fourier.run"
+
+let stats_time = Debug.register_stats_time "Fourier.time"
type eq = { p : Polynome.t; bound : Bound.t; origins : Ground.S.t }
[@@deriving show]
@@ -143,15 +145,18 @@ let add_eq d eqs p bound origins =
(fun g ->
let truth = Base.Option.value_exn (Boolean.is d (Ground.node g)) in
apply d truth g ~f:(fun d bound a b ->
- match bound with
- | Strict
- when Dom_interval.is_integer d a && Dom_interval.is_integer d b
- ->
- Dom_polynome.assume_equality d a
- (Polynome.of_list Q.minus_one [ (b, Q.one) ])
- | Large ->
- Dom_polynome.assume_equality d a (Polynome.monome Q.one b)
- | Strict -> assert false))
+ let p =
+ match bound with
+ | Strict
+ when Dom_interval.is_integer d a
+ && Dom_interval.is_integer d b ->
+ Polynome.of_list Q.minus_one [ (b, Q.one) ]
+ | Large -> Polynome.monome Q.one b
+ | Strict -> assert false
+ in
+ Debug.dprintf4 debug "[LRA/Fourier] Found %a = %a" Node.pp a
+ Polynome.pp p;
+ Dom_polynome.assume_equality d a p))
origins;
eqs
| Some p, _ when Q.sign p < 0 ->
@@ -257,6 +262,8 @@ let fm (d : Egraph.wt) =
in
aux eqs vars
+let fm d = Debug.add_time_during stats_time (fun () -> fm d)
+
module Daemon = struct
let key =
Events.Dem.create
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index 27a7dccab..d80e81848 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -21,33 +21,38 @@
open Colibri2_popop_lib
open Colibri2_core
+let print_poly fmt poly =
+ let print_not_1 first fmt q =
+ if not first && Q.compare q Q.zero >= 0
+ then Format.pp_print_string fmt "+";
+ if Q.equal q Q.zero then Format.pp_print_string fmt "!0!"
+ else if Q.equal Q.minus_one q then Format.pp_print_string fmt "-"
+ else if not (Q.equal Q.one q) then Q.pp fmt q
+ in
+ let print_mono k v (fmt,first) =
+ Format.fprintf fmt "@[%a%a@]@," (print_not_1 first) v Node.pp k;
+ (fmt,false)
+ in
+ let _,first = Node.M.fold print_mono poly (fmt,true) in
+ first
+
module T = struct
type t = { cst : Q.t; poly : Q.t Node.M.t}
[@@deriving eq,ord,hash]
let pp fmt v =
- let print_not_1 first fmt q =
- if not first && Q.compare q Q.zero >= 0
- then Format.pp_print_string fmt "+";
- if Q.equal q Q.zero then Format.pp_print_string fmt "!0!"
- else if Q.equal Q.minus_one q then Format.pp_print_string fmt "-"
- else if not (Q.equal Q.one q) then Q.pp fmt q
- in
- let print_not_0 first fmt q =
- if first
- then Q.pp fmt q
- else
- if not (Q.equal Q.zero q) then begin
- if Q.compare q Q.zero > 0 then Format.pp_print_string fmt "+";
- Q.pp fmt q
- end
- in
- let print_mono k v (fmt,first) =
- Format.fprintf fmt "@[%a%a@]@," (print_not_1 first) v Node.pp k;
- (fmt,false)
- in
+ let print_not_0 first fmt q =
+ if first
+ then Q.pp fmt q
+ else
+ if not (Q.equal Q.zero q) then begin
+ if Q.compare q Q.zero > 0 then Format.pp_print_string fmt "+";
+ Q.pp fmt q
+ end
+ in
+
Format.fprintf fmt "@[";
- let _,first = Node.M.fold print_mono v.poly (fmt,true) in
+ let first = print_poly fmt v.poly in
Format.fprintf fmt "%a@]" (print_not_0 first) v.cst
end
@@ -185,6 +190,10 @@ let of_list cst l =
| Some q' -> none_zero (Q.add q q')) node acc in
{cst;poly= List.fold_left fold Node.M.empty l}
+let of_map cst poly =
+ assert ( Node.M.for_all (fun _ q -> not (Q.equal Q.zero q)) poly );
+ {cst;poly}
+
module ClM = Extmap.Make(Node)
type 'a tree = 'a ClM.view =
@@ -206,3 +215,5 @@ let normalize p =
let conv q = Q.make (Z.divexact q.Q.num num) (Z.divexact q.Q.den den) in
{ poly = Node.M.map conv p.poly;
cst = conv p.cst }
+
+let print_poly fmt poly = let _ = print_poly fmt poly in ()
diff --git a/src_colibri2/theories/LRA/polynome.mli b/src_colibri2/theories/LRA/polynome.mli
index b2cb3e993..2d5aa6c39 100644
--- a/src_colibri2/theories/LRA/polynome.mli
+++ b/src_colibri2/theories/LRA/polynome.mli
@@ -64,6 +64,8 @@ val sub : t -> t -> t
val of_list : Q.t -> (Node.t * Q.t) list -> t
+val of_map : Q.t -> Q.t Node.M.t -> t
+
val x_p_cy : t -> Q.t -> t -> t
val cx_p_cy : Q.t -> t -> Q.t -> t -> t
@@ -82,3 +84,5 @@ val get_tree : t -> Q.t tree * Q.t
val normalize : t -> t
(** divide by the pgcd *)
+
+val print_poly : Q.t Node.M.t Fmt.t
diff --git a/src_colibri2/theories/LRA/simplex.ml b/src_colibri2/theories/LRA/simplex.ml
index b0e874054..b71e33c80 100644
--- a/src_colibri2/theories/LRA/simplex.ml
+++ b/src_colibri2/theories/LRA/simplex.ml
@@ -20,8 +20,9 @@
open Colibri2_popop_lib
open Colibri2_core
+open Base
-let comparisons = Datastructure.Push.create Ground.pp "LRA.simplex.comparisons"
+let comparisons = Datastructure.Push.create Node.pp "LRA.simplex.comparisons"
let scheduled =
Datastructure.Ref.create Base.Bool.pp "LRA.simplex.scheduled" false
@@ -29,7 +30,11 @@ let scheduled =
let debug =
Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "simplex"
-let stats_run = Debug.register_stats_int ~name:"Simplex.run" ~init:0
+let stats_run = Debug.register_stats_int "Simplex.run"
+
+let stats_maximization = Debug.register_stats_int "Simplex.maximization"
+
+let stats_time = Debug.register_stats_time "Simplex.time"
module Var = struct
include Node
@@ -42,7 +47,7 @@ end
module Ex = struct
type t = unit
- let print fmt () = Format.fprintf fmt "()"
+ let print fmt () = Fmt.pf fmt "()"
let empty = ()
@@ -54,7 +59,7 @@ module Rat = struct
let m_one = Q.of_int (-1)
- let print fmt t = Format.fprintf fmt "%s" (Q.to_string t)
+ let print fmt t = Fmt.pf fmt "%s" (Q.to_string t)
let is_int x = Z.equal Z.one x.Q.den
@@ -71,173 +76,167 @@ end
module Sim = OcplibSimplex.Basic.Make (Var) (Rat) (Ex)
-type eq = { p : Polynome.t; bound : Bound.t; origins : Ground.S.t }
-[@@deriving show]
-(** p <= 0 or p < 0 *)
-
-let divide d (p : Polynome.t) =
- try
- (match Polynome.is_cst p with None -> () | Some _ -> raise Exit);
- if Q.sign p.cst <> 0 then raise Exit;
- let l = Node.M.bindings p.poly in
- let l =
- List.fold_left
- (fun acc (e, q) ->
- match
- ( Dom_product.SolveAbs.get_repr d e,
- Dom_product.SolveSign.get_repr d e )
- with
- | None, _ when Egraph.is_equal d RealValue.zero e -> acc
- | None, _ | _, None -> raise Exit
- | Some abs, Some sign -> (abs, sign, q) :: acc)
- [] l
- in
- (* Debug.dprintf4 debug "@[eq:%a@ %a@]" Polynome.pp p
- * Fmt.(list ~sep:(any "+") (using CCPair.swap (pair Q.pp Product.pp)))
- * l; *)
- match l with
- | [] -> raise Exit
- | (hd, __, _) :: _ ->
- let common =
- List.fold_left
- (fun acc (abs, _, _) ->
- Node.M.inter
- (fun _ a b -> if Q.equal a b then Some a else None)
- acc abs.Product.poly)
- hd.Product.poly l
- in
- let common =
- Node.M.fold_left
- (fun acc abs v ->
- if Dom_interval.is_not_zero d abs then Node.M.add abs v acc
- else acc)
- Node.M.empty common
- in
- if Node.M.is_empty common then raise Exit;
- let common = Product.of_map common in
- Debug.dprintf4 debug "[Simplex] found possible division: %a / |%a|"
- Polynome.pp p Product.pp common;
- let cst, l =
- List.fold_left
- (fun (cst, acc) (abs, sign, v) ->
- let abs = Product.div abs common in
- let pos, sign = Sign_product.extract_cst sign in
- let v =
- match pos with Zero -> Q.zero | Pos -> v | Neg -> Q.neg v
- in
- match (Product.classify abs, Sign_product.classify sign) with
- | _, MINUS_ONE -> assert false
- | ONE, PLUS_ONE -> (Q.add v cst, acc)
- | NODE n, NODE n' when Egraph.is_equal d n n' ->
- (cst, (n, v) :: acc)
- | _ ->
- let n = Dom_product.node_of_product d abs sign in
- (cst, (n, v) :: acc))
- (Q.zero, []) l
- in
- Some (Polynome.of_list cst l, common)
- with Exit -> None
+type bound = No | Large of Q.t | Strict of Q.t
+
+let pp_bound_inf fmt = function
+ | No -> ()
+ | Large q -> Fmt.pf fmt "%a ≤" Q.pp q
+ | Strict q -> Fmt.pf fmt "%a <" Q.pp q
+
+let pp_bound_sup fmt = function
+ | No -> ()
+ | Large q -> Fmt.pf fmt "≤ %a" Q.pp q
+ | Strict q -> Fmt.pf fmt "< %a" Q.pp q
+
+let to_bound = function
+ | None -> No
+ | Some (q, Bound.Large) -> Large q
+ | Some (q, Bound.Strict) -> Strict q
+
+let inter_inf inf1 inf2 =
+ match (inf1, inf2) with
+ | No, inf | inf, No -> inf
+ | (Large q1, (Strict q2 as inf) | (Strict q2 as inf), Large q1)
+ when Q.equal q1 q2 ->
+ inf
+ | ((Large q1 | Strict q1) as inf1), ((Strict q2 | Large q2) as inf2) ->
+ if Q.leq q2 q1 then inf1 else inf2
+
+let inter_sup inf1 inf2 =
+ match (inf1, inf2) with
+ | No, inf | inf, No -> inf
+ | (Large q1, (Strict q2 as inf) | (Strict q2 as inf), Large q1)
+ when Q.equal q1 q2 ->
+ inf
+ | ((Large q1 | Strict q1) as inf1), ((Strict q2 | Large q2) as inf2) ->
+ if Q.leq q2 q1 then inf2 else inf1
+
+type eq = { inf : bound; p : Q.t Node.M.t; sup : bound }
+
+let pp_eq fmt { inf; p; sup } =
+ Fmt.pf fmt "%a%a%a" pp_bound_inf inf Polynome.print_poly p pp_bound_sup sup
let delta d eq =
+ let add d src bnd dst =
+ match bnd with
+ | No -> ()
+ | Large dist -> Delta.add_le d src dist dst
+ | Strict dist -> Delta.add_lt d src dist dst
+ in
(* add info to delta *)
- if Node.M.is_num_elt 2 eq.p.poly then
- match Node.M.bindings eq.p.poly with
+ if Node.M.is_num_elt 2 eq.p then
+ match Node.M.bindings eq.p with
| [ (src, a); (dst, b) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
+ add d src eq.sup dst;
+ add d dst eq.inf src
| [ (dst, b); (src, a) ] when Q.equal Q.one a && Q.equal Q.minus_one b ->
- Delta.add d src (Q.neg eq.p.cst) eq.bound dst
+ add d src eq.sup dst;
+ add d dst eq.inf src
| _ -> ()
-let apply d ~f truth g =
- let aux d bound a b =
- let bound =
- if truth then bound
- else match bound with Bound.Large -> Strict | Strict -> Large
- in
- let a, b = if truth then (a, b) else (b, a) in
- f d bound a b
+let add_eq _ eqs eq =
+ let p = Polynome.of_map Q.zero eq.p in
+ Polynome.H.change
+ (function
+ | None -> Some eq
+ | Some eq' ->
+ Some
+ {
+ inf = inter_inf eq'.inf eq.inf;
+ sup = inter_sup eq'.sup eq.sup;
+ p = eq.p;
+ })
+ eqs p;
+ eqs
+
+let mk_eq _ p dom =
+ assert (not (Node.M.is_empty p.Polynome.poly));
+ let _, q = Node.M.choose p.poly in
+ assert (not (Q.equal q Q.zero));
+ let p = Polynome.mult_cst (Q.inv q) p in
+ let inf, sup = Dom_interval.D.get_convexe_hull dom in
+ let inf, sup = if Q.sign q < 0 then (sup, inf) else (inf, sup) in
+ let translate = function
+ | No -> No
+ | Strict c -> Strict (Q.sub (Q.div c q) p.cst)
+ | Large c -> Large (Q.sub (Q.div c q) p.cst)
in
- match Ground.sem g with
- | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- aux d Bound.Strict a b
- | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- aux d Large a b
- | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- aux d Large b a
- | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- aux d Strict b a
- | _ -> assert false
-
-let add_eq d eqs p bound origins =
- match (Polynome.is_cst p, bound) with
- | None, _ ->
- let eq = { p; bound; origins } in
- delta d eq;
- eq :: eqs
- | Some p, Bound.Large when Q.sign p = 0 ->
- Ground.S.iter
- (fun g ->
- let truth = Base.Option.value_exn (Boolean.is d (Ground.node g)) in
- apply d truth g ~f:(fun d bound a b ->
- match bound with
- | Strict
- when Dom_interval.is_integer d a && Dom_interval.is_integer d b
- ->
- Dom_polynome.assume_equality d a
- (Polynome.of_list Q.minus_one [ (b, Q.one) ])
- | Large ->
- Dom_polynome.assume_equality d a (Polynome.monome Q.one b)
- | Strict -> assert false))
- origins;
- eqs
- | Some p, _ when Q.sign p < 0 ->
- Debug.dprintf2 debug "[Simplex] discard %a" Ground.S.pp origins;
- eqs
- | Some p, bound ->
- Debug.dprintf4 Debug.contradiction "[LRA/Simplex] Found %a%a0" Q.pp p
- Bound.pp bound;
- Egraph.contradiction d
-
-let mk_eq d bound a b =
- let ( ! ) n =
- match Dom_polynome.get_repr d n with
- | None -> Polynome.monome Q.one (Egraph.find_def d n)
- | Some p -> p
+ let inf = translate @@ to_bound inf in
+ let sup = translate @@ to_bound sup in
+ { inf; p = p.poly; sup }
+
+let make_equations d (eqs, vars) n =
+ Debug.dprintf2 debug "[Simplex] %a" Node.pp n;
+ let addition (eqs, vars) n =
+ match Dom_interval.get_dom d n with
+ | None -> (eqs, vars)
+ | Some dom ->
+ let p =
+ match Dom_polynome.get_repr d n with
+ | None -> Polynome.monome Q.one (Egraph.find_def d n)
+ | Some p -> p
+ in
+ if Node.M.is_empty p.poly then (eqs, vars)
+ else
+ let eq = mk_eq d p dom in
+ Debug.dprintf6 debug "[Simplex] %a ∈ %a -> %a" Polynome.pp p
+ Dom_interval.D.pp dom pp_eq eq;
+ let eqs, vars =
+ ( add_eq d eqs eq,
+ Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly )
+ in
+ (eqs, vars)
in
- let p, bound' =
- match bound with
- | Bound.Strict
- when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
- (Polynome.add_cst (Polynome.sub !a !b) Q.one, Bound.Large)
- | _ -> (Polynome.sub !a !b, bound)
+ let product acc =
+ let abs = Dom_product.SolveAbs.get_repr d n in
+ let sign = Dom_product.SolveSign.get_repr d n in
+ match (abs, sign) with
+ | Some abs, Some sign ->
+ Debug.dprintf6 debug "[Simplex] %a: %a --- %a" Node.pp n Product.pp abs
+ Sign_product.pp sign;
+ if Sign_product.(equal one sign) then
+ (* only simple case currently *)
+ let all_pos =
+ Node.M.for_all
+ (fun n _ ->
+ let sign = Dom_product.SolveSign.get_repr d n in
+ Option.exists ~f:Sign_product.(equal one) sign)
+ abs.poly
+ in
+ if all_pos then
+ Node.M.fold_left (fun acc n _ -> addition acc n) acc abs.poly
+ else acc
+ else acc
+ | _ -> acc
in
- ( p,
- bound',
- Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b),
- bound )
-
-let make_equations d (eqs, vars) g =
- Debug.dprintf2 debug "[Simplex] %a" Ground.pp g;
- match Boolean.is d (Ground.node g) with
- | None -> (eqs, vars)
- | Some truth -> (
- let p, bound, p_non_norm, bound_non_norm = apply d ~f:mk_eq truth g in
- Debug.dprintf6 debug "[Simplex] %a(%a)%a0" Polynome.pp p Polynome.pp
- p_non_norm Bound.pp bound;
- let eqs, vars =
- ( add_eq d eqs p bound (Ground.S.singleton g),
- Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly )
- in
- match divide d p_non_norm with
- | Some (p', _) ->
- let p' = Dom_polynome.normalize d p' in
- ( add_eq d eqs p' bound_non_norm Ground.S.empty,
- Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly )
- | None -> (eqs, vars))
+ product (addition (eqs, vars) n)
+
+module Edge = struct
+ module T = struct
+ type t = { from : Node.t; to_ : Node.t } [@@deriving show, eq, ord, hash]
+ end
+
+ include T
+ include Popop_stdlib.MkDatatype (T)
+end
+
+let of_bound_sup = function
+ | No -> None
+ | Large q ->
+ assert (Q.is_real q);
+ Some (q, Q.zero)
+ | Strict q ->
+ assert (Q.is_real q);
+ Some (q, Q.minus_one)
+
+let of_bound_inf = function
+ | No -> None
+ | Large q ->
+ assert (Q.is_real q);
+ Some (q, Q.zero)
+ | Strict q ->
+ assert (Q.is_real q);
+ Some (q, Q.one)
let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
(* Env must be sat *)
@@ -245,39 +244,42 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
let s = Lazy.force s in
let h = Node.H.create 10 in
Base.List.iter ~f:(fun (n, q) -> Node.H.replace h n q) s.Sim.Core.main_vars;
+ Base.List.iter ~f:(fun (n, q) -> Node.H.replace h n q) s.Sim.Core.slake_vars;
h
in
- let partition l s =
- let h = val_of_sol s in
- let aux l =
- let l =
- Base.List.stable_sort
- ~compare:(fun n1 n2 ->
- Q.compare (Node.H.find h n1) (Node.H.find h n2))
- l
- in
- let l =
- Base.List.group
- ~break:(fun n1 n2 ->
- not (Q.equal (Node.H.find h n1) (Node.H.find h n2)))
- l
- in
-
- let l =
- Base.List.filter ~f:(function [] | [ _ ] -> false | _ -> true) l
- in
- l
- in
- let l = Base.List.concat_map ~f:aux l in
- (* Debug.dprintf1 debug "partition %s" ([%show: Node.t list list] l); *)
- l
+ let under_approx = Edge.H.create 10 in
+ let _ =
+ Node.S.fold_left
+ (fun acc from ->
+ let is_int_from = Dom_interval.is_integer d from in
+ let acc = Node.S.remove from acc in
+ Node.S.iter
+ (fun to_ ->
+ let is_int_to = Dom_interval.is_integer d to_ in
+ Edge.H.add_new Impossible under_approx { Edge.from; to_ }
+ (is_int_from, is_int_to, Q.inf, Q.minus_inf))
+ acc;
+ acc)
+ vars vars
in
- let pair_seen = Node.H.create 10 in
- let add_pair_seen a b =
- let h = Node.H.memo (fun _ -> Node.H.create 10) pair_seen a in
- Node.H.add_new Impossible h b ()
+ let update_under_approx s =
+ let h = val_of_sol s in
+ Edge.H.filter_mapi
+ (fun { from; to_ } (is_int_from, is_int_to, inf, sup) ->
+ let dist = Q.sub (Node.H.find h to_) (Node.H.find h from) in
+ Debug.dprintf10 debug "[Simplex] under_approx: %a <= %a - %a <= %a : %a"
+ Q.pp inf Node.pp to_ Node.pp from Q.pp sup Q.pp dist;
+ let inf = Q.min inf dist in
+ let sup = Q.max sup dist in
+ if is_int_from || is_int_to then
+ if Q.le inf Q.minus_one || Q.le Q.one sup then None
+ else Some (is_int_from, is_int_to, inf, sup)
+ else if Q.lt inf Q.zero || Q.lt Q.zero sup then None
+ else Some (is_int_from, is_int_to, inf, sup))
+ under_approx
in
- let one_dist env a b =
+ let one_dist env is_int a b =
+ Debug.incr stats_maximization;
(* Debug.dprintf4 debug "one_dist %a %a" Node.pp a Node.pp b; *)
let p = Sim.Core.P.from_list [ (a, Q.one); (b, Q.minus_one) ] in
let env, opt = Sim.Solve.maximize env p in
@@ -286,61 +288,64 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
| Sim.Core.Unsat _ -> assert false
| Sim.Core.Sat _ -> assert false
| Sim.Core.Unbounded s ->
- let s' = Lazy.force s in
- let qa = Base.List.Assoc.find_exn ~equal:Node.equal s'.main_vars a in
- let qb = Base.List.Assoc.find_exn ~equal:Node.equal s'.main_vars b in
- (if Q.equal qa qb then
- let a, b = if Node.compare a b < 0 then (a, b) else (b, a) in
- (* Debug.dprintf4 debug "pair_seen %a %a" Node.pp a Node.pp b; *)
- add_pair_seen a b);
+ update_under_approx s;
+ (* s is often not interesting for the update; all at zero, so the
+ distance is pushed a little further *)
+ let p' = Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ] in
+ let n = Dom_polynome.node_of_polynome d p' in
+ let env', _ =
+ Sim.Assert.poly env p n (of_bound_inf (Large (Q.of_int 2))) () None ()
+ in
+ let env' = Sim.Solve.solve env' in
+ let s =
+ match Sim.Result.get opt env' with
+ | Sim.Core.Sat s -> s
+ | Sim.Core.Unbounded s -> s
+ | _ -> assert false
+ in
(`Distinct, env, s)
| Sim.Core.Max (m, s) ->
- Debug.dprintf2 debug "Max %a" Q.pp (Lazy.force m).max_v;
- let s' = Lazy.force s in
- let qa = Base.List.Assoc.find_exn ~equal:Node.equal s'.main_vars a in
- let qb = Base.List.Assoc.find_exn ~equal:Node.equal s'.main_vars b in
- if Q.equal qa qb then (`NotDistinct, env, s) else (`Distinct, env, s)
- in
- let rec test_equality env l =
- match l with
- | [] -> env
- | [ _ ] :: l -> test_equality env l
- | [] :: _ -> assert false
- | (a :: l1) :: l2 -> (
- let skip =
- match Node.H.find_opt pair_seen a with
- | None -> Base.List.hd l1
- | Some h -> Base.List.find l1 ~f:(fun b -> not (Node.H.mem h b))
+ let m = Lazy.force m in
+ Debug.dprintf2 debug "Max %a" Q.pp m.max_v;
+ (if m.is_le then Delta.add_le else Delta.add_lt) d a m.max_v b;
+ let notdistinct =
+ if is_int then Q.lt (Q.abs m.max_v) Q.one else Q.equal m.max_v Q.zero
in
- match skip with
- | None -> test_equality env (l1 :: l2)
- | Some b -> (
- match one_dist env a b with
+ if notdistinct then (`NotDistinct, env, s) else (`Distinct, env, s)
+ in
+ (* test equality and propagate small distance *)
+ let rec test_equality env =
+ match Edge.H.choose under_approx with
+ | None -> env
+ | Some (({ from; to_ } as e), (is_int_from, is_int_to, _, _)) -> (
+ Edge.H.remove under_approx e;
+ let is_int = is_int_from && is_int_to in
+ match one_dist env is_int from to_ with
+ | `Distinct, env, s ->
+ update_under_approx s;
+ let env =
+ if is_int_from || is_int_to then (
+ let _, env, s = one_dist env is_int to_ from in
+ update_under_approx s;
+ env)
+ else env
+ in
+ test_equality env
+ | `NotDistinct, env, s -> (
+ update_under_approx s;
+ match one_dist env is_int to_ from with
| `Distinct, env, s ->
- Debug.dprintf1 debug "Distinct %s"
- ([%show: (Node.t * Q.t) list]
- (Lazy.force s).Sim.Core.main_vars);
- let l = partition l s in
- test_equality env l
- | `NotDistinct, env, s -> (
- let l = partition l s in
- match one_dist env b a with
- | `Distinct, env, s ->
- let l = partition l s in
- test_equality env l
- | `NotDistinct, env, s -> (
- let l = partition l s in
- Egraph.merge d a b;
- match l with
- | [] -> assert false
- | ([] | [ _ ]) :: _ -> assert false
- | (a' :: l1) :: l2 ->
- assert (Node.equal a a');
- test_equality env (l1 :: l2)))))
+ update_under_approx s;
+ test_equality env
+ | `NotDistinct, env, s ->
+ update_under_approx s;
+ Debug.dprintf4 debug "[LRA/Simplex] Found %a = %a" Node.pp from
+ Node.pp to_;
+ Egraph.merge d from to_;
+ test_equality env))
in
- let l = [ Node.S.elements vars ] in
- let l = partition l s in
- test_equality env l
+ update_under_approx s;
+ test_equality env
let update_domains d env =
let update_domain n ((v : Sim.Core.var_info), _) =
@@ -385,7 +390,7 @@ let simplex (d : Egraph.wt) =
Datastructure.Ref.set scheduled d false;
let eqs, vars =
Datastructure.Push.fold comparisons d ~f:(make_equations d)
- ~init:([], Node.S.empty)
+ ~init:(Polynome.H.create 10, Node.S.empty)
in
let env = Sim.Core.empty ~is_int:false ~check_invs:false ~debug:0 in
let of_poly (p : Polynome.t) =
@@ -393,49 +398,47 @@ let simplex (d : Egraph.wt) =
(fun n r acc -> fst (Sim.Core.P.accumulate n r acc))
p.poly Sim.Core.P.empty
in
- let of_bound_sup q = function
- | Bound.Large -> (q, Q.zero)
- | Strict -> (q, Q.minus_one)
- in
- let of_bound_inf q = function
- | Bound.Large -> (q, Q.zero)
- | Strict -> (q, Q.one)
- in
let add_vars env v =
let inf, sup =
match Egraph.get_dom d Dom_interval.dom v with
- | None -> (None, None)
- | Some d -> Dom_interval.D.get_convexe_hull d
+ | None -> (No, No)
+ | Some d ->
+ let conv = function
+ | None -> No
+ | Some (q, Bound.Large) -> Large q
+ | Some (q, Bound.Strict) -> Strict q
+ in
+ let inf, sup = Dom_interval.D.get_convexe_hull d in
+ (conv inf, conv sup)
in
- let app f = function None -> None | Some (q, b) -> Some (f q b) in
let env, _ =
- Sim.Assert.var env v (app of_bound_inf inf) () (app of_bound_sup sup) ()
+ Sim.Assert.var env v (of_bound_inf inf) () (of_bound_sup sup) ()
in
env
in
let env = Node.S.fold_left add_vars env vars in
(* Debug.dprintf2 debug "[Simplex] after_adding variables: %a"
* (Sim.Core.print Unknown) env; *)
- let add_eqs env eq =
- assert (not (Node.M.is_empty eq.p.poly));
- if Node.M.is_num_elt 1 eq.p.poly then
- let n, q = Node.M.choose eq.p.poly in
- if Q.sign q < 0 then
- let b = of_bound_inf (Q.neg (Q.div eq.p.cst q)) eq.bound in
- let env, _ = Sim.Assert.var env n (Some b) () None () in
- env
- else
- let b = of_bound_sup (Q.neg (Q.div eq.p.cst q)) eq.bound in
- let env, _ = Sim.Assert.var env n None () (Some b) () in
- env
+ let add_eqs _ eq (env, vars) =
+ assert (not (Node.M.is_empty eq.p));
+ Debug.dprintf2 debug "%a@." pp_eq eq;
+ if Node.M.is_num_elt 1 eq.p then (
+ let n, q = Node.M.choose eq.p in
+ assert (Q.equal q Q.one);
+ let inf = of_bound_inf eq.inf in
+ let sup = of_bound_sup eq.sup in
+ let env, _ = Sim.Assert.var env n inf () sup () in
+ (env, vars))
else
- let b = of_bound_sup (Q.neg eq.p.cst) eq.bound in
- let p = Polynome.sub_cst eq.p eq.p.cst in
+ let inf = of_bound_inf eq.inf in
+ let sup = of_bound_sup eq.sup in
+ let p = Polynome.of_map Q.zero eq.p in
let n = Dom_polynome.node_of_polynome d p in
- let env, _ = Sim.Assert.poly env (of_poly p) n None () (Some b) () in
- env
+ let vars = Node.S.add n vars in
+ let env, _ = Sim.Assert.poly env (of_poly p) n inf () sup () in
+ (env, vars)
in
- let env = List.fold_left add_eqs env eqs in
+ let env, vars = Polynome.H.fold add_eqs eqs (env, vars) in
let env = Sim.Solve.solve env in
let res = Sim.Result.get None env in
(* Debug.dprintf2 debug "[Simplex] Solving done: %a" (Sim.Core.print res) env; *)
@@ -448,7 +451,9 @@ let simplex (d : Egraph.wt) =
let env = find_equalities d vars env s in
update_domains d env
-module Daemon = struct
+let simplex d = Debug.add_time_during stats_time (fun () -> simplex d)
+
+module DaemonSimplex = struct
let key =
Events.Dem.create
(module struct
@@ -475,25 +480,68 @@ module Daemon = struct
let run d () = simplex d
end
-let () = Events.register (module Daemon)
+let () = Events.register (module DaemonSimplex)
+
+let ord_inv = function
+ | Expr.Lt -> Expr.Gt
+ | Expr.Leq -> Expr.Geq
+ | Expr.Geq -> Expr.Leq
+ | Expr.Gt -> Expr.Lt
+ | _ -> assert false
+
+let ord_neg = function
+ | Expr.Lt -> Expr.Geq
+ | Expr.Leq -> Expr.Gt
+ | Expr.Geq -> Expr.Lt
+ | Expr.Gt -> Expr.Leq
+ | _ -> assert false
+
+let dom_inter = function
+ | Expr.Lt -> Dom_interval.D.lt
+ | Expr.Leq -> Dom_interval.D.le
+ | Expr.Gt -> Dom_interval.D.gt
+ | Expr.Geq -> Dom_interval.D.ge
+ | _ -> assert false
+
+let build = function
+ | Expr.Lt -> LRA_build.lt
+ | Expr.Leq -> LRA_build.le
+ | Expr.Gt -> LRA_build.gt
+ | Expr.Geq -> LRA_build.ge
+ | _ -> assert false
(** {2 Initialization} *)
let converter d (f : Ground.t) =
match Ground.sem f with
| {
- app = { builtin = Expr.Lt | Expr.Leq | Expr.Geq | Expr.Gt };
+ app = { builtin = (Expr.Lt | Expr.Leq | Expr.Geq | Expr.Gt) as builtin };
tyargs = [];
args;
} ->
- let attach n =
- Dom_polynome.events_repr_change d ~node:n Daemon.enqueue;
- Events.attach_repr d n Daemon.enqueue
+ let n, builtin =
+ let a, b = IArray.extract2_exn args in
+ (* Special case needed for avoiding infinite loop *)
+ if Node.equal a RealValue.zero then (b, ord_inv builtin)
+ else if Node.equal b RealValue.zero then (a, builtin)
+ else
+ let a, b, builtin =
+ if Node.compare a b < 0 then (a, b, builtin)
+ else (b, a, ord_inv builtin)
+ in
+ (LRA_build.sub d a b, builtin)
in
- IArray.iter ~f:attach args;
- Events.attach_value d (Ground.node f) Boolean.dom (fun d n _ ->
- Daemon.enqueue d n);
- Datastructure.Push.push comparisons d f;
- Events.new_pending_daemon d Daemon.key ();
+ Egraph.register d n;
+
+ let n' = build builtin d n RealValue.zero in
+ Egraph.register d n';
+ Egraph.merge d (Ground.node f) n';
+
+ Dom_polynome.events_repr_change d ~node:n DaemonSimplex.enqueue;
+ Events.attach_repr d n DaemonSimplex.enqueue;
+ Events.attach_dom d n Dom_interval.dom DaemonSimplex.enqueue;
+
+ Datastructure.Push.push comparisons d n;
+ Events.new_pending_daemon d DaemonSimplex.key ();
Choice.register d f (Boolean.chobool (Ground.node f))
| _ -> ()
diff --git a/src_colibri2/theories/LRA/stages/bound.ml b/src_colibri2/theories/LRA/stages/bound.ml
index b2169edcd..18540b121 100644
--- a/src_colibri2/theories/LRA/stages/bound.ml
+++ b/src_colibri2/theories/LRA/stages/bound.ml
@@ -1,30 +1,31 @@
module T = struct
- type t =
- | Strict | Large
- [@@deriving eq, ord, hash]
+ type t = Strict | Large [@@deriving eq, ord, hash]
let pp fmt = function
| Strict -> CCFormat.string fmt "<"
| Large -> CCFormat.string fmt "≤"
-
end
include T
-include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
+include Colibri2_popop_lib.Popop_stdlib.MkDatatype (T)
-let compare_inf b1 b2 = match b1,b2 with
+let compare_inf b1 b2 =
+ match (b1, b2) with
| Large, Strict -> -1
| Strict, Large -> 1
| Large, Large | Strict, Strict -> 0
-let compare_inf_sup b1 b2 = match b1,b2 with
+let compare_inf_sup b1 b2 =
+ match (b1, b2) with
| Large, Strict -> 1
| Strict, Large -> 1
| Large, Large -> 0
| Strict, Strict -> 1
-let compare_sup b1 b2 = - (compare_inf b1 b2)
+let compare_sup b1 b2 = -compare_inf b1 b2
let compare_bounds_inf = CCOrd.pair Q.compare compare_inf
+
let compare_bounds_sup = CCOrd.pair Q.compare compare_sup
+
let compare_bounds_inf_sup = CCOrd.pair Q.compare compare_inf_sup
diff --git a/src_colibri2/theories/LRA/stages/stage1/interval.ml b/src_colibri2/theories/LRA/stages/stage1/interval.ml
index febd3c046..fc23775b0 100644
--- a/src_colibri2/theories/LRA/stages/stage1/interval.ml
+++ b/src_colibri2/theories/LRA/stages/stage1/interval.ml
@@ -22,51 +22,77 @@ open Colibri2_popop_lib
open Colibri2_stdlib.Std
module Convexe = struct
-
include Colibrics_lib.Interval.Convexe
- include (struct
- type bound = Colibrics_lib.Interval.Bound.t =
- | Strict | Large
+ include struct
+ type bound = Colibrics_lib.Interval.Bound.t = Strict | Large
[@@deriving eq, ord, hash]
- type t = Colibrics_lib.Interval.Convexe.t = private
+ type t = Colibrics_lib.Interval.Convexe.t =
| Finite of Q.t * bound * Q.t * bound
| InfFinite of Q.t * bound
| FiniteInf of Q.t * bound
| Inf
- [@@ deriving eq, ord, hash]
- end)
+ [@@deriving eq, ord, hash]
+ end
let pp fmt t =
let print_bound_left fmt = function
- | Large -> Format.fprintf fmt "["
- | Strict -> Format.fprintf fmt "]" in
+ | Large -> Format.fprintf fmt "["
+ | Strict -> Format.fprintf fmt "]"
+ in
let print_bound_right fmt = function
- | Large -> Format.fprintf fmt "]"
- | Strict -> Format.fprintf fmt "[" in
+ | Large -> Format.fprintf fmt "]"
+ | Strict -> Format.fprintf fmt "["
+ in
match t with
- | Finite (q1,b1,q2,b2) ->
- Format.fprintf fmt "%a%a;%a%a"
- print_bound_left b1 Q.pp q1
- Q.pp q2 print_bound_right b2
- | InfFinite (q1,b1) ->
- Format.fprintf fmt "]-∞;%a%a"
- Q.pp q1 print_bound_right b1
- | FiniteInf(q1,b1) ->
- Format.fprintf fmt "%a%a;+∞["
- print_bound_left b1 Q.pp q1
- | Inf ->
- Format.fprintf fmt "]-∞;+∞["
+ | Finite (q1, b1, q2, b2) ->
+ Format.fprintf fmt "%a%a;%a%a" print_bound_left b1 Q.pp q1 Q.pp q2
+ print_bound_right b2
+ | InfFinite (q1, b1) ->
+ Format.fprintf fmt "]-∞;%a%a" Q.pp q1 print_bound_right b1
+ | FiniteInf (q1, b1) ->
+ Format.fprintf fmt "%a%a;+∞[" print_bound_left b1 Q.pp q1
+ | Inf -> Format.fprintf fmt "]-∞;+∞["
- include Popop_stdlib.MkDatatype(struct
- type nonrec t = t
- let equal = equal let compare = compare
- let hash = hash let hash_fold_t = hash_fold_t let pp = pp
- end)
+ include Popop_stdlib.MkDatatype (struct
+ type nonrec t = t
+
+ let equal = equal
+
+ let compare = compare
+
+ let hash = hash
+
+ let hash_fold_t = hash_fold_t
+
+ let pp = pp
+ end)
let invariant _ = true (* proved in why3 *)
+ let of_bound : Colibrics_lib.Interval.Bound.t -> Bound.t = function
+ | Strict -> Strict
+ | Large -> Large
+
+ let to_bound : Bound.t -> Colibrics_lib.Interval.Bound.t = function
+ | Strict -> Strict
+ | Large -> Large
+
+ let get_convexe_hull : t -> (Q.t * Bound.t) option * (Q.t * Bound.t) option =
+ function
+ | Finite (q1, b1, q2, b2) -> (Some (q1, of_bound b1), Some (q2, of_bound b2))
+ | InfFinite (q, b) -> (None, Some (q, of_bound b))
+ | FiniteInf (q, b) -> (Some (q, of_bound b), None)
+ | Inf -> (None, None)
+
+ let from_convexe_hull (c1, c2) : t =
+ match (c1, c2) with
+ | None, None -> Inf
+ | Some (q1, b1), None -> FiniteInf (q1, to_bound b1)
+ | None, Some (q1, b1) -> InfFinite (q1, to_bound b1)
+ | Some (q1, b1), Some (q2, b2) -> Finite (q1, to_bound b1, q2, to_bound b2)
+
(* let nb_incr = 100
* let z_nb_incr = Z.of_int nb_incr
* let choose_rnd rnd = function
@@ -113,7 +139,6 @@ module Convexe = struct
* assert (invariant t);
* Some t
* end *)
-
end
(*
module ConvexeWithDivider = struct
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index 43567cacd..7f1de41ec 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -473,38 +473,56 @@ let bool_init_diff_to_value d =
~already_registered:[ Boolean.value_true; Boolean.value_false ]
(** {2 Interpretations} *)
-let init_check d =
- Interp.Register.check d (fun d t ->
- let interp n = Opt.get_exn Impossible (Egraph.get_value d n) in
- let ( !> ) n =
- Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp n))
- in
- let check r =
- Interp.check_of_bool (Value.equal r (interp (Ground.node t)))
- in
- let ( !< ) b =
- let r = if b then Boolean.values_true else Boolean.values_false in
- check r
- in
- match Ground.sem t with
- | { app = { builtin = Expr.Equal }; tyargs = [ _ ]; args; ty = _ } ->
- assert (IArray.not_empty args);
- !<(IArray.for_alli_non_empty_exn ~init:interp
- ~f:(fun _ a t -> Value.equal a (interp t))
- args)
- | { app = { builtin = Expr.Equiv }; tyargs = [ _ ]; args; ty = _ } ->
- let a, b = IArray.extract2_exn args in
- !<(Value.equal (interp a) (interp b))
- | { app = { builtin = Expr.Distinct }; tyargs = [ _ ]; args; ty = _ } -> (
- try
- let fold acc v = Value.S.add_new Exit (interp v) acc in
- let _ = IArray.fold ~f:fold ~init:Value.S.empty args in
- check Boolean.values_true
- with Exit -> check Boolean.values_false)
- | { app = { builtin = Expr.Ite }; tyargs = [ _ ]; args; ty = _ } ->
- let c, a, b = IArray.extract3_exn args in
- check (if !>c then interp a else interp b)
- | _ -> NA)
+module Check = struct
+ let interp d n = Opt.get_exn Impossible (Egraph.get_value d n)
+
+ let compute_ground d t =
+ let ( !> ) n =
+ Boolean.BoolValue.value (Boolean.BoolValue.coerce_nodevalue (interp d n))
+ in
+ let check r = Some r in
+ let ( !< ) b =
+ let r = if b then Boolean.values_true else Boolean.values_false in
+ check r
+ in
+ match Ground.sem t with
+ | { app = { builtin = Expr.Equal }; tyargs = [ _ ]; args; ty = _ } ->
+ assert (IArray.not_empty args);
+ !<(IArray.for_alli_non_empty_exn ~init:(interp d)
+ ~f:(fun _ a t -> Value.equal a (interp d t))
+ args)
+ | { app = { builtin = Expr.Equiv }; tyargs = [ _ ]; args; ty = _ } ->
+ let a, b = IArray.extract2_exn args in
+ !<(Value.equal (interp d a) (interp d b))
+ | { app = { builtin = Expr.Distinct }; tyargs = [ _ ]; args; ty = _ } -> (
+ try
+ let fold acc v = Value.S.add_new Exit (interp d v) acc in
+ let _ = IArray.fold ~f:fold ~init:Value.S.empty args in
+ check Boolean.values_true
+ with Exit -> check Boolean.values_false)
+ | { app = { builtin = Expr.Ite }; tyargs = [ _ ]; args; ty = _ } ->
+ let c, a, b = IArray.extract3_exn args in
+ check (if !>c then interp d a else interp d b)
+ | _ -> None
+
+ let init_check d =
+ Interp.Register.check d (fun d t ->
+ let check r =
+ Interp.check_of_bool (Value.equal r (interp d (Ground.node t)))
+ in
+ match compute_ground d t with None -> NA | Some v -> check v);
+ Interp.Register.compute d (fun d t ->
+ match compute_ground d t with None -> NA | Some v -> Value v)
+
+ let attach d g =
+ let f d g =
+ match compute_ground d g with
+ | None -> raise Impossible
+ | Some v -> Egraph.set_value d (Ground.node g) v
+ in
+
+ Interp.WatchArgs.create d f g
+end
let converter d (t : Ground.t) =
let res = Ground.node t in
@@ -522,15 +540,19 @@ let converter d (t : Ground.t) =
in
match Ground.sem t with
| { app = { builtin = Expr.Equal }; tyargs = [ _ ]; args = l; _ } ->
+ Check.attach d t;
IArray.iter ~f:reg l;
reg_and_merge (equality_iter mark d (IArray.to_list l))
| { app = { builtin = Expr.Equiv }; tyargs = [ _ ]; args; _ } ->
+ Check.attach d t;
let a, b = IArray.extract2_exn args in
reg_and_merge (equality_iter mark d [ of_term a; of_term b ])
| { app = { builtin = Expr.Distinct }; tyargs = [ _ ]; args; _ } ->
+ Check.attach d t;
IArray.iter ~f:reg args;
reg_and_merge (disequality d (IArray.to_list args))
| { app = { builtin = Expr.Ite }; tyargs = [ _ ]; args; _ } ->
+ Check.attach d t;
let c, a, b = IArray.extract3_exn args in
new_ite d res (of_term c) a b
| { app = { builtin = Expr.Xor }; tyargs = []; args; _ } ->
@@ -542,7 +564,7 @@ let th_register env =
attach_new_equalities env;
Ground.register_converter env converter;
bool_init_diff_to_value env;
- init_check env;
+ Check.init_check env;
()
let () = Init.add_default_theory th_register
diff --git a/src_colibri2/theories/quantifier/common.ml b/src_colibri2/theories/quantifier/common.ml
index 0bf08501f..78b5f18a5 100644
--- a/src_colibri2/theories/quantifier/common.ml
+++ b/src_colibri2/theories/quantifier/common.ml
@@ -26,13 +26,10 @@ let debug =
let debug_full =
Debug.register_flag ~desc:"Handling of quantifiers full" "quantifiers.full"
-let nb_instantiation = Debug.register_stats_int ~name:"instantiation" ~init:0
+let nb_instantiation = Debug.register_stats_int "instantiation"
-let nb_eager_instantiation =
- Debug.register_stats_int ~name:"eager_instantiation" ~init:0
+let nb_eager_instantiation = Debug.register_stats_int "eager_instantiation"
-let nb_delayed_instantiation =
- Debug.register_stats_int ~name:"delayed_instantiation" ~init:0
+let nb_delayed_instantiation = Debug.register_stats_int "delayed_instantiation"
-let nb_new_instantiation =
- Debug.register_stats_int ~name:"new_instantiation" ~init:0
+let nb_new_instantiation = Debug.register_stats_int "new_instantiation"
--
GitLab