diff options
Diffstat (limited to 'subprojects')
6 files changed, 277 insertions, 156 deletions
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java new file mode 100644 index 00000000..81bf712a --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefinery.java | |||
@@ -0,0 +1,38 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import tools.refinery.store.model.Model; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
11 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
12 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
13 | |||
14 | public class AbstractRefinery { | ||
15 | protected final ProblemTrace problemTrace; | ||
16 | protected final ModelStore store; | ||
17 | protected final Model model; | ||
18 | protected final ReasoningAdapter reasoningAdapter; | ||
19 | |||
20 | public AbstractRefinery(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | ||
21 | this.problemTrace = problemTrace; | ||
22 | this.store = store; | ||
23 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
24 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
25 | } | ||
26 | |||
27 | public ProblemTrace getProblemTrace() { | ||
28 | return problemTrace; | ||
29 | } | ||
30 | |||
31 | public ModelStore getModelStore() { | ||
32 | return store; | ||
33 | } | ||
34 | |||
35 | public Model getModel() { | ||
36 | return model; | ||
37 | } | ||
38 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java new file mode 100644 index 00000000..b60a3890 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/AbstractRefineryBuilder.java | |||
@@ -0,0 +1,152 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Provider; | ||
10 | import org.eclipse.emf.common.util.URI; | ||
11 | import org.eclipse.emf.ecore.resource.Resource; | ||
12 | import org.eclipse.xtext.diagnostics.Severity; | ||
13 | import org.eclipse.xtext.resource.IResourceFactory; | ||
14 | import org.eclipse.xtext.resource.XtextResourceSet; | ||
15 | import org.eclipse.xtext.util.LazyStringInputStream; | ||
16 | import org.eclipse.xtext.validation.CheckMode; | ||
17 | import org.eclipse.xtext.validation.IResourceValidator; | ||
18 | import tools.refinery.generator.impl.ProblemTraceImpl; | ||
19 | import tools.refinery.language.model.problem.Problem; | ||
20 | import tools.refinery.language.semantics.model.ModelInitializer; | ||
21 | import tools.refinery.store.query.ModelQueryBuilder; | ||
22 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | ||
23 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
24 | import tools.refinery.store.util.CancellationToken; | ||
25 | |||
26 | import java.io.File; | ||
27 | import java.io.IOException; | ||
28 | import java.io.InputStream; | ||
29 | import java.util.Collection; | ||
30 | import java.util.Map; | ||
31 | |||
32 | public abstract class AbstractRefineryBuilder<T> { | ||
33 | @Inject | ||
34 | private Provider<XtextResourceSet> resourceSetProvider; | ||
35 | |||
36 | @Inject | ||
37 | private IResourceFactory resourceFactory; | ||
38 | |||
39 | @Inject | ||
40 | private IResourceValidator resourceValidator; | ||
41 | |||
42 | @Inject | ||
43 | protected ModelInitializer initializer; | ||
44 | |||
45 | @Inject | ||
46 | private ProblemTraceImpl problemTrace; | ||
47 | |||
48 | protected CancellationToken cancellationToken = CancellationToken.NONE; | ||
49 | private boolean problemLoaded; | ||
50 | private ModelQueryBuilder queryEngineBuilder; | ||
51 | protected Collection<Concreteness> requiredInterpretations; | ||
52 | |||
53 | protected AbstractRefineryBuilder(Collection<Concreteness> defaultRequiredInterpretations) { | ||
54 | requiredInterpretations = defaultRequiredInterpretations; | ||
55 | } | ||
56 | |||
57 | protected abstract T self(); | ||
58 | |||
59 | public T cancellationToken(CancellationToken cancellationToken) { | ||
60 | this.cancellationToken = cancellationToken; | ||
61 | return self(); | ||
62 | } | ||
63 | |||
64 | public T fromString(String problemString) throws IOException { | ||
65 | try (var stream = new LazyStringInputStream(problemString)) { | ||
66 | return fromStream(stream); | ||
67 | } | ||
68 | } | ||
69 | |||
70 | public T fromStream(InputStream inputStream) throws IOException { | ||
71 | var resourceSet = resourceSetProvider.get(); | ||
72 | var resource = resourceFactory.createResource(URI.createFileURI("__synthetic.problem")); | ||
73 | resourceSet.getResources().add(resource); | ||
74 | resource.load(inputStream, Map.of()); | ||
75 | return fromResource(resource); | ||
76 | } | ||
77 | |||
78 | public T fromFile(File file) throws IOException { | ||
79 | return fromFile(file.getAbsolutePath()); | ||
80 | } | ||
81 | |||
82 | public T fromFile(String filePath) throws IOException { | ||
83 | return fromUri(URI.createFileURI(filePath)); | ||
84 | } | ||
85 | |||
86 | public T fromUri(URI uri) throws IOException { | ||
87 | var resourceSet = resourceSetProvider.get(); | ||
88 | var resource = resourceFactory.createResource(uri); | ||
89 | resourceSet.getResources().add(resource); | ||
90 | resource.load(Map.of()); | ||
91 | return fromResource(resource); | ||
92 | } | ||
93 | |||
94 | public T fromResource(Resource resource) { | ||
95 | var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> { | ||
96 | cancellationToken.checkCancelled(); | ||
97 | return Thread.interrupted(); | ||
98 | }); | ||
99 | cancellationToken.checkCancelled(); | ||
100 | var errors = issues.stream() | ||
101 | .filter(issue -> issue.getSeverity() == Severity.ERROR) | ||
102 | .toList(); | ||
103 | if (!errors.isEmpty()) { | ||
104 | throw new ValidationErrorsException(resource.getURI(), errors); | ||
105 | } | ||
106 | if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) { | ||
107 | throw new IllegalArgumentException("Model generation problem not found in resource " + resource.getURI()); | ||
108 | } | ||
109 | return problem(problem); | ||
110 | } | ||
111 | |||
112 | public T problem(Problem problem) { | ||
113 | if (problemLoaded) { | ||
114 | throw new IllegalStateException("Problem was already set"); | ||
115 | } | ||
116 | initializer.readProblem(problem); | ||
117 | problemTrace.setInitializer(initializer); | ||
118 | problemLoaded = true; | ||
119 | return self(); | ||
120 | } | ||
121 | |||
122 | public ProblemTrace getProblemTrace() { | ||
123 | checkProblem(); | ||
124 | return problemTrace; | ||
125 | } | ||
126 | |||
127 | public T queryEngine(ModelQueryBuilder queryEngineBuilder) { | ||
128 | if (this.queryEngineBuilder != null) { | ||
129 | throw new IllegalStateException("Query engine was already set"); | ||
130 | } | ||
131 | this.queryEngineBuilder = queryEngineBuilder; | ||
132 | return self(); | ||
133 | } | ||
134 | |||
135 | public T requiredInterpretations(Collection<Concreteness> requiredInterpretations) { | ||
136 | this.requiredInterpretations = requiredInterpretations; | ||
137 | return self(); | ||
138 | } | ||
139 | |||
140 | protected void checkProblem() { | ||
141 | if (!problemLoaded) { | ||
142 | throw new IllegalStateException("Problem was not loaded"); | ||
143 | } | ||
144 | } | ||
145 | |||
146 | protected ModelQueryBuilder getQueryEngineBuilder() { | ||
147 | if (queryEngineBuilder == null) { | ||
148 | return QueryInterpreterAdapter.builder(); | ||
149 | } | ||
150 | return queryEngineBuilder; | ||
151 | } | ||
152 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java index 4c3e52f3..e5115352 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGenerator.java | |||
@@ -10,10 +10,7 @@ import tools.refinery.language.model.problem.Relation; | |||
10 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; | 10 | import tools.refinery.store.dse.strategy.BestFirstStoreManager; |
11 | import tools.refinery.store.dse.transition.VersionWithObjectiveValue; | 11 | import tools.refinery.store.dse.transition.VersionWithObjectiveValue; |
12 | import tools.refinery.store.map.Version; | 12 | import tools.refinery.store.map.Version; |
13 | import tools.refinery.store.model.Model; | ||
14 | import tools.refinery.store.model.ModelStore; | 13 | import tools.refinery.store.model.ModelStore; |
15 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
16 | import tools.refinery.store.reasoning.ReasoningStoreAdapter; | ||
17 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | 14 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; |
18 | import tools.refinery.store.reasoning.literal.Concreteness; | 15 | import tools.refinery.store.reasoning.literal.Concreteness; |
19 | import tools.refinery.store.reasoning.representation.PartialSymbol; | 16 | import tools.refinery.store.reasoning.representation.PartialSymbol; |
@@ -22,35 +19,16 @@ import tools.refinery.store.representation.TruthValue; | |||
22 | 19 | ||
23 | import java.util.Collection; | 20 | import java.util.Collection; |
24 | 21 | ||
25 | public class ModelGenerator { | 22 | public class ModelGenerator extends AbstractRefinery { |
26 | private final ProblemTrace problemTrace; | ||
27 | private final ModelStore store; | ||
28 | private final Model model; | ||
29 | private final ReasoningAdapter reasoningAdapter; | ||
30 | private final Version initialVersion; | 23 | private final Version initialVersion; |
31 | 24 | ||
32 | private int randomSeed = 1; | 25 | private int randomSeed = 1; |
33 | 26 | ||
34 | public ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | 27 | public ModelGenerator(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { |
35 | this.problemTrace = problemTrace; | 28 | super(problemTrace, store, modelSeed); |
36 | this.store = store; | ||
37 | model = store.getAdapter(ReasoningStoreAdapter.class).createInitialModel(modelSeed); | ||
38 | reasoningAdapter = model.getAdapter(ReasoningAdapter.class); | ||
39 | initialVersion = model.commit(); | 29 | initialVersion = model.commit(); |
40 | } | 30 | } |
41 | 31 | ||
42 | public ProblemTrace getProblemTrace() { | ||
43 | return problemTrace; | ||
44 | } | ||
45 | |||
46 | public ModelStore getModelStore() { | ||
47 | return store; | ||
48 | } | ||
49 | |||
50 | public Model getModel() { | ||
51 | return model; | ||
52 | } | ||
53 | |||
54 | public int getRandomSeed() { | 32 | public int getRandomSeed() { |
55 | return randomSeed; | 33 | return randomSeed; |
56 | } | 34 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java index 98b6653d..d14cbe3a 100644 --- a/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelGeneratorBuilder.java | |||
@@ -5,135 +5,22 @@ | |||
5 | */ | 5 | */ |
6 | package tools.refinery.generator; | 6 | package tools.refinery.generator; |
7 | 7 | ||
8 | import com.google.inject.Inject; | ||
9 | import com.google.inject.Provider; | ||
10 | import org.eclipse.emf.common.util.URI; | ||
11 | import org.eclipse.emf.ecore.resource.Resource; | ||
12 | import org.eclipse.xtext.diagnostics.Severity; | ||
13 | import org.eclipse.xtext.resource.IResourceFactory; | ||
14 | import org.eclipse.xtext.resource.XtextResourceSet; | ||
15 | import org.eclipse.xtext.util.LazyStringInputStream; | ||
16 | import org.eclipse.xtext.validation.CheckMode; | ||
17 | import org.eclipse.xtext.validation.IResourceValidator; | ||
18 | import tools.refinery.generator.impl.ProblemTraceImpl; | ||
19 | import tools.refinery.language.model.problem.Problem; | ||
20 | import tools.refinery.language.semantics.model.ModelInitializer; | ||
21 | import tools.refinery.store.dse.propagation.PropagationAdapter; | 8 | import tools.refinery.store.dse.propagation.PropagationAdapter; |
22 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; | 9 | import tools.refinery.store.dse.transition.DesignSpaceExplorationAdapter; |
23 | import tools.refinery.store.model.ModelStore; | 10 | import tools.refinery.store.model.ModelStore; |
24 | import tools.refinery.store.query.ModelQueryBuilder; | ||
25 | import tools.refinery.store.query.interpreter.QueryInterpreterAdapter; | ||
26 | import tools.refinery.store.reasoning.ReasoningAdapter; | 11 | import tools.refinery.store.reasoning.ReasoningAdapter; |
27 | import tools.refinery.store.reasoning.literal.Concreteness; | 12 | import tools.refinery.store.reasoning.literal.Concreteness; |
28 | import tools.refinery.store.statecoding.StateCoderAdapter; | 13 | import tools.refinery.store.statecoding.StateCoderAdapter; |
29 | import tools.refinery.store.util.CancellationToken; | ||
30 | 14 | ||
31 | import java.io.File; | ||
32 | import java.io.IOException; | ||
33 | import java.io.InputStream; | ||
34 | import java.util.Collection; | ||
35 | import java.util.Map; | ||
36 | import java.util.Set; | 15 | import java.util.Set; |
37 | 16 | ||
38 | public abstract class ModelGeneratorBuilder { | 17 | public final class ModelGeneratorBuilder extends AbstractRefineryBuilder<ModelGeneratorBuilder> { |
39 | @Inject | 18 | public ModelGeneratorBuilder() { |
40 | private Provider<XtextResourceSet> resourceSetProvider; | 19 | super(Set.of(Concreteness.CANDIDATE)); |
41 | |||
42 | @Inject | ||
43 | private IResourceFactory resourceFactory; | ||
44 | |||
45 | @Inject | ||
46 | private IResourceValidator resourceValidator; | ||
47 | |||
48 | @Inject | ||
49 | private ModelInitializer initializer; | ||
50 | |||
51 | @Inject | ||
52 | private ProblemTraceImpl problemTrace; | ||
53 | |||
54 | private CancellationToken cancellationToken = CancellationToken.NONE; | ||
55 | private boolean problemLoaded; | ||
56 | private ModelQueryBuilder queryEngineBuilder; | ||
57 | private Collection<Concreteness> requiredInterpretations = Set.of(Concreteness.CANDIDATE); | ||
58 | |||
59 | public ModelGeneratorBuilder cancellationToken(CancellationToken cancellationToken) { | ||
60 | this.cancellationToken = cancellationToken; | ||
61 | return this; | ||
62 | } | ||
63 | |||
64 | public ModelGeneratorBuilder fromString(String problemString) throws IOException { | ||
65 | try (var stream = new LazyStringInputStream(problemString)) { | ||
66 | return fromStream(stream); | ||
67 | } | ||
68 | } | ||
69 | |||
70 | public ModelGeneratorBuilder fromStream(InputStream inputStream) throws IOException { | ||
71 | var resourceSet = resourceSetProvider.get(); | ||
72 | var resource = resourceFactory.createResource(URI.createFileURI("__synthetic.problem")); | ||
73 | resourceSet.getResources().add(resource); | ||
74 | resource.load(inputStream, Map.of()); | ||
75 | return fromResource(resource); | ||
76 | } | ||
77 | |||
78 | public ModelGeneratorBuilder fromFile(File file) throws IOException { | ||
79 | return fromFile(file.getAbsolutePath()); | ||
80 | } | ||
81 | |||
82 | public ModelGeneratorBuilder fromFile(String filePath) throws IOException { | ||
83 | return fromUri(URI.createFileURI(filePath)); | ||
84 | } | ||
85 | |||
86 | public ModelGeneratorBuilder fromUri(URI uri) throws IOException { | ||
87 | var resourceSet = resourceSetProvider.get(); | ||
88 | var resource = resourceFactory.createResource(uri); | ||
89 | resourceSet.getResources().add(resource); | ||
90 | resource.load(Map.of()); | ||
91 | return fromResource(resource); | ||
92 | } | ||
93 | |||
94 | public ModelGeneratorBuilder fromResource(Resource resource) { | ||
95 | var issues = resourceValidator.validate(resource, CheckMode.ALL, () -> { | ||
96 | cancellationToken.checkCancelled(); | ||
97 | return Thread.interrupted(); | ||
98 | }); | ||
99 | cancellationToken.checkCancelled(); | ||
100 | var errors = issues.stream() | ||
101 | .filter(issue -> issue.getSeverity() == Severity.ERROR) | ||
102 | .toList(); | ||
103 | if (!errors.isEmpty()) { | ||
104 | throw new ValidationErrorsException(resource.getURI(), errors); | ||
105 | } | ||
106 | if (resource.getContents().isEmpty() || !(resource.getContents().get(0) instanceof Problem problem)) { | ||
107 | throw new IllegalArgumentException("Model generation problem not found in resource " + resource.getURI()); | ||
108 | } | ||
109 | return problem(problem); | ||
110 | } | ||
111 | |||
112 | public ModelGeneratorBuilder problem(Problem problem) { | ||
113 | if (problemLoaded) { | ||
114 | throw new IllegalStateException("Problem was already set"); | ||
115 | } | ||
116 | initializer.readProblem(problem); | ||
117 | problemTrace.setInitializer(initializer); | ||
118 | problemLoaded = true; | ||
119 | return this; | ||
120 | } | ||
121 | |||
122 | public ProblemTrace getProblemTrace() { | ||
123 | checkProblem(); | ||
124 | return problemTrace; | ||
125 | } | ||
126 | |||
127 | public ModelGeneratorBuilder queryEngine(ModelQueryBuilder queryEngineBuilder) { | ||
128 | if (this.queryEngineBuilder != null) { | ||
129 | throw new IllegalStateException("Query engine was already set"); | ||
130 | } | ||
131 | this.queryEngineBuilder = queryEngineBuilder; | ||
132 | return this; | ||
133 | } | 20 | } |
134 | 21 | ||
135 | public ModelGeneratorBuilder requiredInterpretations(Collection<Concreteness> requiredInterpretations) { | 22 | @Override |
136 | this.requiredInterpretations = requiredInterpretations; | 23 | protected ModelGeneratorBuilder self() { |
137 | return this; | 24 | return this; |
138 | } | 25 | } |
139 | 26 | ||
@@ -149,19 +36,6 @@ public abstract class ModelGeneratorBuilder { | |||
149 | .requiredInterpretations(requiredInterpretations)); | 36 | .requiredInterpretations(requiredInterpretations)); |
150 | initializer.configureStoreBuilder(storeBuilder); | 37 | initializer.configureStoreBuilder(storeBuilder); |
151 | var store = storeBuilder.build(); | 38 | var store = storeBuilder.build(); |
152 | return new ModelGenerator(problemTrace, store, initializer.getModelSeed()); | 39 | return new ModelGenerator(getProblemTrace(), store, initializer.getModelSeed()); |
153 | } | ||
154 | |||
155 | private void checkProblem() { | ||
156 | if (!problemLoaded) { | ||
157 | throw new IllegalStateException("Problem was not loaded"); | ||
158 | } | ||
159 | } | ||
160 | |||
161 | private ModelQueryBuilder getQueryEngineBuilder() { | ||
162 | if (queryEngineBuilder == null) { | ||
163 | return QueryInterpreterAdapter.builder(); | ||
164 | } | ||
165 | return queryEngineBuilder; | ||
166 | } | 40 | } |
167 | } | 41 | } |
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java new file mode 100644 index 00000000..8bac1910 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemantics.java | |||
@@ -0,0 +1,42 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import org.eclipse.xtext.naming.QualifiedName; | ||
9 | import tools.refinery.language.model.problem.Relation; | ||
10 | import tools.refinery.store.model.ModelStore; | ||
11 | import tools.refinery.store.reasoning.interpretation.PartialInterpretation; | ||
12 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
13 | import tools.refinery.store.reasoning.representation.PartialSymbol; | ||
14 | import tools.refinery.store.reasoning.seed.ModelSeed; | ||
15 | import tools.refinery.store.representation.TruthValue; | ||
16 | |||
17 | public class ModelSemantics extends AbstractRefinery { | ||
18 | public ModelSemantics(ProblemTrace problemTrace, ModelStore store, ModelSeed modelSeed) { | ||
19 | super(problemTrace, store, modelSeed); | ||
20 | } | ||
21 | |||
22 | public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) { | ||
23 | return reasoningAdapter.getPartialInterpretation(Concreteness.PARTIAL, partialSymbol); | ||
24 | } | ||
25 | |||
26 | public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(Relation relation) { | ||
27 | return getPartialInterpretation(problemTrace.getPartialRelation(relation)); | ||
28 | } | ||
29 | |||
30 | public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(QualifiedName qualifiedName) { | ||
31 | return getPartialInterpretation(problemTrace.getPartialRelation(qualifiedName)); | ||
32 | } | ||
33 | |||
34 | public PartialInterpretation<TruthValue, Boolean> getPartialInterpretation(String qualifiedName) { | ||
35 | return getPartialInterpretation(problemTrace.getPartialRelation(qualifiedName)); | ||
36 | } | ||
37 | |||
38 | public static ModelSemanticsBuilder standaloneBuilder() { | ||
39 | var injector = StandaloneInjectorHolder.getInjector(); | ||
40 | return injector.getInstance(ModelSemanticsBuilder.class); | ||
41 | } | ||
42 | } | ||
diff --git a/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java new file mode 100644 index 00000000..a560ebe4 --- /dev/null +++ b/subprojects/generator/src/main/java/tools/refinery/generator/ModelSemanticsBuilder.java | |||
@@ -0,0 +1,37 @@ | |||
1 | /* | ||
2 | * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/> | ||
3 | * | ||
4 | * SPDX-License-Identifier: EPL-2.0 | ||
5 | */ | ||
6 | package tools.refinery.generator; | ||
7 | |||
8 | import tools.refinery.store.dse.propagation.PropagationAdapter; | ||
9 | import tools.refinery.store.model.ModelStore; | ||
10 | import tools.refinery.store.reasoning.ReasoningAdapter; | ||
11 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
12 | |||
13 | import java.util.Set; | ||
14 | |||
15 | public final class ModelSemanticsBuilder extends AbstractRefineryBuilder<ModelSemanticsBuilder> { | ||
16 | public ModelSemanticsBuilder() { | ||
17 | super(Set.of(Concreteness.PARTIAL)); | ||
18 | } | ||
19 | |||
20 | @Override | ||
21 | protected ModelSemanticsBuilder self() { | ||
22 | return this; | ||
23 | } | ||
24 | |||
25 | public ModelSemantics build() { | ||
26 | checkProblem(); | ||
27 | var storeBuilder = ModelStore.builder() | ||
28 | .cancellationToken(cancellationToken) | ||
29 | .with(getQueryEngineBuilder()) | ||
30 | .with(PropagationAdapter.builder()) | ||
31 | .with(ReasoningAdapter.builder() | ||
32 | .requiredInterpretations(requiredInterpretations)); | ||
33 | initializer.configureStoreBuilder(storeBuilder); | ||
34 | var store = storeBuilder.build(); | ||
35 | return new ModelSemantics(getProblemTrace(), store, initializer.getModelSeed()); | ||
36 | } | ||
37 | } | ||