Skip to content

Commit

Permalink
Add support for minimize/maximize in Optimizers
Browse files Browse the repository at this point in the history
  • Loading branch information
mbovel committed Jan 3, 2022
1 parent efd76f3 commit eb8329b
Show file tree
Hide file tree
Showing 5 changed files with 121 additions and 0 deletions.
90 changes: 90 additions & 0 deletions src/it/scala/inox/solvers/OptimizerSuite.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,90 @@
/* Copyright 2009-2018 EPFL, Lausanne */

package inox
package solvers
package unrolling

class OptimizerSuite extends SolvingTestSuite with DatastructureUtils {
import trees._
import dsl._
import SolverResponses._

override def configurations =
for (nme <- Seq(/*"nativez3-opt", */"smt-z3-opt")) yield {
Seq(optSelectedSolvers(Set(nme)))
}

override def optionsString(options: Options): String = {
"solvr=" + options.findOptionOrDefault(optSelectedSolvers).head
}

implicit val symbols: inox.trees.Symbols = NoSymbols

val program = inox.Program(inox.trees)(symbols)

test("unsatisfiable soft constraint") { implicit ctx =>
val v = Variable.fresh("x", IntegerType())
val clause = GreaterThan(v, IntegerLiteral(BigInt(10)))
val softClause = GreaterThan(IntegerLiteral(BigInt(10)), v)

val factory = SolverFactory.optimizer(program, ctx)
val optimizer = factory.getNewSolver()
try {
optimizer.assertCnstr(clause)
optimizer.assertCnstr(softClause, 1)
optimizer.check(Model) match {
case SatWithModel(model) => model.vars.get(v.toVal).get match {
case IntegerLiteral(n) => n > 10
}
case _ =>
fail("Expected sat-with-model")
}
} finally {
factory.reclaim(optimizer)
}
}

test("n times n, minimize") { implicit ctx =>
val x = Variable.fresh("x", Int32Type())
val prop = GreaterEquals(Times(x, x), Int32Literal(10))

val factory = SolverFactory.optimizer(program, ctx)
val optimizer = factory.getNewSolver()
try {
optimizer.assertCnstr(Not(prop))
optimizer.minimize(x)
optimizer.check(Model) match {
case SatWithModel(model) =>
model.vars.get(x.toVal).get match {
case Int32Literal(c) => assert(c == 0)
}
case _ =>
fail("Expected sat-with-model")
}
} finally {
factory.reclaim(optimizer)
}
}

test("n times n, maximize") { implicit ctx =>
val x = Variable.fresh("x", IntegerType())
val prop = GreaterEquals(Times(x, x), IntegerLiteral(10))

val factory = SolverFactory.optimizer(program, ctx)
val optimizer = factory.getNewSolver()
try {
optimizer.assertCnstr(Not(prop))
optimizer.maximize(x)
optimizer.check(Model) match {
case SatWithModel(model) =>
model.vars.get(x.toVal).get match {
case IntegerLiteral(c) => assert(c == 3)
}
case _ =>
fail("Expected sat-with-model")
}
} finally {
factory.reclaim(optimizer)
}
}
}
2 changes: 2 additions & 0 deletions src/main/scala/inox/solvers/Optimizer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ package solvers
trait AbstractOptimizer extends AbstractSolver {
def assertCnstr(expression: Trees, weight: Int): Unit
def assertCnstr(expression: Trees, weight: Int, group: String): Unit
def minimize(expression: Trees): Unit
def maximize(expression: Trees): Unit
}

trait Optimizer extends AbstractOptimizer with Solver
14 changes: 14 additions & 0 deletions src/main/scala/inox/solvers/smtlib/optimization/Z3Optimizer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -25,4 +25,18 @@ trait Z3Optimizer extends Z3Solver with AbstractOptimizer {
val term = toSMT(expr)(Map())
emit(AssertSoft(term, Some(weight), Some(group)))
}

def minimize(expr: Expr): Unit = {
exprOps.variablesOf(expr).foreach(declareVariable)

val term = toSMT(expr)(Map())
emit(Minimize(term))
}

def maximize(expr: Expr): Unit = {
exprOps.variablesOf(expr).foreach(declareVariable)

val term = toSMT(expr)(Map())
emit(Maximize(term))
}
}
12 changes: 12 additions & 0 deletions src/main/scala/inox/solvers/unrolling/UnrollingOptimizer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,18 @@ trait AbstractUnrollingOptimizer extends AbstractUnrollingSolver with Optimizer
assertCnstr(Implies(b, expression))
underlying.assertCnstr(freeVars(b), weight, group)
}

def minimize(expression: Expr): Unit = {
val b = Variable.fresh("e", expression.getType)
assertCnstr(Equals(b, expression))
underlying.minimize(freeVars(b))
}

def maximize(expression: Expr): Unit = {
val b = Variable.fresh("e", expression.getType)
assertCnstr(Equals(b, expression))
underlying.maximize(freeVars(b))
}
}

trait UnrollingOptimizer extends AbstractUnrollingOptimizer with UnrollingSolver {
Expand Down
3 changes: 3 additions & 0 deletions src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,9 @@ trait NativeZ3Optimizer extends AbstractUnrollingOptimizer with Z3Unrolling { se
def assertCnstr(ast: Z3AST, weight: Int): Unit = tryZ3(optimizer.assertCnstr(ast, weight))
def assertCnstr(ast: Z3AST, weight: Int, group: String): Unit = tryZ3(optimizer.assertCnstr(ast, weight, group))

def maximize(ast: Z3AST): Unit = tryZ3(optimizer.maximize(ast))
def minimize(ast: Z3AST): Unit = tryZ3(optimizer.minimize(ast))

// NOTE @nv: this is very similar to code in AbstractZ3Solver and UninterpretedZ3Solver but
// is difficult to merge due to small API differences between the native Z3
// solvers and optimizers.
Expand Down

0 comments on commit eb8329b

Please sign in to comment.