diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-10-11 15:51:49 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:43:17 -0400 |
commit | 606f6965f3ccec837aa216cbb3f56fdcf943a59b (patch) | |
tree | e9d1283f60b335de331b5e8abd93f040636f871b /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |
parent | implement http requests for the TPTP server (diff) | |
download | VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.gz VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.tar.zst VIATRA-Generator-606f6965f3ccec837aa216cbb3f56fdcf943a59b.zip |
VAMPIRE: complete testing setup
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | 16 |
1 files changed, 12 insertions, 4 deletions
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 | |||
2 | 2 | ||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
4 | 4 | ||
5 | class VampireSolverConfiguration extends LogicSolverConfiguration { | 5 | class VampireSolverConfiguration |
6 | extends LogicSolverConfiguration { | ||
6 | 7 | ||
7 | public var int contCycleLevel = 0 | 8 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | 9 | public var boolean uniquenessDuplicates = false |
9 | public var int iteration = -1 | 10 | public var int iteration = -1 |
10 | public var BackendSolver solver = BackendSolver::VAMP | 11 | public var BackendSolver solver = BackendSolver::VAMPIRE |
11 | public var genModel = true | 12 | public var genModel = true |
13 | public var server = false | ||
12 | //choose needed backend solver | 14 | //choose needed backend solver |
13 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 15 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
14 | } | 16 | } |
15 | 17 | ||
16 | 18 | ||
17 | enum BackendSolver { | 19 | enum BackendSolver { |
18 | VAMP, | 20 | CVC4, |
19 | CVC4 | 21 | DARWINFM, |
22 | EDARWIN, | ||
23 | GEOIII, | ||
24 | IPROVER, | ||
25 | PARADOX, | ||
26 | VAMPIRE, | ||
27 | Z3 | ||
20 | //add needed things | 28 | //add needed things |
21 | } | 29 | } |
22 | 30 | ||