diff options
| author |  OszkarSemerath <oszka@152.66.252.189> | 2017-07-02 23:34:52 +0200 |
|---|---|---|
| committer | OszkarSemerath <oszka@152.66.252.189> | 2017-07-02 23:34:52 +0200 |
| commit | dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8 (patch) | |
| tree | e54329cdb816f2841356936f29f80501e738bb8b /Solvers/SMT-Solver | |
| parent | Alloy implementation of multiple model generation (diff) | |
| download | VIATRA-Generator-dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8.tar.gz VIATRA-Generator-dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8.tar.zst VIATRA-Generator-dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8.zip | |
SMT solver implementation of multiple model generation
Diffstat (limited to 'Solvers/SMT-Solver')
| -rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend index d371b89e..4e2e1890 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | |||
| @@ -41,9 +41,9 @@ class SMTSolver extends LogicReasoner{ | |||
| 41 | } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') | 41 | } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') |
| 42 | } | 42 | } |
| 43 | 43 | ||
| 44 | override getInterpretation(ModelResult modelResult) { | 44 | override getInterpretations(ModelResult modelResult) { |
| 45 | val representation = modelResult.representation as SMTDocument | 45 | val representation = modelResult.representation.head as SMTDocument |
| 46 | val trace = modelResult.trace as Logic2SmtMapperTrace | 46 | val trace = modelResult.trace as Logic2SmtMapperTrace |
| 47 | return new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace) | 47 | return #[new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace)] |
| 48 | } | 48 | } |
| 49 | } \ No newline at end of file | 49 | } \ No newline at end of file |