Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41

package hu.bme.mit.inf.dslreasoner.viatra2logic;

import java.io.IOException;
import java.util.List;
import java.util.Map;

import org.eclipse.xtext.common.types.JvmIdentifiableElement;
import org.eclipse.xtext.xbase.XExpression;

import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement;

public class NumericDynamicProblemSolver extends NumericProblemSolver{
	
//	private NumericZ3ProblemSolver z3Solver;
	private NumericDrealProblemSolver drealSolver;
	
	public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException {
//		this.z3Solver = new NumericZ3ProblemSolver();
		this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout);
	}
	
	public NumericProblemSolver selectSolver(String selection) {
		switch (selection) {
		case "z3":
			return new NumericZ3ProblemSolver();
		case "dreal":
			return this.drealSolver;
		default:
		throw new IllegalArgumentException("Unknown numeric solver selection: " + selection);
		}
	}

	public boolean isSatisfiable(Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches)
			throws Exception {
		throw new Exception("Should not reach here - isSatisfiable");
	}

	public Map<PrimitiveElement, Number> getOneSolution(List<PrimitiveElement> objs,
			Map<XExpression, Iterable<Map<JvmIdentifiableElement, PrimitiveElement>>> matches) throws Exception {
		throw new Exception("Should not reach here - getOneSolution");
	}}