From dc93c0c699b24ea8f43f6c8a6c0852f5780da0c8 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Sun, 2 Jul 2017 23:34:52 +0200 Subject: SMT solver implementation of multiple model generation --- .../src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SMTSolver.xtend | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'Solvers/SMT-Solver') 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{ } else throw new IllegalArgumentException('''The configuration have to be an «SmtSolverConfiguration.simpleName»!''') } - override getInterpretation(ModelResult modelResult) { - val representation = modelResult.representation as SMTDocument + override getInterpretations(ModelResult modelResult) { + val representation = modelResult.representation.head as SMTDocument val trace = modelResult.trace as Logic2SmtMapperTrace - return new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace) + return #[new SmtModelInterpretation(trace.problem,representation,trace.forwardMapper,trace)] } } \ No newline at end of file -- cgit v1.2.3-54-g00ecf