Initial implementation of an optimization solver with unit tests. (#5849)

5 files changed, 382 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c438d9a4f..419b6ff75 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -242,6 +242,8 @@ libcvc4_add_sources(
   smt/model_blocker.h
   smt/node_command.cpp
   smt/node_command.h
+  smt/optimization_solver.cpp
+  smt/optimization_solver.h
   smt/options_manager.cpp
   smt/options_manager.h
   smt/output_manager.cpp
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
new file mode 100644
index 000000000..609ed9813
--- /dev/null
+++ b/src/smt/optimization_solver.cpp
@@ -0,0 +1,137 @@
+/*********************                                                        */
+/*! \file optimization_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Michael Chang
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for optimization queries
+ **/
+
+#include "smt/optimization_solver.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * d_activatedObjective is initialized to a default objective:
+ * default objective constructed with Null Node and OBJECTIVE_UNDEFINED
+ *
+ * d_savedValue is initialized to a default node (Null Node)
+ */
+
+OptimizationSolver::OptimizationSolver(SmtEngine* parent)
+    : d_parent(parent),
+      d_activatedObjective(Node(), OBJECTIVE_UNDEFINED),
+      d_savedValue()
+{
+}
+
+OptimizationSolver::~OptimizationSolver() {}
+
+OptResult OptimizationSolver::checkOpt()
+{
+  // Make sure that the objective is not the default one
+  Assert(d_activatedObjective.getType() != OBJECTIVE_UNDEFINED);
+  Assert(!d_activatedObjective.getNode().isNull());
+
+  // the smt engine to which we send intermediate queries
+  // for the linear search.
+  std::unique_ptr<SmtEngine> optChecker;
+  initializeSubsolver(optChecker);
+  NodeManager* nm = optChecker->getNodeManager();
+
+  // we need to be in incremental mode for multiple objectives since we need to
+  // push pop we need to produce models to inrement on our objective
+  optChecker->setOption("incremental", "true");
+  optChecker->setOption("produce-models", "true");
+
+  // Move assertions from the parent solver to the subsolver
+  std::vector<Node> p_assertions = d_parent->getExpandedAssertions();
+  for (const Node& e : p_assertions)
+  {
+    optChecker->assertFormula(e);
+  }
+
+  // We need to checksat once before the optimization loop so we have a
+  // baseline value to increment
+  Result loop_r = optChecker->checkSat();
+
+  if (loop_r.isUnknown())
+  {
+    return OPT_UNKNOWN;
+  }
+  if (!loop_r.isSat())
+  {
+    return OPT_UNSAT;
+  }
+
+  // Model-value of objective (used in optimization loop)
+  Node value;
+  // asserts objective > old_value (used in optimization loop)
+  Node increment;
+
+  // Workhorse of linear optimization:
+  // This loop will keep incrmenting the objective until unsat
+  // When unsat is hit, the optimized value is the model value just before the
+  // unsat call
+  while (loop_r.isSat())
+  {
+    // get the model-value of objective in last sat call
+    value = optChecker->getValue(d_activatedObjective.getNode());
+
+    // We need to save the value since we need the model value just before the
+    // unsat call
+    Assert(!value.isNull());
+    d_savedValue = value;
+
+    // increment on the model-value of objective:
+    // if we're maximizing increment = objective > old_objective value
+    // if we're minimizing increment = objective < old_objective value
+    if (d_activatedObjective.getType() == OBJECTIVE_MAXIMIZE)
+    {
+      increment = nm->mkNode(kind::GT, d_activatedObjective.getNode(), value);
+    }
+    else
+    {
+      increment = nm->mkNode(kind::LT, d_activatedObjective.getNode(), value);
+    }
+    optChecker->assertFormula(increment);
+    loop_r = optChecker->checkSat();
+  }
+
+  return OPT_OPTIMAL;
+}
+
+void OptimizationSolver::activateObj(const Node& obj, const int& type)
+{
+  d_activatedObjective = Objective(obj, (ObjectiveType)type);
+}
+
+Node OptimizationSolver::objectiveGetValue()
+{
+  Assert(!d_savedValue.isNull());
+  return d_savedValue;
+}
+
+Objective::Objective(Node obj, ObjectiveType type) : d_type(type), d_node(obj)
+{
+}
+
+ObjectiveType Objective::getType() { return d_type; }
+
+Node Objective::getNode() { return d_node; }
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
new file mode 100644
index 000000000..c8a024505
--- /dev/null
+++ b/src/smt/optimization_solver.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file optimization_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Michael Chang
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for optimization queries
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__OPTIMIZATION_SOLVER_H
+#define CVC4__SMT__OPTIMIZATION_SOLVER_H
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "smt/assertions.h"
+#include "util/result.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * An enum for optimization queries.
+ *
+ * Represents whether an objective should be minimized or maximized
+ */
+enum CVC4_PUBLIC ObjectiveType
+{
+  OBJECTIVE_MINIMIZE,
+  OBJECTIVE_MAXIMIZE,
+  OBJECTIVE_UNDEFINED
+};
+
+/**
+ * An enum for optimization queries.
+ *
+ * Represents the result of a checkopt query
+ * (unimplemented) OPT_OPTIMAL: if value was found
+ */
+enum CVC4_PUBLIC OptResult
+{
+  // the original set of assertions has result UNKNOWN
+  OPT_UNKNOWN,
+  // the original set of assertions has result UNSAT
+  OPT_UNSAT,
+  // the optimization loop finished and optimal
+  OPT_OPTIMAL,
+
+  // The last value is here as a preparation for future work
+  // in which pproximate optimizations will be supported.
+
+  // if the solver halted early and value is only approximate
+  OPT_SAT_APPROX
+};
+
+class Objective
+{
+ public:
+  Objective(Node n, ObjectiveType type);
+  ~Objective(){};
+
+  /** A getter for d_type **/
+  ObjectiveType getType();
+  /** A getter for d_node **/
+  Node getNode();
+
+ private:
+  /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
+   * OBJECTIVE_MINIMIZE  **/
+  ObjectiveType d_type;
+  /** The node associated to the term that was used to construct the objective.
+   * **/
+  Node d_node;
+  };
+
+  /**
+   * A solver for optimization queries.
+   * 
+   * This class is responsible for responding to optmization queries. It
+   * spawns a subsolver SmtEngine that captures the parent assertions and 
+   * implements a linear optimization loop. Supports activateObjective, 
+   * checkOpt, and objectiveGetValue in that order.
+   */
+  class OptimizationSolver
+  {
+   public:
+    /** parent is the smt_solver that the user added their assertions to **/
+    OptimizationSolver(SmtEngine* parent);
+    ~OptimizationSolver();
+
+    /** Runs the optimization loop for the activated objective **/
+    OptResult checkOpt();
+    /** Activates an objective: will be optimized for **/
+    void activateObj(const Node& obj, const int& type);
+    /** Gets the value of the optimized objective after checkopt is called **/
+    Node objectiveGetValue();
+
+   private:
+    /** The parent SMT engine **/
+    SmtEngine* d_parent;
+    /** The objectives to optimize for **/
+    Objective d_activatedObjective;
+    /** A saved value of the objective from the last sat call. **/
+    Node d_savedValue;
+  };
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index f3c340a74..9a8bc4dee 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -21,6 +21,7 @@ cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
 cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bv_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
+cvc4_add_unit_test_white(theory_int_opt_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
 cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
new file mode 100644
index 000000000..1e5c2c437
--- /dev/null
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -0,0 +1,126 @@
+#include <iostream>
+#include "smt/optimization_solver.h"
+#include "test_smt.h"
+
+namespace CVC4 {
+
+using namespace theory;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
+{
+ protected:
+  void SetUp() override
+  {
+    TestSmtNoFinishInit::SetUp();
+    d_smtEngine->setOption("produce-assertions", "true");
+    d_smtEngine->finishInit();
+
+    d_optslv.reset(new OptimizationSolver(d_smtEngine.get()));
+    d_intType.reset(new TypeNode(d_nodeManager->integerType()));
+  }
+
+  std::unique_ptr<OptimizationSolver> d_optslv;
+  std::unique_ptr<TypeNode> d_intType;
+};
+
+TEST_F(TestTheoryWhiteIntOpt, max)
+{
+  Node ub = d_nodeManager->mkConst(Rational("100"));
+  Node lb = d_nodeManager->mkConst(Rational("0"));
+
+  // Objectives to be optimized max_cost is max objective
+  Node max_cost = d_nodeManager->mkVar(*d_intType);
+
+  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
+  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
+
+  /* Result of asserts is:
+      0 < max_cost < 100
+  */
+  d_smtEngine->assertFormula(upb);
+  d_smtEngine->assertFormula(lowb);
+
+  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
+
+  // We activate our objective so the subsolver knows to optimize it
+  d_optslv->activateObj(max_cost, max_type);
+
+  OptResult r = d_optslv->checkOpt();
+
+  // We expect max_cost == 99
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+                    d_nodeManager->mkConst(Rational("99")));
+
+  std::cout << "Result is :" << r << std::endl;
+  std::cout << "Optimized max value is: "
+            << d_optslv->objectiveGetValue() << std::endl;
+}
+
+TEST_F(TestTheoryWhiteIntOpt, min)
+{
+  Node ub = d_nodeManager->mkConst(Rational("100"));
+  Node lb = d_nodeManager->mkConst(Rational("0"));
+
+  // Objectives to be optimized max_cost is max objective
+  Node max_cost = d_nodeManager->mkVar(*d_intType);
+
+  Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost);
+  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb);
+
+  /* Result of asserts is:
+      0 < max_cost < 100
+  */
+  d_smtEngine->assertFormula(upb);
+  d_smtEngine->assertFormula(lowb);
+
+  const ObjectiveType min_type = OBJECTIVE_MINIMIZE;
+
+  // We activate our objective so the subsolver knows to optimize it
+  d_optslv->activateObj(max_cost, min_type);
+
+  OptResult r = d_optslv->checkOpt();
+
+  // We expect max_cost == 99
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+                    d_nodeManager->mkConst(Rational("1")));
+
+  std::cout << "Result is :" << r << std::endl;
+  std::cout << "Optimized max value is: "
+            << d_optslv->objectiveGetValue() << std::endl;
+}
+
+TEST_F(TestTheoryWhiteIntOpt, result)
+{
+  Node ub = d_nodeManager->mkConst(Rational("100"));
+  Node lb = d_nodeManager->mkConst(Rational("0"));
+
+  // Objectives to be optimized max_cost is max objective
+  Node max_cost = d_nodeManager->mkVar(*d_intType);
+
+  Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost);
+  Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub);
+
+  /* Result of asserts is:
+      0 > max_cost > 100
+  */
+  d_smtEngine->assertFormula(upb);
+  d_smtEngine->assertFormula(lowb);
+
+  const ObjectiveType max_type = OBJECTIVE_MAXIMIZE;
+
+  // We activate our objective so the subsolver knows to optimize it
+  d_optslv->activateObj(max_cost, max_type);
+
+  // This should return OPT_UNSAT since 0 > x > 100 is impossible.
+  OptResult r = d_optslv->checkOpt();
+
+  // We expect our check to have returned UNSAT
+  ASSERT_EQ(r, OPT_UNSAT);
+
+  std::cout << "Result is :" << r << std::endl;
+}
+}  // namespace test
+}  // namespace CVC4