search

LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
76 stars 38 forks source link

Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} #109

Open krooken opened 1 year ago

krooken commented 1 year ago

I am getting an error message that I cannot understand. I am trying to prove a seemingly simple formula where I have, among others, yp < 0 and yp >= 0 on the left hand side. When I try to close the branch with QE, I get an error saying Input {48, MemoryConstrained[...]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]}. What does this error message mean? If I hide some of the sequents, then I can close the branch with QE, but I am a bit suprised that I have to. I think that I have managed to close similar branched before; what is special about this formula?

KeYmaera X version 5.0.1 Operating System: Windows 10 10.0 Java JVM: Oracle Corporation 17.0.1 with 64 bits Java Home: C:\Program Files\Java\jdk-17.0.1

Input {48, MemoryConstrained[TimeConstrained[Reduce[ForAll[{kyxyp, kyxxp, kyxx, kyxwl, kyxvpMax, kyxv, kyxt$u$, kyxrange, kyxptol, kyxle, kyxaMin, kyxaMax, kyxa, kyxT}, Implies[And[Greater[kyxwl, 0], And[Greater[kyxle, 0], And[Greater[kyxvpMax, 0], And[Greater[kyxrange, 0], And[Greater[kyxptol, 0], And[Less[kyxaMin, 0], And[Greater[kyxaMax, 0], And[Less[Times[kyxT, kyxvpMax], kyxwl], And[Less[Times[kyxT, Minus[0]], kyxwl], And[Greater[kyxxp, kyxrange], And[Greater[kyxT, 0], And[Less[kyxyp, 0], And[GreaterEqual[kyxt$u$, 0], And[ForAll[{kyxs$u$}, Implies[And[LessEqual[0, kyxs$u$], LessEqual[kyxs$u$, kyxt$u$]], And[LessEqual[Plus[kyxs$u$, 0], kyxT], GreaterEqual[Plus[Times[kyxaMax, kyxs$u$], kyxv], 0]]]], And[LessEqual[Subtract[kyxx, kyxle], kyxxp], And[GreaterEqual[kyxyp, 0], And[LessEqual[kyxyp, kyxwl], And[Greater[kyxyp, kyxwl], And[Implies[Less[kyxyp, 0], Greater[Plus[Divide[Times[Times[kyxaMax, Minus[Divide[kyxyp, kyxvpMax]]], Minus[Divide[kyxyp, kyxvpMax]]], 2], Times[kyxv, Minus[Divide[kyxyp, kyxvpMax]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], And[Greater[0, 0], And[Less[0, kyxvpMax], And[LessEqual[kyxaMin, kyxa], And[LessEqual[kyxa, kyxaMax], And[Implies[Greater[kyxyp, kyxwl], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[kyxv, Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], Implies[And[GreaterEqual[kyxyp, 0], LessEqual[kyxyp, kyxwl]], Greater[Subtract[kyxx, kyxle], kyxxp]]]]]]]]]]]]]]]]]]]]]]]]]], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[Plus[Times[kyxaMax, kyxt$u$], kyxv], Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, Plus[Plus[Times[kyxaMax, Divide[Power[kyxt$u$, 2], 2]], Times[kyxv, kyxt$u$]], kyxx]], kyxle]]]], {}, Reals], 5], 8000000000]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} in _QE in _QE at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:296) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:291) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.runExpr(SequentialInterpreter.scala:308) at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.runExpr(SequentialInterpreter.scala:773) at edu.cmu.cs.ls.keymaerax.bellerophon.ExhaustiveSequentialInterpreter.runExpr(SequentialInterpreter.scala:813) at edu.cmu.cs.ls.keymaerax.bellerophon.BelleBaseInterpreter.apply(SequentialInterpreter.scala:45) at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:128) at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:125) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:539) at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264) at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136) at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635) at java.base/java.lang.Thread.run(Thread.java:833) Caused by: Input {48, MemoryConstrained[TimeConstrained[Reduce[ForAll[{kyxyp, kyxxp, kyxx, kyxwl, kyxvpMax, kyxv, kyxt$u$, kyxrange, kyxptol, kyxle, kyxaMin, kyxaMax, kyxa, kyxT}, Implies[And[Greater[kyxwl, 0], And[Greater[kyxle, 0], And[Greater[kyxvpMax, 0], And[Greater[kyxrange, 0], And[Greater[kyxptol, 0], And[Less[kyxaMin, 0], And[Greater[kyxaMax, 0], And[Less[Times[kyxT, kyxvpMax], kyxwl], And[Less[Times[kyxT, Minus[0]], kyxwl], And[Greater[kyxxp, kyxrange], And[Greater[kyxT, 0], And[Less[kyxyp, 0], And[GreaterEqual[kyxt$u$, 0], And[ForAll[{kyxs$u$}, Implies[And[LessEqual[0, kyxs$u$], LessEqual[kyxs$u$, kyxt$u$]], And[LessEqual[Plus[kyxs$u$, 0], kyxT], GreaterEqual[Plus[Times[kyxaMax, kyxs$u$], kyxv], 0]]]], And[LessEqual[Subtract[kyxx, kyxle], kyxxp], And[GreaterEqual[kyxyp, 0], And[LessEqual[kyxyp, kyxwl], And[Greater[kyxyp, kyxwl], And[Implies[Less[kyxyp, 0], Greater[Plus[Divide[Times[Times[kyxaMax, Minus[Divide[kyxyp, kyxvpMax]]], Minus[Divide[kyxyp, kyxvpMax]]], 2], Times[kyxv, Minus[Divide[kyxyp, kyxvpMax]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], And[Greater[0, 0], And[Less[0, kyxvpMax], And[LessEqual[kyxaMin, kyxa], And[LessEqual[kyxa, kyxaMax], And[Implies[Greater[kyxyp, kyxwl], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[kyxv, Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, kyxx], kyxle]]], Implies[And[GreaterEqual[kyxyp, 0], LessEqual[kyxyp, kyxwl]], Greater[Subtract[kyxx, kyxle], kyxxp]]]]]]]]]]]]]]]]]]]]]]]]]], Greater[Plus[Divide[Times[Times[kyxaMax, Divide[Subtract[kyxyp, kyxwl], Minus[0]]], Divide[Subtract[kyxyp, kyxwl], Minus[0]]], 2], Times[Plus[Times[kyxaMax, kyxt$u$], kyxv], Divide[Subtract[kyxyp, kyxwl], Minus[0]]]], Plus[Subtract[kyxxp, Plus[Plus[Times[kyxaMax, Divide[Power[kyxt$u$, 2], 2]], Times[kyxv, kyxt$u$]], kyxx]], kyxle]]]], {}, Reals], 5], 8000000000]} cannot be evaluated, cause: {HoldForm[MessageName[ForAll, "msgs"]]} at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.$anonfun$getAnswer$1(MathematicaCommandRunner.scala:150) at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaConversion$.importResult(MathematicaConversion.scala:33) at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.getAnswer(MathematicaCommandRunner.scala:137) at edu.cmu.cs.ls.keymaerax.tools.qe.JLinkMathematicaCommandRunner.doRun(MathematicaCommandRunner.scala:87) at edu.cmu.cs.ls.keymaerax.tools.qe.BaseMathematicaCommandRunner.run(MathematicaCommandRunner.scala:51) at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaQETool.singleQE(MathematicaQETool.scala:49) at edu.cmu.cs.ls.keymaerax.tools.qe.MathematicaQETool.quantifierElimination(MathematicaQETool.scala:34) at edu.cmu.cs.ls.keymaerax.core.Provable$.proveArithmetic(Proof.scala:521) at edu.cmu.cs.ls.keymaerax.pt.ElidingProvable$.proveArithmetic(TermProvable.scala:439) at edu.cmu.cs.ls.keymaerax.pt.ElidingProvable$.proveArithmeticLemma(TermProvable.scala:442) at edu.cmu.cs.ls.keymaerax.pt.ProvableSig$.proveArithmeticLemma(TermProvable.scala:371) at edu.cmu.cs.ls.keymaerax.tools.ext.Mathematica.$anonfun$qe$1(Mathematica.scala:132) at edu.cmu.cs.ls.keymaerax.tools.ext.MathematicaQEToolBridge.$anonfun$run$1(MathematicaQEToolBridge.scala:29) at edu.cmu.cs.ls.keymaerax.tools.ext.JLinkMathematicaLink.$anonfun$run$2(MathematicaLink.scala:316) at edu.cmu.cs.ls.keymaerax.tools.ext.ToolExecutor.$anonfun$makeFuture$1(ToolExecutor.scala:111) ... 6 more

smitsch commented 1 year ago

The error message means that there is a warning generated by Mathematica/Wolfram Engine, but KeYmaera X couldn't retrieve it for display on the UI. Instead, we display the attempted query. When copying that attempted query and evaluating it in Mathematica or Wolfram Engine directly, the message usually appears on their debug output.

There can be several reasons for warnings in Mathematica, but in this particular case there is a division by zero in some of the "irrelevant" other assumptions.

Once the assumptions that use division by zero are hidden, the QE call on this particular proof obligation succeeds. However, unless the assumptions are completely irrelevant for the entire proof, or you are branching on a quantity (0 vs. !=0) where on the 0 branch the affected assumptions are irrelevant, sooner or later there will be a proof obligation that cannot be proved because of the division by zero.

krooken commented 1 year ago

Great, thank you very much! That helps a lot. I apparently tried to simplify a model a bit too much.

Would it be possible to add the suggestion of entering the query directly in Mathematica/Wolfram Engine to the error message when the warning retrieval fails? Now I know what to do, but I imagine it could be helpful to others.