Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.
private:
/**
* Handles the optimization query specified by objType
- * isMinimize = true will trigger minimization,
+ * isMinimize = true will trigger minimization,
* otherwise trigger maximization
**/
- smt::OptimizationResult optimize(
- SmtEngine* optChecker,
- TNode target,
- bool isMinimize);
+ smt::OptimizationResult optimize(SmtEngine* optChecker,
+ TNode target,
+ bool isMinimize);
};
} // namespace cvc5::omt
}
std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
- OptimizationObjective& objective)
+ const OptimizationObjective& objective)
{
// the datatype of the target node
TypeNode objectiveType = objective.getTarget().getType(true);
}
Node OMTOptimizer::mkStrongIncrementalExpression(
- NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective)
+ NodeManager* nm,
+ TNode lhs,
+ TNode rhs,
+ const OptimizationObjective& objective)
{
constexpr const char lhsTypeError[] =
"lhs type does not match or is not implicitly convertable to the target "
Unreachable();
}
-Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm,
- TNode lhs,
- TNode rhs,
- OptimizationObjective& objective)
+Node OMTOptimizer::mkWeakIncrementalExpression(
+ NodeManager* nm,
+ TNode lhs,
+ TNode rhs,
+ const OptimizationObjective& objective)
{
constexpr const char lhsTypeError[] =
"lhs type does not match or is not implicitly convertable to the target "
* and this is the optimizer for targetNode
**/
static std::unique_ptr<OMTOptimizer> getOptimizerForObjective(
- smt::OptimizationObjective& objective);
+ const smt::OptimizationObjective& objective);
/**
* Given the lhs and rhs expressions, with an optimization objective,
NodeManager* nm,
TNode lhs,
TNode rhs,
- smt::OptimizationObjective& objective);
+ const smt::OptimizationObjective& objective);
/**
* Given the lhs and rhs expressions, with an optimization objective,
NodeManager* nm,
TNode lhs,
TNode rhs,
- smt::OptimizationObjective& objective);
+ const smt::OptimizationObjective& objective);
/**
* Minimize the target node with constraints encoded in optChecker
#include "smt/optimization_solver.h"
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
#include "omt/omt_optimizer.h"
#include "options/smt_options.h"
#include "smt/assertions.h"
OptimizationSolver::OptimizationSolver(SmtEngine* parent)
: d_parent(parent),
d_optChecker(),
- d_objectives(),
+ d_objectives(parent->getUserContext()),
d_results(),
d_objectiveCombination(LEXICOGRAPHIC)
{
OptimizationResult::ResultType OptimizationSolver::checkOpt()
{
+ // if the results of the previous call have different size than the
+ // objectives, then we should clear the pareto optimization context
+ if (d_results.size() != d_objectives.size()) d_optChecker.reset();
+ // initialize the result vector
+ d_results.clear();
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
- // reset the optimization results
- d_results[i] = OptimizationResult();
+ d_results.emplace_back();
}
switch (d_objectiveCombination)
{
}
d_optChecker.reset();
d_objectives.emplace_back(target, type, bvSigned);
- d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
-}
-
-void OptimizationSolver::resetObjectives()
-{
- d_optChecker.reset();
- d_objectives.clear();
- d_results.clear();
}
std::vector<OptimizationResult> OptimizationSolver::getValues()
#ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
#define CVC5__SMT__OPTIMIZATION_SOLVER_H
+#include "context/cdhashmap_forward.h"
+#include "context/cdlist.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "util/result.h"
* @return an enum showing whether the result is optimal, unbounded,
* unsat or unknown.
**/
- ResultType getType() { return d_type; }
+ ResultType getType() const { return d_type; }
/**
* Returns the optimal value.
* @return Node containing the optimal value,
* if getType() is not OPTIMAL, it might return an empty node or a node
* containing non-optimal value
**/
- Node getValue() { return d_value; }
+ Node getValue() const { return d_value; }
private:
/** the indicating whether the result is optimal or something else **/
~OptimizationObjective() = default;
/** A getter for d_type **/
- ObjectiveType getType() { return d_type; }
+ ObjectiveType getType() const { return d_type; }
/** A getter for d_target **/
- Node getTarget() { return d_target; }
+ Node getTarget() const { return d_target; }
/** A getter for d_bvSigned **/
- bool bvIsSigned() { return d_bvSigned; }
+ bool bvIsSigned() const { return d_bvSigned; }
private:
/**
*
* Lexicographic: optimize the objectives one-by-one, in the order they are
* added:
- * v_x = max(x) s.t. phi(x, y) = sat
+ * 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
OptimizationObjective::ObjectiveType type,
bool bvSigned = false);
- /**
- * Clear all the added optimization objectives
- **/
- void resetObjectives();
-
/**
* Returns the values of the optimized objective after checkOpt is called
* @return a vector of Optimization Result,
std::unique_ptr<SmtEngine> d_optChecker;
/** The objectives to optimize for **/
- std::vector<OptimizationObjective> d_objectives;
+ context::CDList<OptimizationObjective> d_objectives;
/** The results of the optimizations from the last checkOpt call **/
std::vector<OptimizationResult> d_results;
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, (uint32_t)0x3FFFFFA1));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, signed_min)
// expect the minimum x = -1
ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 2u));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, signed_max)
// expect the maxmum x =
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 10u));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteBVOpt, min_boundary)
// expect the maximum x = 18
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, 18u));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
} // namespace test
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("99"));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, min)
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("1"));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, result)
// We expect our check to have returned UNSAT
ASSERT_EQ(r, OptimizationResult::UNSAT);
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, open_interval)
// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("112"));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
} // namespace test
ASSERT_EQ(possibleResults.size(), 0);
}
+TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
+{
+ 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));
+
+ // Lexico optimization
+ OptimizationSolver optSolver(d_smtEngine.get());
+
+ optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
+
+ // minimize x
+ optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
+
+ // push
+ d_smtEngine->push();
+
+ // maximize y with `signed` comparison over bit-vectors.
+ optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
+ // maximize z
+ optSolver.addObjective(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 == 18
+ ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+ // z == 0xFFFFFFFF
+ ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+ BitVector(32u, (unsigned)0xFFFFFFFF));
+
+ // pop
+ d_smtEngine->pop();
+
+ // now we only have one objective: (minimize x)
+ r = optSolver.checkOpt();
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ results = optSolver.getValues();
+ ASSERT_EQ(results.size(), 1);
+ ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+ // resetting the assertions also resets the optimization objectives
+ d_smtEngine->resetAssertions();
+ r = optSolver.checkOpt();
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ results = optSolver.getValues();
+ ASSERT_EQ(results.size(), 0);
+}
+
} // namespace test
} // namespace cvc5
projects / cvc5.git / commitdiff