inox Choose under lamba

In this PR https://github.com/epfl-lara/stainless/pull/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)

Apr 25 '21 17:04 jad-hamza

Could you also post the solver debug please?

Apr 25 '21 17:04 samarion

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

Apr 25 '21 18:04 jad-hamza

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

My main suspect are the conditions here: https://github.com/epfl-lara/inox/blob/0157b1ba10bcffec92623650b466c1ea9e4de4e1/src/main/scala/inox/ast/SymbolOps.scala#L409-L412

Apr 26 '21 06:04 samarion

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

Apr 26 '21 07:04 jad-hamza

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: https://github.com/epfl-lara/inox/blob/0157b1ba10bcffec92623650b466c1ea9e4de4e1/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala#L227-L233 Maybe print out the generated clause, as well as template and template.structure.body.

Apr 26 '21 08:04 samarion

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))

Apr 26 '21 08:04 jad-hamza

Oh, then maybe the issue is here: https://github.com/epfl-lara/inox/blob/1b17cb4d38dfddf16286e3346929b7a05267c380/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala#L310-L317

Could you please add some similar debug?

Apr 26 '21 09:04 samarion

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))

Apr 26 '21 09:04 jad-hamza

Very weird, that also looks good...

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

Apr 26 '21 09:04 samarion

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

Apr 26 '21 10:04 samarion

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:

https://github.com/epfl-lara/inox/blob/0157b1ba10bcffec92623650b466c1ea9e4de4e1/src/main/scala/inox/solvers/z3/Z3Native.scala#L592-L625
https://github.com/epfl-lara/inox/blob/6dfb351eeee44a3f13152bf510aceba7936d0e4d/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala#L562-L589
https://github.com/epfl-lara/inox/blob/6dfb351eeee44a3f13152bf510aceba7936d0e4d/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala#L473-L509

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:

The z3ToChooses map would become

val chooses: MutableMap[Choose, Expr] = MutableMap.empty

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
  })

The function would directly return chooses.toMap (instead of using z3ToChooses)

Apr 26 '21 11:04 samarion

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

The best one I have is to remove those clauses

Removing all the arglessEqClauses?

Apr 26 '21 12:04 jad-hamza

Removing all the arglessEqClauses?

Yes, you should remove the clauses here and here.

Apr 26 '21 12:04 samarion

inox inox copied to clipboard

Choose under lamba

inox
inox copied to clipboard