GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/optimization_solver.cpp Lines: 43 44 97.7 %
Date: 2021-03-22 Branches: 57 156 36.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file optimization_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Michael Chang
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The solver for optimization queries
13
 **/
14
15
#include "smt/optimization_solver.h"
16
17
#include "options/smt_options.h"
18
#include "smt/smt_engine.h"
19
#include "theory/quantifiers/quantifiers_attributes.h"
20
#include "theory/smt_engine_subsolver.h"
21
22
using namespace CVC4::theory;
23
24
namespace CVC4 {
25
namespace smt {
26
27
/**
28
 * d_activatedObjective is initialized to a default objective:
29
 * default objective constructed with Null Node and OBJECTIVE_UNDEFINED
30
 *
31
 * d_savedValue is initialized to a default node (Null Node)
32
 */
33
34
6
OptimizationSolver::OptimizationSolver(SmtEngine* parent)
35
    : d_parent(parent),
36
12
      d_activatedObjective(Node(), OBJECTIVE_UNDEFINED),
37
18
      d_savedValue()
38
{
39
6
}
40
41
6
OptimizationSolver::~OptimizationSolver() {}
42
43
6
OptResult OptimizationSolver::checkOpt()
44
{
45
  // Make sure that the objective is not the default one
46
6
  Assert(d_activatedObjective.getType() != OBJECTIVE_UNDEFINED);
47
6
  Assert(!d_activatedObjective.getNode().isNull());
48
49
  // the smt engine to which we send intermediate queries
50
  // for the linear search.
51
12
  std::unique_ptr<SmtEngine> optChecker;
52
6
  initializeSubsolver(optChecker);
53
6
  NodeManager* nm = optChecker->getNodeManager();
54
55
  // we need to be in incremental mode for multiple objectives since we need to
56
  // push pop we need to produce models to inrement on our objective
57
6
  optChecker->setOption("incremental", "true");
58
6
  optChecker->setOption("produce-models", "true");
59
60
  // Move assertions from the parent solver to the subsolver
61
12
  std::vector<Node> p_assertions = d_parent->getExpandedAssertions();
62
18
  for (const Node& e : p_assertions)
63
  {
64
12
    optChecker->assertFormula(e);
65
  }
66
67
  // We need to checksat once before the optimization loop so we have a
68
  // baseline value to increment
69
12
  Result loop_r = optChecker->checkSat();
70
71
6
  if (loop_r.isUnknown())
72
  {
73
    return OPT_UNKNOWN;
74
  }
75
6
  if (!loop_r.isSat())
76
  {
77
2
    return OPT_UNSAT;
78
  }
79
80
  // Model-value of objective (used in optimization loop)
81
8
  Node value;
82
  // asserts objective > old_value (used in optimization loop)
83
8
  Node increment;
84
85
  // Workhorse of linear optimization:
86
  // This loop will keep incrmenting the objective until unsat
87
  // When unsat is hit, the optimized value is the model value just before the
88
  // unsat call
89
404
  while (loop_r.isSat())
90
  {
91
    // get the model-value of objective in last sat call
92
200
    value = optChecker->getValue(d_activatedObjective.getNode());
93
94
    // We need to save the value since we need the model value just before the
95
    // unsat call
96
200
    Assert(!value.isNull());
97
200
    d_savedValue = value;
98
99
    // increment on the model-value of objective:
100
    // if we're maximizing increment = objective > old_objective value
101
    // if we're minimizing increment = objective < old_objective value
102
200
    if (d_activatedObjective.getType() == OBJECTIVE_MAXIMIZE)
103
    {
104
198
      increment = nm->mkNode(kind::GT, d_activatedObjective.getNode(), value);
105
    }
106
    else
107
    {
108
2
      increment = nm->mkNode(kind::LT, d_activatedObjective.getNode(), value);
109
    }
110
200
    optChecker->assertFormula(increment);
111
200
    loop_r = optChecker->checkSat();
112
  }
113
114
4
  return OPT_OPTIMAL;
115
}
116
117
6
void OptimizationSolver::activateObj(const Node& obj, const int& type)
118
{
119
6
  d_activatedObjective = Objective(obj, (ObjectiveType)type);
120
6
}
121
122
8
Node OptimizationSolver::objectiveGetValue()
123
{
124
8
  Assert(!d_savedValue.isNull());
125
8
  return d_savedValue;
126
}
127
128
12
Objective::Objective(Node obj, ObjectiveType type) : d_type(type), d_node(obj)
129
{
130
12
}
131
132
206
ObjectiveType Objective::getType() { return d_type; }
133
134
406
Node Objective::getNode() { return d_node; }
135
136
}  // namespace smt
137
26676
}  // namespace CVC4