From 60f01f46ba232ed6416054f0a6115cb2a9b70b4e Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sat, 10 Jun 2017 19:05:05 +0200 Subject: Migrating Additional projects --- .../reasoner/AlloyAnalyzerConfiguration.xtend | 32 ++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend') diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend new file mode 100644 index 00000000..cdf21174 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/AlloyAnalyzerConfiguration.xtend @@ -0,0 +1,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 +} \ No newline at end of file -- cgit v1.2.3-54-g00ecf