From fce731b1a8add202079dec1c535e7b0936e6f750 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 23 Dec 2016 11:24:29 +0100
Subject: [PATCH] Fixes for function merging transformation
---
...rOrderFunctionsMutableParams10.scala-2.tip | 19 +++++++++++++++++++
src/main/scala/inox/ast/SymbolOps.scala | 11 +++++++----
src/main/scala/inox/tip/Printer.scala | 2 +-
3 files changed, 27 insertions(+), 5 deletions(-)
create mode 100644 src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip
diff --git a/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip b/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip
new file mode 100644
index 000000000..5d7892662
--- /dev/null
+++ b/src/it/resources/regression/tip/UNSAT/HigherOrderFunctionsMutableParams10.scala-2.tip
@@ -0,0 +1,19 @@
+(declare-datatypes () ((A!59 (A!60 (x!539 (_ BitVec 32))))))
+
+(declare-datatypes (A1!0 R!21) ((fun1!11 (fun1!12 (f!40 (=> A1!0 R!21)) (pre!15 (=> A1!0 Bool))))))
+
+(declare-datatypes (A0!6 A1!22) ((tuple2!10 (tuple2!11 (_1!5 A0!6) (_2!5 A1!22)))))
+
+(declare-datatypes () ((FunctionWrapper!5 (FunctionWrapper!6 (f!39 (fun1!11 A!59 (tuple2!10 (_ BitVec 32) A!59)))))))
+
+(declare-datatypes () ((WrapWrapper!5 (WrapWrapper!6 (fw!4 FunctionWrapper!5)))))
+
+(define-fun fImpl!0 ((a!1 A!59)) (tuple2!10 (_ BitVec 32) A!59) (let ((a!26 (A!60 (bvadd (x!539 a!1) #b00000000000000000000000000000001)))) (tuple2!11 (x!539 a!26) a!26)))
+
+(define-fun app!0 ((ww!0 WrapWrapper!5) (a!0 A!59)) (tuple2!10 (_ BitVec 32) A!59) (assume (forall ((x!133 A!59)) (=> (@ (f!40 (fun1!12 (lambda ((x!132 A!59)) true) (lambda ((x!364 A!59)) true))) x!133) (@ (f!40 (fun1!12 (pre!15 (f!39 (fw!4 ww!0))) (lambda ((x!365 A!59)) true))) x!133))) (let ((t!53 (let ((res!38 (@ (f!40 (f!39 (fw!4 ww!0))) a!0))) (tuple2!11 (_1!5 res!38) (_2!5 res!38))))) (tuple2!11 (_1!5 t!53) (_2!5 t!53)))))
+
+(assert (not (let ((wrap!0 (WrapWrapper!6 (FunctionWrapper!6 (fun1!12 (lambda ((a!3 A!59)) (let ((res!40 (fImpl!0 a!3))) (tuple2!11 (_1!5 res!40) (_2!5 res!40)))) (lambda ((a!32 A!59)) true)))))) (let ((x$1!5 (x!539 (_2!5 (app!0 wrap!0 (_2!5 (app!0 wrap!0 (A!60 #b00000000000000000000000000000000)))))))) (= x$1!5 #b00000000000000000000000000000010)))))
+
+(check-sat)
+
+; check-assumptions required here, but not part of tip standard
\ No newline at end of file
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index bd30be6d9..c83185e23 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -1030,10 +1030,6 @@ trait SymbolOps { self: TypeOps =>
val (br, bBindings) = rec(b)
(br, vBindings merge ((i -> vr) +: bBindings))
- case Forall(args, body) =>
- val (recBody, bodyBindings) = rec(body)
- (Forall(args, bodyBindings wrap recBody), Seq.empty)
-
case Assume(pred, body) =>
val (recPred, predBindings) = rec(pred)
val (recBody, bodyBindings) = rec(body)
@@ -1066,6 +1062,13 @@ trait SymbolOps { self: TypeOps =>
val (recRhs, rhsBindings) = rec(rhs)
(Implies(recLhs, rhsBindings wrap recRhs), lhsBindings)
+ case v: Variable => (v, Seq.empty)
+
+ case ex @ VariableExtractor(vs) if vs.nonEmpty =>
+ val Operator(subs, recons) = ex
+ val recSubs = subs.map(rec)
+ (recons(recSubs.map { case (e, bindings) => bindings wrap e }), Seq.empty)
+
case Operator(es, recons) =>
val (recEs, esBindings) = es.map(rec).unzip
(recons(recEs), esBindings.flatten.distinct)
diff --git a/src/main/scala/inox/tip/Printer.scala b/src/main/scala/inox/tip/Printer.scala
index 14b5cc3fa..b113697dd 100644
--- a/src/main/scala/inox/tip/Printer.scala
+++ b/src/main/scala/inox/tip/Printer.scala
@@ -145,7 +145,7 @@ class Printer(val program: InoxProgram, writer: Writer) extends solvers.smtlib.S
val (ours, externals) = adts.partition {
case (adt: ADTType, _) => adt == adt.getADT.definition.typed.toType
- case (tpe @ TupleType(tps), _) => tpe == tuples(tps.size)
+ case (tpe @ TupleType(tps), _) => Some(tpe) == tuples.get(tps.size)
case _ => true
}
--
GitLab