summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/omt/integer_optimizer.h9
-rw-r--r--src/omt/omt_optimizer.cpp16
-rw-r--r--src/omt/omt_optimizer.h6
-rw-r--r--src/smt/optimization_solver.cpp20
-rw-r--r--src/smt/optimization_solver.h21
-rw-r--r--test/unit/theory/theory_bv_opt_white.cpp10
-rw-r--r--test/unit/theory/theory_int_opt_white.cpp8
-rw-r--r--test/unit/theory/theory_opt_multigoal_white.cpp64
8 files changed, 108 insertions, 46 deletions
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h
index 34605cc71..0b62c0816 100644
--- a/src/omt/integer_optimizer.h
+++ b/src/omt/integer_optimizer.h
@@ -36,13 +36,12 @@ class OMTOptimizerInteger : public OMTOptimizer
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
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
index 08f1809ec..2145492db 100644
--- a/src/omt/omt_optimizer.cpp
+++ b/src/omt/omt_optimizer.cpp
@@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node)
}
std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
- OptimizationObjective& objective)
+ const OptimizationObjective& objective)
{
// the datatype of the target node
TypeNode objectiveType = objective.getTarget().getType(true);
@@ -53,7 +53,10 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
}
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 "
@@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression(
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 "
diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h
index 1052865b0..1e8d9e763 100644
--- a/src/omt/omt_optimizer.h
+++ b/src/omt/omt_optimizer.h
@@ -46,7 +46,7 @@ class OMTOptimizer
* 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,
@@ -70,7 +70,7 @@ class OMTOptimizer
NodeManager* nm,
TNode lhs,
TNode rhs,
- smt::OptimizationObjective& objective);
+ const smt::OptimizationObjective& objective);
/**
* Given the lhs and rhs expressions, with an optimization objective,
@@ -94,7 +94,7 @@ class OMTOptimizer
NodeManager* nm,
TNode lhs,
TNode rhs,
- smt::OptimizationObjective& objective);
+ const smt::OptimizationObjective& objective);
/**
* Minimize the target node with constraints encoded in optChecker
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index ffc49710a..e85ea82ef 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -15,6 +15,8 @@
#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"
@@ -29,7 +31,7 @@ namespace smt {
OptimizationSolver::OptimizationSolver(SmtEngine* parent)
: d_parent(parent),
d_optChecker(),
- d_objectives(),
+ d_objectives(parent->getUserContext()),
d_results(),
d_objectiveCombination(LEXICOGRAPHIC)
{
@@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
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)
{
@@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target,
}
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()
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 64591d8f1..6d138deb2 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -18,6 +18,8 @@
#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"
@@ -74,14 +76,14 @@ class OptimizationResult
* @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 **/
@@ -124,13 +126,13 @@ class OptimizationObjective
~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:
/**
@@ -173,7 +175,7 @@ class OptimizationSolver
*
* 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
@@ -215,11 +217,6 @@ class OptimizationSolver
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,
* each containing the outcome and the value.
@@ -293,7 +290,7 @@ class OptimizationSolver
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;
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 66efe7eff..c23ce79dd 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
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)
@@ -87,7 +87,7 @@ 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)
@@ -114,7 +114,7 @@ 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)
@@ -137,7 +137,7 @@ 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)
@@ -161,7 +161,7 @@ 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
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index f16db0c0e..cf0434ddc 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max)
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
Rational("99"));
- d_optslv->resetObjectives();
+ d_smtEngine->resetAssertions();
}
TEST_F(TestTheoryWhiteIntOpt, min)
@@ -101,7 +101,7 @@ 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)
@@ -129,7 +129,7 @@ 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)
@@ -164,7 +164,7 @@ 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
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 1950d9ae2..73c6d9e7e 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -240,5 +240,69 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback