From 17d6aa5028bff14c80f0be6a042c6a68fe8b61b0 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 11 Oct 2019 15:51:49 -0400 Subject: VAMPIRE: complete testing setup --- .../vampire/reasoner/VampireAnalyzerConfiguration.xtend | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 4e9737cb..4c2f1952 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend @@ -2,21 +2,29 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration -class VampireSolverConfiguration extends LogicSolverConfiguration { +class VampireSolverConfiguration + extends LogicSolverConfiguration { public var int contCycleLevel = 0 public var boolean uniquenessDuplicates = false public var int iteration = -1 - public var BackendSolver solver = BackendSolver::VAMP + public var BackendSolver solver = BackendSolver::VAMPIRE public var genModel = true + public var server = false //choose needed backend solver // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J } enum BackendSolver { - VAMP, - CVC4 + CVC4, + DARWINFM, + EDARWIN, + GEOIII, + IPROVER, + PARADOX, + VAMPIRE, + Z3 //add needed things } -- cgit v1.2.3-54-g00ecf