Commit 6f2cb47f authored by eder's avatar eder
Browse files

removing of basic (smt) constraints after solving problem

Issue-Ref: 3641
Issue-Url: https://af3-developer.fortiss.org/issues/3641

Signed-off-by: default avatareder <eder@192.168.17.140>
parent 17bf7348
......@@ -67,6 +67,7 @@ public class Z3Backend implements IDSEBackend {
throw new Exception("No exploration targets defined. Cannot perform DSE.");
}
List<SMTConstraint> basicCons = createBasicSignalConstraints(spec.getSearchSpace());
SolverRun solverRun;
if(solutionTypes.contains(Schedule.class) &&
solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
......@@ -76,7 +77,6 @@ public class Z3Backend implements IDSEBackend {
solverRun = new DeploScheduleRun();
} else if(solutionTypes.contains(TaskToExecutionUnitAllocationTable.class)) {
// Add SMT-specific constraints to define the basic deployment problem.
List<SMTConstraint> basicCons = createBasicSignalConstraints(spec.getSearchSpace());
insertBasicConstraints(spec, basicCons);
if(isDebugVerboseEnabled()) {
System.out.println("DeploymentRun");
......@@ -90,6 +90,8 @@ public class Z3Backend implements IDSEBackend {
}
ExplorationSolution expSolution = solverRun.solve(spec, timeoutMS, monitor);
// remove basic constraints
spec.getTargets().removeAll(basicCons);
return Optional.of(expSolution);
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment