Skip to content
GitLab
Commit d17d364d authored by Simon Barner's avatar Simon Barner
Browse files

Merge branch 'master' of https://git.fortiss.org/af3/af3.git into 4048

parents 618a054b 99ee765f
Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/.ratings
View file @ d17d364d
AF3ExplorationSMTActivator.java 499ee7e7485e622615a4f78be5d2e4f1ca8f235a GREEN
AF3ExplorationSMTActivator.java db8c07de55429ead58b5127affc48232e31819d3 YELLOW
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/AF3ExplorationSMTActivator.java
View file @ d17d364d
......@@ -16,6 +16,8 @@
package org.fortiss.af3.exploration.smt;
import org.eclipse.core.runtime.Plugin;
import org.fortiss.af3.exploration.smt.cli.DumpSMTLibFileCommandLineHandler;
import org.fortiss.tooling.kernel.service.ICommandLineInterfaceService;
import org.osgi.framework.BundleContext;
/**
......@@ -36,6 +38,9 @@ public class AF3ExplorationSMTActivator extends Plugin {
public void start(BundleContext context) throws Exception {
super.start(context);
plugin = this;
ICommandLineInterfaceService cliService = ICommandLineInterfaceService.getInstance();
cliService.registerHandler("--dump-smtlib", new DumpSMTLibFileCommandLineHandler());
}
/** {@inheritDoc} */
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/.ratings
View file @ d17d364d
Z3Backend.java 1ba4698b984ea240a0143cd49730ed929607d365 GREEN
Z3Backend.java c217750b1183c51c4f4952919d70e22b2576d7fa GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/backend/Z3Backend.java
View file @ d17d364d
......@@ -86,21 +86,8 @@ public class Z3Backend implements IDSEBackend {
@Override
public Optional<ExplorationSolution> executeDSE(ExplorationSpecification spec,
SolverSettings settings, IProgressMonitor monitor) throws Exception {
SolverRun solverRun;
int timeout = settings.getTermination().getTimeoutMS().getValue();
Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
if(synthTypes.contains(IDeploymentSynthesis.class) &&
synthTypes.contains(IScheduleSynthesis.class)) {
solverRun = new DeploScheduleRun(spec, timeout);
} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
solverRun = new DeploymentRun(spec, timeout);
} else if(synthTypes.contains(IScheduleSynthesis.class)) {
solverRun = new ScheduleRun(spec, timeout);
} else {
throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
" was found for the given set of syntesises to perform.");
}
SolverRun solverRun = createSolverRun(spec, timeout);
if(isDebugVerboseEnabled()) {
// prints on screen the list of constraints for this run
......@@ -117,6 +104,25 @@ public class Z3Backend implements IDSEBackend {
return Optional.of(expSolution);
}
/**
* Creates a {@link SolverRun} instance that is specific for the {@link ISynthesisCategory}s of
* the given {@link ExplorationSpecification}.
*/
public SolverRun createSolverRun(ExplorationSpecification spec, int timeout) throws Exception {
Collection<Class<? extends ISynthesisCategory>> synthTypes = spec.getSynthTypes();
if(synthTypes.contains(IDeploymentSynthesis.class) &&
synthTypes.contains(IScheduleSynthesis.class)) {
return new DeploScheduleRun(spec, timeout);
} else if(synthTypes.contains(IDeploymentSynthesis.class)) {
return new DeploymentRun(spec, timeout);
} else if(synthTypes.contains(IScheduleSynthesis.class)) {
return new ScheduleRun(spec, timeout);
} else {
throw new Exception("No applicable " + SolverRun.class.getSimpleName() +
" was found for the given set of syntesises to perform.");
}
}
/** {@inheritDoc} */
@Override
public String getName() {
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/cli/.ratings 0 → 100644
View file @ d17d364d
DumpSMTLibFileCommandLineHandler.java 95604962b4db14786ec8143663278c4a865bbd55 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/cli/DumpSMTLibFileCommandLineHandler.java 0 → 100644
View file @ d17d364d
/*-------------------------------------------------------------------------+
| Copyright 2020 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.cli;
import static org.fortiss.af3.exploration.service.IDSEBackend.EXPLORATION_TYPE.FEASIBILITY_CHECK;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.findMatchingDSEProject;
import static org.fortiss.af3.exploration.util.ExplorationCLIUtils.getExplorationTypeByArgument;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationSpecification;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getFirstParentWithType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.info;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import org.fortiss.af3.exploration.AF3ExplorationActivator;
import org.fortiss.af3.exploration.model.ExplorationSpecification;
import org.fortiss.af3.exploration.model.IExplorationConstraint;
import org.fortiss.af3.exploration.model.IExplorationObjective;
import org.fortiss.af3.exploration.model.IExplorationTarget;
import org.fortiss.af3.exploration.model.SolverSettings;
import org.fortiss.af3.exploration.model.project.DSE;
import org.fortiss.af3.exploration.model.project.ProcessStep;
import org.fortiss.af3.exploration.model.project.RuleSet;
import org.fortiss.af3.exploration.model.synthesiscategory.ISynthesisCategory;
import org.fortiss.af3.exploration.service.IDSEBackend;
import org.fortiss.af3.exploration.service.IDSEBackendService;
import org.fortiss.af3.exploration.smt.AF3ExplorationSMTActivator;
import org.fortiss.af3.exploration.smt.backend.Z3Backend;
import org.fortiss.af3.exploration.smt.solver.SolverRun;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.tooling.kernel.extension.ICommandLineSwitchHandler;
import com.microsoft.z3.Solver;
/**
* Handler to dump a SMT-Lib description of and exploration problem defined in a {@link DSE}
* project. To construct the {@link ExplorationSpecification} that is optimized, all defined
* {@link IExplorationConstraint}s matching the synthesis type are used.
* This handler supports only the generation of feasibility checks. It is intended to be used with
* solvers that support the SMT-Lib standard 2.5 such as CVC4.
*
* @author diewald
*/
public final class DumpSMTLibFileCommandLineHandler implements ICommandLineSwitchHandler {
/** DSE service used for the exploration. */
private final IDSEBackendService dseService = IDSEBackendService.getInstance();
/** {@inheritDoc} */
@Override
public boolean hasAdditionalArgument() {
return true;
}
/** {@inheritDoc} */
@Override
public void handleCLISwitch(String argument) {
DSE matchingDSE = findMatchingDSEProject(argument);
if(matchingDSE == null) {
return;
}
Set<Class<? extends ISynthesisCategory>> solutionType =
getExplorationTypeByArgument(argument);
if(solutionType.isEmpty()) {
return;
}
// Get & set the Z3 solver.
Optional<IDSEBackend> optBackend = getFirst(
dseService.findBySynthTypeAndName(solutionType, FEASIBILITY_CHECK, "Z3 (SMT)"));
if(!optBackend.isPresent()) {
error(AF3ExplorationActivator.getDefault(),
"Could not find the Z3 backend to perform the exploration.");
return;
}
Z3Backend z3Backend = (Z3Backend)optBackend.get();
Map<IDSEBackend, SolverSettings> settings = new HashMap<>();
settings.put(z3Backend, z3Backend.getSolverSettings());
ExplorationSpecification expSpec = constructExplorationSpecification(matchingDSE);
expSpec.getSynthTypes().addAll(solutionType);
SolverRun solverRun;
try {
solverRun = z3Backend.createSolverRun(expSpec, 1000);
} catch(Exception e) {
error(AF3ExplorationActivator.getDefault(),
"Could not create a solver run instance for the given synthesis type.", e);
return;
}
int numExplorationObjectives =
pickInstanceOf(IExplorationObjective.class, expSpec.getTargets()).size();
if(numExplorationObjectives > 0) {
info(AF3ExplorationSMTActivator.getDefault(),
"Optimization statements will not be " +
"dumped. This switch is only inteded to check feasibility of an " +
"optimization problem. For debugging optimization problems, set " +
"the environment varaible DSE_DEBUG_VERBOSE to \"true\".");
}
Solver solver = solverRun.createConstraintSolver();
String smtLibStr = "(set-logic ALL)\n" + "(check-sat)\n" + solver.toString();
String af3PrjName = getFirstParentWithType(matchingDSE, FileProject.class).getName();
solverRun.dumpSMTLibFile(smtLibStr, af3PrjName);
}
/**
* Constructs an {@link ExplorationSpecification} using all {@link IExplorationTarget}s from the
* given {@link DSE}.
*/
private ExplorationSpecification constructExplorationSpecification(DSE matchingDSE) {
ExplorationSpecification expSpec = createExplorationSpecification();
ProcessStep dseStep = matchingDSE.getCurrentStep();
expSpec.getTargets().addAll(getTargetsFromRuleSets(matchingDSE));
expSpec.setSearchSpace(dseStep.getSuperSetMap());
return expSpec;
}
/** Collects all targets referenced by {@link RuleSet}s of the given {@link DSE}. */
private static Collection<IExplorationTarget<?>> getTargetsFromRuleSets(DSE dse) {
Collection<IExplorationTarget<?>> allExplorationTargets = new ArrayList<>();
ProcessStep dseStep = dse.getCurrentStep();
for(RuleSet ruleSet : dseStep.getRuleSets()) {
allExplorationTargets = ruleSet.getExplorationTargets();
}
return allExplorationTargets;
}
}
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/.ratings
View file @ d17d364d
......@@ -3,7 +3,7 @@ BasicDeploymentConstraint.java 06515032af8bac566160d16c14fff0d44365b0d2 GREEN
BasicScheduleConstraint.java f8f5b991f1cc90ec129ef33b5575c68e49b08a7b GREEN
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 642825f94e172094f7412e9e3e8f7f35414c8228 GREEN
DSMLtoSMTTransformator.java 29663e8526f5c7d3acd85eab4f5609b9f0fcba54 GREEN
DSMLtoSMTTransformator.java 5de3aed222e049b2990308a1294b468cef6e35bf GREEN
DefaultExpressionTransformator.java b890bc609fe9cc45c0af88524ae83cf367ccaee4 GREEN
EnergyConstraintDefinition.java f394e4195ed678ae294b48dbe3c39c783f9c927d GREEN
ExpressionTransformator.java 81dfc30221e519aa8175693353ace8992687327f GREEN
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/modeltransformation/DSMLtoSMTTransformator.java
View file @ d17d364d
......@@ -15,6 +15,7 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.modeltransformation;
import static com.microsoft.z3.Z3javaAPIWrapper.createBoolConst;
import static com.microsoft.z3.Z3javaAPIWrapper.createEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createInteger;
import static com.microsoft.z3.Z3javaAPIWrapper.createReal;
......@@ -48,6 +49,7 @@ import java.util.Optional;
import javax.activation.UnsupportedDataTypeException;
import org.apache.commons.lang3.tuple.Pair;
import org.eclipse.emf.common.util.BasicEList;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.allocation.model.AllocationEntry;
......@@ -111,35 +113,37 @@ public class DSMLtoSMTTransformator {
* Caches all Z3 expressions that have ever been constructed from {@link IExplorationTarget}s by
* this {@link DSMLtoSMTTransformator}.
*/
private BiMap<IExplorationTarget<?>, Expr> expressionCache = HashBiMap.create();
private final BiMap<IExplorationTarget<?>, Expr> expressionCache = HashBiMap.create();
/**
* Map of transformed {@link IExplorationTarget}s from the latest
* {@link #transform(ExplorationSpecification)} call.
*/
private BiMap<IExplorationTarget<?>, Expr> transformedExpressions = HashBiMap.create();
private final BiMap<IExplorationTarget<?>, Expr> transformedExpressions = HashBiMap.create();
/**
* Remembers the {@link Expr}s constructed from {@link IModelElement} properties during the
* latest {@link #transform(ExplorationSpecification)} call.
*/
private Collection<Expr> elementPropertyExpressions = new ArrayList<>();
private final Collection<Expr> elementPropertyExpressions = new ArrayList<>();
/** Constraints which shall be tracked. */
private List<BoolExpr> constraintsToTrack;
private final Map<BoolExpr, Pair<BoolExpr, IExplorationConstraint<?>>> constraintsToTrack =
new HashMap<>();
/** Minimization expressions. */
private List<ArithExpr> toMinimize;
private final List<ArithExpr> toMinimize = new ArrayList<>();
/** Maximization expressions. */
private List<ArithExpr> toMaximize;
private final List<ArithExpr> toMaximize = new ArrayList<>();
/** Predicate to generate {@link Expr}s used for tracking UNSAT cores. */
private final boolean trackConstraints;
/** Constructor. */
public DSMLtoSMTTransformator(Context context) {
public DSMLtoSMTTransformator(Context context, boolean trackConstraints) {
this.context = context;
constraintsToTrack = new ArrayList<>();
toMaximize = new ArrayList<>();
toMinimize = new ArrayList<>();
this.trackConstraints = trackConstraints;
}
/** Transforms the given {@link RuleSet}s into {@link BoolExpr}. */
......@@ -166,15 +170,13 @@ public class DSMLtoSMTTransformator {
if(explorationTgt instanceof IExplorationConstraint) {
IExplorationConstraint<?> smtConstraint =
(IExplorationConstraint<?>)explorationTgt;
Expr smtExpr = extractSMTExpr(smtConstraint);
addExpression(smtExpr, explorationTgt);
extractSMTExpr(smtConstraint);
} else if(explorationTgt instanceof IExplorationObjective) {
IExplorationObjective<?> smtObjective =
(IExplorationObjective<?>)explorationTgt;
for(IExplorationConstraint<?> constraint : smtObjective
.getImplicitConstraints()) {
Expr smtExpr = extractSMTExpr(constraint);
addExpression(smtExpr, constraint);
extractSMTExpr(constraint);
}
IExpression expression = smtObjective.getExpression();
......@@ -206,6 +208,7 @@ public class DSMLtoSMTTransformator {
error(getDefault(), e.getMessage());
}
}
return true;
}
......@@ -242,9 +245,13 @@ public class DSMLtoSMTTransformator {
Expr smt = constraintTransformationAdapter.transform(constraint.getExpression(),
new HashMap<Set<IModelElement>, IModelElement>());
if(!constraint.isImplicit()) {
constraintsToTrack.add((BoolExpr)smt);
if(trackConstraints && !constraint.isImplicit()) {
BoolExpr trackExpr = createBoolConst(getContext(), "tracking_" + smt.getId());
constraintsToTrack.put((BoolExpr)smt, Pair.of(trackExpr, constraint));
}
addExpression(smt, constraint);
return smt;
}
......@@ -482,7 +489,7 @@ public class DSMLtoSMTTransformator {
}
/** The constraints which shall be tracked in order to be used for unsat cores. */
public List<BoolExpr> getConstraintToTrack() {
public Map<BoolExpr, Pair<BoolExpr, IExplorationConstraint<?>>> getConstraintToTrack() {
return constraintsToTrack;
}
......
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/.ratings
View file @ d17d364d
DeploScheduleRun.java 80cdbab8a15e29af0cbf545f38e0da4e1d705e43 GREEN
DeploymentRun.java f5bf9f64d22962dae8150e306b6e574efdf5164d GREEN
ScheduleRun.java 614e816019684359a0b31411aaca2e62aff35891 GREEN
SolverRun.java 02add460f3bbf15e53ca7a80f2a0f820a39dce9b GREEN
SolverRun.java 5068ae0c9d2083bcfcd10740781faa47928e9ca8 GREEN
org.fortiss.af3.exploration.smt/src/org/fortiss/af3/exploration/smt/solver/SolverRun.java
View file @ d17d364d
......@@ -15,11 +15,11 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.solver;
import static com.microsoft.z3.Z3javaAPIWrapper.createBoolConst;
import static com.microsoft.z3.Z3javaAPIWrapper.createOptimize;
import static java.io.File.separator;
import static java.lang.System.currentTimeMillis;
import static java.util.stream.Collectors.toMap;
import static org.eclipse.core.runtime.Assert.isTrue;
import static org.eclipse.core.runtime.Platform.getLocation;
import static org.fortiss.af3.exploration.model.solutions.SolutionState.OPTIMAL;
import static org.fortiss.af3.exploration.model.solutions.SolutionState.OPTIMIZED;
import static org.fortiss.af3.exploration.model.solutions.SolutionState.UNKNOWN;
......@@ -30,6 +30,7 @@ import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.cr
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createExplorationSolution;
import static org.fortiss.af3.exploration.util.ExplorationModelElementFactory.createSingleExplorationSolution;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import static org.fortiss.af3.project.utils.FileUtils.getDefaultGeneralProjectPath;
import static org.fortiss.tooling.base.utils.BaseMathUtils.convertNumber;
import static org.fortiss.tooling.base.utils.BaseMathUtils.isFloatNumber;
import static org.fortiss.tooling.base.utils.BaseMathUtils.isIntegerNumber;
......@@ -40,20 +41,18 @@ import static org.fortiss.tooling.kernel.utils.LoggingUtils.info;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.warning;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.Collection;
import java.util.Date;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import javax.activation.UnsupportedDataTypeException;
import org.apache.commons.lang3.tuple.Pair;
import org.eclipse.core.runtime.Assert;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.jobs.Job;
......@@ -71,6 +70,7 @@ import org.fortiss.af3.exploration.smt.modeltransformation.DSMLtoSMTTransformato
import org.fortiss.af3.exploration.util.ExplorationUtils;
import org.fortiss.tooling.base.model.element.IModelElement;
import com.ibm.icu.text.SimpleDateFormat;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
......@@ -104,7 +104,7 @@ public abstract class SolverRun {
* References the {@link DSMLtoSMTTransformator} that holds the solver-internal problem
* description.
*/
protected DSMLtoSMTTransformator transformation;
protected DSMLtoSMTTransformator transformator;
/** Constructor. */
public SolverRun(ExplorationSpecification expSpec, int timeoutMS,
......@@ -120,8 +120,8 @@ public abstract class SolverRun {
expSpec.getTargets().addAll(0, basicConstraints);
parameters.put("timeout", timeoutMS + "");
transformation = new DSMLtoSMTTransformator(new Context(parameters));
transformation.transform(expSpec);
transformator = new DSMLtoSMTTransformator(new Context(parameters), false);
transformator.transform(expSpec);
}
/** Constructor. */
......@@ -129,7 +129,7 @@ public abstract class SolverRun {
final String solutionNamePrefix) throws Exception {
this.expSpec = expSpec;
this.solutionNamePrefix = solutionNamePrefix;
this.transformation = transformation;
this.transformator = transformation;
if(isDebugVerboseEnabled()) {
System.out.println(solutionNamePrefix + "Run");
......@@ -164,20 +164,20 @@ public abstract class SolverRun {
}
if(numExplorationObjectives == 0) {
if(!solveNonOptimized(parameters, transformation, expSolution, monitor)) {
if(!solveNonOptimized(parameters, transformator, expSolution, monitor)) {
return expSolution;
}
} else if(!solveOptimized(numberOfRuns, transformation, expSolution, monitor)) {
} else if(!solveOptimized(numberOfRuns, transformator, expSolution, monitor)) {
return expSolution;
}
if(expSolution.getSolutionState() == UNSAT) {
// Problem is not solvable: Dump UnSAT core for user aid.
parameters.put("unsat_core", "true");
try(Context context2 = new Context(parameters)) {
transformation = new DSMLtoSMTTransformator(context2);
transformation.transform(expSpec);
solveNonOptimized(parameters, transformation, expSolution, monitor);
try(Context trackingCtx = new Context(parameters)) {
transformator = new DSMLtoSMTTransformator(trackingCtx, true);
transformator.transform(expSpec);
solveNonOptimized(parameters, transformator, expSolution, monitor);
}
}
} catch(Z3Exception e) {
......@@ -195,17 +195,17 @@ public abstract class SolverRun {
* the given {@link ExplorationSolution}.
*/
private void extractFailedConstraints(BoolExpr[] unsatCores, ExplorationSolution expSolution,
Map<Expr, IExplorationConstraint<?>> constraintMapping) {
Map<BoolExpr, Pair<BoolExpr, IExplorationConstraint<?>>> trackingConstraints) {
Map<Expr, IExplorationConstraint<?>> trackingExpressions =
trackingConstraints.values().stream().collect(toMap(Pair::getLeft, Pair::getRight));
Set<IExplorationConstraint<?>> seenConstraints = new HashSet<>();
Collection<IExplorationConstraint<?>> infeasConstraints = expSolution.getUnsatConstraints();
for(BoolExpr boolExpr : unsatCores) {
IExplorationConstraint<?> constraint = constraintMapping.get(boolExpr);
IExplorationConstraint<?> constraint = trackingExpressions.get(boolExpr);
if(constraint != null) {
String actionMsg;
if(!seenConstraints.contains(constraint)) {
expSolution.getUnsatConstraints().add(constraint);
seenConstraints.add(constraint);
if(!infeasConstraints.contains(constraint)) {
infeasConstraints.add(constraint);
actionMsg = "extracted";
} else {
actionMsg = "skipped (already seen)";
......@@ -281,21 +281,7 @@ public abstract class SolverRun {
private boolean solveOptimized(int numberOfRuns, DSMLtoSMTTransformator transformation,
ExplorationSolution expSolution, IProgressMonitor monitor) throws Z3Exception {
// Parameters for optimizing solver.
Optimize solver = createOptimize(transformation.getContext());
for(ArithExpr a : transformation.getToMinimize()) {
solver.MkMinimize(a);
}
for(ArithExpr a : transformation.getToMaximize()) {
solver.MkMaximize(a);
}
if(isDebugVerboseEnabled()) {
printToFile(solver.toString());
}
// Constraints
Collection<BoolExpr> z3Constraints =
filterByType(transformation.getConstraints(), BoolExpr.class);
solver.Add(z3Constraints.toArray(new BoolExpr[0]));
Optimize solver = createZ3Optimizer();
logZ3info(("\n SMT Problem: \n" + (solver.toString())));
Map<Expr, IExplorationObjective<?>> objectiveMapping = transformation.getObjectiveMapping();
......@@ -368,6 +354,27 @@ public abstract class SolverRun {
return true;
}
/** Creates a Z3 {@link Optimize} instance. */
public Optimize createZ3Optimizer() {
Optimize solver = createOptimize(transformator.getContext());
for(ArithExpr a : transformator.getToMinimize()) {
solver.MkMinimize(a);
}
for(ArithExpr a : transformator.getToMaximize()) {
solver.MkMaximize(a);
}
if(isDebugVerboseEnabled()) {
dumpSMTLibFile(solver.toString(), "SMT_DEBUG");
}
// Add Constraints
Collection<BoolExpr> z3Constraints =
filterByType(transformator.getConstraints(), BoolExpr.class);
solver.Add(z3Constraints.toArray(new BoolExpr[0]));
return solver;
}
/**
* Updates the overall status of the {@link ExplorationSolution} based its own state and the
* ones
......@@ -404,33 +411,11 @@ public abstract class SolverRun {
IProgressMonitor monitor) throws Z3Exception {
boolean dumpUnsatCores = "true".equals(parameters.get("unsat_core"));
// non optimizing smt solver
Solver solver = transformation.getContext().mkSolver();
Solver solver = createConstraintSolver();
logZ3info("Parameters: " + solver.getParameterDescriptions());
final Collection<BoolExpr> constraints =
filterByType(transformation.getConstraints(), BoolExpr.class);
Map<Expr, IExplorationConstraint<?>> constraintMapping = null;
if(dumpUnsatCores) {
constraintMapping = transformation.getConstraintMapping();