Code Monkey home page Code Monkey logo

Comments (13)

samarion avatar samarion commented on September 25, 2024 1

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. inox/src/main/scala/inox/solvers/z3/Z3Native.scala

    Lines 592 to 625 in 0157b1b

    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. inox/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala

    Lines 562 to 589 in 6dfb351

    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. inox/src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala

    Lines 473 to 509 in 6dfb351

    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)

from inox.

samarion avatar samarion commented on September 25, 2024

Could you also post the solver debug please?

from inox.

jad-hamza avatar jad-hamza commented on September 25, 2024

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

from inox.

samarion avatar samarion commented on September 25, 2024

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

My main suspect are the conditions here:

inox/src/main/scala/inox/ast/SymbolOps.scala

Lines 409 to 412 in 0157b1b

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

from inox.

jad-hamza avatar jad-hamza commented on September 25, 2024

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

from inox.

samarion avatar samarion commented on September 25, 2024

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:

inox/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala

Lines 227 to 233 in 0157b1b

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.

from inox.

jad-hamza avatar jad-hamza commented on September 25, 2024

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

from inox.

samarion avatar samarion commented on September 25, 2024

Oh, then maybe the issue is here:

inox/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala

Lines 310 to 317 in 1b17cb4

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?

from inox.

jad-hamza avatar jad-hamza commented on September 25, 2024

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

from inox.

samarion avatar samarion commented on September 25, 2024

Very weird, that also looks good...

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

from inox.

samarion avatar samarion commented on September 25, 2024

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

from inox.

jad-hamza avatar jad-hamza commented on September 25, 2024

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

The best one I have is to remove those clauses

Removing all the arglessEqClauses?

from inox.

samarion avatar samarion commented on September 25, 2024

Removing all the arglessEqClauses?

Yes, you should remove the clauses here and here.

from inox.

Related Issues (20)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.