GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/omt/integer_optimizer.cpp Lines: 28 28 100.0 %
Date: 2021-09-15 Branches: 39 82 47.6 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Michael Chang, Yancheng Ou
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * Optimizer for Integer type.
14
 */
15
16
#include "omt/integer_optimizer.h"
17
18
#include "options/smt_options.h"
19
#include "smt/smt_engine.h"
20
21
using namespace cvc5::smt;
22
namespace cvc5::omt {
23
24
8
OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
25
                                                 TNode target,
26
                                                 bool isMinimize)
27
{
28
  // linear search for integer goal
29
  // the smt engine to which we send intermediate queries
30
  // for the linear search.
31
8
  NodeManager* nm = optChecker->getNodeManager();
32
8
  optChecker->push();
33
16
  Result intermediateSatResult = optChecker->checkSat();
34
  // Model-value of objective (used in optimization loop)
35
16
  Node value;
36
16
  if (intermediateSatResult.isUnknown()
37
8
      || intermediateSatResult.isSat() == Result::UNSAT)
38
  {
39
2
    return OptimizationResult(intermediateSatResult, value);
40
  }
41
  // node storing target > old_value (used in optimization loop)
42
12
  Node increment;
43
6
  Kind incrementalOperator = kind::NULL_EXPR;
44
6
  if (isMinimize)
45
  {
46
    // if objective is minimize,
47
    // then assert optimization_target < current_model_value
48
4
    incrementalOperator = kind::LT;
49
  }
50
  else
51
  {
52
    // if objective is maximize,
53
    // then assert optimization_target > current_model_value
54
2
    incrementalOperator = kind::GT;
55
  }
56
12
  Result lastSatResult = intermediateSatResult;
57
  // Workhorse of linear search:
58
  // This loop will keep incrmenting/decrementing the objective until unsat
59
  // When unsat is hit,
60
  // the optimized value is the model value just before the unsat call
61
410
  while (intermediateSatResult.isSat() == Result::SAT)
62
  {
63
202
    lastSatResult = intermediateSatResult;
64
202
    value = optChecker->getValue(target);
65
202
    Assert(!value.isNull());
66
202
    increment = nm->mkNode(incrementalOperator, target, value);
67
202
    optChecker->assertFormula(increment);
68
202
    intermediateSatResult = optChecker->checkSat();
69
  }
70
6
  optChecker->pop();
71
6
  return OptimizationResult(lastSatResult, value);
72
}
73
74
4
OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker,
75
                                                 TNode target)
76
{
77
4
  return this->optimize(optChecker, target, true);
78
}
79
4
OptimizationResult OMTOptimizerInteger::maximize(SmtEngine* optChecker,
80
                                                 TNode target)
81
{
82
4
  return this->optimize(optChecker, target, false);
83
}
84
85
29577
}  // namespace cvc5::omt