Merge pull request #171 from mbovel/mb/optimizer-suite

Add support for model minimization and maximization

src/it/scala/inox/solvers/OptimizerSuite.scala

@@ -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)
+    }
+  }
+}

src/main/scala/inox/solvers/Optimizer.scala

@@ -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

src/main/scala/inox/solvers/smtlib/optimization/Z3Optimizer.scala

@@ -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))
+  }
 }

src/main/scala/inox/solvers/unrolling/UnrollingOptimizer.scala

@@ -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 {

src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala

@@ -17,7 +17,7 @@ trait NativeZ3Optimizer extends AbstractUnrollingOptimizer with Z3Unrolling { se
 
   override val name = "native-z3-opt"
 
-  protected object underlying extends {
+  protected val underlying = NativeZ3Solver.synchronized(new {
     val program: targetProgram.type = targetProgram
     val context = self.context
   } with AbstractOptimizer with Z3Native {
@@ -32,13 +32,16 @@ trait NativeZ3Optimizer extends AbstractUnrollingOptimizer with Z3Unrolling { se
     private[this] val optimizer: ScalaZ3Optimizer = z3.mkOptimizer()
 
     private def tryZ3[T](res: => T): Option[T] =
-      // @nv: Z3 optimizer throws an exceptiopn when canceled instead of returning Unknown
+      // @nv: Z3 optimizer throws an exception when canceled instead of returning Unknown
       try { Some(res) } catch { case e: Z3Exception if e.getMessage == "canceled" => None }
 
     def assertCnstr(ast: Z3AST): Unit = tryZ3(optimizer.assertCnstr(ast))
     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.
@@ -74,5 +77,7 @@ trait NativeZ3Optimizer extends AbstractUnrollingOptimizer with Z3Unrolling { se
       super.pop()
       optimizer.pop()
     }
-  }
+  })
+
+  override def free(): Unit = NativeZ3Solver.synchronized(super.free())
 }