Disabled CVC4 and Princess -- revisit this once the rest is clean.

Author: gsps

src/main/scala/inox/solvers/SolverFactory.scala

@@ -229,6 +229,9 @@ object SolverFactory {
         () => new SolverBase(p, ctx, enc, chooseEnc)
       })
 
+      // FIXME(gsps): No idea why CVC4Solver is not found here.
+      // FIXME(gsps): Probably have to move `chooses` and maybe `theories` into constructors.
+      /*
       case "smt-cvc4" => create(p)(finalName, {
         val ev = sem.getEvaluator(ctx)
         val chooseEnc = ChooseEncoder(p)(enc)
@@ -237,11 +240,11 @@ object SolverFactory {
         val progEnc = fullEnc andThen theoryEnc
         val targetSem = progEnc.targetProgram.getSemantics
 
-        () => new {
+        () => new UnrollingSolver with TimeoutSolver with tip.TipDebugger {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with UnrollingSolver with TimeoutSolver with tip.TipDebugger {
+
           val semantics = sem
           val chooses: chooseEnc.type = chooseEnc
           val theories: theoryEnc.type = theoryEnc
@@ -250,27 +253,31 @@ object SolverFactory {
           override protected lazy val fullEncoder = fullEnc
           override protected lazy val programEncoder = progEnc
 
-          protected val underlying = new {
+          protected val underlying = inox.solvers.smtlib.CVC4Solver {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
-          } with smtlib.CVC4Solver {
+
             val semantics: program.Semantics = targetSem
           }
         }
       })
+      */
 
+      // FIXME(gsps): AbstractPrincessSolver and PrincessSolver still have lots of errors.
+      // FIXME(gsps): Probably have to move `chooses` and maybe `theories` into constructors.
+      /*
       case "princess" => create(p)(finalName, {
         val ev = sem.getEvaluator(ctx)
         val chooseEnc = ChooseEncoder(p)(enc)
         val fullEnc = enc andThen chooseEnc
         val theoryEnc = theories.Princess(fullEnc)(ev)
         val progEnc = fullEnc andThen theoryEnc
 
-        () => new {
+        () => new princess.PrincessSolver with TimeoutSolver {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with princess.PrincessSolver with TimeoutSolver {
+
           val semantics = sem
           val chooses: chooseEnc.type = chooseEnc
           override protected lazy val theories: theoryEnc.type = theoryEnc
@@ -280,6 +287,7 @@ object SolverFactory {
           lazy val targetSemantics: targetProgram.Semantics = targetProgram.getSemantics
         }
       })
+      */
 
       case _ => throw FatalError("Unknown solver: " + finalName)
     }

src/main/scala/inox/solvers/princess/AbstractPrincessSolver.scala

@@ -1,4 +1,4 @@
-/* Copyright 2009-2018 EPFL, Lausanne */
+/*/* Copyright 2009-2018 EPFL, Lausanne */
 
 package inox
 package solvers
@@ -539,3 +539,4 @@ trait AbstractPrincessSolver extends AbstractSolver with ADTManagers {
 
   def interrupt() = interruptCheckSat = true
 }
+*/

src/main/scala/inox/solvers/princess/PrincessSolver.scala

@@ -1,4 +1,4 @@
-/* Copyright 2009-2018 EPFL, Lausanne */
+/*/* Copyright 2009-2018 EPFL, Lausanne */
 
 package inox
 package solvers
@@ -24,20 +24,20 @@ trait PrincessSolver extends AbstractUnrollingSolver { self =>
     val targetProgram: Program { val trees: fullEncoder.targetProgram.trees.type }
   } = solvers.theories.Princess(fullEncoder)(semantics.getEvaluator)
 
-  protected object underlying extends {
+  protected object underlying extends AbstractPrincessSolver {
     val program: targetProgram.type = targetProgram
     val context = self.context
-  } with AbstractPrincessSolver {
+
     lazy val semantics = targetSemantics
   }
 
   type Encoded = IExpression
 
-  object templates extends {
+  object templates extends Templates {
     val program: targetProgram.type = targetProgram
     val context = self.context
     val semantics: targetProgram.Semantics = self.targetSemantics
-  } with Templates {
+    
     import program.trees._
 
     type Encoded = self.Encoded
@@ -88,9 +88,9 @@ trait PrincessSolver extends AbstractUnrollingSolver { self =>
 
   protected def declareVariable(v: t.Variable): IExpression = underlying.declareVariable(v)
 
-  protected def wrapModel(model: underlying.Model): super.ModelWrapper = ModelWrapper(model)
+  protected def wrapModel(model: underlying.Model): ModelWrapper = PrincessModelWrapper(model)
 
-  private case class ModelWrapper(model: underlying.Model) extends super.ModelWrapper {
+  private case class PrincessModelWrapper(model: underlying.Model) extends ModelWrapper {
     private val chooses: MutableMap[Identifier, t.Expr] = MutableMap.empty
     import IExpression._
 
@@ -146,3 +146,4 @@ trait PrincessSolver extends AbstractUnrollingSolver { self =>
     underlying.free()
   }
 }
+*/