Skip to content
Snippets Groups Projects
Commit e7595b2c authored by François Bobot's avatar François Bobot
Browse files

[Definition] add limited eager folding

parent e18d0c3d
No related branches found
No related tags found
1 merge request!26Fix and domain propagation
Pipeline #52210 passed
Stage: test
Hide whitespace changes
Inline Side-by-side
colibri2/stdlib/context.ml
+ 14
− 8
View file @ e7595b2c
......@@ -70,28 +70,34 @@ module Ref = struct
match r.previous with
| [] -> ()
| { at } :: _ when at.alive -> ()
| _ ->
| { at = _; value } :: l ->
let rec aux v = function
| { at; value } :: l when not at.alive -> aux value l
| l ->
r.contents <- v;
r.previous <- l
in
aux r.contents r.previous
aux value l
let set_aux (r : _ t) v =
match r.previous with
| { at } :: _ when bp_equal at (bp r.context) -> r.contents <- v
| _ ->
r.previous <- { at = bp r.context; value = r.contents } :: r.previous;
r.contents <- v
let set r v =
rewind r;
if not (CCEqual.physical r.contents v) then
match r.previous with
| { at } :: _ when bp_equal at (bp r.context) -> r.contents <- v
| _ ->
r.previous <- { at = bp r.context; value = r.contents } :: r.previous;
r.contents <- v
if not (CCEqual.physical r.contents v) then set_aux r v
let get r =
rewind r;
r.contents
let incr r =
rewind r;
set_aux r (1 + r.contents)
let creator (h : 'a t) = h.context
let pp pp fmt r = pp fmt (get r)
end
......
colibri2/stdlib/context.mli
+ 3
− 0
View file @ e7595b2c
......@@ -64,6 +64,9 @@ module Ref : sig
val get : 'a t -> 'a
(** Get the current value of the reference *)
val incr : int t -> unit
(** Increment the current value of the reference *)
val creator : 'a t -> creator
val pp : 'a Fmt.t -> 'a t Fmt.t
end
......
colibri2/tests/solve/all/unsat/dune.inc
+ 3
− 0
View file @ e7595b2c
......@@ -20,6 +20,9 @@
--dont-print-result %{dep:lost_in_search_union.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:lost_in_search_union.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:mjrty-Mjrty-mjrtyqtvc_3.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mjrty-Mjrty-mjrtyqtvc_3.psmt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:mul_abs.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_abs.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
......
colibri2/tests/solve/all/unsat/mjrty-Mjrty-mjrtyqtvc_3.psmt2 0 → 100644
+ 384
− 0
View file @ e7595b2c
;; produced by local colibri2.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
;;; SMT-LIB2: integer arithmetic
(declare-sort string 0)
(declare-datatypes ((tuple0 0))
(((Tuple0))))
(declare-datatypes ((ref 1))
((par (a) ((refqtmk (contents a))))))
;; "prefix !"
(define-fun prefix_ex (par (a1)
((r (ref a1))) a1
(contents r)))
(declare-sort infix_mngt 2)
;; "infix @"
(declare-fun infix_at (par (a2
b)
((infix_mngt a2
b)
a2) b))
;; "get"
(define-fun get (par (a1
b1)
((f (infix_mngt a1 b1)) (x a1)) b1
(infix_at f x)))
;; "set"
(declare-fun set (par (a1
b1)
((infix_mngt a1
b1)
a1
b1) (infix_mngt a1
b1)))
;; "set'def"
(assert (par (a1 b1)
(forall ((f (infix_mngt a1 b1)) (x a1) (v b1) (y a1))
(= (infix_at (set f x v) y) (ite (= y x) v (infix_at f y))))))
;; "mixfix []"
(define-fun mixfix_lbrb (par (a1
b1)
((f (infix_mngt a1 b1)) (x a1)) b1
(infix_at f x)))
;; "mixfix [<-]"
(define-fun mixfix_lblsmnrb (par (a1
b1)
((f (infix_mngt a1 b1)) (x a1) (v b1)) (infix_mngt a1 b1)
(set f x v)))
(declare-sort array 1)
;; "elts"
(declare-fun elts (par (a1)
((array a1)) (infix_mngt Int
a1)))
;; "length"
(declare-fun length (par (a1)
((array a1)) Int))
;; "array'invariant"
(assert (par (a1)
(forall ((self (array a1)))
(! (<= 0 (length self)) :pattern ((length self)) ))))
;; "mixfix []"
(define-fun mixfix_lbrb1 (par (a1)
((a3 (array a1)) (i Int)) a1
(infix_at (elts a3) i)))
;; "mixfix [<-]"
(declare-fun mixfix_lblsmnrb1 (par (a1)
((array a1)
Int
a1) (array a1)))
;; "mixfix [<-]'spec"
(assert (par (a1)
(forall ((a3 (array a1)) (i Int) (v a1))
(and
(= (length (mixfix_lblsmnrb1 a3 i v)) (length a3))
(= (elts (mixfix_lblsmnrb1 a3 i v)) (set (elts a3) i v))))))
;; "make"
(declare-fun make (par (a1)
(Int
a1) (array a1)))
;; "make_spec"
(assert (par (a1)
(forall ((n Int) (v a1))
(=>
(>= n 0)
(and
(forall ((i Int))
(=> (and (<= 0 i) (< i n)) (= (mixfix_lbrb1 (make n v) i) v)))
(= (length (make n v)) n))))))
;; "numof"
(declare-fun numof ((infix_mngt Int
Bool)
Int
Int) Int)
;; "numof'def"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(ite (<= b2 a3)
(= (numof p a3 b2) 0)
(ite (= (infix_at p (- b2 1)) true)
(= (numof p a3 b2) (+ 1 (numof p a3 (- b2 1))))
(= (numof p a3 b2) (numof p a3 (- b2 1)))))))
;; "Numof_bounds"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(< a3 b2)
(and (<= 0 (numof p a3 b2)) (<= (numof p a3 b2) (- b2 a3))))))
;; "Numof_append"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int) (c Int))
(=>
(and (<= a3 b2) (<= b2 c))
(= (numof p a3 c) (+ (numof p a3 b2) (numof p b2 c))))))
;; "Numof_left_no_add"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(< a3 b2)
(=>
(not (= (infix_at p a3) true))
(= (numof p a3 b2) (numof p (+ a3 1) b2))))))
;; "Numof_left_add"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(< a3 b2)
(=>
(= (infix_at p a3) true)
(= (numof p a3 b2) (+ 1 (numof p (+ a3 1) b2)))))))
;; "Empty"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(forall ((n Int))
(=> (and (<= a3 n) (< n b2)) (not (= (infix_at p n) true))))
(= (numof p a3 b2) 0))))
;; "Full"
(assert
(forall ((p (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(<= a3 b2)
(=>
(forall ((n Int))
(=> (and (<= a3 n) (< n b2)) (= (infix_at p n) true)))
(= (numof p a3 b2) (- b2 a3))))))
;; "numof_increasing"
(assert
(forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int))
(=> (and (<= i j) (<= j k)) (<= (numof p i j) (numof p i k)))))
;; "numof_strictly_increasing"
(assert
(forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int) (l Int))
(=>
(and (<= i j) (and (<= j k) (< k l)))
(=> (= (infix_at p k) true) (< (numof p i j) (numof p i l))))))
;; "numof_change_any"
(assert
(forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(forall ((j Int))
(=>
(and (<= a3 j) (< j b2))
(=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
(>= (numof p2 a3 b2) (numof p1 a3 b2)))))
;; "numof_change_some"
(assert
(forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a3 Int) (b2 Int) (i Int))
(=>
(and (<= a3 i) (< i b2))
(=>
(forall ((j Int))
(=>
(and (<= a3 j) (< j b2))
(=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
(=>
(not (= (infix_at p1 i) true))
(=> (= (infix_at p2 i) true) (> (numof p2 a3 b2) (numof p1 a3 b2))))))))
;; "numof_change_equiv"
(assert
(forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a3 Int) (b2 Int))
(=>
(forall ((j Int))
(=>
(and (<= a3 j) (< j b2))
(= (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
(= (numof p2 a3 b2) (numof p1 a3 b2)))))
;; "fc"
(declare-fun fc (par (a1)
((array a1)
a1) (infix_mngt Int
Bool)))
;; "fc'def"
(assert (par (a1)
(forall ((a3 (array a1)) (v a1) (i Int))
(= (= (infix_at (fc a3 v) i) true) (= (mixfix_lbrb1 a3 i) v)))))
;; "numof"
(define-fun numof1 (par (a1)
((a3 (array a1)) (v a1) (l Int) (u Int)) Int
(numof (fc a3 v) l u)))
(declare-sort candidate 0)
;; "a"
(declare-fun a3 () (array candidate))
;; "Requires"
(assert (<= 1 (length a3)))
;; "n"
(define-fun n () Int
(length a3))
;; "length'result'unused"
(define-fun lengthqtresultqtunused () Int
n)
;; "mixfix []'result'unused"
(define-fun mixfix_lbrbqtresultqtunused () candidate
(mixfix_lbrb1 a3 0))
;; "cand'unused"
(define-fun candqtunused () (ref candidate)
(refqtmk (mixfix_lbrb1 a3 0)))
;; "ref'result'unused"
(define-fun refqtresultqtunused () (ref candidate)
(refqtmk (mixfix_lbrb1 a3 0)))
;; "k'unused"
(define-fun kqtunused () (ref Int)
(refqtmk 0))
;; "ref'result'unused"
(define-fun refqtresultqtunused1 () (ref Int)
(refqtmk 0))
;; "infix -'result'unused"
(define-fun infix_mnqtresultqtunused () Int
(- n 1))
;; "H"
(assert (<= 0 (+ (- n 1) 1)))
;; "k"
(declare-fun k () Int)
;; "cand"
(declare-fun cand () candidate)
;; "cand'unused"
(define-fun candqtunused1 () (ref candidate)
(refqtmk cand))
;; "k"
(define-fun k1 () (ref Int)
(refqtmk k))
;; "i"
(declare-fun i () Int)
;; "H"
(assert (<= 0 i))
;; "H"
(assert (<= i (- n 1)))
;; "H"
(assert (<= 0 k))
;; "H"
(assert (<= k (numof1 a3 cand 0 i)))
;; "LoopInvariant"
(assert (<= (* 2 (- (numof1 a3 cand 0 i) k)) (- i k)))
;; "LoopInvariant"
(assert
(forall ((c candidate))
(=> (not (= c cand)) (<= (* 2 (numof1 a3 c 0 i)) (- i k)))))
;; "prefix !'result'unused"
(define-fun prefix_exqtresultqtunused () Int
k)
;; "infix ='result'unused"
(define-fun infix_eqqtresultqtunused () Bool
(ite (= k 0) true false))
;; "H"
(assert (= k 0))
;; "mixfix []'result'unused"
(define-fun mixfix_lbrbqtresultqtunused1 () candidate
(mixfix_lbrb1 a3 i))
;; "cand"
(declare-fun cand1 () candidate)
;; "cand'unused"
(define-fun candqtunused2 () (ref candidate)
(refqtmk cand1))
;; "Ensures"
(assert (= cand1 (mixfix_lbrb1 a3 i)))
;; "k"
(declare-fun k2 () Int)
;; "k'unused"
(define-fun kqtunused1 () (ref Int)
(refqtmk k2))
;; "Ensures"
(assert (= k2 1))
;; "H"
(assert (<= 0 k2))
;; "H"
(assert (<= k2 (numof1 a3 cand1 0 (+ i 1))))
;; "LoopInvariant"
(assert (<= (* 2 (- (numof1 a3 cand1 0 (+ i 1)) k2)) (- (+ i 1) k2)))
;; "c"
(declare-fun c () candidate)
;; "H"
(assert (not (= c cand1)))
;; "Hinst"
;;(assert (=> (not (= c cand)) (<= (* 2 (numof1 a3 c 0 i)) (- i k))))
;;(assert (= (numof1 a3 c 0 i) (numof (fc a3 c) 0 i)))
;;(assert (= (numof (fc a3 c) 0 i) (numof (fc a3 c) 0 i)))
;;(assert (= (numof1 a3 c 0 i) (numof1 a3 c 0 i)))
;;(assert (= (numof (fc a3 c) 0 (+ i 1)) (numof (fc a3 c) 0 (+ i 1))))
(assert (let ((p (fc a3 c))(a3 0)(b2 (+ i 1)))
(ite (<= b2 a3)
(= (numof p a3 b2) 0)
(ite (= (infix_at p (- b2 1)) true)
(= (numof p a3 b2) (+ 1 (numof p a3 (- b2 1))))
(= (numof p a3 b2) (numof p a3 (- b2 1)))))))
;; Goal "mjrty'vc"
;; File "/home/bobot/Sources/why3.master/examples/mjrty.mlw", line 36, characters 6-11
(assert (not (<= (* 2 (numof1 a3 c 0 (+ i 1))) (- (+ i 1) k2))))
(check-sat)
colibri2/theories/quantifier/definitions.ml
+ 9
− 2
View file @ e7595b2c
......@@ -35,6 +35,8 @@ let criteria d (_sym : Expr.Term.Const.t) _tyl _tvl (body : Expr.term) =
| Expr.Binder (_, _) -> false
| Expr.Match (_, _) -> false
let nb_eager_folding = 25
let handler d (sym : Expr.Term.Const.t) tyl tvl body =
if criteria d sym tyl tvl body then
let tys, tvs =
......@@ -44,6 +46,7 @@ let handler d (sym : Expr.Term.Const.t) tyl tvl body =
List.for_all (fun v -> Expr.Ty.Var.S.mem v tys) tyl
&& List.for_all (fun v -> Expr.Term.Var.S.mem v tvs) tvl
then
let nb_folding = Context.Ref.create (Egraph.context d) (-1) in
match Pattern.of_term_exn ~subst:Ground.Subst.empty body with
| exception Pattern.Unconvertible -> ()
| pat ->
......@@ -63,7 +66,11 @@ let handler d (sym : Expr.Term.Const.t) tyl tvl body =
Debug.dprintf2 Common.debug "Fold definition of %a" Ground.Term.pp
t;
let n = Ground.node (Ground.index t) in
DaemonLastEffortUncontextual.schedule_immediately d (fun d ->
Egraph.register d n))
if Context.Ref.get nb_folding < nb_eager_folding then (
Context.Ref.incr nb_folding;
Egraph.register d n)
else
DaemonLastEffortUncontextual.schedule_immediately d (fun d ->
Egraph.register d n))
let th_register d = Ground.Defs.add_handler d handler
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment