aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend
blob: cdf2117469f02074d1c4aef6bc023ecd15f9f834 (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
package hu.bme.mit.inf.dlsreasoner.alloy.reasoner

import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration

class AlloySolverConfiguration extends LogicSolverConfiguration {
	/*public var boolean createCommonSupertype
	public var int intScope = 1 // 5 by default
	public def setIntScopeFor(int max) {
		intScope = 31 - Integer.numberOfLeadingZeros(max) + 1
	}*/
	public var int symmetry = 0 // by default
	public var AlloyBackendSolver solver = AlloyBackendSolver.SAT4J
	public var boolean writeToFile = false
}

enum AlloyBackendSolver {
	BerkMinPIPE,
	SpearPIPE,
	MiniSatJNI,
	MiniSatProverJNI,
	LingelingJNI,
	PLingelingJNI,
	GlucoseJNI,
	CryptoMiniSatJNI,
	SAT4J,
	CNF,
	KodKod
}

enum TypeMappingTechnique {
	FilteredTypes
}