Rebase of Optim Alt-Ergo

alt-ergo-lib.opam

@@ -1,5 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+version: "dev"
 synopsis: "The Alt-Ergo SMT prover library"
 description: """
 This is the core library used in the Alt-Ergo SMT solver.

alt-ergo-parsers.opam

@@ -1,5 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+version: "dev"
 synopsis: "The Alt-Ergo SMT prover parser library"
 description: """
 This is the parser library used in the Alt-Ergo SMT solver.

alt-ergo.opam

@@ -1,5 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+version: "dev"
 synopsis: "The Alt-Ergo SMT prover"
 description: """
 Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.

altgr-ergo.opam

@@ -1,5 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+version: "dev"
 synopsis: "The GUI for the Alt-Ergo SMT prover"
 description: """
 Altgr-Ergo is the graphical interface for the Alt-Ergo SMT prover.

dune-project

@@ -4,6 +4,7 @@
 (generate_opam_files true)
 
 (name alt-ergo)
+(version dev)
 (authors "Alt-Ergo developers")
 (maintainers "Alt-Ergo developers")
 (source (github OCamlPro/alt-ergo))

examples/optim-examples/bug-disj.ae

@@ -0,0 +1,13 @@
+logic m1, m2, ae : prop
+logic A, M, S : int
+
+axiom a1:
+ if ae then A = 0 else A = 1
+
+axiom a2:
+ if (m1 or m2) then M = 0 else M = 1
+
+goal g:
+ S = A + M ->
+ minimize(S, 1) ->
+ false

examples/optim-examples/bug-disj.smt2

@@ -0,0 +1,12 @@
+logic m1, m2, ae : prop
+logic x, y : int
+
+axiom a1:
+ x = if ae then 0 else 1
+
+axiom a2:
+ y = if (m1 or m2) then 0 else 1
+
+goal g:
+ minimize(x + y, 1) ->
+ false

examples/optim-examples/bug-soudness-if-split-beyond-unbounded-vals.ae

@@ -0,0 +1,12 @@
+logic x, y, z : int
+
+axiom a: 0 <= x <= 33
+
+axiom a: minimize (z, 3)
+axiom a: maximize (x, 1)
+axiom a: maximize (y, 2)
+
+goal g:
+ 1 <= z <= 11 ->
+ 0 <= y  <= 10 ->
+ false

examples/optim-examples/challenge.ae

@@ -0,0 +1,14 @@
+logic x : int
+logic y : int
+logic P : int -> prop
+logic Q : prop
+
+goal g:
+maximize(x,1) ->
+maximize(y,2) ->
+
+P(x) -> (* just to introduce x and set its max to +infinity *)
+ (Q and (0 <= y <= 10)) or (not Q and (1000 <= y <= 1000)) ->
+
+(*x <= 50 ->*)
+ false

examples/optim-examples/disj-1.ae

@@ -0,0 +1,38 @@
+logic x, y : int
+logic p, q : int -> prop
+
+(*
+goal g: (* max is 200 *)
+maximize(x, 1) ->
+0 <= x <= 1000 ->
+((x <= 50) or (x <= 200)) ->
+false
+*)
+
+(*
+goal g: (* max is 200 *)
+  maximize(x, 1) ->
+  ((y >= 10) or (y <= 200)) ->
+  false
+*)
+
+
+(*
+goal g:
+maximize(x, 1) ->
+(p(x) or q(x))
+*)
+
+(*
+goal g: (* max is x = 50, y = 500 *)
+  maximize(x, 1) ->
+  maximize(y, 2) ->
+  ((x <= 50 and y <= 300) or (x = 50 and y <= 500)) ->
+  false
+*)
+
+goal g: (* max is x = 50, y = 500 *)
+  maximize(x, 1) ->
+  maximize(y, 2) ->
+  ((x <= 40 and y <= 500) or (x <= 50 and y <= 300)) ->
+  false

examples/optim-examples/incrementality.ae

@@ -0,0 +1,14 @@
+logic x, y, z, t,u  : int
+
+goal g:
+ maximize(x, 1) ->
+ minimize(y, 2) ->
+ maximize(z, 3) ->
+ 0 <= x <= 10 ->
+ 0 <= y - 2 * x <= 100 ->
+ 0 <= z  <= x * y ->
+ 10 < t  ->
+ -50 <= u <= 40 ->
+ maximize(u, 4) ->
+
+ false

examples/optim-examples/issue-6.ae

@@ -0,0 +1,13 @@
+logic x, y : int
+logic f : int -> int
+
+goal g:
+  maximize(f(x), 1) ->
+  maximize(x, 2) ->
+  maximize(y, 3) ->
+  maximize(f(y), 4) ->
+  f(y) >= 20 ->
+  x > y ->
+  0 <= x ->
+  0 <= f(x) <= 10 ->
+  false

examples/optim-examples/issue-7-b.ae

@@ -0,0 +1,11 @@
+logic x : int
+logic f : int -> int
+logic P : int -> prop
+
+goal g:
+  maximize(x,1) ->
+  maximize(f(x), 2) ->
+  P(x) ->
+  0 <= f(x) <= 100 ->
+  1 <= x <= 5 -> (* ordering of constraints is important *)
+  false

examples/optim-examples/issue-7.ae

@@ -0,0 +1,12 @@
+logic x, y : int
+logic f : int -> int
+logic P : int -> prop
+
+goal g:
+  P(x) ->
+  0 <= f(x) <= 100 ->
+  f(y) = 50 ->
+  x = 1 -> (* ordering of constraints is important *)
+  maximize(x,1) ->
+  maximize(f(x), 2) ->
+  false

examples/optim-examples/micro.ae

@@ -0,0 +1,20 @@
+goal g1 :
+  forall x : int.
+  forall z : int.
+  maximize(x,1) ->
+  maximize(z,2) ->
+  2 * x <= 125 ->
+  0 <= z <= 10 ->
+  false
+
+(* z is a "don't care" in this second example, because y is already
+unbounded. (although y and z are independant *)
+
+goal g :
+  forall y : int.
+  minimize(y,1) ->
+  3 * y <= 125 ->
+  forall z : int.
+  maximize(z,2) ->
+  0 <= z <= 10 ->
+  false

examples/optim-examples/nano_unbounded.ae

@@ -0,0 +1,4 @@
+goal g :
+forall x : int.
+maximize(x,1) ->
+x >= 0 -> false