From d4eff1395a943753cf751a6431b057e297d73c8b Mon Sep 17 00:00:00 2001 From: Andre Platzer Date: Fri, 2 Sep 2016 20:24:28 -0400 Subject: [PATCH] Temporarily disable inverse characteristic method again since the converters need list generalizations etc. --- .../cmu/cs/ls/keymaerax/btactics/DifferentialTactics.scala | 5 +++-- .../scala/edu/cmu/cs/ls/keymaerax/tools/Mathematica.scala | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DifferentialTactics.scala b/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DifferentialTactics.scala index 263b4e894a..e79c299bc3 100644 --- a/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DifferentialTactics.scala +++ b/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DifferentialTactics.scala @@ -614,7 +614,8 @@ private object DifferentialTactics { ) & ODE(pos) | noCut(pos) | // if no differential cut succeeded, just skip and go for a direct proof. //@todo could swap diffSolve before above line with noCut once diffSolve quickly detects by dependencies whether it solves - TactixLibrary.diffSolve()(pos) | + TactixLibrary.diffSolve()(pos) +/*| ChooseSome( //@todo should memoize the results of the differential invariant generator () => InvariantGenerator.extendedDifferentialInvariantGenerator(seq,pos), @@ -627,7 +628,7 @@ private object DifferentialTactics { // show diffCut, but don't use yet another diffCut noCut(pos) & done ) - ) & ODE(pos) + ) & ODE(pos) */ }) diff --git a/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/tools/Mathematica.scala b/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/tools/Mathematica.scala index ba5a629270..6f184144a0 100644 --- a/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/tools/Mathematica.scala +++ b/keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/tools/Mathematica.scala @@ -19,7 +19,7 @@ import scala.collection.immutable.Map * @author Stefan Mitsch * @todo Code Review: Move non-critical tool implementations into a separate package tactictools */ -class Mathematica extends ToolBase("Mathematica") with QETool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool with PDESolverTool { +class Mathematica extends ToolBase("Mathematica") with QETool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool /*with PDESolverTool*/ { // JLink, shared between tools private val link = new JLinkMathematicaLink