diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-02-01 16:03:30 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:06:28 -0400 |
commit | 57e614aabedc176ba9965d0ca5e6daa23c5f4758 (patch) | |
tree | 16806454dff463419af99b14f6abfab3d1fa5291 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill | |
parent | FAM MM transformation works (diff) | |
download | VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.gz VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.tar.zst VIATRA-Generator-57e614aabedc176ba9965d0ca5e6daa23c5f4758.zip |
Fix FAM Test. Begin Grammar Fix.
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill')
5 files changed, 312 insertions, 28 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend index 64484b88..cbe53bff 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend | |||
@@ -1,18 +1,18 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated | 4 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetupGenerated |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Vampire2LogicMapper | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireHandler | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException | 11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasonerException |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 14 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
9 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper | ||
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguagePackage | ||
11 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 15 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
12 | import java.io.PrintWriter | ||
13 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup | ||
14 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper | ||
15 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapper_FilteredTypes | ||
16 | 16 | ||
17 | class VampireSolver extends LogicReasoner{ | 17 | class VampireSolver extends LogicReasoner{ |
18 | 18 | ||
@@ -23,14 +23,14 @@ class VampireSolver extends LogicReasoner{ | |||
23 | } | 23 | } |
24 | 24 | ||
25 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) | 25 | val Logic2VampireLanguageMapper forwardMapper = new Logic2VampireLanguageMapper(new Logic2VampireLanguageMapper_TypeMapper_FilteredTypes) |
26 | // //not for now | 26 | val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper |
27 | // val VampireHandler handler = new VampireHandler | 27 | val VampireHandler handler = new VampireHandler |
28 | // val Vampire2LogicMapper backwardMapper = new Vampire2LogicMapper | ||
29 | 28 | ||
30 | val fileName = "problem.tptp" | ||
31 | 29 | ||
32 | override solve(LogicProblem problem, LogicSolverConfiguration configuration, ReasonerWorkspace workspace) throws LogicReasonerException { | 30 | val fileName = "vampireProblem.tptp" |
33 | val vampireConfig = configuration.asConfig | 31 | |
32 | override solve(LogicProblem problem, LogicSolverConfiguration config, ReasonerWorkspace workspace) throws LogicReasonerException { | ||
33 | val vampireConfig = config.asConfig | ||
34 | 34 | ||
35 | // Start: Logic -> Vampire mapping | 35 | // Start: Logic -> Vampire mapping |
36 | val transformationStart = System.currentTimeMillis | 36 | val transformationStart = System.currentTimeMillis |
@@ -41,36 +41,38 @@ class VampireSolver extends LogicReasoner{ | |||
41 | 41 | ||
42 | var String fileURI = null; | 42 | var String fileURI = null; |
43 | var String vampireCode = null; | 43 | var String vampireCode = null; |
44 | vampireCode = workspace.writeModelToString(vampireProblem,fileName) | ||
44 | if(vampireConfig.writeToFile) { | 45 | if(vampireConfig.writeToFile) { |
45 | fileURI = workspace.writeModel(vampireProblem,fileName).toFileString | 46 | fileURI = workspace.writeModel(vampireProblem,fileName).toFileString |
46 | } else { | 47 | } |
47 | vampireCode = workspace.writeModelToString(vampireProblem,fileName) | 48 | |
48 | } | 49 | //Result as String |
50 | |||
51 | |||
49 | val transformationTime = System.currentTimeMillis - transformationStart | 52 | val transformationTime = System.currentTimeMillis - transformationStart |
50 | // Finish: Logic -> Vampire mapping | 53 | // Finish: Logic -> Vampire mapping |
51 | 54 | ||
52 | //Creates a file containing the tptp code after transformation | 55 | |
53 | val out = new PrintWriter("output/files/vampireCode.tptp") | 56 | /* |
54 | out.println(vampireCode) | ||
55 | out.close() | ||
56 | |||
57 | |||
58 | /* | ||
59 | * not for now -> Start: Solving Alloy problem | ||
60 | * | ||
61 | // Start: Solving Alloy problem | 57 | // Start: Solving Alloy problem |
62 | val solverStart = System.currentTimeMillis | 58 | val solverStart = System.currentTimeMillis |
63 | val result2 = handler.callSolver(alloyProblem,workspace,alloyConfig,fileURI,alloyCode) | 59 | //Calling Solver (Currently Manually) |
64 | val logicResult = backwardMapper.transformOutput(problem,configuration.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | 60 | val result2 = handler.callSolver(vampireProblem,workspace,vampireConfig,vampireCode) |
61 | // val result2 = null | ||
62 | //TODO | ||
63 | //Backwards Mapper | ||
64 | val logicResult = backwardMapper.transformOutput(problem,config.solutionScope.numberOfRequiredSolution,result2,forwardTrace,transformationTime) | ||
65 | |||
65 | val solverFinish = System.currentTimeMillis-solverStart | 66 | val solverFinish = System.currentTimeMillis-solverStart |
66 | // Finish: Solving Alloy problem | 67 | // Finish: Solving Alloy problem |
67 | 68 | ||
68 | if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) | 69 | if(vampireConfig.writeToFile) workspace.deactivateModel(fileName) |
69 | 70 | ||
70 | return logicResult | 71 | return logicResult |
71 | */ | ||
72 | 72 | ||
73 | /*/ | ||
73 | return null // for now | 74 | return null // for now |
75 | //*/ | ||
74 | } | 76 | } |
75 | 77 | ||
76 | def asConfig(LogicSolverConfiguration configuration){ | 78 | def asConfig(LogicSolverConfiguration configuration){ |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 9b316210..cd48a032 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -55,7 +55,7 @@ class Logic2VampireLanguageMapper { | |||
55 | } | 55 | } |
56 | 56 | ||
57 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, | 57 | public def TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> transformProblem(LogicProblem problem, |
58 | VampireSolverConfiguration configuration) { | 58 | VampireSolverConfiguration config) { |
59 | // create model bases | 59 | // create model bases |
60 | // TODO | 60 | // TODO |
61 | val initialComment = createVLSComment => [ | 61 | val initialComment = createVLSComment => [ |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend index 01c4f5af..41e2137c 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -97,6 +97,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
97 | } | 97 | } |
98 | 98 | ||
99 | // 5. create fof function that is an or with all the elements in map | 99 | // 5. create fof function that is an or with all the elements in map |
100 | // Do this only if there are more than 1 type | ||
100 | val hierarch = createVLSFofFormula => [ | 101 | val hierarch = createVLSFofFormula => [ |
101 | it.name = "hierarchyHandler" | 102 | it.name = "hierarchyHandler" |
102 | it.fofRole = "axiom" | 103 | it.fofRole = "axiom" |
@@ -115,6 +116,7 @@ class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Logic2Vamp | |||
115 | ] | 116 | ] |
116 | 117 | ||
117 | trace.specification.formulas += hierarch | 118 | trace.specification.formulas += hierarch |
119 | |||
118 | } | 120 | } |
119 | 121 | ||
120 | def boolean dfsSupertypeCheck(Type type, Type type2) { | 122 | def boolean dfsSupertypeCheck(Type type, Type type2) { |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend new file mode 100644 index 00000000..5cb0198e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend | |||
@@ -0,0 +1,66 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicresultFactory | ||
5 | |||
6 | class Vampire2LogicMapper { | ||
7 | val extension LogicresultFactory resultFactory = LogicresultFactory.eINSTANCE | ||
8 | |||
9 | public def transformOutput(LogicProblem problem, int requiredNumberOfSolution, VampireSolutionModel vampireSolution, Logic2VampireLanguageMapperTrace trace, long transformationTime) { | ||
10 | val models = vampireSolution.aswers.map[it.key].toList | ||
11 | |||
12 | if(!monitoredAlloySolution.finishedBeforeTimeout) { | ||
13 | return createInsuficientResourcesResult => [ | ||
14 | it.problem = problem | ||
15 | it.representation += models | ||
16 | it.trace = trace | ||
17 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
18 | ] | ||
19 | } else { | ||
20 | if(models.last.satisfiable || requiredNumberOfSolution == -1) { | ||
21 | return createModelResult => [ | ||
22 | it.problem = problem | ||
23 | it.representation += models | ||
24 | it.trace = trace | ||
25 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
26 | ] | ||
27 | } else { | ||
28 | return createInconsistencyResult => [ | ||
29 | it.problem = problem | ||
30 | it.representation += models | ||
31 | it.trace = trace | ||
32 | it.statistics = transformStatistics(monitoredAlloySolution,transformationTime) | ||
33 | ] | ||
34 | } | ||
35 | } | ||
36 | } | ||
37 | |||
38 | def transformStatistics(MonitoredAlloySolution solution, long transformationTime) { | ||
39 | createStatistics => [ | ||
40 | it.transformationTime = transformationTime as int | ||
41 | for(solutionIndex : 0..<solution.aswers.size) { | ||
42 | val solutionTime = solution.aswers.get(solutionIndex).value | ||
43 | it.entries+= createIntStatisticEntry => [ | ||
44 | it.name = '''Answer«solutionIndex»Time''' | ||
45 | it.value = solutionTime.intValue | ||
46 | ] | ||
47 | } | ||
48 | it.entries+= createIntStatisticEntry => [ | ||
49 | it.name = "Alloy2KodKodTransformationTime" | ||
50 | it.value = solution.kodkodTime as int | ||
51 | ] | ||
52 | it.entries+= createIntStatisticEntry => [ | ||
53 | it.name = "Alloy2KodKodTransformationTime" | ||
54 | it.value = solution.kodkodTime as int | ||
55 | ] | ||
56 | it.entries+= createStringStatisticEntry => [ | ||
57 | it.name = "warnings" | ||
58 | it.value = '''[«FOR warning : solution.warnings SEPARATOR ","»«warning»«ENDFOR»]''' | ||
59 | ] | ||
60 | ] | ||
61 | } | ||
62 | |||
63 | def sum(Iterable<Long> ints) { | ||
64 | ints.reduce[p1, p2|p1+p2] | ||
65 | } | ||
66 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend new file mode 100644 index 00000000..aefa1a7e --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend | |||
@@ -0,0 +1,214 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireBackendSolver | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | ||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
6 | import com.google.common.util.concurrent.SimpleTimeLimiter | ||
7 | import com.google.common.util.concurrent.UncheckedTimeoutException | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
9 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
10 | import java.util.ArrayList | ||
11 | import java.util.HashMap | ||
12 | import java.util.LinkedList | ||
13 | import java.util.List | ||
14 | import java.util.Map | ||
15 | import java.util.concurrent.Callable | ||
16 | import java.util.concurrent.TimeUnit | ||
17 | import org.eclipse.emf.common.command.Command | ||
18 | import org.eclipse.xtend.lib.annotations.Data | ||
19 | |||
20 | class VampireSolverException extends Exception{ | ||
21 | new(String s) { super(s) } | ||
22 | new(String s, Exception e) { super(s,e) } | ||
23 | new(String s, List<String> errors, Exception e) { | ||
24 | super(s + '\n' + errors.join('\n'), e) | ||
25 | } | ||
26 | } | ||
27 | |||
28 | @Data class VampireSolutionModel{ | ||
29 | // List<String> warnings | ||
30 | // List<String> debugs | ||
31 | // long kodkodTime | ||
32 | // val List<Pair<A4Solution, Long>> aswers | ||
33 | // val boolean finishedBeforeTimeout | ||
34 | |||
35 | |||
36 | } | ||
37 | |||
38 | class VampireHandler { | ||
39 | |||
40 | //val fileName = "problem.als" | ||
41 | |||
42 | public def callSolver(VampireModel problem, ReasonerWorkspace workspace, VampireSolverConfiguration configuration,String vampireCode) { | ||
43 | /* | ||
44 | //Prepare | ||
45 | val warnings = new LinkedList<String> | ||
46 | val debugs = new LinkedList<String> | ||
47 | val runtime = new ArrayList<Long> | ||
48 | val reporter = new A4Reporter() { | ||
49 | override debug(String message) { debugs += message } | ||
50 | override resultSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
51 | override resultUNSAT (Object command, long solvingTime, Object solution) { runtime += solvingTime } | ||
52 | override warning(ErrorWarning msg) { warnings += msg.message } | ||
53 | } | ||
54 | |||
55 | val options = new A4Options() => [ | ||
56 | it.symmetry = configuration.symmetry | ||
57 | it.noOverflow = true | ||
58 | it.solver = getSolver(configuration.getSolver, configuration) | ||
59 | if(configuration.getSolver.externalSolver) { | ||
60 | it.solverDirectory = configuration.solverPath | ||
61 | } | ||
62 | //it.inferPartialInstance | ||
63 | //it.tempDirectory = CommonPlugin.resolve(workspace.workspaceURI).toFileString | ||
64 | ] | ||
65 | |||
66 | // Transform | ||
67 | var Command command = null; | ||
68 | var CompModule compModule = null | ||
69 | |||
70 | // Start: Alloy -> Kodkod | ||
71 | val kodkodTransformStart = System.currentTimeMillis(); | ||
72 | try { | ||
73 | compModule = CompUtil.parseEverything_fromString(reporter,alloyCode) | ||
74 | if(compModule.allCommands.size != 1) | ||
75 | throw new UnsupportedOperationException('''Alloy files with multiple commands are not supported!''') | ||
76 | command = compModule.allCommands.head | ||
77 | } catch (Err e){ | ||
78 | throw new AlloySolverException(e.message,warnings,e) | ||
79 | } | ||
80 | val kodkodTransformFinish = System.currentTimeMillis - kodkodTransformStart | ||
81 | // Finish: Alloy -> Kodkod | ||
82 | |||
83 | val limiter = new SimpleTimeLimiter | ||
84 | val callable = new AlloyCallerWithTimeout(warnings,debugs,reporter,options,command,compModule,configuration) | ||
85 | var List<Pair<A4Solution, Long>> answers | ||
86 | var boolean finished | ||
87 | if(configuration.runtimeLimit == LogicSolverConfiguration::Unlimited) { | ||
88 | answers = callable.call | ||
89 | finished = true | ||
90 | } else { | ||
91 | try{ | ||
92 | answers = limiter.callWithTimeout(callable,configuration.runtimeLimit,TimeUnit.SECONDS,true) | ||
93 | finished = true | ||
94 | } catch (UncheckedTimeoutException e) { | ||
95 | answers = callable.partialAnswers | ||
96 | finished = false | ||
97 | } | ||
98 | } | ||
99 | |||
100 | new MonitoredAlloySolution(warnings,debugs,kodkodTransformFinish,answers,finished) | ||
101 | */ | ||
102 | } | ||
103 | /* | ||
104 | val static Map<SolverConfiguration, SatSolver> previousSolverConfigurations = new HashMap | ||
105 | def getSolverConfiguration(AlloyBackendSolver backedSolver, String path, String[] options) { | ||
106 | val config = new SolverConfiguration(backedSolver,path,options) | ||
107 | if(previousSolverConfigurations.containsKey(config)) { | ||
108 | return previousSolverConfigurations.get(config) | ||
109 | } else { | ||
110 | val id ='''DSLReasoner_Alloy_«previousSolverConfigurations.size»_«backedSolver»''' | ||
111 | val newSolver = A4Options.SatSolver.make(id,id,path,options) | ||
112 | previousSolverConfigurations.put(config,newSolver) | ||
113 | return newSolver | ||
114 | } | ||
115 | } | ||
116 | |||
117 | def getSolver(AlloyBackendSolver backedSolver, AlloySolverConfiguration configuration) { | ||
118 | switch(backedSolver){ | ||
119 | case BerkMinPIPE: return A4Options.SatSolver.BerkMinPIPE | ||
120 | case SpearPIPE: return A4Options.SatSolver.SpearPIPE | ||
121 | case MiniSatJNI: return A4Options.SatSolver.MiniSatJNI | ||
122 | case MiniSatProverJNI: return A4Options.SatSolver.MiniSatProverJNI | ||
123 | case LingelingJNI: return A4Options.SatSolver.LingelingJNI | ||
124 | case PLingelingJNI: return getSolverConfiguration(backedSolver,configuration.solverPath,null) | ||
125 | case GlucoseJNI: return A4Options.SatSolver.GlucoseJNI | ||
126 | case CryptoMiniSatJNI: return A4Options.SatSolver.CryptoMiniSatJNI | ||
127 | case SAT4J: return A4Options.SatSolver.SAT4J | ||
128 | case CNF: return A4Options.SatSolver.CNF | ||
129 | case KodKod: return A4Options.SatSolver.KK | ||
130 | } | ||
131 | } | ||
132 | |||
133 | def isExternalSolver(AlloyBackendSolver backedSolver) { | ||
134 | return !(backedSolver == AlloyBackendSolver.SAT4J) | ||
135 | } | ||
136 | */ | ||
137 | } | ||
138 | /* | ||
139 | class VampireCallerWithTimeout implements Callable<List<Pair<A4Solution,Long>>>{ | ||
140 | |||
141 | val List<String> warnings | ||
142 | val List<String> debugs | ||
143 | val A4Reporter reporter | ||
144 | val A4Options options | ||
145 | |||
146 | val Command command | ||
147 | val CompModule compModule | ||
148 | val AlloySolverConfiguration configuration | ||
149 | |||
150 | val List<Pair<A4Solution,Long>> answers = new LinkedList() | ||
151 | |||
152 | new(List<String> warnings, | ||
153 | List<String> debugs, | ||
154 | A4Reporter reporter, | ||
155 | A4Options options, | ||
156 | Command command, | ||
157 | CompModule compModule, | ||
158 | AlloySolverConfiguration configuration) | ||
159 | { | ||
160 | this.warnings = warnings | ||
161 | this.debugs = debugs | ||
162 | this.reporter = reporter | ||
163 | this.options = options | ||
164 | this.command = command | ||
165 | this.compModule = compModule | ||
166 | this.configuration = configuration | ||
167 | } | ||
168 | |||
169 | override call() throws Exception { | ||
170 | val startTime = System.currentTimeMillis | ||
171 | |||
172 | // Start: Execute | ||
173 | var A4Solution lastAnswer = null | ||
174 | try { | ||
175 | if(!configuration.progressMonitor.isCancelled) { | ||
176 | do{ | ||
177 | if(lastAnswer == null) { | ||
178 | lastAnswer = TranslateAlloyToKodkod.execute_command(reporter,compModule.allSigs,command,options) | ||
179 | } else { | ||
180 | lastAnswer = lastAnswer.next | ||
181 | } | ||
182 | configuration.progressMonitor.workedBackwardTransformation(configuration.solutionScope.numberOfRequiredSolution) | ||
183 | |||
184 | val runtime = System.currentTimeMillis -startTime | ||
185 | synchronized(this) { | ||
186 | answers += (lastAnswer->runtime) | ||
187 | } | ||
188 | } while(lastAnswer.satisfiable != false && !hasEnoughSolution(answers) && !configuration.progressMonitor.isCancelled) | ||
189 | |||
190 | } | ||
191 | }catch(Exception e) { | ||
192 | warnings +=e.message | ||
193 | } | ||
194 | // Finish: execute | ||
195 | return answers | ||
196 | } | ||
197 | |||
198 | def hasEnoughSolution(List<?> answers) { | ||
199 | if(configuration.solutionScope.numberOfRequiredSolution < 0) return false | ||
200 | else return answers.size() == configuration.solutionScope.numberOfRequiredSolution | ||
201 | } | ||
202 | |||
203 | public def getPartialAnswers() { | ||
204 | return answers | ||
205 | } | ||
206 | |||
207 | } | ||
208 | /* | ||
209 | @Data class SolverConfiguration { | ||
210 | VampireBackendSolver backendSolver | ||
211 | String path | ||
212 | String[] options | ||
213 | } | ||
214 | */ | ||