Temporarily disable inverse characteristic method again since the con…

…verters need list generalizations etc.
LS-Lab · Sep 3, 2016 · d4eff13 · d4eff13
1 parent f314335
commit d4eff13
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 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
@@ -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
@@ -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