From b56f057276a150f4bef82648472d0f719ca949fe Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Thu, 10 Nov 2016 17:49:29 +0100
Subject: [PATCH] TIP parsing and printing working and tested
---
build.sbt | 2 +-
.../SAT/AssociativityProperties.scala-0.tip | 13 +
.../SAT/AssociativityProperties.scala-1.tip | 13 +
.../regression/tip/SAT/BraunTree.scala-1.tip | 25 ++
.../tip/SAT/PositiveMap.scala-0.tip | 23 ++
.../UNSAT/BinarySearchTreeQuant2.scala-0.tip | 22 ++
.../UNSAT/BinarySearchTreeQuant2.scala-1.tip | 29 ++
.../tip/UNSAT/Closures2.scala-0.tip | 13 +
.../tip/UNSAT/Closures2.scala-1.tip | 13 +
.../tip/UNSAT/Closures2.scala-2.tip | 17 ++
.../tip/UNSAT/MergeSort2.scala-0.tip | 39 +++
.../tip/UNSAT/MergeSort2.scala-1.tip | 33 ++
src/it/scala/inox/tip/TIPTestSuite.scala | 30 ++
src/main/scala/inox/solvers/ADTManagers.scala | 2 +
.../scala/inox/solvers/SolverFactory.scala | 8 +-
.../inox/solvers/smtlib/CVC4Target.scala | 15 +-
.../inox/solvers/smtlib/SMTLIBTarget.scala | 48 ++-
.../scala/inox/solvers/smtlib/Z3Target.scala | 19 +-
.../solvers/unrolling/UnrollingSolver.scala | 8 +-
src/main/scala/inox/tip/Parser.scala | 37 ++-
src/main/scala/inox/tip/Printer.scala | 281 +++++++++++++-----
src/main/scala/inox/tip/TipDebugger.scala | 46 ++-
src/main/scala/inox/tip/TipExtensions.scala | 5 +-
23 files changed, 583 insertions(+), 158 deletions(-)
create mode 100644 src/it/resources/regression/tip/SAT/AssociativityProperties.scala-0.tip
create mode 100644 src/it/resources/regression/tip/SAT/AssociativityProperties.scala-1.tip
create mode 100644 src/it/resources/regression/tip/SAT/BraunTree.scala-1.tip
create mode 100644 src/it/resources/regression/tip/SAT/PositiveMap.scala-0.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-0.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/BinarySearchTreeQuant2.scala-1.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/Closures2.scala-0.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/Closures2.scala-1.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/Closures2.scala-2.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/MergeSort2.scala-0.tip
create mode 100644 src/it/resources/regression/tip/UNSAT/MergeSort2.scala-1.tip
create mode 100644 src/it/scala/inox/tip/TIPTestSuite.scala
diff --git a/build.sbt b/build.sbt
index 4486befa0..4a6567e6e 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 000000000..f4b839e5c
--- /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 000000000..f78677222
--- /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 000000000..c6d86b690
--- /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 000000000..6b1e9120d
--- /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 000000000..cf80afb9b
--- /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 000000000..ec3af4004
--- /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 000000000..96aefd182
--- /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 000000000..64fbf0fa1
--- /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 000000000..df38d5557
--- /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 000000000..32d0fa071
--- /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 000000000..0e6992280
--- /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 000000000..ae2aae5b8
--- /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 22d8617d8..7e32ee341 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 211ad6aad..12a5891cb 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 099b8bdd8..997ea7459 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 f02654597..30c6f85a7 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 838a996ab..b9d5db152 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 c40001bb2..8aa6d10e5 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 f73e2f585..52f8fa69d 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 e234c40a9..5d76756b2 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 806d83e98..701521024 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 cdbdae3f3..0f22f3d8a 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)
--
GitLab