diff options
author | 2017-07-02 23:34:52 +0200 | |
---|---|---|
committer | 2017-07-02 23:34:52 +0200 | |
commit | dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8 (patch) | |
tree | e54329cdb816f2841356936f29f80501e738bb8b /Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt | |
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/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt')
-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 |