aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
blob: c3b344eb28665fbd420d62c56bcae170cd6a2a4c (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
package ca.mcgill.ecse.dslreasoner.vampire.reasoner

import hu.bme.mit.inf.dslreasoner.logic.model.builder.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::LOCVAMP
	public var genModel = true
	public var server = false
	//choose needed backend solver
//	public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
}


enum BackendSolver {
	CVC4,
	DARWINFM,
	EDARWIN,
	GEOIII,
	IPROVER,
	PARADOX,
	VAMPIRE,
	Z3,
	LOCVAMP
	//add needed things
}


enum TypeMappingTechnique {
	//default
	FilteredTypes
}