From fc505b6b171a2d54c3bad6078031b028b55131d3 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 14 Jul 2019 00:56:19 +0200 Subject: Polyhedron abstraction with Z3 for cardinality propagation --- .../cardinality/PolyhedronScopePropagator.xtend | 153 +++++++++++++++ .../cardinality/PolyhedronSolver.xtend | 115 ++++++++++++ .../logic2viatra/cardinality/ScopePropagator.xtend | 149 +++++++++++++++ .../cardinality/Z3PolyhedronSolver.xtend | 206 +++++++++++++++++++++ 4 files changed, 623 insertions(+) create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality') diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend new file mode 100644 index 00000000..8f210ffb --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronScopePropagator.xtend @@ -0,0 +1,153 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.google.common.collect.ImmutableList +import com.google.common.collect.ImmutableMap +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialPrimitiveInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import java.util.ArrayDeque +import java.util.HashMap +import java.util.HashSet +import java.util.Map +import java.util.Set + +class PolyhedronScopePropagator extends ScopePropagator { + val Map scopeBounds + val LinearConstraint topLevelBounds + val PolyhedronSaturationOperator operator + + new(PartialInterpretation p, Set possibleNewDynamicTypes, PolyhedronSolver solver) { + super(p) + val instanceCounts = possibleNewDynamicTypes.toInvertedMap[new Dimension(name, 0, null)] + val primitiveDimensions = new HashMap + val constraintsBuilder = ImmutableList.builder + val scopeBoundsBuilder = ImmutableMap.builder + // Dimensions for instantiable types were created according to the type analysis, + // but for any possible primitive types, we create them on demand, + // as there is no Type directly associated with a PartialPrimitiveInterpretation. + for (scope : p.scopes) { + switch (targetTypeInterpretation : scope.targetTypeInterpretation) { + PartialPrimitiveInterpretation: { + val dimension = primitiveDimensions.computeIfAbsent(targetTypeInterpretation) [ interpretation | + new Dimension(interpretation.eClass.name, 0, null) + ] + scopeBoundsBuilder.put(scope, dimension) + } + PartialComplexTypeInterpretation: { + val complexType = targetTypeInterpretation.interpretationOf + val dimensions = findSubtypeDimensions(complexType, instanceCounts) + switch (dimensions.size) { + case 0: + if (scope.minNewElements > 0) { + throw new IllegalArgumentException("Found scope for " + complexType.name + + ", but the type cannot be instantiated") + } + case 1: + scopeBoundsBuilder.put(scope, dimensions.head) + default: { + val constraint = new LinearConstraint(dimensions.toInvertedMap[1], null, null) + constraintsBuilder.add(constraint) + scopeBoundsBuilder.put(scope, constraint) + } + } + } + default: + throw new IllegalArgumentException("Unknown PartialTypeInterpretation: " + targetTypeInterpretation) + } + } + val allDimensions = ImmutableList.builder.addAll(instanceCounts.values).addAll(primitiveDimensions.values).build + scopeBounds = scopeBoundsBuilder.build + topLevelBounds = new LinearConstraint(allDimensions.toInvertedMap[1], null, null) + constraintsBuilder.add(topLevelBounds) + val expressionsToSaturate = ImmutableList.builder.addAll(scopeBounds.values).add(topLevelBounds).build + val polyhedron = new Polyhedron(allDimensions, constraintsBuilder.build, expressionsToSaturate) + operator = solver.createSaturationOperator(polyhedron) + } + + private def findSubtypeDimensions(Type type, Map instanceCounts) { + val subtypes = new HashSet + val dimensions = new HashSet + val stack = new ArrayDeque + stack.addLast(type) + while (!stack.empty) { + val subtype = stack.removeLast + if (subtypes.add(subtype)) { + val dimension = instanceCounts.get(subtype) + if (dimension !== null) { + dimensions.add(dimension) + } + stack.addAll(subtype.subtypes) + } + } + dimensions + } + + override void propagateAllScopeConstraints() { + populatePolyhedronFromScope() + val result = operator.saturate() + if (result == PolyhedronSaturationResult.EMPTY) { + throw new IllegalStateException("Scope bounds cannot be satisfied") + } else { + populateScopesFromPolyhedron() + if (result != PolyhedronSaturationResult.SATURATED) { + super.propagateAllScopeConstraints() + } + } + } + + private def populatePolyhedronFromScope() { + topLevelBounds.lowerBound = partialInterpretation.minNewElements + if (partialInterpretation.maxNewElements >= 0) { + topLevelBounds.upperBound = partialInterpretation.maxNewElements + } + for (pair : scopeBounds.entrySet) { + val scope = pair.key + val bounds = pair.value + bounds.lowerBound = scope.minNewElements + if (scope.maxNewElements >= 0) { + bounds.upperBound = scope.maxNewElements + } + } + } + + private def populateScopesFromPolyhedron() { + checkFiniteBounds(topLevelBounds) + if (partialInterpretation.minNewElements > topLevelBounds.lowerBound) { + throw new IllegalArgumentException('''Lower bound of «topLevelBounds» smaller than top-level scope: «partialInterpretation.minNewElements»''') + } else if (partialInterpretation.minNewElements != topLevelBounds.lowerBound) { + partialInterpretation.minNewElements = topLevelBounds.lowerBound + } + if (partialInterpretation.maxNewElements >= 0 && + partialInterpretation.maxNewElements < topLevelBounds.upperBound) { + throw new IllegalArgumentException('''Upper bound of «topLevelBounds» larger than top-level scope: «partialInterpretation.maxNewElements»''') + } else if (partialInterpretation.maxNewElements != topLevelBounds.upperBound) { + partialInterpretation.maxNewElements = topLevelBounds.upperBound + } + for (pair : scopeBounds.entrySet) { + val scope = pair.key + val bounds = pair.value + checkFiniteBounds(bounds) + if (scope.minNewElements > bounds.lowerBound) { + throw new IllegalArgumentException('''Lower bound of «bounds» smaller than «scope.targetTypeInterpretation» scope: «scope.minNewElements»''') + } else if (scope.minNewElements != bounds.lowerBound) { + scope.minNewElements = bounds.lowerBound + } + if (scope.maxNewElements >= 0 && scope.maxNewElements < bounds.upperBound) { + throw new IllegalArgumentException('''Upper bound of «bounds» larger than «scope.targetTypeInterpretation» scope: «scope.maxNewElements»''') + } else if (scope.maxNewElements != bounds.upperBound) { + scope.maxNewElements = bounds.upperBound + } + } + } + + private def checkFiniteBounds(LinearBoundedExpression bounds) { + if (bounds.lowerBound === null) { + throw new IllegalArgumentException("Infinite lower bound: " + bounds) + } + if (bounds.upperBound === null) { + throw new IllegalArgumentException("Infinite upper bound: " + bounds) + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend new file mode 100644 index 00000000..08bf25b9 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/PolyhedronSolver.xtend @@ -0,0 +1,115 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import java.util.List +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +interface PolyhedronSolver { + def PolyhedronSaturationOperator createSaturationOperator(Polyhedron polyhedron) +} + +enum PolyhedronSaturationResult { + SATURATED, + EMPTY, + UNKNOWN +} + +interface PolyhedronSaturationOperator extends AutoCloseable { + def Polyhedron getPolyhedron() + + def PolyhedronSaturationResult saturate() +} + +@FinalFieldsConstructor +@Accessors +class Polyhedron { + /** + * The list of dimensions (variables) for this polyhedron. + * + * This list must not be modified after the polyhedron was created. + * However, lower and upper bounds of the dimensions may be changed. + * + * Names of dimensions in this list are assumed to be unique. + */ + val List dimensions + + /** + * The list of constraints defining this polyhedron. + * + * The list and its elements may be freely modified. + */ + val List constraints + + /** + * The list of constraints that should be saturated (tightened) + * when a {@link PolyhedronSaturationOperator} is invoked. + * + * This list may be freely modified. + * + * Place all dimensions and constraints here to saturate all the bounds. + */ + val List expressionsToSaturate + + override toString() ''' + Dimensions: + «FOR dimension : dimensions» + «dimension» + «ENDFOR» + Constraints: + «FOR constraint : constraints» + «constraint» + «ENDFOR» +««« Saturate: +««« «FOR expression : expressionsToSaturate» +««« «IF expression instanceof Dimension»dimension«ELSEIF expression instanceof LinearConstraint»constraint«ELSE»unknown«ENDIF» «expression» +««« «ENDFOR» + ''' + +} + +@Accessors +abstract class LinearBoundedExpression { + var Integer lowerBound + var Integer upperBound +} + +@Accessors +class Dimension extends LinearBoundedExpression { + val String name + + @FinalFieldsConstructor + new() { + } + + new(String name, Integer lowerBound, Integer upperBound) { + this(name) + this.lowerBound = lowerBound + this.upperBound = upperBound + } + + override toString() { + '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«name»«IF upperBound !== null» <= «upperBound»«ENDIF»''' + } + +} + +@Accessors +class LinearConstraint extends LinearBoundedExpression { + val Map coefficients + + @FinalFieldsConstructor + new() { + } + + new(Map coefficients, Integer lowerBound, Integer upperBound) { + this(coefficients) + this.lowerBound = lowerBound + this.upperBound = upperBound + } + + override toString() { + '''«IF lowerBound !== null»«lowerBound» <= «ENDIF»«FOR pair : coefficients.entrySet SEPARATOR " + "»«IF pair.value != 1»«pair.value» * «ENDIF»«pair.key.name»«ENDFOR»«IF upperBound !== null» <= «upperBound»«ENDIF»''' + } + +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend new file mode 100644 index 00000000..c8fb3409 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/ScopePropagator.xtend @@ -0,0 +1,149 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialComplexTypeInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialTypeInterpratation +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.Scope +import java.util.HashMap +import java.util.HashSet +import java.util.Map +import java.util.Set +import org.eclipse.xtend.lib.annotations.Accessors + +enum ScopePropagatorStrategy { + BasicTypeHierarchy, + PolyhedralTypeHierarchy +} + +class ScopePropagator { + @Accessors(PROTECTED_GETTER) PartialInterpretation partialInterpretation + Map type2Scope + + val Map> superScopes + val Map> subScopes + + new(PartialInterpretation p) { + partialInterpretation = p + type2Scope = new HashMap + for (scope : p.scopes) { + type2Scope.put(scope.targetTypeInterpretation, scope) + } + + superScopes = new HashMap + subScopes = new HashMap + for (scope : p.scopes) { + superScopes.put(scope, new HashSet) + subScopes.put(scope, new HashSet) + } + + for (scope : p.scopes) { + val target = scope.targetTypeInterpretation + if (target instanceof PartialComplexTypeInterpretation) { + val supertypeInterpretations = target.supertypeInterpretation + for (supertypeInterpretation : supertypeInterpretations) { + val supertypeScope = type2Scope.get(supertypeInterpretation) + superScopes.get(scope).add(supertypeScope) + subScopes.get(supertypeScope).add(scope) + } + } + } + } + + def propagateAllScopeConstraints() { + var boolean hadChanged + do { + hadChanged = false + for (superScopeEntry : superScopes.entrySet) { + val sub = superScopeEntry.key + hadChanged = propagateLowerLimitUp(sub, partialInterpretation) || hadChanged + hadChanged = propagateUpperLimitDown(sub, partialInterpretation) || hadChanged + for (sup : superScopeEntry.value) { + hadChanged = propagateLowerLimitUp(sub, sup) || hadChanged + hadChanged = propagateUpperLimitDown(sub, sup) || hadChanged + } + } + } while (hadChanged) + } + + def propagateAdditionToType(PartialTypeInterpratation t) { +// println('''Adding to «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + val targetScope = type2Scope.get(t) + targetScope.removeOne + val sups = superScopes.get(targetScope) + sups.forEach[removeOne] + if (this.partialInterpretation.minNewElements > 0) { + this.partialInterpretation.minNewElements = this.partialInterpretation.minNewElements - 1 + } + if (this.partialInterpretation.maxNewElements > 0) { + this.partialInterpretation.maxNewElements = this.partialInterpretation.maxNewElements - 1 + } else if (this.partialInterpretation.maxNewElements === 0) { + throw new IllegalArgumentException('''Inconsistent object creation: lower node limit is 0!''') + } + propagateAllScopeConstraints + +// println('''Target Scope: «targetScope.minNewElements» - «targetScope.maxNewElements»''') +// println(''' «this.partialInterpretation.minNewElements» - «this.partialInterpretation.maxNewElements»''') +// this.partialInterpretation.scopes.forEach[println(''' «(it.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name»: «it.minNewElements»-«it.maxNewElements»''')] +// println('''All constraints are propagated upon increasing «(t as PartialComplexTypeInterpretation).interpretationOf.name»''') + } + + private def propagateLowerLimitUp(Scope subScope, Scope superScope) { + if (subScope.minNewElements > superScope.minNewElements) { + superScope.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, Scope superScope) { + if (superScope.maxNewElements >= 0 && + (superScope.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> «(superScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» +// subScope.maxNewElements «subScope.maxNewElements» = superScope.maxNewElements «superScope.maxNewElements» +// ''') + subScope.maxNewElements = superScope.maxNewElements + return true + } else { + return false + } + } + + private def propagateLowerLimitUp(Scope subScope, PartialInterpretation p) { + if (subScope.minNewElements > p.minNewElements) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// p.minNewElements «p.minNewElements» = subScope.minNewElements «subScope.minNewElements» +// ''') + p.minNewElements = subScope.minNewElements + return true + } else { + return false + } + } + + private def propagateUpperLimitDown(Scope subScope, PartialInterpretation p) { + if (p.maxNewElements >= 0 && (p.maxNewElements < subScope.maxNewElements || subScope.maxNewElements < 0)) { +// println(''' +// «(subScope.targetTypeInterpretation as PartialComplexTypeInterpretation).interpretationOf.name» -> nodes +// subScope.maxNewElements «subScope.maxNewElements» = p.maxNewElements «p.maxNewElements» +// ''') + subScope.maxNewElements = p.maxNewElements + return true + } else { + return false + } + } + + private def removeOne(Scope scope) { + if (scope.maxNewElements === 0) { + throw new IllegalArgumentException('''Inconsistent object creation: «scope.targetTypeInterpretation»''') + } else if (scope.maxNewElements > 0) { + scope.maxNewElements = scope.maxNewElements - 1 + } + if (scope.minNewElements > 0) { + scope.minNewElements = scope.minNewElements - 1 + } + } +} diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend new file mode 100644 index 00000000..f1a84f2d --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/cardinality/Z3PolyhedronSolver.xtend @@ -0,0 +1,206 @@ +package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.cardinality + +import com.microsoft.z3.ArithExpr +import com.microsoft.z3.Context +import com.microsoft.z3.Expr +import com.microsoft.z3.IntNum +import com.microsoft.z3.Optimize +import com.microsoft.z3.Status +import com.microsoft.z3.Symbol +import java.util.Map +import org.eclipse.xtend.lib.annotations.Accessors +import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor + +class Z3PolyhedronSolver implements PolyhedronSolver { + val boolean lpRelaxation + + @FinalFieldsConstructor + new() { + } + + new() { + this(true) + } + + override createSaturationOperator(Polyhedron polyhedron) { + new Z3SaturationOperator(polyhedron, lpRelaxation) + } +} + +class Z3SaturationOperator implements PolyhedronSaturationOperator { + static val INFINITY_SYMBOL_NAME = "oo" + static val MULT_SYMBOL_NAME = "*" + + extension val Context context + val Symbol infinitySymbol + val Symbol multSymbol + @Accessors val Polyhedron polyhedron + val Map variables + + new(Polyhedron polyhedron, boolean lpRelaxation) { + context = new Context + infinitySymbol = context.mkSymbol(INFINITY_SYMBOL_NAME) + multSymbol = context.mkSymbol(MULT_SYMBOL_NAME) + this.polyhedron = polyhedron + variables = polyhedron.dimensions.toInvertedMap [ dimension | + val name = dimension.name + if (lpRelaxation) { + mkRealConst(name) + } else { + mkIntConst(name) + } + ] + } + + override saturate() { + val status = doSaturate() + convertStatusToSaturationResult(status) + } + + private def convertStatusToSaturationResult(Status status) { + switch (status) { + case SATISFIABLE: + PolyhedronSaturationResult.SATURATED + case UNSATISFIABLE: + PolyhedronSaturationResult.EMPTY + case UNKNOWN: + PolyhedronSaturationResult.UNKNOWN + default: + throw new IllegalArgumentException("Unknown Status: " + status) + } + } + + private def doSaturate() { + for (expressionToSaturate : polyhedron.expressionsToSaturate) { + val expr = expressionToSaturate.toExpr + val lowerResult = saturateLowerBound(expr, expressionToSaturate) + if (lowerResult != Status.SATISFIABLE) { + return lowerResult + } + val upperResult = saturateUpperBound(expr, expressionToSaturate) + if (upperResult != Status.SATISFIABLE) { + return upperResult + } + } + Status.SATISFIABLE + } + + private def saturateLowerBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { + val optimize = prepareOptimize + val handle = optimize.MkMinimize(expr) + val status = optimize.Check() + if (status == Status.SATISFIABLE) { + val value = switch (resultExpr : handle.lower) { + IntNum: + resultExpr.getInt() + default: + if (isNegativeInfinity(resultExpr)) { + null + } else { + throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) + } + } + expressionToSaturate.lowerBound = value + } + status + } + + private def saturateUpperBound(ArithExpr expr, LinearBoundedExpression expressionToSaturate) { + val optimize = prepareOptimize + val handle = optimize.MkMaximize(expr) + val status = optimize.Check() + if (status == Status.SATISFIABLE) { + val value = switch (resultExpr : handle.upper) { + IntNum: + resultExpr.getInt() + default: + if (isPositiveInfinity(resultExpr)) { + null + } else { + throw new IllegalArgumentException("Integer result expected, got: " + resultExpr) + } + } + expressionToSaturate.upperBound = value + } + status + } + + private def isPositiveInfinity(Expr expr) { + expr.app && expr.getFuncDecl.name == infinitySymbol + } + + private def isNegativeInfinity(Expr expr) { + // Negative infinity is represented as (* (- 1) oo) + if (!expr.app || expr.getFuncDecl.name != multSymbol || expr.numArgs != 2) { + return false + } + isPositiveInfinity(expr.args.get(1)) + } + + private def prepareOptimize() { + val optimize = mkOptimize() + assertConstraints(optimize) + optimize + } + + private def assertConstraints(Optimize it) { + for (pair : variables.entrySet) { + assertBounds(pair.value, pair.key) + } + for (constraint : polyhedron.constraints) { + val expr = createLinearCombination(constraint.coefficients) + assertBounds(expr, constraint) + } + } + + private def assertBounds(Optimize it, ArithExpr expression, LinearBoundedExpression bounds) { + val lowerBound = bounds.lowerBound + val upperBound = bounds.upperBound + if (lowerBound == upperBound) { + if (lowerBound === null) { + return + } + Assert(mkEq(expression, mkInt(lowerBound))) + } else { + if (lowerBound !== null) { + Assert(mkGe(expression, mkInt(lowerBound))) + } + if (upperBound !== null) { + Assert(mkLe(expression, mkInt(upperBound))) + } + } + } + + private def toExpr(LinearBoundedExpression linearBoundedExpression) { + switch (linearBoundedExpression) { + Dimension: variables.get(linearBoundedExpression) + LinearConstraint: createLinearCombination(linearBoundedExpression.coefficients) + default: throw new IllegalArgumentException("Unknown linear bounded expression:" + linearBoundedExpression) + } + } + + private def createLinearCombination(Map coefficients) { + val size = coefficients.size + val array = newArrayOfSize(size) + var int i = 0 + for (pair : coefficients.entrySet) { + val variable = variables.get(pair.key) + if (variable === null) { + throw new IllegalArgumentException("Unknown dimension: " + pair.key.name) + } + val coefficient = pair.value + val term = if (coefficient == 1) { + variable + } else { + mkMul(mkInt(coefficient), variable) + } + array.set(i, term) + i++ + } + mkAdd(array) + } + + override close() throws Exception { + context.close() + } +} -- cgit v1.2.3-70-g09d2