Comments (9)
jad-hamza
commented on September 28, 2024
I think you need to write (check-sat) to get an output
from inox.
romac
commented on September 28, 2024
@jad-hamza Right! Thanks. With it it also crashes Inox, with the following stack trace (which I forgot to include earlier):
Exception in thread "main" java.util.NoSuchElementException: key not found: x$1
at scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:101)
at scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:99)
at inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprStructure$12(TemplateGenerator.scala:143)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
at scala.collection.immutable.Set$Set2.foreach(Set.scala:132)
at scala.collection.TraversableLike.map(TraversableLike.scala:237)
at scala.collection.TraversableLike.map$(TraversableLike.scala:230)
at scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:51)
at scala.collection.SetLike.map(SetLike.scala:104)
at scala.collection.SetLike.map$(SetLike.scala:104)
at scala.collection.AbstractSet.map(Set.scala:51)
at inox.solvers.unrolling.TemplateGenerator.mkExprStructure(TemplateGenerator.scala:143)
at inox.solvers.unrolling.TemplateGenerator.mkExprStructure$(TemplateGenerator.scala:78)
at inox.solvers.z3.Z3Unrolling$templates$.mkExprStructure(Z3Unrolling.scala:28)
at inox.solvers.unrolling.QuantificationTemplates$QuantificationTemplate$.apply(QuantificationTemplates.scala:131)
at inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprClauses$7(TemplateGenerator.scala:407)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
at scala.collection.immutable.List.foreach(List.scala:392)
at scala.collection.TraversableLike.map(TraversableLike.scala:237)
at scala.collection.TraversableLike.map$(TraversableLike.scala:230)
at scala.collection.immutable.List.map(List.scala:298)
at inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:397)
at inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:260)
at inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprClauses$9(TemplateGenerator.scala:434)
at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:237)
at scala.collection.immutable.List.foreach(List.scala:392)
at scala.collection.TraversableLike.map(TraversableLike.scala:237)
at scala.collection.TraversableLike.map$(TraversableLike.scala:230)
at scala.collection.immutable.List.map(List.scala:298)
at inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:434)
at inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:278)
at inox.solvers.unrolling.TemplateGenerator.recAnd$1(TemplateGenerator.scala:297)
at inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:317)
at inox.solvers.unrolling.TemplateGenerator.mkExprClauses(TemplateGenerator.scala:437)
at inox.solvers.unrolling.TemplateGenerator.mkExprClauses$(TemplateGenerator.scala:237)
at inox.solvers.z3.Z3Unrolling$templates$.mkExprClauses(Z3Unrolling.scala:28)
at inox.solvers.unrolling.TemplateGenerator.mkClauses(TemplateGenerator.scala:68)
at inox.solvers.unrolling.TemplateGenerator.mkClauses$(TemplateGenerator.scala:67)
at inox.solvers.z3.Z3Unrolling$templates$.mkClauses(Z3Unrolling.scala:28)
at inox.solvers.unrolling.Templates.$anonfun$instantiateExpr$1(Templates.scala:865)
at inox.solvers.unrolling.Templates.instantiate(Templates.scala:831)
at inox.solvers.unrolling.Templates.instantiateExpr(Templates.scala:862)
at inox.solvers.unrolling.Templates.instantiateExpr$(Templates.scala:861)
at inox.solvers.z3.Z3Unrolling$templates$.instantiateExpr(Z3Unrolling.scala:28)
at inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$assertCnstr$5(UnrollingSolver.scala:183)
at scala.util.Try$.apply(Try.scala:213)
at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
at inox.utils.TimerStorage.run(Timer.scala:88)
at inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$assertCnstr$1(UnrollingSolver.scala:181)
at scala.util.Try$.apply(Try.scala:213)
at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
at inox.utils.TimerStorage.run(Timer.scala:88)
at inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr(UnrollingSolver.scala:163)
at inox.solvers.unrolling.AbstractUnrollingSolver.assertCnstr$(UnrollingSolver.scala:163)
at inox.solvers.SolverFactory$$anon$2.inox$tip$TipDebugger$$super$assertCnstr(SolverFactory.scala:125)
at inox.tip.TipDebugger.assertCnstr(TipDebugger.scala:91)
at inox.tip.TipDebugger.assertCnstr$(TipDebugger.scala:89)
at inox.solvers.SolverFactory$$anon$2.assertCnstr(SolverFactory.scala:125)
at inox.solvers.SolverFactory$$anon$2.assertCnstr(SolverFactory.scala:125)
at inox.solvers.SimpleSolverAPI.solveSAT(SimpleSolverAPI.scala:34)
at inox.solvers.SimpleSolverAPI.solveSAT$(SimpleSolverAPI.scala:31)
at inox.solvers.SimpleSolverAPI$$anon$1.solveSAT(SimpleSolverAPI.scala:57)
at inox.Main$.$anonfun$main$3(Main.scala:234)
at inox.Main$.$anonfun$main$3$adapted(Main.scala:224)
at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:792)
at scala.collection.immutable.List.foreach(List.scala:392)
at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:791)
at inox.Main$.$anonfun$main$1(Main.scala:224)
at inox.Main$.$anonfun$main$1$adapted(Main.scala:224)
at scala.collection.immutable.List.foreach(List.scala:392)
at inox.Main$.main(Main.scala:224)
at inox.Main.main(Main.scala)
from inox.
jad-hamza
commented on September 28, 2024
New version minimized with @romac:
(declare-const b1 Bool)
(define-fun mm ((b2 Bool)) Bool
(choose res Bool (forall ((b3 Bool)) (= b3 b2)))
)
(assert (mm (mm b1)))
(check-sat)from inox.
samarion
commented on September 28, 2024
Could someone maybe add some printing in mkExprStructure and show me the output so I can help debug the issue?
from inox.
jad-hamza
commented on September 28, 2024
Sure, here is some debug output for normalizeStructure and mkExprStructure:
In normalizeStructure:
====================================================================================================
(args,List(b3$3: Boolean))
(expr,b3$3 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == b1$0)))
(perverseApps, onlySimple, inFunction:,true,false,false)
(bindings,List(x$0: Boolean))
(newExpr,x$0 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == x$1)))
----------
deps:
----------
In mkExprStructure:
====================================================================================================
(pathVar,start$0)
(expr,∀b3$2: Boolean. (b3$2 == choose((res$1: Boolean) => ∀b3$1: Boolean. (b3$1 == b1$0))))
----------
substMap:
b1$0 -> b1$0!0
start$0 -> start$0!1
res$2 -> res$2!2
----------
(onlySimple,false)
(struct,∀x$0: Boolean. (x$0 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == x$1))))
----------
deps:
----------
(exprOps.variablesOf(struct),Set(x$1))
Exception in thread "main" java.util.NoSuchElementException: key not found: x$1The printing code is:
implicit val printerOps = new PrinterOptions(printUniqueIds = true)
println("\n\n")
println("In normalizeStructure:")
println("=" * 100)
println("args", args.map(_.asString))
println("expr", expr.asString)
println("perverseApps, onlySimple, inFunction:", preserveApps, onlySimple, inFunction)
println("bindings", bindings.map(_.asString))
println("newExpr", newExpr.asString)
println("-" * 10)
println("deps:")
println(deps.map(p => p._1.asString + " -> " + p._2.asString).mkString("\n"))
println("-" * 10)and
println("\n\n")
println("In mkExprStructure:")
println("=" * 100)
println("pathVar", pathVar.asString)
println("expr", expr.asString)
println("-" * 10)
println("substMap:")
println(substMap.map(p => p._1.asString + " -> " + p._2).mkString("\n"))
println("-" * 10)
println("onlySimple", onlySimple)
println("struct", struct.asString)
println("-" * 10)
println("deps:")
println(deps.map(p => p._1.asString + " -> " + p._2.asString).mkString("\n"))
println("-" * 10)
println("exprOps.variablesOf(struct)", exprOps.variablesOf(struct).map(_.asString))from inox.
samarion
commented on September 28, 2024
Well, I'm really not sure because the logic in normalizeStructure is horribly convoluted and I can't remember what I was thinking when I wrote that monster, but my first guess would be that this line is wrong:
inox/src/main/scala/inox/ast/SymbolOps.scala
Line 463 in 1b17cb4
I would expect the transformation of free variables in the choose should rather look like the Variable case above:
inox/src/main/scala/inox/ast/SymbolOps.scala
Lines 432 to 434 in 1b17cb4
from inox.
jad-hamza
commented on September 28, 2024
Thanks! Here is the output after the change in #138
In normalizeStructure:
====================================================================================================
(args,List(b3$3: Boolean))
(expr,b3$3 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == b1$0)))
(perverseApps, onlySimple, inFunction:,true,false,false)
(bindings,List(x$0: Boolean))
(newExpr,x$0 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == x$1)))
----------
deps:
x$1 -> b1$0
----------
In mkExprStructure:
====================================================================================================
(pathVar,start$0)
(expr,∀b3$2: Boolean. (b3$2 == choose((res$1: Boolean) => ∀b3$1: Boolean. (b3$1 == b1$0))))
----------
substMap:
b1$0 -> b1$0!0
start$0 -> start$0!1
res$2 -> res$2!2
----------
(onlySimple,false)
(struct,∀x$0: Boolean. (x$0 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == x$1))))
----------
deps:
x$1 -> b1$0
----------
(exprOps.variablesOf(struct),Set(x$1))
In normalizeStructure:
====================================================================================================
(args,List(b3$5: Boolean))
(expr,b3$5 == x$2)
(perverseApps, onlySimple, inFunction:,true,false,false)
(bindings,List(x$0: Boolean))
(newExpr,x$0 == x$1)
----------
deps:
x$1 -> x$2
----------
In mkExprStructure:
====================================================================================================
(pathVar,start$0)
(expr,∀b3$4: Boolean. (b3$4 == x$2))
----------
substMap:
x$0 -> b3$2!3
res$2 -> res$2!2
start$0 -> start$0!1
x$2 -> b1$0!0
res$3 -> res$3!4
b1$0 -> b1$0!0
----------
(onlySimple,false)
(struct,∀x$0: Boolean. (x$0 == x$1))
----------
deps:
x$1 -> x$2
----------
(exprOps.variablesOf(struct),Set(x$1))
[ Error ] Quantification x$0 == choose((res$1: Boolean) => ∀b3$4: Boolean. (b3$4 == x$2)) does not fit in supported fragment.
[ Error ] Reason: No matchers found.
[ Error ] Model obtained was:
[ Error ] b1$0: Boolean -> false
[ Info ] InoxIssue.scala => UNKNOWNfrom inox.
samarion
commented on September 28, 2024
That looks correct. The forall((b3: Boolean) => b3 == b2) isn't supported by the Inox quantifier instantiation procedure which explains the warning.
from inox.
samarion
commented on September 28, 2024
Fixed by Jad's PR.
from inox.
Related Issues (20)
- Unsat file reported as SAT HOT 2
- Error in documentation when compiling HOT 6
- Inox error when using set.toList in Stainless HOT 3
- Lookup failure in Definitions.scala (line 197), for apply. HOT 4
- Choose under lamba HOT 13
- Missing support for str.++
- Code explosion in mergeCalls HOT 3
- Key not found error when using --debug=tip from Stainless HOT 3
- Mismatch between hasInstance and simplestValue HOT 6
- Integration of `rust-interop` in `master`
- Type error in tip printed from Stainless HOT 2
- ChooseEncoder doesn't transform all the trees
- Underapproximate unfolding
- StackOverflowError on an equivalence checking example
- Enable reading smt-lib files with dependent types for future text interface from Stainless
- Migrate to Scala 3.2 HOT 1
- CVC4/5 unsupported feature shows an error even though another solver is verifying the VC HOT 2
- Inox does not compile on Scala 3.3.1 + HOT 5
- Add a sequence type: finitary arrays from natural numbers to some type
- Provision timeout in unrolling solver HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
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.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from inox.