GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/optimization_solver.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file optimization_solver.h
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 "cvc4_private.h"
16
17
#ifndef CVC4__SMT__OPTIMIZATION_SOLVER_H
18
#define CVC4__SMT__OPTIMIZATION_SOLVER_H
19
20
#include "expr/node.h"
21
#include "expr/type_node.h"
22
#include "smt/assertions.h"
23
#include "util/result.h"
24
25
namespace CVC4 {
26
27
class SmtEngine;
28
29
namespace smt {
30
31
/**
32
 * An enum for optimization queries.
33
 *
34
 * Represents whether an objective should be minimized or maximized
35
 */
36
enum ObjectiveType
37
{
38
  OBJECTIVE_MINIMIZE,
39
  OBJECTIVE_MAXIMIZE,
40
  OBJECTIVE_UNDEFINED
41
};
42
43
/**
44
 * An enum for optimization queries.
45
 *
46
 * Represents the result of a checkopt query
47
 * (unimplemented) OPT_OPTIMAL: if value was found
48
 */
49
enum OptResult
50
{
51
  // the original set of assertions has result UNKNOWN
52
  OPT_UNKNOWN,
53
  // the original set of assertions has result UNSAT
54
  OPT_UNSAT,
55
  // the optimization loop finished and optimal
56
  OPT_OPTIMAL,
57
58
  // The last value is here as a preparation for future work
59
  // in which pproximate optimizations will be supported.
60
61
  // if the solver halted early and value is only approximate
62
  OPT_SAT_APPROX
63
};
64
65
6
class Objective
66
{
67
 public:
68
  Objective(Node n, ObjectiveType type);
69
12
  ~Objective(){};
70
71
  /** A getter for d_type **/
72
  ObjectiveType getType();
73
  /** A getter for d_node **/
74
  Node getNode();
75
76
 private:
77
  /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
78
   * OBJECTIVE_MINIMIZE  **/
79
  ObjectiveType d_type;
80
  /** The node associated to the term that was used to construct the objective.
81
   * **/
82
  Node d_node;
83
  };
84
85
  /**
86
   * A solver for optimization queries.
87
   *
88
   * This class is responsible for responding to optmization queries. It
89
   * spawns a subsolver SmtEngine that captures the parent assertions and
90
   * implements a linear optimization loop. Supports activateObjective,
91
   * checkOpt, and objectiveGetValue in that order.
92
   */
93
  class OptimizationSolver
94
  {
95
   public:
96
    /** parent is the smt_solver that the user added their assertions to **/
97
    OptimizationSolver(SmtEngine* parent);
98
    ~OptimizationSolver();
99
100
    /** Runs the optimization loop for the activated objective **/
101
    OptResult checkOpt();
102
    /** Activates an objective: will be optimized for **/
103
    void activateObj(const Node& obj, const int& type);
104
    /** Gets the value of the optimized objective after checkopt is called **/
105
    Node objectiveGetValue();
106
107
   private:
108
    /** The parent SMT engine **/
109
    SmtEngine* d_parent;
110
    /** The objectives to optimize for **/
111
    Objective d_activatedObjective;
112
    /** A saved value of the objective from the last sat call. **/
113
    Node d_savedValue;
114
  };
115
116
}  // namespace smt
117
}  // namespace CVC4
118
119
#endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */