[feat] Specific Vampire mode for TTA

ConsoleRunner.fs

@@ -103,13 +103,13 @@ type SolveArguments =
             | Table -> "Generate .csv statistics table after solving"
             | Transform _ -> "Apply additional transformations to the problem (default: disabled; the solver is run on the original)"
 
-let private solverByName = function
+let private solverByName options = function
     | MyZ3 -> MyZ3Solver() :> SolverProgramRunner
     | Z3 -> Z3Solver() :> SolverProgramRunner
     | Eldarica -> EldaricaSolver() :> SolverProgramRunner
     | CVC_Ind -> CVC4IndSolver() :> SolverProgramRunner
     | VeriMAP -> VeriMAPiddtSolver() :> SolverProgramRunner
-    | Vampire -> VampireSolver() :> SolverProgramRunner
+    | Vampire -> VampireSolver(options) :> SolverProgramRunner
     | CVC_FMF -> CVCFiniteSolver() :> SolverProgramRunner
     | RCHC -> RCHCSolver() :> SolverProgramRunner
 //    | All -> AllSolver() :> SolverProgramRunner
@@ -190,13 +190,14 @@ let private solve_from_path (solver : SolverProgramRunner) (transformer : Transf
 
 let private solve outputPath runSame (options : ParseResults<SolveArguments>) =
     let solver_name = options.GetResult(Solver)
-    let solver = solverByName solver_name
-    let transformer =
+    let transformer, opts =
         match options.TryGetResult(Transform) with
         | Some _ as transformOptions ->
             let mode = solverNameToTransformMode solver_name
-            modeToTransformerProgram mode transformOptions runSame |> fst |> Some
-        | None -> None
+            let t, opts = modeToTransformerProgram mode transformOptions runSame
+            Some t, Some opts
+        | None -> None, None
+    let solver = solverByName opts solver_name
     match options.TryGetResult(Path) with
     | None ->
         match options.Contains(In) with

Solvers.fs

@@ -166,9 +166,15 @@ type VeriMAPiddtSolver () =
 
 type private refutationSource = Axiom | Inference of string * string list
 
-type VampireSolver () =
+type VampireSolver (options : transformOptions option) =
     inherit SolverProgramRunner ()
 
+    let isRunOnTTATransform =
+        match options with
+        | Some options -> options.tta_transform
+        | None -> false
+    let mode = if isRunOnTTATransform then "-sa fmb" else "--mode chccomp"
+
     let splitModules output =
         let reDelimiter = Regex("^(% )?[-]+$")
         let isDelimiter s = reDelimiter.Match(s).Success
@@ -287,7 +293,7 @@ type VampireSolver () =
     override x.Name = "Vampire"
     override x.BinaryName = "vampire"
     override x.BinaryOptions filename =
-        $"""--mode chccomp --memory_limit {MEMORY_LIMIT_MB} --time_limit {SECONDS_TIMEOUT}s %s{filename}"""
+        $"""{mode} --memory_limit {MEMORY_LIMIT_MB} --time_limit {SECONDS_TIMEOUT}s %s{filename}"""
 
     override x.InterpretResult error raw_output =
         let output = Environment.split raw_output