From 52a015c1558b9ce5fb10f27d41e508dfec1e79d6 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 25 Jul 2019 19:03:01 +0200 Subject: Make polyhedron solvers more robust --- .../AbstractPolyhedronSaturationOperator.xtend | 53 ++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend new file mode 100644 index 00000000..94f97e94 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/AbstractPolyhedronSaturationOperator.xtend @@ -0,0 +1,53 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import org.eclipse.xtend.lib.annotations.Accessors + +abstract class AbstractPolyhedronSaturationOperator implements PolyhedronSaturationOperator { + @Accessors val Polyhedron polyhedron + + new(Polyhedron polyhedron) { + if (polyhedron.dimensions.empty) { + throw new IllegalArgumentException("Polyhedron must have at least one dimension.") + } + this.polyhedron = polyhedron + } + + override saturate() { + if (polyhedron.expressionsToSaturate.empty) { + return PolyhedronSaturationResult.SATURATED + } + for (constraint : polyhedron.constraints) { + if (constraint.zero) { + if (constraint.lowerBound !== null && constraint.lowerBound > 0) { + return PolyhedronSaturationResult.EMPTY + } + if (constraint.upperBound !== null && constraint.upperBound < 0) { + return PolyhedronSaturationResult.EMPTY + } + } else { + if (constraint.lowerBound !== null && constraint.upperBound !== null && + constraint.upperBound < constraint.lowerBound) { + return PolyhedronSaturationResult.EMPTY + } + } + } + doSaturate() + } + + protected def PolyhedronSaturationResult doSaturate() + + protected def getNonTrivialConstraints() { + ImmutableList.copyOf(polyhedron.constraints.filter [ constraint | + (constraint.lowerBound !== null || constraint.upperBound !== null) && !constraint.zero + ]) + } + + private static def isZero(LinearConstraint constraint) { + constraint.coefficients.values.forall[it == 0] + } + + override close() throws Exception { + // Nothing to close by default. + } +} -- cgit v1.2.3-54-g00ecf