diff --git a/build.sbt b/build.sbt
index 4486befa0059e552e805929e0c5876c5cc8eba8a..4a6567e6ec23a273f612585422f12c40db971cb5 100644
--- a/build.sbt
+++ b/build.sbt
@@ -55,7 +55,7 @@ testOptions in ItTest := Seq(Tests.Argument("-oDF"))
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10eaaee4ea0ff6567f4f866922cb871bae2da0ac")
-lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "567ede66f8df3e5cfc3dbcd5d01b4e7a65fd0719")
+lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "850580ae86e299a1baa0eaef9e24eed905fefe58")
lazy val root = (project in file("."))
.configs(IntegrationTest)
diff --git a/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-0.tip b/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-0.tip
new file mode 100644
index 0000000000000000000000000000000000000000..f4b839e5c103294823b57bab63ae0ca07c72479d
--- /dev/null
+++ b/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-0.tip
@@ -0,0 +1,13 @@
+(declare-datatypes (A1!1 A2!0 R!22) ((fun2!1 (fun2!2 (f!36 (=> A1!1 A2!0 R!22)) (pre!10 (=> A1!1 A2!0 Bool))))))
+
+(define-fun (par (A!1) (isCommutative!0 ((f!1 (fun2!1 A!1 A!1 A!1))) Bool (forall ((x!1 A!1)(y!1 A!1)) (= (assume (@ (pre!10 f!1) x!1 y!1) (@ (f!36 f!1) x!1 y!1)) (assume (@ (pre!10 f!1) y!1 x!1) (@ (f!36 f!1) y!1 x!1)))))))
+
+(declare-const (par (A!4) (f!4 (fun2!1 A!4 A!4 A!4))))
+
+(define-fun (par (A!0) (isAssociative!0 ((f!0 (fun2!1 A!0 A!0 A!0))) Bool (forall ((x!0 A!0)(y!0 A!0) (z!0 A!0)) (= (assume (@ (pre!10 f!0) (assume (@ (pre!10 f!0) x!0 y!0) (@ (f!36 f!0) x!0 y!0)) z!0) (@ (f!36 f!0) (assume (@ (pre!10 f!0) x!0 y!0) (@ (f!36 f!0) x!0 y!0)) z!0)) (assume (@ (pre!10 f!0) x!0 (assume (@ (pre!10 f!0) y!0 z!0) (@ (f!36 f!0) y!0 z!0))) (@ (f!36 f!0) x!0 (assume (@ (pre!10 f!0) y!0 z!0) (@ (f!36 f!0) y!0 z!0)))))))))
+
+(assert (par (A!4) (not (=> (isCommutative!0 (as f!4 (fun2!1 A!4 A!4 A!4))) (isAssociative!0 (as f!4 (fun2!1 A!4 A!4 A!4)))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-1.tip b/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-1.tip
new file mode 100644
index 0000000000000000000000000000000000000000..f78677222e0a53b6986bcdafe1d2396912766e6a
--- /dev/null
+++ b/src/it/resources/regression/tip/SAT/AssociativityProperties.scala-1.tip
@@ -0,0 +1,13 @@
+(declare-datatypes (A1!1 A2!0 R!22) ((fun2!5 (fun2!6 (f!40 (=> A1!1 A2!0 R!22)) (pre!12 (=> A1!1 A2!0 Bool))))))
+
+(define-fun (par (A!0) (isAssociative!0 ((f!0 (fun2!5 A!0 A!0 A!0))) Bool (forall ((x!0 A!0)(y!0 A!0) (z!0 A!0)) (= (assume (@ (pre!12 f!0) (assume (@ (pre!12 f!0) x!0 y!0) (@ (f!40 f!0) x!0 y!0)) z!0) (@ (f!40 f!0) (assume (@ (pre!12 f!0) x!0 y!0) (@ (f!40 f!0) x!0 y!0)) z!0)) (assume (@ (pre!12 f!0) x!0 (assume (@ (pre!12 f!0) y!0 z!0) (@ (f!40 f!0) y!0 z!0))) (@ (f!40 f!0) x!0 (assume (@ (pre!12 f!0) y!0 z!0) (@ (f!40 f!0) y!0 z!0)))))))))
+
+(declare-const (par (A!3) (f!3 (fun2!5 A!3 A!3 A!3))))
+
+(define-fun (par (A!1) (isCommutative!0 ((f!1 (fun2!5 A!1 A!1 A!1))) Bool (forall ((x!1 A!1)(y!1 A!1)) (= (assume (@ (pre!12 f!1) x!1 y!1) (@ (f!40 f!1) x!1 y!1)) (assume (@ (pre!12 f!1) y!1 x!1) (@ (f!40 f!1) y!1 x!1)))))))
+
+(assert (par (A!3) (not (=> (isAssociative!0 (as f!3 (fun2!5 A!3 A!3 A!3))) (isCommutative!0 (as f!3 (fun2!5 A!3 A!3 A!3)))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/SAT/BraunTree.scala-1.tip b/src/it/resources/regression/tip/SAT/BraunTree.scala-1.tip
new file mode 100644
index 0000000000000000000000000000000000000000..c6d86b69029791edc0e60a5a6d3c36897df36aa5
--- /dev/null
+++ b/src/it/resources/regression/tip/SAT/BraunTree.scala-1.tip
@@ -0,0 +1,25 @@
+(declare-datatypes () ((Tree!3 (Leaf!3) (Node!3 (value!6 (_ BitVec 32)) (left!8 Tree!3) (right!8 Tree!3)))))
+
+(declare-const |error: Match is non-exhaustive!58| (_ BitVec 32))
+
+(define-fun-rec height!0 ((tree!1 Tree!3)) (_ BitVec 32) (ite (is-Node!3 tree!1) (let ((l!0 (height!0 (left!8 tree!1)))) (let ((r!0 (height!0 (right!8 tree!1)))) (let ((max!0 (ite (bvsgt l!0 r!0) l!0 r!0))) (bvadd #b00000000000000000000000000000001 max!0)))) (ite (is-Leaf!3 tree!1) #b00000000000000000000000000000000 |error: Match is non-exhaustive!58|)))
+
+(declare-const |error: Match is non-exhaustive!62| Bool)
+
+(define-fun-rec isBraun!0 ((tree!2 Tree!3)) Bool (ite (is-Node!3 tree!2) (and (and (isBraun!0 (left!8 tree!2)) (isBraun!0 (right!8 tree!2))) (let ((l!1 (height!0 (left!8 tree!2)))) (let ((r!1 (height!0 (right!8 tree!2)))) (or (= l!1 r!1) (= l!1 (bvadd r!1 #b00000000000000000000000000000001)))))) (ite (is-Leaf!3 tree!2) true |error: Match is non-exhaustive!62|)))
+
+(declare-const tree!0 Tree!3)
+
+(declare-const |error: Match is non-exhaustive!27| Tree!3)
+
+(define-fun-rec insert!0 ((tree!0 Tree!3) (x!0 (_ BitVec 32))) Tree!3 (assume (isBraun!0 tree!0) (let ((res!0 (ite (is-Node!3 tree!0) (Node!3 (value!6 tree!0) (insert!0 (left!8 tree!0) x!0) (right!8 tree!0)) (ite (is-Leaf!3 tree!0) (Node!3 x!0 Leaf!3 Leaf!3) |error: Match is non-exhaustive!27|)))) (assume (isBraun!0 res!0) res!0))))
+
+(declare-const x!0 (_ BitVec 32))
+
+(declare-const |error: Match is non-exhaustive!76| Tree!3)
+
+(assert (not (=> (isBraun!0 tree!0) (isBraun!0 (ite (is-Node!3 tree!0) (Node!3 (value!6 tree!0) (insert!0 (left!8 tree!0) x!0) (right!8 tree!0)) (ite (is-Leaf!3 tree!0) (Node!3 x!0 Leaf!3 Leaf!3) |error: Match is non-exhaustive!76|))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/SAT/PositiveMap.scala-0.tip b/src/it/resources/regression/tip/SAT/PositiveMap.scala-0.tip
new file mode 100644
index 0000000000000000000000000000000000000000..6b1e9120d9741beb0935ee00071d3afa3d8a0c9d
--- /dev/null
+++ b/src/it/resources/regression/tip/SAT/PositiveMap.scala-0.tip
@@ -0,0 +1,23 @@
+(declare-datatypes () ((List!5 (Nil!2) (Cons!2 (head!5 (_ BitVec 32)) (tail!7 List!5)))))
+
+(declare-const |error: Match is non-exhaustive!46| Bool)
+
+(define-fun-rec positive!0 ((list!0 List!5)) Bool (ite (is-Cons!2 list!0) (ite (bvslt (head!5 list!0) #b00000000000000000000000000000000) false (positive!0 (tail!7 list!0))) (ite (is-Nil!2 list!0) true |error: Match is non-exhaustive!46|)))
+
+(declare-const list!1 List!5)
+
+(declare-datatypes (A1!0 R!21) ((fun1!1 (fun1!2 (f!32 (=> A1!0 R!21)) (pre!10 (=> A1!0 Bool))))))
+
+(declare-const f!0 (fun1!1 (_ BitVec 32) (_ BitVec 32)))
+
+(declare-const |error: Match is non-exhaustive!42| List!5)
+
+(define-fun-rec positiveMap_failling_1!0 ((f!0 (fun1!1 (_ BitVec 32) (_ BitVec 32))) (list!1 List!5)) List!5 (let ((res!0 (ite (is-Cons!2 list!1) (let ((fh!0 (assume (@ (pre!10 f!0) (head!5 list!1)) (@ (f!32 f!0) (head!5 list!1))))) (let ((nh!0 (ite (bvslt fh!0 #b11111111111111111111111111111111) #b00000000000000000000000000000000 fh!0))) (Cons!2 nh!0 (positiveMap_failling_1!0 f!0 (tail!7 list!1))))) (ite (is-Nil!2 list!1) Nil!2 |error: Match is non-exhaustive!42|)))) (assume (positive!0 res!0) res!0)))
+
+(declare-const |error: Match is non-exhaustive!75| List!5)
+
+(assert (not (positive!0 (ite (is-Cons!2 list!1) (let ((fh!0 (assume (@ (pre!10 f!0) (head!5 list!1)) (@ (f!32 f!0) (head!5 list!1))))) (Cons!2 (ite (bvslt fh!0 #b11111111111111111111111111111111) #b00000000000000000000000000000000 fh!0) (positiveMap_failling_1!0 f!0 (tail!7 list!1)))) (ite (is-Nil!2 list!1) Nil!2 |error: Match is non-exhaustive!75|)))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-0.tip b/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-0.tip
new file mode 100644
index 0000000000000000000000000000000000000000..cf80afb9b492307198009137099af6776b8de82b
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-0.tip
@@ -0,0 +1,22 @@
+(declare-datatypes () ((Tree!1 (Node!1 (left!3 Tree!1) (value!2 Int) (right!3 Tree!1)) (Leaf!1))))
+
+(define-fun (par (T!2) (empty!0 () (Set T!2) (as emptyset T!2))))
+
+(declare-const |error: Match is non-exhaustive!25| (Set Int))
+
+(define-fun-rec content!0 ((thiss!51 Tree!1)) (Set Int) (ite (is-Leaf!1 thiss!51) (as empty!0 (Set Int)) (ite (is-Node!1 thiss!51) (union (union (content!0 (left!3 thiss!51)) (insert (as emptyset Int) (value!2 thiss!51))) (content!0 (right!3 thiss!51))) |error: Match is non-exhaustive!25|)))
+
+(define-fun inv!0 ((thiss!14 Tree!1)) Bool (and (forall ((x!0 Int)) (=> (member x!0 (content!0 (left!3 thiss!14))) (< x!0 (value!2 thiss!14)))) (forall ((x!1 Int)) (=> (member x!1 (content!0 (right!3 thiss!14))) (< (value!2 thiss!14) x!1)))))
+
+(datatype-invariant thiss!114 Tree!1 (ite (is-Node!1 thiss!114) (inv!0 (assume (is-Node!1 thiss!114) thiss!114)) true))
+(declare-const tree!0 Tree!1)
+
+(define-fun inv!2 ((thiss!114 Tree!1)) Bool (ite (is-Node!1 thiss!114) (inv!0 (assume (is-Node!1 thiss!114) thiss!114)) true))
+
+(declare-const value!1 Int)
+
+(assert (not (=> (is-Leaf!1 tree!0) (inv!2 (Node!1 (assume (inv!2 Leaf!1) Leaf!1) value!1 (assume (inv!2 Leaf!1) Leaf!1))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-1.tip b/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-1.tip
new file mode 100644
index 0000000000000000000000000000000000000000..ec3af400454f20c539f9528f308633c017f87a4d
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-1.tip
@@ -0,0 +1,29 @@
+(declare-datatypes () ((Tree!17 (Node!17 (left!19 Tree!17) (value!18 Int) (right!19 Tree!17)) (Leaf!17))))
+
+(define-fun (par (T!2) (empty!0 () (Set T!2) (as emptyset T!2))))
+
+(declare-const |error: Match is non-exhaustive!25| (Set Int))
+
+(define-fun-rec content!0 ((thiss!51 Tree!17)) (Set Int) (ite (is-Leaf!17 thiss!51) (as empty!0 (Set Int)) (ite (is-Node!17 thiss!51) (union (union (content!0 (left!19 thiss!51)) (insert (as emptyset Int) (value!18 thiss!51))) (content!0 (right!19 thiss!51))) |error: Match is non-exhaustive!25|)))
+
+(declare-const tree!0 Tree!17)
+
+(define-fun inv!0 ((thiss!14 Tree!17)) Bool (and (forall ((x!0 Int)) (=> (member x!0 (content!0 (left!19 thiss!14))) (< x!0 (value!18 thiss!14)))) (forall ((x!1 Int)) (=> (member x!1 (content!0 (right!19 thiss!14))) (< (value!18 thiss!14) x!1)))))
+
+(define-fun inv!2 ((thiss!114 Tree!17)) Bool (ite (is-Node!17 thiss!114) (inv!0 (assume (is-Node!17 thiss!114) thiss!114)) true))
+
+(declare-const value!1 Int)
+
+(declare-const |error: Match is non-exhaustive!51| Tree!17)
+
+(define-fun-rec insert!0 ((tree!0 Tree!17) (value!1 Int)) Tree!17 (let ((res!0 (ite (is-Leaf!17 tree!0) (assume (inv!2 (Node!17 (assume (inv!2 Leaf!17) Leaf!17) value!1 (assume (inv!2 Leaf!17) Leaf!17))) (Node!17 (assume (inv!2 Leaf!17) Leaf!17) value!1 (assume (inv!2 Leaf!17) Leaf!17))) (ite (is-Node!17 tree!0) (ite (< (value!18 tree!0) value!1) (assume (inv!2 (Node!17 (left!19 tree!0) (value!18 tree!0) (insert!0 (right!19 tree!0) value!1))) (Node!17 (left!19 tree!0) (value!18 tree!0) (insert!0 (right!19 tree!0) value!1))) (ite (> (value!18 tree!0) value!1) (assume (inv!2 (Node!17 (insert!0 (left!19 tree!0) value!1) (value!18 tree!0) (right!19 tree!0))) (Node!17 (insert!0 (left!19 tree!0) value!1) (value!18 tree!0) (right!19 tree!0))) (assume (inv!2 (Node!17 (left!19 tree!0) (value!18 tree!0) (right!19 tree!0))) (Node!17 (left!19 tree!0) (value!18 tree!0) (right!19 tree!0))))) |error: Match is non-exhaustive!51|)))) (assume (= (content!0 res!0) (union (content!0 tree!0) (insert (as emptyset Int) value!1))) res!0)))
+
+(declare-const |error: Match is non-exhaustive!75| Tree!17)
+
+(datatype-invariant thiss!114 Tree!17 (ite (is-Node!17 thiss!114) (inv!0 (assume (is-Node!17 thiss!114) thiss!114)) true))
+
+(assert (not (= (content!0 (ite (is-Leaf!17 tree!0) (assume (inv!2 (Node!17 (assume (inv!2 Leaf!17) Leaf!17) value!1 (assume (inv!2 Leaf!17) Leaf!17))) (Node!17 (assume (inv!2 Leaf!17) Leaf!17) value!1 (assume (inv!2 Leaf!17) Leaf!17))) (ite (is-Node!17 tree!0) (ite (< (value!18 tree!0) value!1) (assume (inv!2 (Node!17 (left!19 tree!0) (value!18 tree!0) (insert!0 (right!19 tree!0) value!1))) (Node!17 (left!19 tree!0) (value!18 tree!0) (insert!0 (right!19 tree!0) value!1))) (ite (> (value!18 tree!0) value!1) (assume (inv!2 (Node!17 (insert!0 (left!19 tree!0) value!1) (value!18 tree!0) (right!19 tree!0))) (Node!17 (insert!0 (left!19 tree!0) value!1) (value!18 tree!0) (right!19 tree!0))) (assume (inv!2 (Node!17 (left!19 tree!0) (value!18 tree!0) (right!19 tree!0))) (Node!17 (left!19 tree!0) (value!18 tree!0) (right!19 tree!0))))) |error: Match is non-exhaustive!75|))) (union (content!0 tree!0) (insert (as emptyset Int) value!1)))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/Closures2.scala-0.tip b/src/it/resources/regression/tip/UNSAT/Closures2.scala-0.tip
new file mode 100644
index 0000000000000000000000000000000000000000..96aefd1820861edd19bbf7fc3efcd9436242ae52
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/Closures2.scala-0.tip
@@ -0,0 +1,13 @@
+(declare-datatypes (A1!0 R!21) ((fun1!1 (fun1!2 (f!31 (=> A1!0 R!21)) (pre!10 (=> A1!0 Bool))))))
+
+(define-fun union!0 ((s1!0 (fun1!1 (_ BitVec 32) Bool)) (s2!0 (fun1!1 (_ BitVec 32) Bool))) (fun1!1 (_ BitVec 32) Bool) (fun1!2 (lambda ((x!1 (_ BitVec 32))) (or (assume (@ (pre!10 s1!0) x!1) (@ (f!31 s1!0) x!1)) (assume (@ (pre!10 s2!0) x!1) (@ (f!31 s2!0) x!1)))) (lambda ((x!44 (_ BitVec 32))) true)))
+
+(define-fun set!0 ((i!0 (_ BitVec 32))) (fun1!1 (_ BitVec 32) Bool) (fun1!2 (lambda ((x!0 (_ BitVec 32))) (= x!0 i!0)) (lambda ((x!45 (_ BitVec 32))) true)))
+
+(define-fun set123!0 () (fun1!1 (_ BitVec 32) Bool) (union!0 (set!0 #b00000000000000000000000000000001) (union!0 (set!0 #b00000000000000000000000000000010) (set!0 #b00000000000000000000000000000011))))
+
+(assert (not (let ((s2!3 (union!0 set123!0 (set!0 #b00000000000000000000000000000100)))) (let ((holds!29 (and (and (and (assume (@ (pre!10 s2!3) #b00000000000000000000000000000001) (@ (f!31 s2!3) #b00000000000000000000000000000001)) (assume (@ (pre!10 s2!3) #b00000000000000000000000000000010) (@ (f!31 s2!3) #b00000000000000000000000000000010))) (assume (@ (pre!10 s2!3) #b00000000000000000000000000000011) (@ (f!31 s2!3) #b00000000000000000000000000000011))) (assume (@ (pre!10 s2!3) #b00000000000000000000000000000100) (@ (f!31 s2!3) #b00000000000000000000000000000100))))) holds!29))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/Closures2.scala-1.tip b/src/it/resources/regression/tip/UNSAT/Closures2.scala-1.tip
new file mode 100644
index 0000000000000000000000000000000000000000..64fbf0fa1091e0591984ef69dc1aeb5c693d7f0c
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/Closures2.scala-1.tip
@@ -0,0 +1,13 @@
+(declare-datatypes (A1!0 R!21) ((fun1!5 (fun1!6 (f!33 (=> A1!0 R!21)) (pre!12 (=> A1!0 Bool))))))
+
+(define-fun union!0 ((s1!0 (fun1!5 (_ BitVec 32) Bool)) (s2!0 (fun1!5 (_ BitVec 32) Bool))) (fun1!5 (_ BitVec 32) Bool) (fun1!6 (lambda ((x!1 (_ BitVec 32))) (or (assume (@ (pre!12 s1!0) x!1) (@ (f!33 s1!0) x!1)) (assume (@ (pre!12 s2!0) x!1) (@ (f!33 s2!0) x!1)))) (lambda ((x!44 (_ BitVec 32))) true)))
+
+(define-fun set!0 ((i!0 (_ BitVec 32))) (fun1!5 (_ BitVec 32) Bool) (fun1!6 (lambda ((x!0 (_ BitVec 32))) (= x!0 i!0)) (lambda ((x!45 (_ BitVec 32))) true)))
+
+(define-fun set123!0 () (fun1!5 (_ BitVec 32) Bool) (union!0 (set!0 #b00000000000000000000000000000001) (union!0 (set!0 #b00000000000000000000000000000010) (set!0 #b00000000000000000000000000000011))))
+
+(assert (not (let ((s3!1 (union!0 set123!0 set123!0))) (let ((holds!31 (and (and (assume (@ (pre!12 s3!1) #b00000000000000000000000000000001) (@ (f!33 s3!1) #b00000000000000000000000000000001)) (assume (@ (pre!12 s3!1) #b00000000000000000000000000000010) (@ (f!33 s3!1) #b00000000000000000000000000000010))) (assume (@ (pre!12 s3!1) #b00000000000000000000000000000011) (@ (f!33 s3!1) #b00000000000000000000000000000011))))) holds!31))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/Closures2.scala-2.tip b/src/it/resources/regression/tip/UNSAT/Closures2.scala-2.tip
new file mode 100644
index 0000000000000000000000000000000000000000..df38d5557fb66c698a80e69e6965b7702365c499
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/Closures2.scala-2.tip
@@ -0,0 +1,17 @@
+(declare-datatypes (A1!0 R!21) ((fun1!9 (fun1!10 (f!35 (=> A1!0 R!21)) (pre!14 (=> A1!0 Bool))))))
+
+(define-fun union!0 ((s1!0 (fun1!9 (_ BitVec 32) Bool)) (s2!0 (fun1!9 (_ BitVec 32) Bool))) (fun1!9 (_ BitVec 32) Bool) (fun1!10 (lambda ((x!1 (_ BitVec 32))) (or (assume (@ (pre!14 s1!0) x!1) (@ (f!35 s1!0) x!1)) (assume (@ (pre!14 s2!0) x!1) (@ (f!35 s2!0) x!1)))) (lambda ((x!44 (_ BitVec 32))) true)))
+
+(define-fun set!0 ((i!0 (_ BitVec 32))) (fun1!9 (_ BitVec 32) Bool) (fun1!10 (lambda ((x!0 (_ BitVec 32))) (= x!0 i!0)) (lambda ((x!45 (_ BitVec 32))) true)))
+
+(define-fun set123!0 () (fun1!9 (_ BitVec 32) Bool) (union!0 (set!0 #b00000000000000000000000000000001) (union!0 (set!0 #b00000000000000000000000000000010) (set!0 #b00000000000000000000000000000011))))
+
+(define-fun diff!0 ((s1!2 (fun1!9 (_ BitVec 32) Bool)) (s2!2 (fun1!9 (_ BitVec 32) Bool))) (fun1!9 (_ BitVec 32) Bool) (fun1!10 (lambda ((x!3 (_ BitVec 32))) (and (assume (@ (pre!14 s1!2) x!3) (@ (f!35 s1!2) x!3)) (not (assume (@ (pre!14 s2!2) x!3) (@ (f!35 s2!2) x!3))))) (lambda ((x!43 (_ BitVec 32))) true)))
+
+(define-fun intersection!0 ((s1!1 (fun1!9 (_ BitVec 32) Bool)) (s2!1 (fun1!9 (_ BitVec 32) Bool))) (fun1!9 (_ BitVec 32) Bool) (fun1!10 (lambda ((x!2 (_ BitVec 32))) (and (assume (@ (pre!14 s1!1) x!2) (@ (f!35 s1!1) x!2)) (assume (@ (pre!14 s2!1) x!2) (@ (f!35 s2!1) x!2)))) (lambda ((x!42 (_ BitVec 32))) true)))
+
+(assert (not (let ((s1!4 set123!0)) (let ((holds!30 (let ((s3!0 (diff!0 s1!4 (intersection!0 s1!4 (union!0 (set!0 #b00000000000000000000000000000001) (set!0 #b00000000000000000000000000000011)))))) (and (and (assume (@ (pre!14 s3!0) #b00000000000000000000000000000010) (@ (f!35 s3!0) #b00000000000000000000000000000010)) (not (assume (@ (pre!14 s3!0) #b00000000000000000000000000000001) (@ (f!35 s3!0) #b00000000000000000000000000000001)))) (not (assume (@ (pre!14 s3!0) #b00000000000000000000000000000011) (@ (f!35 s3!0) #b00000000000000000000000000000011))))))) holds!30))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-0.tip b/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-0.tip
new file mode 100644
index 0000000000000000000000000000000000000000..32d0fa071b9df21d23aa0f2a1f16dde59e821048
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-0.tip
@@ -0,0 +1,39 @@
+(declare-datatypes (T!4) ((List!8 (Nil!5) (Cons!5 (h!50 T!4) (t!57 (List!8 T!4))))))
+
+(declare-const list!3 (List!8 Int))
+
+(declare-datatypes (A0!3 A1!13) ((tuple2!4 (tuple2!5 (_1!2 A0!3) (_2!2 A1!13)))))
+
+(declare-const |error: Match is non-exhaustive!67| Int)
+
+(define-fun-rec (par (T!91) (size!0 ((thiss!106 (List!8 T!91))) Int (let ((x$1!2 (ite (is-Nil!5 thiss!106) 0 (ite (is-Cons!5 thiss!106) (+ 1 (size!0 (t!57 thiss!106))) |error: Match is non-exhaustive!67|)))) (assume (>= x$1!2 0) x$1!2)))))
+
+(declare-const |error: Match is non-exhaustive!61| (tuple2!4 (List!8 Int) (List!8 Int)))
+
+(define-fun (par (T!2) (empty!0 () (Bag T!2) (as bag.empty T!2))))
+
+(declare-const (par (T!0) (|error: Match is non-exhaustive!68| (Bag T!0))))
+
+(define-fun-rec (par (T!0) (bag!0 ((list!0 (List!8 T!0))) (Bag T!0) (ite (is-Nil!5 list!0) (as empty!0 (Bag T!0)) (ite (is-Cons!5 list!0) (bag.insert (bag!0 (t!57 list!0)) (h!50 list!0)) (as |error: Match is non-exhaustive!68| (Bag T!0)))))))
+
+(define-fun-rec split!0 ((list!2 (List!8 Int))) (tuple2!4 (List!8 Int) (List!8 Int)) (assume (> (size!0 list!2) 1) (let ((res!1 (ite (and (is-Cons!5 list!2) (<= (size!0 (t!57 list!2)) 2)) (tuple2!5 (Cons!5 (h!50 list!2) (as Nil!5 (List!8 Int))) (t!57 list!2)) (ite (and (is-Cons!5 list!2) (is-Cons!5 (t!57 list!2))) (let ((x$1!0 (tuple2!5 (_1!2 (split!0 (t!57 (t!57 list!2)))) (_2!2 (split!0 (t!57 (t!57 list!2))))))) (let ((s1!0 (_1!2 x$1!0))) (let ((s2!0 (_2!2 x$1!0))) (tuple2!5 (Cons!5 (h!50 list!2) s1!0) (Cons!5 (h!50 (t!57 list!2)) s2!0))))) |error: Match is non-exhaustive!61|)))) (assume (and (and (and (= (bag.union (bag!0 (_1!2 res!1)) (bag!0 (_2!2 res!1))) (bag!0 list!2)) (= (+ (size!0 (_1!2 res!1)) (size!0 (_2!2 res!1))) (size!0 list!2))) (> (size!0 (_1!2 res!1)) 0)) (> (size!0 (_2!2 res!1)) 0)) res!1))))
+
+(define-fun-rec isSorted!0 ((list!1 (List!8 Int))) Bool (ite (and (is-Cons!5 list!1) (is-Cons!5 (t!57 list!1))) (and (<= (h!50 list!1) (h!50 (t!57 list!1))) (isSorted!0 (t!57 list!1))) true))
+
+(declare-const (par (T!31) (|error: Match is non-exhaustive!7| (List!8 T!31))))
+
+(declare-const (par (T!50) (|error: Match is non-exhaustive!26| (Set T!50))))
+
+(define-fun-rec (par (T!50) (content!2 ((thiss!38 (List!8 T!50))) (Set T!50) (ite (is-Nil!5 thiss!38) (as emptyset T!50) (ite (is-Cons!5 thiss!38) (union (insert (as emptyset T!50) (h!50 thiss!38)) (content!2 (t!57 thiss!38))) (as |error: Match is non-exhaustive!26| (Set T!50)))))))
+
+(define-fun-rec (par (T!31) (++!0 ((thiss!10 (List!8 T!31)) (that!10 (List!8 T!31))) (List!8 T!31) (let ((res!5 (ite (is-Nil!5 thiss!10) that!10 (ite (is-Cons!5 thiss!10) (Cons!5 (h!50 thiss!10) (++!0 (t!57 thiss!10) that!10)) (as |error: Match is non-exhaustive!7| (List!8 T!31)))))) (assume (and (and (= (content!2 res!5) (union (content!2 thiss!10) (content!2 that!10))) (= (size!0 res!5) (+ (size!0 thiss!10) (size!0 that!10)))) (or (not (= that!10 (as Nil!5 (List!8 T!31)))) (= res!5 thiss!10))) res!5)))))
+
+(define-fun-rec merge!0 ((l1!0 (List!8 Int)) (l2!0 (List!8 Int))) (List!8 Int) (assume (and (isSorted!0 l1!0) (isSorted!0 l2!0)) (let ((res!0 (ite (and (is-Cons!5 l1!0) (is-Cons!5 l2!0)) (ite (<= (h!50 l1!0) (h!50 l2!0)) (Cons!5 (h!50 l1!0) (merge!0 (t!57 l1!0) l2!0)) (Cons!5 (h!50 l2!0) (merge!0 l1!0 (t!57 l2!0)))) (++!0 l1!0 l2!0)))) (assume (and (and (isSorted!0 res!0) (= (bag!0 res!0) (bag.union (bag!0 l1!0) (bag!0 l2!0)))) (= (size!0 res!0) (+ (size!0 l1!0) (size!0 l2!0)))) res!0))))
+
+(define-fun-rec mergeSort!0 ((list!3 (List!8 Int))) (List!8 Int) (let ((res!2 (ite (and (is-Cons!5 list!3) (is-Cons!5 (t!57 list!3))) (let ((x$2!0 (tuple2!5 (_1!2 (split!0 list!3)) (_2!2 (split!0 list!3))))) (let ((s1!2 (_1!2 x$2!0))) (let ((s2!2 (_2!2 x$2!0))) (merge!0 (mergeSort!0 s1!2) (mergeSort!0 s2!2))))) list!3))) (assume (and (and (isSorted!0 res!2) (= (bag!0 res!2) (bag!0 list!3))) (= (size!0 res!2) (size!0 list!3))) res!2)))
+
+(assert (not (let ((res!34 (ite (and (is-Cons!5 list!3) (is-Cons!5 (t!57 list!3))) (let ((x$2!0 (tuple2!5 (_1!2 (split!0 list!3)) (_2!2 (split!0 list!3))))) (merge!0 (mergeSort!0 (_1!2 x$2!0)) (mergeSort!0 (_2!2 x$2!0)))) list!3))) (and (and (isSorted!0 res!34) (= (bag!0 res!34) (bag!0 list!3))) (= (size!0 res!34) (size!0 list!3))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-1.tip b/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-1.tip
new file mode 100644
index 0000000000000000000000000000000000000000..0e699228036b9b34dc752308bf7e1b8ab7eb6544
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/MergeSort2.scala-1.tip
@@ -0,0 +1,33 @@
+(declare-datatypes (T!4) ((List!16 (Nil!13) (Cons!13 (h!58 T!4) (t!65 (List!16 T!4))))))
+
+(define-fun-rec isSorted!0 ((list!1 (List!16 Int))) Bool (ite (and (is-Cons!13 list!1) (is-Cons!13 (t!65 list!1))) (and (<= (h!58 list!1) (h!58 (t!65 list!1))) (isSorted!0 (t!65 list!1))) true))
+
+(declare-const l1!0 (List!16 Int))
+
+(declare-const l2!0 (List!16 Int))
+
+(declare-const (par (T!31) (|error: Match is non-exhaustive!7| (List!16 T!31))))
+
+(declare-const (par (T!50) (|error: Match is non-exhaustive!26| (Set T!50))))
+
+(define-fun-rec (par (T!50) (content!2 ((thiss!38 (List!16 T!50))) (Set T!50) (ite (is-Nil!13 thiss!38) (as emptyset T!50) (ite (is-Cons!13 thiss!38) (union (insert (as emptyset T!50) (h!58 thiss!38)) (content!2 (t!65 thiss!38))) (as |error: Match is non-exhaustive!26| (Set T!50)))))))
+
+(declare-const |error: Match is non-exhaustive!67| Int)
+
+(define-fun-rec (par (T!91) (size!0 ((thiss!106 (List!16 T!91))) Int (let ((x$1!2 (ite (is-Nil!13 thiss!106) 0 (ite (is-Cons!13 thiss!106) (+ 1 (size!0 (t!65 thiss!106))) |error: Match is non-exhaustive!67|)))) (assume (>= x$1!2 0) x$1!2)))))
+
+(define-fun-rec (par (T!31) (++!0 ((thiss!10 (List!16 T!31)) (that!10 (List!16 T!31))) (List!16 T!31) (let ((res!5 (ite (is-Nil!13 thiss!10) that!10 (ite (is-Cons!13 thiss!10) (Cons!13 (h!58 thiss!10) (++!0 (t!65 thiss!10) that!10)) (as |error: Match is non-exhaustive!7| (List!16 T!31)))))) (assume (and (and (= (content!2 res!5) (union (content!2 thiss!10) (content!2 that!10))) (= (size!0 res!5) (+ (size!0 thiss!10) (size!0 that!10)))) (or (not (= that!10 (as Nil!13 (List!16 T!31)))) (= res!5 thiss!10))) res!5)))))
+
+(define-fun (par (T!2) (empty!0 () (Bag T!2) (as bag.empty T!2))))
+
+(declare-const (par (T!0) (|error: Match is non-exhaustive!68| (Bag T!0))))
+
+(define-fun-rec (par (T!0) (bag!0 ((list!0 (List!16 T!0))) (Bag T!0) (ite (is-Nil!13 list!0) (as empty!0 (Bag T!0)) (ite (is-Cons!13 list!0) (bag.insert (bag!0 (t!65 list!0)) (h!58 list!0)) (as |error: Match is non-exhaustive!68| (Bag T!0)))))))
+
+(define-fun-rec merge!0 ((l1!0 (List!16 Int)) (l2!0 (List!16 Int))) (List!16 Int) (assume (and (isSorted!0 l1!0) (isSorted!0 l2!0)) (let ((res!0 (ite (and (is-Cons!13 l1!0) (is-Cons!13 l2!0)) (ite (<= (h!58 l1!0) (h!58 l2!0)) (Cons!13 (h!58 l1!0) (merge!0 (t!65 l1!0) l2!0)) (Cons!13 (h!58 l2!0) (merge!0 l1!0 (t!65 l2!0)))) (++!0 l1!0 l2!0)))) (assume (and (and (isSorted!0 res!0) (= (bag!0 res!0) (bag.union (bag!0 l1!0) (bag!0 l2!0)))) (= (size!0 res!0) (+ (size!0 l1!0) (size!0 l2!0)))) res!0))))
+
+(assert (not (=> (and (isSorted!0 l1!0) (isSorted!0 l2!0)) (let ((res!32 (ite (and (is-Cons!13 l1!0) (is-Cons!13 l2!0)) (ite (<= (h!58 l1!0) (h!58 l2!0)) (Cons!13 (h!58 l1!0) (merge!0 (t!65 l1!0) l2!0)) (Cons!13 (h!58 l2!0) (merge!0 l1!0 (t!65 l2!0)))) (++!0 l1!0 l2!0)))) (and (and (isSorted!0 res!32) (= (bag!0 res!32) (bag.union (bag!0 l1!0) (bag!0 l2!0)))) (= (size!0 res!32) (+ (size!0 l1!0) (size!0 l2!0))))))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/it/scala/inox/tip/TIPTestSuite.scala b/src/it/scala/inox/tip/TIPTestSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ae2aae5b8fa16362b985cfa008ddab217e772bde
--- /dev/null
+++ b/src/it/scala/inox/tip/TIPTestSuite.scala
@@ -0,0 +1,30 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import solvers._
+import org.scalatest._
+
+class TIPTestSuite extends FunSuite with ResourceUtils {
+
+ val ctx = TestContext.empty
+
+ for (file <- resourceFiles("regression/tip/SAT", _.endsWith(".tip"))) {
+ test(s"SAT - ${file.getName}") {
+ for ((syms, expr) <- new tip.Parser(file).parseScript) {
+ val program = InoxProgram(ctx, syms)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isSAT)
+ }
+ }
+ }
+
+ for (file <- resourceFiles("regression/tip/UNSAT", _.endsWith(".tip"))) {
+ test(s"UNSAT - ${file.getName}") {
+ for ((syms, expr) <- new tip.Parser(file).parseScript) {
+ val program = InoxProgram(ctx, syms)
+ assert(SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr).isUNSAT)
+ }
+ }
+ }
+}
diff --git a/src/main/scala/inox/solvers/ADTManagers.scala b/src/main/scala/inox/solvers/ADTManagers.scala
index 22d8617d81236126cfdf9e3b04971a7282d17596..7e32ee3415b62e80fbb397a4617083fa679e6a1d 100644
--- a/src/main/scala/inox/solvers/ADTManagers.scala
+++ b/src/main/scala/inox/solvers/ADTManagers.scala
@@ -32,6 +32,8 @@ trait ADTManagers {
private val declared = new IncrementalSet[Type]
protected val incrementals = Seq(declared)
+ def types: Set[Type] = declared.toSet
+
def declareADTs(tpe: Type, declare: Seq[(Type, DataType)] => Unit): Unit = {
val deps = typeDependencies(tpe)
val transitiveDeps: Map[Type, Set[Type]] = utils.fixpoint { (map: Map[Type, Set[Type]]) =>
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
index 211ad6aad4d196e22747f35e462ad417bf472368..12a5891cba57f840688fb5a2a9b6f201062b8c46 100644
--- a/src/main/scala/inox/solvers/SolverFactory.scala
+++ b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -83,7 +83,7 @@ object SolverFactory {
val program: p.type = p
val options = opts
val encoder = enc
- } with z3.NativeZ3Solver with TimeoutSolver {
+ } with z3.NativeZ3Solver with TimeoutSolver with tip.TipDebugger {
val evaluator = ev
})
@@ -91,7 +91,7 @@ object SolverFactory {
val program: p.type = p
val options = opts
val encoder = enc
- } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver with tip.TipDebugger {
val evaluator = ev
lazy val modelEvaluator = RecursiveEvaluator(targetProgram, options)
@@ -105,7 +105,7 @@ object SolverFactory {
val program: p.type = p
val options = opts
val encoder = enc
- } with unrolling.UnrollingSolver with theories.CVC4Theories with TimeoutSolver {
+ } with unrolling.UnrollingSolver with theories.CVC4Theories with TimeoutSolver with tip.TipDebugger {
val evaluator = ev
lazy val modelEvaluator = RecursiveEvaluator(targetProgram, options)
@@ -119,7 +119,7 @@ object SolverFactory {
val program: p.type = p
val options = opts
val encoder = enc
- } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver {
+ } with unrolling.UnrollingSolver with theories.Z3Theories with TimeoutSolver with tip.TipDebugger {
val evaluator = ev
lazy val modelEvaluator = RecursiveEvaluator(targetProgram, options)
diff --git a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
index 099b8bdd898336cf617105c213eb0f2d81b13cf5..997ea74593a4727b18e53e666f97ab0c9ba8dfae 100644
--- a/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/CVC4Target.scala
@@ -25,17 +25,10 @@ trait CVC4Target extends SMTLIBTarget with SMTLIBDebugger {
new CVC4Interpreter("cvc4", opts.toArray)
}
- override protected def declareSort(t: Type): Sort = {
- val tpe = bestRealType(t)
- sorts.cachedB(tpe) {
- tpe match {
- case SetType(base) =>
- Sets.SetSort(declareSort(base))
- case StringType => Strings.StringSort()
- case _ =>
- super.declareSort(t)
- }
- }
+ override protected def computeSort(t: Type): Sort = t match {
+ case SetType(base) => Sets.SetSort(declareSort(base))
+ case StringType => Strings.StringSort()
+ case _ => super.computeSort(t)
}
override protected def fromSMT(t: Term, otpe: Option[Type] = None)
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index f0265459700f5b81fde1c7f65fb741d1a94d3e52..30c6f85a77f2ed9e33bd6e44f6d0a761659294b0 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -97,13 +97,13 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
protected def freshSym(name: String): SSymbol = id2sym(FreshIdentifier(name))
/* Metadata for CC, and variables */
- protected val constructors = new IncrementalBijection[Type, SSymbol]()
- protected val selectors = new IncrementalBijection[(Type, Int), SSymbol]()
- protected val testers = new IncrementalBijection[Type, SSymbol]()
- protected val variables = new IncrementalBijection[Variable, SSymbol]()
- protected val sorts = new IncrementalBijection[Type, Sort]()
- protected val functions = new IncrementalBijection[TypedFunDef, SSymbol]()
- protected val lambdas = new IncrementalBijection[FunctionType, SSymbol]()
+ protected val constructors = new IncrementalBijection[Type, SSymbol]
+ protected val selectors = new IncrementalBijection[(Type, Int), SSymbol]
+ protected val testers = new IncrementalBijection[Type, SSymbol]
+ protected val variables = new IncrementalBijection[Variable, SSymbol]
+ protected val sorts = new IncrementalBijection[Type, Sort]
+ protected val functions = new IncrementalBijection[TypedFunDef, SSymbol]
+ protected val lambdas = new IncrementalBijection[FunctionType, SSymbol]
/* Helper functions */
@@ -129,7 +129,12 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
quantifiedTerm(quantifier, exprOps.variablesOf(body).toSeq.map(_.toVal), body)
}
- protected def declareSort(t: Type): Sort = bestRealType(t) match {
+ protected final def declareSort(t: Type): Sort = {
+ val tpe = bestRealType(t)
+ sorts.cachedB(tpe)(computeSort(tpe))
+ }
+
+ protected def computeSort(t: Type): Sort = t match {
case BooleanType => Core.BoolSort()
case IntegerType => Ints.IntSort()
case RealType => Reals.RealSort()
@@ -137,9 +142,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
case CharType => FixedSizeBitVectors.BitVectorSort(32)
case mt @ MapType(from, to) =>
- sorts.cachedB(mt) {
- Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
- }
+ Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
case FunctionType(from, to) =>
Ints.IntSort()
@@ -251,7 +254,7 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
declareVariable(Variable(FreshIdentifier("Unit"), UnitType))
case IntegerLiteral(i) => if (i >= 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
- case BVLiteral(bits, size) => FixedSizeBitVectors.BitVectorLit(List.range(1, size + 1).map(i => bits(i)))
+ case BVLiteral(bits, size) => FixedSizeBitVectors.BitVectorLit(List.range(1, size + 1).map(i => bits(size + 1 - i)))
case FractionLiteral(n, d) => Reals.Div(Reals.NumeralLit(n), Reals.NumeralLit(d))
case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
@@ -278,27 +281,18 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
case io @ IsInstanceOf(e, ADTType(id, tps)) =>
val adt = ADTType(id, tps map bestRealType)
declareSort(adt)
- val cases = adt.lookupADT match {
- case Some(tsort: TypedADTSort) =>
- tsort.constructors
- case Some(tcons: TypedADTConstructor) =>
- Seq(tcons)
- case None =>
- unsupported(io, "isInstanceOf on non-class")
- }
- val oneOf = cases map (_.toType) map testers.toB
- oneOf match {
- case Seq(tester) =>
+ adt.getADT match {
+ case tcons: TypedADTConstructor =>
+ val tester = testers.toB(tcons.toType)
FunctionApplication(tester, Seq(toSMT(e)))
- case more =>
- val es = freshSym("e")
- SMTLet(VarBinding(es, toSMT(e)), Seq(),
- SmtLibConstructors.or(oneOf.map(FunctionApplication(_, Seq(es: Term)))))
+ case _ =>
+ toSMT(BooleanLiteral(true))
}
case ADT(ADTType(id, tps), es) =>
val adt = ADTType(id, tps map bestRealType)
declareSort(adt)
+ println(adt, constructors)
val constructor = constructors.toB(adt)
if (es.isEmpty) {
constructor
diff --git a/src/main/scala/inox/solvers/smtlib/Z3Target.scala b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
index 838a996ab4c418812cc0bc34c8a6ab55cfc3a760..b9d5db1522af24d206486f0c4002ebeb33163f22 100644
--- a/src/main/scala/inox/solvers/smtlib/Z3Target.scala
+++ b/src/main/scala/inox/solvers/smtlib/Z3Target.scala
@@ -44,19 +44,12 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
s
}
- override protected def declareSort(t: Type): Sort = {
- val tpe = bestRealType(t)
- sorts.cachedB(tpe) {
- tpe match {
- case SetType(base) =>
- super.declareSort(BooleanType)
- Sort(SMTIdentifier(setSort), Seq(declareSort(base)))
- case BagType(base) =>
- declareSort(MapType(base, IntegerType))
- case _ =>
- super.declareSort(t)
- }
- }
+ override protected def computeSort(t: Type): Sort = t match {
+ case SetType(base) =>
+ declareSort(BooleanType)
+ Sort(SMTIdentifier(setSort), Seq(declareSort(base)))
+ case BagType(base) => declareSort(MapType(base, IntegerType))
+ case _ => super.computeSort(t)
}
override protected def fromSMT(t: Term, otpe: Option[Type] = None)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index c40001bb25cb7078660dda7b47d6a90a946d370c..8aa6d10e5024b3174fdd30398b8706dec12fb6d0 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -47,11 +47,6 @@ trait AbstractUnrollingSolver extends Solver { self =>
protected final def encode(tpe: Type): t.Type = programEncoder.encode(tpe)
protected final def decode(tpe: t.Type): Type = programEncoder.decode(tpe)
- /*
- protected final def encode(ft: FunctionType): t.FunctionType =
- programEncoder.encode(ft).asInstanceOf[t.FunctionType]
- */
-
protected val templates: Templates {
val program: targetProgram.type
type Encoded = self.Encoded
@@ -246,7 +241,8 @@ trait AbstractUnrollingSolver extends Solver { self =>
rec(v, tpe)
}
- if (wrapped.modelEval(v, tpe).isDefined) {
+ val ev = wrapped.modelEval(v, tpe).filterNot(_.isInstanceOf[Variable])
+ if (ev.isDefined) {
val (functions, recons) = functionsOf(v, tpe)
recons(functions.map { case (f, tpe) =>
extractFunction(f, bestRealType(tpe).asInstanceOf[FunctionType])
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index f73e2f58556fae8a9519664e27ec3542e4ffb28f..52f8fa69d62ab197f4dc1aefc5da471ce3d3ffa2 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -43,6 +43,14 @@ class Parser(file: File) {
(for (cmd <- script.commands) yield cmd match {
case CheckSat() =>
val expr: Expr = locals.symbols.andJoin(assertions)
+ for (fd <- locals.symbols.functions.values) {
+ if (fd.fullBody.getType(locals.symbols) == Untyped) {
+ println(locals.symbols.explainTyping(fd.fullBody)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
+ }
+ }
+ if (expr.getType(locals.symbols) == Untyped) {
+ println(locals.symbols.explainTyping(expr)(PrinterOptions(printUniqueIds = true, symbols = Some(locals.symbols))))
+ }
Some((locals.symbols, expr))
case _ =>
@@ -297,10 +305,6 @@ class Parser(file: File) {
(None, locals.withSymbols(
locals.symbols.withFunctions(Seq(fd)).withADTs(optAdt.toSeq)))
- case CheckSat() =>
- // FIXME: what do I do with this??
- (None, locals)
-
case _ =>
throw new MissformedTIPException("unknown TIP command " + cmd, cmd.optPos)
}
@@ -396,6 +400,10 @@ class Parser(file: File) {
case QualifiedIdentifier(SimpleIdentifier(sym), None) if locals.isVariable(sym) =>
locals.getVariable(sym)
+ case QualifiedIdentifier(SimpleIdentifier(sym), Some(sort)) if locals.isVariable(sym) =>
+ val v = locals.getVariable(sym).asInstanceOf[Variable]
+ Variable(v.id, extractSort(sort))
+
case SMTAssume(pred, body) =>
Assume(extractTerm(pred), extractTerm(body))
@@ -442,7 +450,7 @@ class Parser(file: File) {
IntegerLiteral(n)
case FixedSizeBitVectors.BitVectorLit(bs) =>
- BVLiteral(BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i }, bs.size)
+ BVLiteral(BitSet.empty ++ bs.reverse.zipWithIndex.collect { case (true, i) => i + 1 }, bs.size)
case SDecimal(value) =>
FractionLiteral(
@@ -504,7 +512,18 @@ class Parser(file: File) {
case FunctionApplication(QualifiedIdentifier(SimpleIdentifier(sym), None), Seq(term))
if locals.isADTSelector(sym) =>
- ADTSelector(extractTerm(term), locals.getADTSelector(sym))
+ val id = locals.getADTSelector(sym)
+ val adt = extractTerm(term)
+ adt.getType(locals.symbols) match {
+ case tpe: ADTType => tpe.getADT(locals.symbols) match {
+ case tcons: TypedADTConstructor => ADTSelector(adt, id)
+ case tsort: TypedADTSort =>
+ val tcons = tsort.constructors.find(_.fields.exists(vd => vd.id == id)).getOrElse {
+ throw new MissformedTIPException("Coulnd't find corresponding constructor", sym.optPos)
+ }
+ ADTSelector(AsInstanceOf(adt, tcons.toType).setPos(term.optPos), id)
+ }
+ }
case FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("distinct")), None), args) =>
val es = args.map(extractTerm).toArray
@@ -644,17 +663,17 @@ class Parser(file: File) {
}).setPos(term.optPos)
protected def extractSort(sort: Sort)(implicit locals: Locals): Type = (sort match {
- case Sort(SMTIdentifier(SSymbol("bitvector"), Seq(SNumeral(n))), Seq()) => BVType(n.toInt)
+ case Sort(SMTIdentifier(SSymbol("bitvector" | "BitVec"), Seq(SNumeral(n))), Seq()) => BVType(n.toInt)
case Sort(SimpleIdentifier(SSymbol("Bool")), Seq()) => BooleanType
case Sort(SimpleIdentifier(SSymbol("Int")), Seq()) => IntegerType
case Sort(SimpleIdentifier(SSymbol("Array")), Seq(from, to)) =>
MapType(extractSort(from), extractSort(to))
- case Sort(SimpleIdentifier(SSymbol("Set")), Seq(base)) =>
+ case Sets.SetSort(base) =>
SetType(extractSort(base))
- case Sort(SimpleIdentifier(SSymbol("Bag")), Seq(base)) =>
+ case Bags.BagSort(base) =>
BagType(extractSort(base))
case Sort(SimpleIdentifier(SSymbol("=>")), params :+ res) =>
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index e234c40a9f038eeadbaf4e97e2a35defb6f592b7..5d76756b2612726c3ed4c976de998fb315308463 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -5,6 +5,8 @@ package tip
import smtlib.parser.Terms.{Forall => SMTForall, Identifier => SMTIdentifier, _}
import smtlib.parser.Commands.{Constructor => SMTConstructor, _}
+import smtlib.theories._
+import smtlib.theories.experimental._
import smtlib.extensions.tip.Terms.{Lambda => SMTLambda, Application => SMTApplication, _}
import smtlib.extensions.tip.Commands._
import smtlib.Interpreter
@@ -15,6 +17,8 @@ import Commands._
import java.io.Writer
import scala.collection.mutable.{Map => MutableMap}
+import utils._
+
class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.SMTLIBTarget {
import program._
import program.trees._
@@ -52,26 +56,72 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
def interrupt(): Unit = free()
}
+ protected val extraVars = new Bijection[Variable, SSymbol]
+
def printScript(expr: Expr): Unit = {
val tparams = exprOps.collect(e => typeParamsOf(e.getType))(expr)
- val bindings = exprOps.variablesOf(expr).map(v => v.id -> (id2sym(v.id): Term)).toMap
val cmd = if (tparams.nonEmpty) {
- AssertPar(tparams.map(tp => id2sym(tp.id)).toSeq, toSMT(expr)(bindings))
+ AssertPar(tparams.map(tp => id2sym(tp.id)).toSeq, toSMT(expr)(Map.empty))
} else {
- Assert(toSMT(expr)(bindings))
+ Assert(toSMT(expr)(Map.empty))
+ }
+
+ val invariants = adtManager.types
+ .collect { case adt: ADTType => adt }
+ .map(_.getADT.definition)
+ .flatMap(_.invariant)
+
+ for (fd <- invariants) {
+ val Seq(vd) = fd.params
+ if (fd.tparams.isEmpty) {
+ emit(DatatypeInvariant(
+ id2sym(vd.id),
+ declareSort(vd.tpe),
+ toSMT(fd.fullBody)(Map(vd.id -> id2sym(vd.id)))
+ ))
+ } else {
+ val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
+ emit(DatatypeInvariantPar(
+ tps,
+ id2sym(vd.id),
+ declareSort(vd.tpe),
+ toSMT(fd.fullBody)(Map(vd.id -> id2sym(vd.id)))
+ ))
+ }
}
+
emit(cmd)
}
- protected def liftADTType(adt: ADTType): Type = adt.getADT.definition.typed.toType
+ def emit(s: String): Unit = writer.write(s)
+
+ protected def liftADTType(adt: ADTType): Type = adt.getADT.definition.root.typed.toType
protected val tuples: MutableMap[Int, TupleType] = MutableMap.empty
+ override protected def computeSort(t: Type): Sort = t match {
+ case FunctionType(from, to) =>
+ Sort(SimpleIdentifier(SSymbol("=>")), from.map(declareSort) :+ declareSort(to))
+
+ case BagType(base) =>
+ Bags.BagSort(declareSort(base))
+
+ case SetType(base) =>
+ Sets.SetSort(declareSort(base))
+
+ case StringType =>
+ Strings.StringSort()
+
+ case _ => super.computeSort(t)
+ }
+
override protected def declareStructuralSort(t: Type): Sort = t match {
case adt: ADTType =>
- adtManager.declareADTs(liftADTType(adt), declareDatatypes)
+ val tpe = liftADTType(adt)
+ adtManager.declareADTs(tpe, declareDatatypes)
val tpSorts = adt.tps.map(declareSort)
- Sort(SMTIdentifier(id2sym(adt.id)), tpSorts)
+ val Sort(id, _) = sorts.toB(tpe)
+ Sort(id, tpSorts)
case TupleType(ts) =>
val tpe = tuples.getOrElseUpdate(ts.size, {
@@ -81,23 +131,34 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
val tpSorts = ts.map(declareSort)
Sort(sorts.toB(tpe).id, tpSorts)
+ case tp: TypeParameter =>
+ Sort(SMTIdentifier(id2sym(tp.id)), Nil)
+
case _ => super.declareStructuralSort(t)
}
override protected def declareDatatypes(datatypes: Seq[(Type, DataType)]): Unit = {
- for ((tpe, DataType(id, _)) <- datatypes) {
- sorts += tpe -> Sort(SMTIdentifier(id2sym(id)))
- }
-
- val (generics, adts) = datatypes.partition {
+ val adts = datatypes.filterNot {
case (_: TypeParameter, _) => true
case _ => false
}
- val genericSyms = generics.map { case (_, DataType(id, _)) => id2sym(id) }
+ for ((tpe, DataType(id, _)) <- adts) {
+ val tparams: Seq[TypeParameter] = tpe match {
+ case ADTType(_, tps) => tps.map(_.asInstanceOf[TypeParameter])
+ case TupleType(tps) => tps.map(_.asInstanceOf[TypeParameter])
+ case _ => Seq.empty
+ }
+
+ val tpSorts = tparams.map(tp => Sort(SMTIdentifier(id2sym(tp.id))))
+ sorts += tpe -> Sort(SMTIdentifier(id2sym(id)), tpSorts)
+ }
+
+ val generics = adts.flatMap { case (tp, _) => typeParamsOf(tp) }.toSet
+ val genericSyms = generics.map(tp => id2sym(tp.id))
if (adts.nonEmpty) {
- emit(DeclareDatatypesPar(genericSyms,
+ emit(DeclareDatatypesPar(genericSyms.toList,
(for ((tpe, DataType(sym, cases)) <- adts.toList) yield {
id2sym(sym) -> (for (c <- cases) yield {
val s = id2sym(c.sym)
@@ -112,84 +173,86 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
}).toList
}).toList
))
-
- val invariants = adts
- .collect { case (adt: ADTType, _) => adt }
- .map(_.getADT.definition)
- .flatMap(_.invariant)
-
- for (fd <- invariants) {
- val Seq(vd) = fd.params
- if (fd.tparams.isEmpty) {
- emit(DatatypeInvariant(
- id2sym(vd.id),
- declareSort(vd.tpe),
- toSMT(fd.fullBody)(Map(vd.id -> id2sym(vd.id)))
- ))
- } else {
- val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
- emit(DatatypeInvariantPar(
- tps,
- id2sym(vd.id),
- declareSort(vd.tpe),
- toSMT(fd.fullBody)(Map(vd.id -> id2sym(vd.id)))
- ))
- }
- }
}
}
override protected def declareFunction(tfd: TypedFunDef): SSymbol = {
val fd = tfd.fd
- val scc = transitiveCallees(fd).filter(fd2 => transitivelyCalls(fd2, fd))
- if (scc.size <= 1) {
- val (sym, params, returnSort, body) = (
- id2sym(fd.id),
- fd.params.map(vd => SortedVar(id2sym(vd.id), declareSort(vd.tpe))),
- declareSort(fd.returnType),
- toSMT(fd.fullBody)(fd.params.map(vd => vd.id -> (id2sym(vd.id): Term)).toMap)
- )
+ functions.getB(fd.typed) match {
+ case Some(sym) => sym
+ case None =>
+ functions += fd.typed -> id2sym(fd.id)
- val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
+ val scc = transitiveCallees(fd).filter(fd2 => transitivelyCalls(fd2, fd))
+ if (scc.size <= 1) {
+ val (sym, params, returnSort, body) = (
+ id2sym(fd.id),
+ fd.params.map(vd => SortedVar(id2sym(vd.id), declareSort(vd.tpe))),
+ declareSort(fd.returnType),
+ toSMT(fd.fullBody)(fd.params.map(vd => vd.id -> (id2sym(vd.id): Term)).toMap)
+ )
- emit((scc.isEmpty, tps.isEmpty) match {
- case (true, true) => DefineFun(FunDef(sym, params, returnSort, body))
- case (false, true) => DefineFunRec(FunDef(sym, params, returnSort, body))
- case (true, false) => DefineFunPar(tps, FunDef(sym, params, returnSort, body))
- case (false, false) => DefineFunRecPar(tps, FunDef(sym, params, returnSort, body))
- })
- } else {
- val (decs, bodies) = (for (fd <- scc.toList) yield {
- val (sym, params, returnSort) = (
- id2sym(fd.id),
- fd.params.map(vd => SortedVar(id2sym(vd.id), declareSort(vd.tpe))),
- declareSort(fd.returnType)
- )
-
- val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
+ val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
- val dec = if (tps.isEmpty) {
- Right(FunDec(sym, params, returnSort))
+ emit((scc.isEmpty, tps.isEmpty) match {
+ case (true, true) => DefineFun(FunDef(sym, params, returnSort, body))
+ case (false, true) => DefineFunRec(FunDef(sym, params, returnSort, body))
+ case (true, false) => DefineFunPar(tps, FunDef(sym, params, returnSort, body))
+ case (false, false) => DefineFunRecPar(tps, FunDef(sym, params, returnSort, body))
+ })
} else {
- Left(FunDecPar(tps, sym, params, returnSort))
+ functions ++= scc.toList.map(fd => fd.typed -> id2sym(fd.id))
+
+ val (decs, bodies) = (for (fd <- scc.toList) yield {
+ val (sym, params, returnSort) = (
+ id2sym(fd.id),
+ fd.params.map(vd => SortedVar(id2sym(vd.id), declareSort(vd.tpe))),
+ declareSort(fd.returnType)
+ )
+
+ val tps = fd.tparams.map(tpd => declareSort(tpd.tp).id.symbol)
+
+ val dec = if (tps.isEmpty) {
+ Right(FunDec(sym, params, returnSort))
+ } else {
+ Left(FunDecPar(tps, sym, params, returnSort))
+ }
+
+ val body = toSMT(fd.fullBody)(fd.params.map(vd => vd.id -> (id2sym(vd.id): Term)).toMap)
+ (dec, body)
+ }).unzip
+
+ emit(if (decs.exists(_.isLeft)) {
+ DefineFunsRecPar(decs, bodies)
+ } else {
+ DefineFunsRec(decs.map(_.right.get), bodies)
+ })
}
- val body = toSMT(fd.fullBody)(fd.params.map(vd => vd.id -> (id2sym(vd.id): Term)).toMap)
- (dec, body)
- }).unzip
-
- emit(if (decs.exists(_.isLeft)) {
- DefineFunsRecPar(decs, bodies)
- } else {
- DefineFunsRec(decs.map(_.right.get), bodies)
- })
+ id2sym(fd.id)
}
-
- id2sym(fd.id)
}
override protected def toSMT(e: Expr)(implicit bindings: Map[Identifier, Term]): Term = e match {
+ case v @ Variable(id, tp) =>
+ val sort = declareSort(tp)
+ bindings.get(id) orElse variables.getB(v).map(s => s: Term) getOrElse {
+ val tps = typeParamsOf(tp).toSeq
+ val sym = extraVars.cachedB(v) {
+ val sym = id2sym(id)
+ emit(if (tps.nonEmpty) {
+ DeclareConstPar(tps.map(tp => id2sym(tp.id)), sym, sort)
+ } else {
+ DeclareConst(sym, sort)
+ })
+ sym
+ }
+
+ if (tps.nonEmpty) QualifiedIdentifier(SMTIdentifier(sym), Some(sort))
+ else QualifiedIdentifier(SMTIdentifier(sym), None)
+ }
+
case Lambda(args, body) =>
val (newBindings, params) = args.map { vd =>
val sym = id2sym(vd.id)
@@ -222,9 +285,77 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
case BagAdd(bag, elem) => Bags.Insert(toSMT(bag), toSMT(elem))
case MultiplicityInBag(elem, bag) => Bags.Multiplicity(toSMT(elem), toSMT(bag))
+ case BagUnion(b1, b2) => Bags.Union(toSMT(b1), toSMT(b2))
case BagIntersection(b1, b2) => Bags.Intersection(toSMT(b1), toSMT(b2))
case BagDifference(b1, b2) => Bags.Difference(toSMT(b1), toSMT(b2))
+ case FiniteSet(elems, base) =>
+ val empty = Sets.EmptySet(declareSort(base))
+ elems match {
+ case x :: xs => Sets.Insert(empty, toSMT(x), xs.map(toSMT) : _*)
+ case _ => empty
+ }
+
+ case SetAdd(set, elem) => Sets.Insert(toSMT(set), toSMT(elem))
+ case ElementOfSet(elem, set) => Sets.Member(toSMT(elem), toSMT(set))
+ case SubsetOf(s1, s2) => Sets.Subset(toSMT(s1), toSMT(s2))
+ case SetIntersection(s1, s2) => Sets.Intersection(toSMT(s1), toSMT(s2))
+ case SetUnion(s1, s2) => Sets.Union(toSMT(s1), toSMT(s2))
+ case SetDifference(s1, s2) => Sets.Setminus(toSMT(s1), toSMT(s2))
+
+ case StringLiteral(value) => Strings.StringLit(value)
+ case StringConcat(s1, s2) => Strings.Concat(toSMT(s1), toSMT(s2))
+ case SubString(s, start, end) => Strings.Substring(toSMT(s), toSMT(start), toSMT(end))
+ case StringLength(s) => Strings.Length(toSMT(s))
+
+ case ADT(tpe @ ADTType(id, tps), es) =>
+ val tcons = tpe.getADT.definition.typed.toConstructor
+ val adt = tcons.toType
+ val sort = declareSort(tpe)
+ val constructor = constructors.toB(adt)
+ if (es.isEmpty) {
+ if (tcons.tps.nonEmpty) QualifiedIdentifier(SMTIdentifier(constructor), Some(sort))
+ else constructor
+ } else {
+ FunctionApplication(constructor, es.map(toSMT))
+ }
+
+ case s @ ADTSelector(e, id) =>
+ val tcons = e.getType.asInstanceOf[ADTType].getADT.definition.typed.toConstructor
+ val adt = tcons.toType
+ declareSort(adt)
+ val selector = selectors.toB(adt -> s.selectorIndex)
+ FunctionApplication(selector, Seq(toSMT(e)))
+
+ case IsInstanceOf(e, t: ADTType) =>
+ val tdef = t.getADT.definition.typed
+ if (tdef.definition.isSort) {
+ toSMT(BooleanLiteral(true))
+ } else {
+ val adt = tdef.toConstructor.toType
+ declareSort(adt)
+ val tester = testers.toB(adt)
+ FunctionApplication(tester, Seq(toSMT(e)))
+ }
+
+ case t @ Tuple(es) =>
+ declareSort(t.getType)
+ val tpe = tuples(es.size)
+ val constructor = constructors.toB(tpe)
+ FunctionApplication(constructor, es.map(toSMT))
+
+ case ts @ TupleSelect(t, i) =>
+ declareSort(t.getType)
+ val tpe = tuples(t.getType.asInstanceOf[TupleType].dimension)
+ val selector = selectors.toB((tpe, i - 1))
+ FunctionApplication(selector, Seq(toSMT(t)))
+
+ case fi @ FunctionInvocation(id, tps, Seq()) if tps.nonEmpty =>
+ QualifiedIdentifier(
+ SMTIdentifier(declareFunction(fi.tfd)),
+ Some(declareSort(fi.tfd.returnType))
+ )
+
case _ => super.toSMT(e)
}
}
diff --git a/src/main/scala/inox/tip/TipDebugger.scala b/src/main/scala/inox/tip/TipDebugger.scala
index 806d83e983c9cdbee91af7ffbb9452552d91214b..7015210242a1fd7c66820d27f841014689143690 100644
--- a/src/main/scala/inox/tip/TipDebugger.scala
+++ b/src/main/scala/inox/tip/TipDebugger.scala
@@ -7,31 +7,57 @@ import utils._
import solvers._
trait TipDebugger extends Solver {
+ val program: Program
import program._
+ import program.trees._
+ import SolverResponses._
+
+ protected val encoder: ast.ProgramEncoder { val sourceProgram: program.type; val t: inox.trees.type }
implicit val debugSection: DebugSection
abstract override def free(): Unit = {
super.free()
- debugOut.foreach(_.close())
+ debugOut.foreach(_.free())
}
- protected lazy val debugOut: Option[java.io.FileWriter] = {
+ protected lazy val debugOut: Option[tip.Printer] = {
if (ctx.reporter.isDebugEnabled) {
- val file = ctx.options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
- val n = DebugFileNumbers.next(file)
- val fileName = s"tip-sessions/$file-$n.tip"
+ val files = ctx.options.findOptionOrDefault(Main.optFiles)
+ if (files.nonEmpty && files.forall(_.getName.endsWith(".tip"))) {
+ // don't output TIP when running on a TIP benchmark
+ None
+ } else {
+ val file = files.headOption.map(_.getName).getOrElse("NA")
+ val n = DebugFileNumbers.next(file)
+ val fileName = s"tip-sessions/$file-$n.tip"
- val javaFile = new java.io.File(fileName)
- javaFile.getParentFile.mkdirs()
+ val javaFile = new java.io.File(fileName)
+ javaFile.getParentFile.mkdirs()
- ctx.reporter.debug(s"Outputting tip session into $fileName")
- val fw = new java.io.FileWriter(javaFile, false)
- Some(fw)
+ ctx.reporter.debug(s"Outputting tip session into $fileName")
+ val fw = new java.io.FileWriter(javaFile, false)
+ Some(new tip.Printer(encoder.targetProgram, fw))
+ }
} else {
None
}
}
+
+ abstract override def assertCnstr(expr: Expr): Unit = {
+ debugOut.foreach { o => o.printScript(encoder.encode(expr)) }
+ super.assertCnstr(expr)
+ }
+
+ abstract override def check(config: CheckConfiguration): config.Response[Model, Assumptions] = {
+ debugOut.foreach { o => o.emit(_root_.smtlib.parser.Commands.CheckSat()) }
+ super.check(config)
+ }
+
+ abstract override def checkAssumptions(config: Configuration)(assumptions: Set[Expr]): config.Response[Model, Assumptions] = {
+ debugOut.foreach { o => o.emit("; check-assumptions required here, but not part of tip standard") }
+ super.checkAssumptions(config)(assumptions)
+ }
}
// Unique numbers
diff --git a/src/main/scala/inox/tip/TipExtensions.scala b/src/main/scala/inox/tip/TipExtensions.scala
index cdbdae3f3e1cbb0168ba3c1df37f8fcd72bbffef..0f22f3d8af7ab36e672d22dd7a8c90446cf8a9a9 100644
--- a/src/main/scala/inox/tip/TipExtensions.scala
+++ b/src/main/scala/inox/tip/TipExtensions.scala
@@ -37,7 +37,7 @@ object Commands {
ctx.print(sort)
ctx.print(" ")
ctx.print(pred)
- ctx.print(")")
+ ctx.print(")\n")
}
}
@@ -50,7 +50,7 @@ object Commands {
ctx.print(sort)
ctx.print(" ")
ctx.print(pred)
- ctx.print("))")
+ ctx.print("))\n")
}
}
}
@@ -71,6 +71,7 @@ class TipParser(lexer: TipLexer) extends SMTParser(lexer) {
override protected def parseTermWithoutParens: Term = getPeekToken.kind match {
case Tokens.Assume =>
+ eat(Tokens.Assume)
val pred = parseTerm
val body = parseTerm
Assume(pred, body)