Choose under lamba #139
Comments
|
Could you also post the solver debug please? |
|
Sure: |
|
Hmm, seems like something is going wrong in My main suspect are the conditions here: inox/src/main/scala/inox/ast/SymbolOps.scala Lines 409 to 412 in 0157b1b |
|
I added debug output in the beginning of [ 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 |
|
Haha, your Well, inox/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala Lines 227 to 233 in 0157b1b Maybe print out the generated clause, as well as template and template.structure.body.
|
Oops :)
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)) |
|
Oh, then maybe the issue is here: inox/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala Lines 310 to 317 in 1b17cb4 Could you please add some similar debug? |
|
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)) |
|
Very weird, that also looks good... Where is the |
|
Ohhh, wait I see what's going wrong. Hmm, I'll need to think about it a bit to see how to fix this. |
|
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:
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 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
val chooses: MutableMap[Choose, Expr] = MutableMap.empty
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
})
|
|
Wow that's a lot! Thanks, I'll try this.
Removing all the |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
eq2makes Inox returnSAT. (removing the assertion oneq1makes Inox returnSATas well)The text was updated successfully, but these errors were encountered: