Merge pull request #23 from AdrienChampion/master

v1.7

.travis.yml

@@ -18,8 +18,6 @@ env:
   global:
   - RUSTFLAGS="-C link-dead-code"
 
-cache: cargo
-
 addons:
   apt:
     packages:

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "hoice"
-version = "1.5.0"
+version = "1.7.0"
 authors = ["Adrien Champion <adrien.champion@email.com>"]
 description = "A ICE-based Horn clause solver."
 homepage = "https://github.com/hopv/hoice"
@@ -31,14 +31,15 @@ panic = 'unwind'
 bench = [ ]
 
 [dependencies]
+libc = "*"
 lazy_static = "*"
 clap = "*"
 hashconsing = { git = "https://github.com/AdrienChampion/hashconsing" }
 error-chain = "*"
 ansi_term = "*"
-rsmt2 = { git = "https://github.com/kino-mc/rsmt2" }
+rsmt2 = "^0.9.11"
 num = "*"
 mylib = { git = "https://github.com/AdrienChampion/mylib" }
 either = "*"
 rand = "*"
-isatty = "*"
+atty = "*"

rsc/inactive/adt/list-synasc-unsat.smt2

@@ -0,0 +1,20 @@
+(set-logic HORN)
+
+(declare-fun Concat ((List Int) (List Int) (List Int)) Bool)
+
+(assert (forall ((y (List Int)))
+           (Concat nil y y)))
+
+(assert (forall ((x (List Int))(y (List Int))(r (List Int))(i Int))
+           (=> (Concat x y r) (Concat (Cons i x) y (Cons i r)) )))
+
+(assert (forall ((x (List Int))(y (List Int))(r (List Int))(i Int))
+           (=> (Concat x y r) (Concat x y (Cons i r)) )))
+
+(assert (forall ((x (List Int))(y (List Int))(r (List Int)))
+           (=> (and (not (= r nil)) (Concat x y r)) (or (= (head r) (head x)) (= (head r) (head y)) ))))
+
+(assert (forall ((x (List Int))(y (List Int))(r (List Int))(nx Int)(ny Int)(nr Int))
+           (=> (and (Concat x y r) (= nx (_size x)) (= ny (_size y)) (= nr (_size r))) (= (+ nr 1) (+ nx ny)))))
+
+(check-sat)

rsc/inactive/adt/list-synasc.smt2

@@ -0,0 +1,21 @@
+(set-logic HORN)
+
+(declare-datatypes () (
+  (IList Nil (Cons (head Int) (tail IList)) )
+))
+
+(declare-fun Concat (IList IList IList) Bool)
+
+(assert (forall ((y IList))
+           (Concat Nil y y)))
+
+(assert (forall ((x IList)(y IList)(r IList)(i Int))
+           (=> (Concat x y r) (Concat (Cons i x) y (Cons i r)) )))
+
+(assert (forall ((x IList)(y IList)(r IList))
+           (=> (and (not (= r Nil)) (Concat x y r)) (or (= (head r) (head x)) (= (head r) (head y)) ))))
+
+(assert (forall ((x IList)(y IList)(r IList)(nx Int)(ny Int)(nr Int))
+           (=> (and (Concat x y r) (= nx (_size x)) (= ny (_size y)) (= nr (_size r))) (= (+ nr 1) (+ nx ny)))))
+
+(check-sat)

rsc/inactive/adt/record-cex.smt2

@@ -0,0 +1,41 @@
+(set-logic HORN)
+
+(declare-datatypes () (
+  (ArRec0 (new (dflt Int)) )
+) )
+
+(define-fun storeRec0 ((new ArRec0) (old ArRec0) (ind Int) (val Int)) Bool
+  (and (= val (dflt old)) (= old new))
+)
+(define-fun selectRec0 ((rec ArRec0) (ind Int)) Int
+  (dflt rec)
+)
+
+(declare-fun p0 ( Int ArRec0 ArRec0) Bool)
+(declare-fun p1 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p2 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p3 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p4 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p5 ( Int ArRec0 ArRec0) Bool)
+(declare-fun p6 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p7 ( Int ArRec0 ArRec0 Int) Bool)
+(declare-fun p8 ( Int ArRec0 ArRec0) Bool)
+
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0))(=> (= n 1) (p0 n a1 a2))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p0 n a1 a2) (= a 0)) (p1 n a1 a2 a))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p1 n a1 a2 a) (<= a (- n 1))) (p2 n a1 a2 a))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int) (a1_p ArRec0))(=> (and (p2 n a1 a2 a) (storeRec0 a1_p a1 a 1)) (p3 n a1_p a2 a))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int) (a2_p ArRec0))(=> (and (p3 n a1 a2 a) (storeRec0 a2_p a2 a 1)) (p4 n a1 a2_p a))))
+
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (p4 n a1 a2 a) (let ((ap (+ a 1))) (p1 n a1 a2 ap)))))
+
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p1 n a1 a2 a) (>= a n)) (p5 n a1 a2))))
+
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p5 n a1 a2) (= a 0)) (p6 n a1 a2 a))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p6 n a1 a2 a) (<= a (- n 1))) (p7 n a1 a2 a))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (p7 n a1 a2 a) (not (= (selectRec0 a1 a) (selectRec0 a2 a))))))
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (and (p6 n a1 a2 a) (>= a n)) (p8 n a1 a2))))
+
+(assert (forall ( (n Int) (a1 ArRec0) (a2 ArRec0) (a Int))(=> (p7 n a1 a2 a) (let ((ap (+ a 1))) (p6 n a1 a2 ap)))))
+
+(check-sat)

rsc/inactive/adt/simple-adt-horn.smt2

@@ -0,0 +1,20 @@
+(set-logic HORN)
+
+(declare-datatypes () (
+  (Pair (P (left Int) (right Bool)) )
+) )
+
+(declare-fun I1 (Pair) Bool)
+(declare-fun I2 (Pair) Bool)
+
+(assert (forall ((unused Bool)) (I1 (P 0 true))))
+(assert (forall ((p Pair))
+           (=> (I1 p) (I2 (P (+ (left p) 1) (not (right p)))))))
+(assert (forall ((p Pair))
+           (=> (I2 p) (I1 (P (* (left p) 2) (not (right p)))))))
+
+(assert (forall ((p Pair))
+           (=> (I1 p) (and (>= (left p) 0) (right p)))))
+
+(check-sat)
+(get-model)

rsc/inactive/adt/sorted.smt2

@@ -0,0 +1,108 @@
+(set-logic HORN)
+
+(declare-datatypes () (
+  (Lst nil (cons (head Int) (tail Lst)))
+) )
+
+
+; let rev =
+;   let rec loop acc = function
+;   | [] -> acc
+;   | h :: t -> loop (h :: acc) t
+;   in
+;   loop []
+
+; Post-condition.
+(declare-fun
+  rev_pst ( Lst Lst Lst ) Bool
+)
+; Terminal case.
+(assert
+  (forall ( (acc Lst) )
+    (rev_pst acc nil acc)
+) )
+; Recursive case.
+(assert
+  (forall ( (acc Lst) (lst Lst) (res Lst) )
+  (=>
+    (and
+      (not (= lst nil))
+      (rev_pst
+        (cons (head lst) acc)
+        (tail lst)
+        res
+      )
+    )
+    (rev_pst acc lst res)
+  )
+) )
+
+
+; let rec sorted = function
+; | nil | _ :: nil => true
+; | h1 :: h2 :: t => (h1 < h2) and (sorted (h2 :: t))
+; (* STRICTLY sorted~~~~~^ *)
+
+; Post-condition.
+(declare-fun
+  srt_pst ( Lst Bool ) Bool
+)
+; Terminal cases.
+(assert
+  (forall ( (unused Bool) )
+  (srt_pst nil true)
+) )
+(assert
+  (forall ( (hd Int) )
+  (srt_pst (cons hd nil) true)
+) )
+(assert
+  (forall ( (lst Lst) )
+  (=>
+    (and
+      (not (= lst nil))
+      (not (= (tail lst) nil))
+      (not (< (head lst) (head (tail lst))))
+    )
+    (srt_pst lst false)
+  )
+) )
+; Recursive case.
+(assert
+  (forall ( (lst Lst) (res Bool) )
+  (=>
+    (and
+      (not (= lst nil))
+      (not (= (tail lst) nil))
+      (< (head lst) (head (tail lst)))
+      (srt_pst (tail lst) res)
+    )
+    (srt_pst lst res)
+  )
+) )
+
+
+; let main lst =
+;   if lst = (rev lst)
+;   and (sorted lst)
+;   and (sorted (rev lst))
+;   then match lst
+;   | nil | _ :: nil => ()
+;   | _ => assert false
+(assert
+  (forall ( (lst1 Lst) (lst2 Lst) )
+  (=>
+    (and
+      (rev_pst nil lst1 lst2)
+      (srt_pst lst1 true)
+      (srt_pst lst2 true)
+      (not (= lst1 nil))
+      (not (= (tail lst1) nil))
+    )
+    false
+  )
+) )
+
+
+(check-sat)
+(get-model)