Add support for box optimization -- independently optimize each goal as if the other goals do not exist.
Single minimize() / maximize() now maintains the pushed / popped context.
Of course unit tests are here as well.
/******************************************************************************
* Top contributors (to current version):
- * Yancheng Ou, Michael Chang
+ * Yancheng Ou
*
* This file is part of the cvc5 project.
*
intermediateSatResult = optChecker->checkSat();
if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
{
+ optChecker->pop();
return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::SAT)
// lowerBound == pivot ==> upperbound = lowerbound + 1
// and lowerbound <= target < upperbound is UNSAT
// return the upperbound
+ optChecker->pop();
return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
else
}
else
{
+ optChecker->pop();
return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
optChecker->pop();
intermediateSatResult = optChecker->checkSat();
if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
{
+ optChecker->pop();
return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::SAT)
// upperbound = lowerbound + 1
// and lowerbound < target <= upperbound is UNSAT
// return the lowerbound
+ optChecker->pop();
return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
else
}
else
{
+ optChecker->pop();
return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
optChecker->pop();
/******************************************************************************
* Top contributors (to current version):
- * Yancheng Ou, Michael Chang
+ * Michael Chang, Yancheng Ou
*
* This file is part of the cvc5 project.
*
// the smt engine to which we send intermediate queries
// for the linear search.
NodeManager* nm = optChecker->getNodeManager();
-
+ optChecker->push();
Result intermediateSatResult = optChecker->checkSat();
// Model-value of objective (used in optimization loop)
Node value;
{
return OptimizationResult(OptimizationResult::UNSAT, value);
}
- // asserts objective > old_value (used in optimization loop)
+ // node storing target > old_value (used in optimization loop)
Node increment;
Kind incrementalOperator = kind::NULL_EXPR;
if (isMinimize)
optChecker->assertFormula(increment);
intermediateSatResult = optChecker->checkSat();
}
+ optChecker->pop();
return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
/******************************************************************************
* Top contributors (to current version):
- * Yancheng Ou, Michael Chang, Aina Niemetz
+ * Yancheng Ou, Aina Niemetz
*
* This file is part of the cvc5 project.
*
}
else
{
- return nullptr;
+ Unimplemented() << "Target type " << objectiveType
+ << " does not support optimization";
}
}
}
else
{
- Unimplemented() << "Target type does not support optimization";
+ Unimplemented() << "Target type " << targetType
+ << " does not support optimization";
}
}
case OptimizationObjective::MAXIMIZE:
}
else
{
- Unimplemented() << "Target type does not support optimization";
+ Unimplemented() << "Target type " << targetType
+ << " does not support optimization";
}
}
default:
}
else
{
- Unimplemented() << "Target type does not support optimization";
+ Unimplemented() << "Target type " << targetType
+ << " does not support optimization";
}
}
case OptimizationObjective::MAXIMIZE:
}
else
{
- Unimplemented() << "Target type does not support optimization";
+ Unimplemented() << "Target type " << targetType
+ << " does not support optimization";
}
}
default:
/******************************************************************************
* Top contributors (to current version):
- * Michael Chang, Yancheng Ou, Aina Niemetz
+ * Yancheng Ou, Michael Chang, Aina Niemetz
*
* This file is part of the cvc5 project.
*
namespace cvc5 {
namespace smt {
-OptimizationResult::ResultType OptimizationSolver::checkOpt()
+OptimizationSolver::OptimizationSolver(SmtEngine* parent)
+ : d_parent(parent),
+ d_optChecker(),
+ d_objectives(),
+ d_results(),
+ d_objectiveCombination(BOX)
{
- Assert(d_objectives.size() == 1);
- // NOTE: currently we are only dealing with single obj
- std::unique_ptr<OMTOptimizer> optimizer =
- OMTOptimizer::getOptimizerForObjective(d_objectives[0]);
-
- if (!optimizer) return OptimizationResult::UNSUPPORTED;
+}
- OptimizationResult optResult;
- std::unique_ptr<SmtEngine> optChecker = createOptCheckerWithTimeout(d_parent);
- if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE)
- {
- optResult =
- optimizer->maximize(optChecker.get(), d_objectives[0].getTarget());
- }
- else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE)
+OptimizationResult::ResultType OptimizationSolver::checkOpt()
+{
+ switch (d_objectiveCombination)
{
- optResult =
- optimizer->minimize(optChecker.get(), d_objectives[0].getTarget());
+ case BOX: return optimizeBox(); break;
+ default:
+ Unimplemented()
+ << "Only BOX objective combination is supported in current version";
}
-
- d_results[0] = optResult;
- return optResult.getType();
+ Unreachable();
}
void OptimizationSolver::pushObjective(
TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned)
{
+ if (!OMTOptimizer::nodeSupportsOptimization(target))
+ {
+ CVC5_FATAL()
+ << "Objective not pushed: Target node does not support optimization";
+ }
+ d_optChecker.reset();
d_objectives.emplace_back(target, type, bvSigned);
- d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node());
+ d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
}
void OptimizationSolver::popObjective()
{
+ d_optChecker.reset();
d_objectives.pop_back();
d_results.pop_back();
}
return d_results;
}
+void OptimizationSolver::setObjectiveCombination(
+ ObjectiveCombination combination)
+{
+ d_objectiveCombination = combination;
+}
+
std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
{
return optChecker;
}
+OptimizationResult::ResultType OptimizationSolver::optimizeBox()
+{
+ // resets the optChecker
+ d_optChecker = createOptCheckerWithTimeout(d_parent);
+ OptimizationResult partialResult;
+ OptimizationResult::ResultType aggregatedResultType =
+ OptimizationResult::OPTIMAL;
+ std::unique_ptr<OMTOptimizer> optimizer;
+ for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+ {
+ optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
+ // checks whether the objective type is maximize or minimize
+ switch (d_objectives[i].getType())
+ {
+ case OptimizationObjective::MAXIMIZE:
+ partialResult = optimizer->maximize(d_optChecker.get(),
+ d_objectives[i].getTarget());
+ break;
+ case OptimizationObjective::MINIMIZE:
+ partialResult = optimizer->minimize(d_optChecker.get(),
+ d_objectives[i].getTarget());
+ break;
+ default:
+ CVC5_FATAL()
+ << "Optimization objective is neither MAXIMIZE nor MINIMIZE";
+ }
+ // match the optimization result type, and aggregate the results of
+ // subproblems
+ switch (partialResult.getType())
+ {
+ case OptimizationResult::OPTIMAL: break;
+ case OptimizationResult::UNBOUNDED: break;
+ case OptimizationResult::UNSAT:
+ if (aggregatedResultType == OptimizationResult::OPTIMAL)
+ {
+ aggregatedResultType = OptimizationResult::UNSAT;
+ }
+ break;
+ case OptimizationResult::UNKNOWN:
+ aggregatedResultType = OptimizationResult::UNKNOWN;
+ break;
+ default: Unreachable();
+ }
+
+ d_results[i] = partialResult;
+ }
+ // kill optChecker after optimization ends
+ d_optChecker.reset();
+ return aggregatedResultType;
+}
+
} // namespace smt
} // namespace cvc5
/******************************************************************************
* Top contributors (to current version):
- * Michael Chang, Yancheng Ou, Aina Niemetz
+ * Yancheng Ou, Michael Chang, Aina Niemetz
*
* This file is part of the cvc5 project.
*
**/
enum ResultType
{
- // the type of the target is not supported
- UNSUPPORTED,
// whether the value is optimal is UNKNOWN
UNKNOWN,
// the original set of assertions has result UNSAT
: d_type(type), d_value(value)
{
}
- OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
+ OptimizationResult() : d_type(UNKNOWN), d_value() {}
~OptimizationResult() = default;
/**
* Returns an enum indicating whether
* the result is optimal or not.
* @return an enum showing whether the result is optimal, unbounded,
- * unsat, unknown or unsupported.
+ * unsat or unknown.
**/
ResultType getType() { return d_type; }
/**
class OptimizationSolver
{
public:
+ /**
+ * An enum specifying how multiple objectives are dealt with.
+ * Definition:
+ * phi(x, y): set of assertions with variables x and y
+ *
+ * Box: treat the objectives as independent objectives
+ * v_x = max(x) s.t. phi(x, y) = sat
+ * v_y = max(y) s.t. phi(x, y) = sat
+ *
+ * Lexicographic: optimize the objectives one-by-one, in the order they push
+ * v_x = max(x) s.t. phi(x, y) = sat
+ * v_y = max(y) s.t. phi(v_x, y) = sat
+ *
+ * Pareto: optimize multiple goals to a state such that
+ * further optimization of one goal will worsen the other goal(s)
+ * (v_x, v_y) s.t. phi(v_x, v_y) = sat, and
+ * forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y)
+ **/
+ enum ObjectiveCombination
+ {
+ BOX,
+ LEXICOGRAPHIC,
+ PARETO,
+ };
/**
* Constructor
* @param parent the smt_solver that the user added their assertions to
**/
- OptimizationSolver(SmtEngine* parent)
- : d_parent(parent), d_objectives(), d_results()
- {
- }
+ OptimizationSolver(SmtEngine* parent);
~OptimizationSolver() = default;
/**
* Run the optimization loop for the pushed objective
- * NOTE: this function currently supports only single objective
- * for multiple pushed objectives it always optimizes the first one.
- * Add support for multi-obj later
*/
OptimizationResult::ResultType checkOpt();
bool bvSigned = false);
/**
- * Pop the most recent objective.
+ * Pop the most recently successfully-pushed objective.
**/
void popObjective();
**/
std::vector<OptimizationResult> getValues();
+ /**
+ * Sets the objective combination
+ **/
+ void setObjectiveCombination(ObjectiveCombination combination);
+
private:
/**
* Initialize an SMT subsolver for offline optimization purpose
bool needsTimeout = false,
unsigned long timeout = 0);
- /** The parent SMT engine **/
+ /**
+ * Optimize multiple goals in Box order
+ * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED;
+ * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
+ * UNKNOWN if any of the objective is UNKNOWN.
+ **/
+ OptimizationResult::ResultType optimizeBox();
+
+ /** A pointer to the parent SMT engine **/
SmtEngine* d_parent;
+ /** A subsolver for offline optimization **/
+ std::unique_ptr<SmtEngine> d_optChecker;
+
/** The objectives to optimize for **/
std::vector<OptimizationObjective> d_objectives;
/** The results of the optimizations from the last checkOpt call **/
std::vector<OptimizationResult> d_results;
+
+ /** The current objective combination method **/
+ ObjectiveCombination d_objectiveCombination;
};
} // namespace smt
cvc5_add_unit_test_white(theory_bv_int_blaster_white theory)
cvc5_add_unit_test_white(theory_engine_white theory)
cvc5_add_unit_test_white(theory_int_opt_white theory)
+cvc5_add_unit_test_white(theory_opt_multigoal_white theory)
cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory)
/******************************************************************************
* Top contributors (to current version):
- * Yancheng Ou, Michael Chang
+ * Yancheng Ou
*
* This file is part of the cvc5 project.
*
d_optslv->popObjective();
}
+
} // namespace test
} // namespace cvc5
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
-
// We activate our objective so the subsolver knows to optimize it
d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
-
// We activate our objective so the subsolver knows to optimize it
d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
-
// We activate our objective so the subsolver knows to optimize it
d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
// This should return OPT_UNSAT since 0 > x > 100 is impossible.
OptimizationResult::ResultType r = d_optslv->checkOpt();
-
+
// We expect our check to have returned UNSAT
ASSERT_EQ(r, OptimizationResult::UNSAT);
d_optslv->popObjective();
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Yancheng Ou
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * White-box testing for multigoal optimization.
+ */
+#include <iostream>
+
+#include "smt/optimization_solver.h"
+#include "test_smt.h"
+#include "util/bitvector.h"
+
+namespace cvc5 {
+
+using namespace theory;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryWhiteOptMultigoal : public TestSmtNoFinishInit
+{
+ protected:
+ void SetUp() override
+ {
+ TestSmtNoFinishInit::SetUp();
+ d_smtEngine->setOption("produce-assertions", "true");
+ d_smtEngine->finishInit();
+
+ d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u)));
+ }
+
+ std::unique_ptr<TypeNode> d_BV32Type;
+};
+
+TEST_F(TestTheoryWhiteOptMultigoal, box)
+{
+ d_smtEngine->resetAssertions();
+ Node x = d_nodeManager->mkVar(*d_BV32Type);
+ Node y = d_nodeManager->mkVar(*d_BV32Type);
+ Node z = d_nodeManager->mkVar(*d_BV32Type);
+
+ // 18 <= x
+ d_smtEngine->assertFormula(d_nodeManager->mkNode(
+ kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+
+ // y <= x
+ d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+ // Box optimization
+ OptimizationSolver optSolver(d_smtEngine.get());
+
+ optSolver.setObjectiveCombination(OptimizationSolver::BOX);
+
+ // minimize x
+ optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false);
+ // maximize y with `signed` comparison over bit-vectors.
+ optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true);
+ // maximize z
+ optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false);
+
+ OptimizationResult::ResultType r = optSolver.checkOpt();
+
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+
+ std::vector<OptimizationResult> results = optSolver.getValues();
+
+ // x == 18
+ ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+ // y == 0x7FFFFFFF
+ ASSERT_EQ(results[1].getValue().getConst<BitVector>(),
+ BitVector(32u, (unsigned)0x7FFFFFFF));
+
+ // z == 0xFFFFFFFF
+ ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+ BitVector(32u, (unsigned)0xFFFFFFFF));
+}
+
+} // namespace test
+} // namespace cvc5
projects / cvc5.git / commitdiff