Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Choose under lamba #139

Open
jad-hamza opened this issue Apr 25, 2021 · 13 comments
Open

Choose under lamba #139

jad-hamza opened this issue Apr 25, 2021 · 13 comments

Comments

@jad-hamza
Copy link
Contributor

In this PR epfl-lara/stainless#946, I changed the way VCs are generated in the type-checker, and the following file is now valid:
https://github.com/epfl-lara/stainless/blob/965b0ec485e62715003738e73605bd4dbb5da1da/frontends/benchmarks/verification/invalid/Equations1.scala
But I was expecting the second equations to fail, because the makeEqual(x, y) evidence shouldn't "leak".

I've narrowed the issue to this tip file, on which Inox returns UNSAT (I've tried z3 and cvc4 1.8).
Surprisingly, removing the assertion on eq2 makes Inox return SAT. (removing the assertion on eq1 makes Inox return SAT as well)

(declare-datatypes (A B) ((RAEquations (RaCons (lhs (=> A)) (rhs (=> A)) (ev (=> B))))))
(datatype-invariant (par (A B) this (RAEquations A B) (= (@ (lhs this)) (@ (rhs this)))))

(declare-datatypes () ((Unit (Uu))))

(define-fun makeEqual ((x Int) (y Int)) Unit (choose unused Unit (= x y)))

(declare-const x Int)
(declare-const y Int)

(declare-const eq1 (RAEquations Int Unit))
(declare-const eq2 (RAEquations Int Unit))

(assert (= eq1 (RaCons (lambda () x) (lambda () x) (lambda () (makeEqual x y)))))
(assert (= eq2 (RaCons (lambda () x) (lambda () x) (lambda () Uu))))
(assert (not (= y x)))

(check-sat)
@samarion
Copy link
Member

Could you also post the solver debug please?

@jad-hamza
Copy link
Contributor Author

Sure:

[ Debug  ] Invoking solver z3 with -in -smt2
[ Debug  ] Outputting smt session into smt-sessions/z3-gg.tip-0.smt2
[ Debug  ] -> registering free function b$10 ==> eq1.lhs: () => BigInt
[ Debug  ] -> registering free function b$10 ==> eq1.rhs: () => BigInt
[ Debug  ] -> registering free function b$10 ==> eq1.ev: () => Unit
[ Debug  ] -> registering free function b$11 ==> eq2.lhs: () => BigInt
[ Debug  ] -> registering free function b$11 ==> eq2.rhs: () => BigInt
[ Debug  ] -> registering free function b$11 ==> eq2.ev: () => Unit
[ Debug  ]  -> instantiating matcher m$1 ==> inv$RAEquations[BigInt, Unit](eq1)
[ Debug  ]  -> instantiating matcher m$3 ==> inv$RAEquations[BigInt, Unit](eq2)
[ Debug  ]   . start$1
[ Debug  ]   . b$10 ==> (b_free$1 == ¬b_next$1)
[ Debug  ]   . b$10 ==> (tp$13 == b_and$1)
[ Debug  ]   . b$10 ==> (b_free$3 == ¬b_next$3)
[ Debug  ]   . b$10 ==> (tp$15 == b_and$3)
[ Debug  ]   . b$10 ==> (b_free$5 == ¬b_next$5)
[ Debug  ]   . b$10 ==> (tp$16 == b_and$5)
[ Debug  ]   . b$11 ==> (b_free$7 == ¬b_next$7)
[ Debug  ]   . b$11 ==> (tp$17 == b_and$7)
[ Debug  ]   . b$11 ==> (b_free$9 == ¬b_next$9)
[ Debug  ]   . b$11 ==> (tp$14 == b_and$9)
[ Debug  ]   . b$11 ==> (b_free$11 == ¬b_next$11)
[ Debug  ]   . b$11 ==> (tp$12 == b_and$11)
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . (b$10 && start$1 && lambda$12() == eq1.lhs()) ==> (lambda$12 == eq1.lhs)
[ Debug  ]   . (b$10 && start$1 && lambda$12() == eq1.rhs()) ==> (lambda$12 == eq1.rhs)
[ Debug  ]   . (b$11 && start$1 && lambda$12() == eq2.lhs()) ==> (lambda$12 == eq2.lhs)
[ Debug  ]   . (b$11 && start$1 && lambda$12() == eq2.rhs()) ==> (lambda$12 == eq2.rhs)
[ Debug  ]   . b$10 ==> (b_next$1 == (start$1 && lambda$12 == eq1.lhs || b_next$13))
[ Debug  ]   . b$10 ==> (b_next$3 == (start$1 && lambda$12 == eq1.rhs || b_next$15))
[ Debug  ]   . b$11 ==> (b_next$7 == (start$1 && lambda$12 == eq2.lhs || b_next$17))
[ Debug  ]   . b$11 ==> (b_next$9 == (start$1 && lambda$12 == eq2.rhs || b_next$19))
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . b$10 ==> (b_next$5 == (start$1 && lambda$13 == eq1.ev || b_next$21))
[ Debug  ]   . b$11 ==> (b_next$11 == (start$1 && lambda$13 == eq2.ev || b_next$23))
[ Debug  ]   . bs$1 == (b$8 && start$1)
[ Debug  ]   . bs$1 ==> (lambda$14 ≠ lambda$13)
[ Debug  ]   . (b$10 && b$8 && lambda$14() == eq1.ev()) ==> (lambda$14 == eq1.ev)
[ Debug  ]   . (b$11 && b$8 && lambda$14() == eq2.ev()) ==> (lambda$14 == eq2.ev)
[ Debug  ]   . b$10 ==> (b_next$21 == (b$8 && lambda$14 == eq1.ev || b_next$25))
[ Debug  ]   . b$11 ==> (b_next$23 == (b$8 && lambda$14 == eq2.ev || b_next$27))
[ Debug  ]   . b$11 ==> (e$6 == (tp$17 && tp$14 && tp$12))
[ Debug  ]   . b$10 ==> (e$7 == (tp$13 && tp$15 && tp$16))
[ Debug  ]   . start$1 ==> (¬res$5 ==> ¬e$8)
[ Debug  ]   . start$1 ==> (res$5 == (eq1 == RaCons[BigInt, Unit](lambda$12, lambda$12, lambda$13)))
[ Debug  ]   . start$1 ==> e$8
[ Debug  ]   . start$1 ==> (inv$RAEquations[BigInt, Unit](eq1) && e$7)
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . start$1 ==> (inv$RAEquations[BigInt, Unit](eq2) && e$6)
[ Debug  ]   . b$9 ==> (e$8 == (y ≠ x))
[ Debug  ]   . b$8 ==> (¬res$6 ==> ¬e$8)
[ Debug  ]   . b$8 ==> (res$6 == (eq2 == RaCons[BigInt, Unit](lambda$12, lambda$12, lambda$14)))
[ Debug  ]   . (start$1 && res$5) == b$8
[ Debug  ]   . (b$8 && res$6) == b$9
[ Debug  ]   . start$1 == b$10
[ Debug  ]   . start$1 == b$11
[ Debug  ]   . start$1 ==> m$1
[ Debug  ]   . start$1 ==> m$3
[ Debug  ]  - Running search...
[ Debug  ]  - Finished search with blocked literals
[ Debug  ]  - Running search without blocked literals (w/o lucky test)
[ Debug  ]  - Finished search without blocked literals
[  Info  ] gg.tip => UNSAT

@samarion
Copy link
Member

Hmm, seems like something is going wrong in normalizeStructure again. Could you add some debug there?

My main suspect are the conditions here:

if (!minimal) None
else if (isLocal(e, path, true) && isAlwaysPure(e)) Some(Seq())
else if (isLocal(e, path, false) && (isPureIn(e, path) || isCalled)) Some(path.conditions)
else None

@jad-hamza
Copy link
Contributor Author

I added debug output in the beginning of normalizeStructure, then in the unapply call you mention to debug which branch was taken, and then some debug output at the end of normalizeStructure:

[ Debug  ] Invoking solver z3 with -in -smt2
[ Debug  ] Outputting smt session into smt-sessions/z3-gg.tip-0.smt2
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(perverseApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(perverseApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,makeEqual$0(x$1, y$1))
(perverseApps, onlySimple, inFunction:,false,false,true)



unapply: makeEqual$0(x$1, y$1)
final else branch




End of normalizeStructure:
(bindings,List())
(newExpr,makeEqual$0(x$2, x$5))
----------
deps:
x$5 -> y$1
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(perverseApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(perverseApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,Uu$0())
(perverseApps, onlySimple, inFunction:,false,false,true)



unapply: Uu$0()
isLocal(e, path, true) && isAlwaysPure(e)




End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> Uu$0()
====================================================================================================
[ Debug  ] -> registering free function b$10 ==> eq1.lhs: () => BigInt
[ Debug  ] -> registering free function b$10 ==> eq1.rhs: () => BigInt
[ Debug  ] -> registering free function b$10 ==> eq1.ev: () => Unit
[ Debug  ] -> registering free function b$11 ==> eq2.lhs: () => BigInt
[ Debug  ] -> registering free function b$11 ==> eq2.rhs: () => BigInt
[ Debug  ] -> registering free function b$11 ==> eq2.ev: () => Unit
[ Debug  ]  -> instantiating matcher m$1 ==> inv$RAEquations[BigInt, Unit](eq1)
[ Debug  ]  -> instantiating matcher m$3 ==> inv$RAEquations[BigInt, Unit](eq2)
[ Debug  ]   . start$1
[ Debug  ]   . b$10 ==> (b_free$1 == ¬b_next$1)
[ Debug  ]   . b$10 ==> (tp$13 == b_and$1)
[ Debug  ]   . b$10 ==> (b_free$3 == ¬b_next$3)
[ Debug  ]   . b$10 ==> (tp$15 == b_and$3)
[ Debug  ]   . b$10 ==> (b_free$5 == ¬b_next$5)
[ Debug  ]   . b$10 ==> (tp$16 == b_and$5)
[ Debug  ]   . b$11 ==> (b_free$7 == ¬b_next$7)
[ Debug  ]   . b$11 ==> (tp$17 == b_and$7)
[ Debug  ]   . b$11 ==> (b_free$9 == ¬b_next$9)
[ Debug  ]   . b$11 ==> (tp$14 == b_and$9)
[ Debug  ]   . b$11 ==> (b_free$11 == ¬b_next$11)
[ Debug  ]   . b$11 ==> (tp$12 == b_and$11)
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . (b$10 && start$1 && lambda$12() == eq1.lhs()) ==> (lambda$12 == eq1.lhs)
[ Debug  ]   . (b$10 && start$1 && lambda$12() == eq1.rhs()) ==> (lambda$12 == eq1.rhs)
[ Debug  ]   . (b$11 && start$1 && lambda$12() == eq2.lhs()) ==> (lambda$12 == eq2.lhs)
[ Debug  ]   . (b$11 && start$1 && lambda$12() == eq2.rhs()) ==> (lambda$12 == eq2.rhs)
[ Debug  ]   . b$10 ==> (b_next$1 == (start$1 && lambda$12 == eq1.lhs || b_next$13))
[ Debug  ]   . b$10 ==> (b_next$3 == (start$1 && lambda$12 == eq1.rhs || b_next$15))
[ Debug  ]   . b$11 ==> (b_next$7 == (start$1 && lambda$12 == eq2.lhs || b_next$17))
[ Debug  ]   . b$11 ==> (b_next$9 == (start$1 && lambda$12 == eq2.rhs || b_next$19))
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . b$10 ==> (b_next$5 == (start$1 && lambda$13 == eq1.ev || b_next$21))
[ Debug  ]   . b$11 ==> (b_next$11 == (start$1 && lambda$13 == eq2.ev || b_next$23))
[ Debug  ]   . bs$1 == (b$8 && start$1)
[ Debug  ]   . bs$1 ==> (lambda$14 ≠ lambda$13)
[ Debug  ]   . (b$10 && b$8 && lambda$14() == eq1.ev()) ==> (lambda$14 == eq1.ev)
[ Debug  ]   . (b$11 && b$8 && lambda$14() == eq2.ev()) ==> (lambda$14 == eq2.ev)
[ Debug  ]   . b$10 ==> (b_next$21 == (b$8 && lambda$14 == eq1.ev || b_next$25))
[ Debug  ]   . b$11 ==> (b_next$23 == (b$8 && lambda$14 == eq2.ev || b_next$27))
[ Debug  ]   . b$11 ==> (e$6 == (tp$17 && tp$14 && tp$12))
[ Debug  ]   . b$10 ==> (e$7 == (tp$13 && tp$15 && tp$16))
[ Debug  ]   . start$1 ==> (¬res$5 ==> ¬e$8)
[ Debug  ]   . start$1 ==> (res$5 == (eq1 == RaCons[BigInt, Unit](lambda$12, lambda$12, lambda$13)))
[ Debug  ]   . start$1 ==> e$8
[ Debug  ]   . start$1 ==> (inv$RAEquations[BigInt, Unit](eq1) && e$7)
[ Debug  ]   . start$1 ==> true
[ Debug  ]   . start$1 ==> (inv$RAEquations[BigInt, Unit](eq2) && e$6)
[ Debug  ]   . b$9 ==> (e$8 == (y ≠ x))
[ Debug  ]   . b$8 ==> (¬res$6 ==> ¬e$8)
[ Debug  ]   . b$8 ==> (res$6 == (eq2 == RaCons[BigInt, Unit](lambda$12, lambda$12, lambda$14)))
[ Debug  ]   . (start$1 && res$5) == b$8
[ Debug  ]   . (b$8 && res$6) == b$9
[ Debug  ]   . start$1 == b$10
[ Debug  ]   . start$1 == b$11
[ Debug  ]   . start$1 ==> m$1
[ Debug  ]   . start$1 ==> m$3
[ Debug  ]  - Running search...
[ Debug  ]  - Finished search with blocked literals
[ Debug  ]  - Running search without blocked literals (w/o lucky test)
[ Debug  ]  - Finished search without blocked literals
[  Info  ] gg.tip => UNSAT

@samarion
Copy link
Member

Haha, your perverseApps always make me laugh :)

Well, normalizeStructure seems to be behaving correctly. Just to confirm that's really where the bad clauses are being generated, could you please add some debug here:

if (ft.from.isEmpty) clauses ++= (for {
template <- byType(ft).values.toList
if canBeEqual(template.ids._2, f) && isPureTemplate(template)
} yield {
val (tmplApp, fApp) = (mkApp(template.ids._2, ft, Seq.empty), mkApp(f, ft, Seq.empty))
mkImplies(mkAnd(b, template.start, mkEquals(tmplApp, fApp)), mkEquals(template.ids._2, f))
})

Maybe print out the generated clause, as well as template and template.structure.body.

@jad-hamza
Copy link
Contributor Author

Haha, your perverseApps always make me laugh :)

Oops :)

Maybe print out the generated clause, as well as template and template.structure.body.

I added debug like this:

    println("clauses")
    println(clauses.mkString("\n"))

    if (ft.from.isEmpty) clauses ++= (for {
      template <- byType(ft).values.toList
      if canBeEqual(template.ids._2, f) && isPureTemplate(template)
    } yield {
      val (tmplApp, fApp) = (mkApp(template.ids._2, ft, Seq.empty), mkApp(f, ft, Seq.empty))
      val res = mkImplies(mkAnd(b, template.start, mkEquals(tmplApp, fApp)), mkEquals(template.ids._2, f))
      println("res", res)
      println("template", template)
      println("template.structure.body", template.structure.body)
      res
    })

and got:

====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,makeEqual$0(x$1, y$1))
(preserveApps, onlySimple, inFunction:,false,false,true)



unapply: makeEqual$0(x$1, y$1)
final else branch




End of normalizeStructure:
(bindings,List())
(newExpr,makeEqual$0(x$2, x$5))
----------
deps:
x$2 -> x$1
x$5 -> y$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,Uu$0())
(preserveApps, onlySimple, inFunction:,false,false,true)



unapply: Uu$0()
isLocal(e, path, true) && isAlwaysPure(e)




End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> Uu$0()
====================================================================================================
clauses
(=> b$2!45 (= b_free$0!47 (not b_next$0!48)))
(=> b$2!45 (= tp$0!40 b_and$0!49))
clauses
(=> b$2!45 (= b_free$1!50 (not b_next$1!51)))
(=> b$2!45 (= tp$1!39 b_and$1!52))
clauses
(=> b$2!45 (= b_free$2!53 (not b_next$2!54)))
(=> b$2!45 (= tp$2!35 b_and$2!55))
clauses
(=> b$3!46 (= b_free$3!56 (not b_next$3!57)))
(=> b$3!46 (= tp$3!36 b_and$3!58))
clauses
(=> b$3!46 (= b_free$4!59 (not b_next$4!60)))
(=> b$3!46 (= tp$4!32 b_and$4!61))
clauses
(=> b$3!46 (= b_free$5!62 (not b_next$5!63)))
(=> b$3!46 (= tp$5!33 b_and$5!64))

@samarion
Copy link
Member

Oh, then maybe the issue is here:

val arglessEqClauses: Clauses = if (newTemplate.tpe.from.nonEmpty || !isPureTemplate(newTemplate)) {
Seq.empty
} else {
for ((b,f) <- freeFunctions(newTemplate.tpe).toSeq if canBeEqual(idT, f)) yield {
val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
}
}

Could you please add some similar debug?

@jad-hamza
Copy link
Contributor Author

New debug statements:

      println("\n\narglessEqClauses")
      println("newTemplate.tpe.from.nonEmpty", newTemplate.tpe.from.nonEmpty)
      println("!isPureTemplate(newTemplate)", !isPureTemplate(newTemplate))
      println("freeFunctions(newTemplate.tpe).toSeq", freeFunctions(newTemplate.tpe).toSeq)

      // make sure we introduce sound equality constraints between closures that take no arguments
      val arglessEqClauses: Clauses = if (newTemplate.tpe.from.nonEmpty || !isPureTemplate(newTemplate)) {
        Seq.empty
      } else {
        for ((b,f) <- freeFunctions(newTemplate.tpe).toSeq if canBeEqual(idT, f)) yield {
          val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
          val res = mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
          println()
          println("res", res)
          println("b", b)
          println("f", f)
          res
        }
      }
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,makeEqual$0(x$1, y$1))
(preserveApps, onlySimple, inFunction:,false,false,true)



unapply: makeEqual$0(x$1, y$1)
final else branch




End of normalizeStructure:
(bindings,List())
(newExpr,makeEqual$0(x$2, x$5))
----------
deps:
x$2 -> x$1
x$5 -> y$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,x$1)
(preserveApps, onlySimple, inFunction:,false,false,true)


End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> x$1
====================================================================================================
====================================================================================================
Beginning of normalizeStructure:
(args,List())
(expr,Uu$0())
(preserveApps, onlySimple, inFunction:,false,false,true)



unapply: Uu$0()
isLocal(e, path, true) && isAlwaysPure(e)




End of normalizeStructure:
(bindings,List())
(newExpr,x$2)
----------
deps:
x$2 -> Uu$0()
====================================================================================================
clauses
(=> b$2!45 (= b_free$0!47 (not b_next$0!48)))
(=> b$2!45 (= tp$0!40 b_and$0!49))
clauses
(=> b$2!45 (= b_free$1!50 (not b_next$1!51)))
(=> b$2!45 (= tp$1!39 b_and$1!52))
clauses
(=> b$2!45 (= b_free$2!53 (not b_next$2!54)))
(=> b$2!45 (= tp$2!35 b_and$2!55))
clauses
(=> b$3!46 (= b_free$3!56 (not b_next$3!57)))
(=> b$3!46 (= tp$3!36 b_and$3!58))
clauses
(=> b$3!46 (= b_free$4!59 (not b_next$4!60)))
(=> b$3!46 (= tp$4!32 b_and$4!61))
clauses
(=> b$3!46 (= b_free$5!62 (not b_next$5!63)))
(=> b$3!46 (= tp$5!33 b_and$5!64))


arglessEqClauses
(newTemplate.tpe.from.nonEmpty,false)
(!isPureTemplate(newTemplate),false)
(freeFunctions(newTemplate.tpe).toSeq,Vector((b$2!45,(lhs$1 eq1$0!0)), (b$2!45,(rhs$1 eq1$0!0)), (b$3!46,(lhs$1 eq2$0!3)), (b$3!46,(rhs$1 eq2$0!3))))

(res,(=> (and b$2!45
         start$0!4
         (= (dynLambda$0!9 lambda$0!65) (dynLambda$0!9 (lhs$1 eq1$0!0))))
    (= lambda$0!65 (lhs$1 eq1$0!0))))
(b,b$2!45)
(f,(lhs$1 eq1$0!0))

(res,(=> (and b$2!45
         start$0!4
         (= (dynLambda$0!9 lambda$0!65) (dynLambda$0!9 (rhs$1 eq1$0!0))))
    (= lambda$0!65 (rhs$1 eq1$0!0))))
(b,b$2!45)
(f,(rhs$1 eq1$0!0))

(res,(=> (and b$3!46
         start$0!4
         (= (dynLambda$0!9 lambda$0!65) (dynLambda$0!9 (lhs$1 eq2$0!3))))
    (= lambda$0!65 (lhs$1 eq2$0!3))))
(b,b$3!46)
(f,(lhs$1 eq2$0!3))

(res,(=> (and b$3!46
         start$0!4
         (= (dynLambda$0!9 lambda$0!65) (dynLambda$0!9 (rhs$1 eq2$0!3))))
    (= lambda$0!65 (rhs$1 eq2$0!3))))
(b,b$3!46)
(f,(rhs$1 eq2$0!3))


arglessEqClauses
(newTemplate.tpe.from.nonEmpty,false)
(!isPureTemplate(newTemplate),true)
(freeFunctions(newTemplate.tpe).toSeq,Vector((b$2!45,(ev$1 eq1$0!0)), (b$3!46,(ev$1 eq2$0!3))))


arglessEqClauses
(newTemplate.tpe.from.nonEmpty,false)
(!isPureTemplate(newTemplate),false)
(freeFunctions(newTemplate.tpe).toSeq,Vector((b$2!45,(ev$1 eq1$0!0)), (b$3!46,(ev$1 eq2$0!3))))

(res,(=> (and b$2!45
         b$0!43
         (= (dynLambda$1!13 lambda$5!81) (dynLambda$1!13 (ev$1 eq1$0!0))))
    (= lambda$5!81 (ev$1 eq1$0!0))))
(b,b$2!45)
(f,(ev$1 eq1$0!0))

(res,(=> (and b$3!46
         b$0!43
         (= (dynLambda$1!13 lambda$5!81) (dynLambda$1!13 (ev$1 eq2$0!3))))
    (= lambda$5!81 (ev$1 eq2$0!3))))
(b,b$3!46)
(f,(ev$1 eq2$0!3))

@samarion
Copy link
Member

Very weird, that also looks good...

Where is the (b$10 && b$8 && lambda$14() == eq1.ev()) ==> (lambda$14 == eq1.ev) clause coming from?

@samarion
Copy link
Member

Ohhh, wait I see what's going wrong. Hmm, I'll need to think about it a bit to see how to fix this.

@samarion
Copy link
Member

Urgh, I don't have any idea how to provide a nice fix for this.

The best one I have is to remove those clauses and fix extraction to use chooses (similarly to how I describe extraction in my thesis). This would mean changing the extraction logic in the following three places:

  1. case ft: FunctionType if seen(t) => z3ToChooses.getOrElse(t, {
    val res = Choose(Variable.fresh("x", ft, true).toVal, BooleanLiteral(true))
    z3ToChooses(t) = res
    res
    })
    case ft @ FunctionType(fts, tt) => z3ToLambdas.getOrElse(t, {
    val n = t.toString.split("!").last.init.toInt
    val args = fts.map(tpe => ValDef.fresh("x", tpe, true))
    val res = uniquateClosure(n, lambdas.getB(ft)
    .flatMap(decl => model.getFuncInterpretations.find(_._1 == decl))
    .map { case (_, mapping, elseValue) =>
    val body = mapping.foldLeft(rec(elseValue, tt, seen + t)) { case (elze, (z3Args, z3Result)) =>
    if (t == z3Args.head) {
    val cond = andJoin((args zip z3Args.tail).map { case (vd, z3Arg) =>
    Equals(vd.toVariable, rec(z3Arg, vd.getType, seen + t))
    })
    IfExpr(cond, rec(z3Result, tt, seen + t), elze)
    } else {
    elze
    }
    }
    Lambda(args, body)
    }.getOrElse(try {
    simplestValue(ft, allowSolver = false).asInstanceOf[Lambda]
    } catch {
    case _: NoSimpleValue =>
    Lambda(args, Choose(ValDef.fresh("res", tt), BooleanLiteral(true)))
    }))
    z3ToLambdas(t) = res
    res
  2. val res = uniquateClosure(count, lambdas.getB(ft)
    .flatMap { dynLambda =>
    context.withSeen(n -> ft).getFunction(dynLambda, FunctionType(IntegerType() +: ft.from, ft.to))
    }.map { case Lambda(dispatcher +: args, body) =>
    val dv = dispatcher.toVariable
    val dispatchedBody = exprOps.postMap {
    case Equals(`dv`, IntegerLiteral(i)) => Some(BooleanLiteral(n == i))
    case Equals(IntegerLiteral(i), `dv`) => Some(BooleanLiteral(n == i))
    case Equals(`dv`, UMinus(IntegerLiteral(i))) => Some(BooleanLiteral(n == -i))
    case Equals(UMinus(IntegerLiteral(i)), `dv`) => Some(BooleanLiteral(n == -i))
    case _ => None
    } (body)
    val simpBody = simplifyByConstructors(dispatchedBody)
    assert(!(exprOps.variablesOf(simpBody) contains dispatcher.toVariable), "Dispatcher still in lambda body")
    Lambda(args, simpBody)
    }.getOrElse(try {
    simplestValue(ft, allowSolver = false).asInstanceOf[Lambda]
    } catch {
    case _: NoSimpleValue =>
    val args = ft.from.map(tpe => ValDef.fresh("x", tpe, true))
    Lambda(args, Choose(ValDef.fresh("res", ft), BooleanLiteral(true)))
    }))
    context.lambdas(n -> ft) = res
    res
    })
  3. ctx.lambdas.getOrElse(n, {
    val newCtx = ctx.withSeen(n)
    val params = ft.from.map(tpe => ValDef.fresh("x", tpe, true))
    val res = uniquateClosure(n.intValue, lambdas.getB(ft)
    .flatMap { fun =>
    val interps = ctx.model.interpretation.flatMap {
    case (SimpleAPI.IntFunctionLoc(`fun`, ptr +: args), SimpleAPI.IntValue(res)) =>
    if (ctx.model.eval(iterm === ptr) contains true) {
    val optArgs = (args zip ft.from).map(p => rec(p._1, p._2)(newCtx))
    val optRes = rec(res, ft.to)(newCtx)
    if (optArgs.forall(_.isDefined) && optRes.isDefined) {
    Some(optArgs.map(_.get) -> optRes.get)
    } else {
    None
    }
    } else {
    None
    }
    case _ => None
    }.toSeq.sortBy(_.toString)
    if (interps.nonEmpty) Some(interps) else None
    }.map { interps =>
    Lambda(params, interps.foldRight(interps.head._2) { case ((args, res), elze) =>
    IfExpr(andJoin((params zip args).map(p => Equals(p._1.toVariable, p._2))), res, elze)
    })
    }.getOrElse(try {
    simplestValue(ft, allowSolver = false).asInstanceOf[Lambda]
    } catch {
    case _: NoSimpleValue =>
    Lambda(params, Choose(ValDef.fresh("res", ft.to), BooleanLiteral(true)))
    }))
    ctx.lambdas(n) = res
    res
    })

The new extraction logic should basically always extract lambda values into a value of the form

Lambda(args, Choose(res, BooleanLiteral(true)))

and then we can add the mapping res -> extract(lambdaBody) to the choose map generated by the solver.

The only drawback with this approach is that models output by the solver won't look as nice to users since there will be one level of indirection between lambdas and their bodies. Maybe this can be "fixed" within the model printing logic.


As an example, the extraction code in Z3Native.scala under fromZ3Formula would be changed as follows:

  1. The z3ToChooses map would become
val chooses: MutableMap[Choose, Expr] = MutableMap.empty
  1. The FunctionType case(s) under rec would become
  case ft @ FunctionType(fts, tt) => z3ToLambdas.getOrElse(t, {
    val args = fts.map(tpe => ValDef.fresh("x", tpe, true))
    val choose = Choose(Variable.fresh("x", tt, true).toVal, BooleanLiteral(true))
    val lambda = Lambda(args, choose)
    z3ToLambdas(t) = lambda

    chooses(choose) = lambdas.getB(ft)
      .flatMap(decl => model.getFuncInterpretations.find(_._1 == decl))
      .map { case (_, mapping, elseValue) =>
        ... // same as before except we extract the lambda body (instead of the full lambda)
      })
    lambda
  })
  1. The function would directly return chooses.toMap (instead of using z3ToChooses)

@jad-hamza
Copy link
Contributor Author

Wow that's a lot! Thanks, I'll try this.

The best one I have is to remove those clauses

Removing all the arglessEqClauses?

@samarion
Copy link
Member

Removing all the arglessEqClauses?

Yes, you should remove the clauses here and here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants