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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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)
--- /dev/null
+#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
projects / cvc5.git / commitdiff