GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/strategy.cpp Lines: 55 97 56.7 %
Date: 2021-03-23 Branches: 87 254 34.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file strategy.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds
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 Implementation of non-linear solver
13
 **/
14
15
#include "theory/arith/nl/strategy.h"
16
17
#include <iostream>
18
19
#include "base/check.h"
20
#include "options/arith_options.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
namespace nl {
26
27
std::ostream& operator<<(std::ostream& os, InferStep step)
28
{
29
  switch (step)
30
  {
31
    case InferStep::BREAK: return os << "BREAK";
32
    case InferStep::FLUSH_WAITING_LEMMAS: return os << "FLUSH_WAITING_LEMMAS";
33
    case InferStep::CAD_INIT: return os << "CAD_INIT";
34
    case InferStep::CAD_FULL: return os << "CAD_FULL";
35
    case InferStep::NL_FACTORING: return os << "NL_FACTORING";
36
    case InferStep::IAND_INIT: return os << "IAND_INIT";
37
    case InferStep::IAND_FULL: return os << "IAND_FULL";
38
    case InferStep::IAND_INITIAL: return os << "IAND_INITIAL";
39
    case InferStep::ICP: return os << "ICP";
40
    case InferStep::NL_INIT: return os << "NL_INIT";
41
    case InferStep::NL_MONOMIAL_INFER_BOUNDS:
42
      return os << "NL_MONOMIAL_INFER_BOUNDS";
43
    case InferStep::NL_MONOMIAL_MAGNITUDE0:
44
      return os << "NL_MONOMIAL_MAGNITUDE0";
45
    case InferStep::NL_MONOMIAL_MAGNITUDE1:
46
      return os << "NL_MONOMIAL_MAGNITUDE1";
47
    case InferStep::NL_MONOMIAL_MAGNITUDE2:
48
      return os << "NL_MONOMIAL_MAGNITUDE2";
49
    case InferStep::NL_MONOMIAL_SIGN: return os << "NL_MONOMIAL_SIGN";
50
    case InferStep::NL_RESOLUTION_BOUNDS: return os << "NL_RESOLUTION_BOUNDS";
51
    case InferStep::NL_SPLIT_ZERO: return os << "NL_SPLIT_ZERO";
52
    case InferStep::NL_TANGENT_PLANES: return os << "NL_TANGENT_PLANES";
53
    case InferStep::NL_TANGENT_PLANES_WAITING:
54
      return os << "NL_TANGENT_PLANES_WAITING";
55
    case InferStep::TRANS_INIT: return os << "TRANS_INIT";
56
    case InferStep::TRANS_INITIAL: return os << "TRANS_INITIAL";
57
    case InferStep::TRANS_MONOTONIC: return os << "TRANS_MONOTONIC";
58
    case InferStep::TRANS_TANGENT_PLANES: return os << "TRANS_TANGENT_PLANES";
59
    default: Unreachable(); return os << "UNKNOWN_STEP";
60
  }
61
}
62
63
namespace {
64
/** Puts a new InferStep into a StepSequence */
65
11422
inline StepSequence& operator<<(StepSequence& steps, InferStep s)
66
{
67
11422
  steps.emplace_back(s);
68
11422
  return steps;
69
}
70
}  // namespace
71
72
405
void Interleaving::add(const StepSequence& ss, std::size_t constant)
73
{
74
405
  d_branches.emplace_back(Branch{ss, constant});
75
405
  d_size += constant;
76
405
}
77
void Interleaving::resetCounter() { d_counter = 0; }
78
79
2742
const StepSequence& Interleaving::get()
80
{
81
2742
  Assert(!d_branches.empty())
82
      << "Can not get next sequence from an empty interleaving.";
83
2742
  std::size_t cnt = d_counter;
84
  // Increase the counter
85
2742
  d_counter = (d_counter + 1) % d_size;
86
2742
  for (const auto& branch : d_branches)
87
  {
88
2742
    if (cnt < branch.d_interleavingConstant)
89
    {
90
      // This is the current branch
91
2742
      return branch.d_steps;
92
    }
93
    cnt -= branch.d_interleavingConstant;
94
  }
95
  Assert(false) << "Something went wrong.";
96
  return d_branches[0].d_steps;
97
}
98
2742
bool Interleaving::empty() const { return d_branches.empty(); }
99
100
38708
bool StepGenerator::hasNext() const { return d_next < d_steps.size(); }
101
38484
InferStep StepGenerator::next() { return d_steps[d_next++]; }
102
103
2742
bool Strategy::isStrategyInit() const { return !d_interleaving.empty(); }
104
405
void Strategy::initializeStrategy()
105
{
106
810
  StepSequence one;
107
810
  if (options::nlICP())
108
  {
109
    one << InferStep::ICP << InferStep::BREAK;
110
  }
111
405
  if (options::nlExt())
112
  {
113
405
    one << InferStep::NL_INIT << InferStep::TRANS_INIT << InferStep::BREAK;
114
810
    if (options::nlExtSplitZero())
115
    {
116
      one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK;
117
    }
118
405
    one << InferStep::TRANS_INITIAL << InferStep::BREAK;
119
  }
120
405
  one << InferStep::IAND_INIT;
121
405
  one << InferStep::IAND_INITIAL << InferStep::BREAK;
122
405
  if (options::nlExt())
123
  {
124
405
    one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK;
125
405
    one << InferStep::TRANS_MONOTONIC << InferStep::BREAK;
126
405
    one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK;
127
405
    one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK;
128
405
    one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK;
129
405
    one << InferStep::NL_MONOMIAL_INFER_BOUNDS;
130
810
    if (options::nlExtTangentPlanes()
131
405
        && options::nlExtTangentPlanesInterleave())
132
    {
133
      one << InferStep::NL_TANGENT_PLANES;
134
    }
135
405
    one << InferStep::BREAK;
136
405
    one << InferStep::FLUSH_WAITING_LEMMAS << InferStep::BREAK;
137
810
    if (options::nlExtFactor())
138
    {
139
405
      one << InferStep::NL_FACTORING << InferStep::BREAK;
140
    }
141
810
    if (options::nlExtResBound())
142
    {
143
      one << InferStep::NL_MONOMIAL_INFER_BOUNDS << InferStep::BREAK;
144
    }
145
810
    if (options::nlExtTangentPlanes()
146
405
        && !options::nlExtTangentPlanesInterleave())
147
    {
148
84
      one << InferStep::NL_TANGENT_PLANES_WAITING;
149
    }
150
896
    if (options::nlExtTfTangentPlanes())
151
    {
152
403
      one << InferStep::TRANS_TANGENT_PLANES;
153
    }
154
405
    one << InferStep::BREAK;
155
  }
156
405
  one << InferStep::IAND_FULL << InferStep::BREAK;
157
405
  if (options::nlCad())
158
  {
159
    one << InferStep::CAD_INIT;
160
  }
161
405
  if (options::nlCad())
162
  {
163
    one << InferStep::CAD_FULL << InferStep::BREAK;
164
  }
165
166
405
  d_interleaving.add(one);
167
405
}
168
2742
StepGenerator Strategy::getStrategy()
169
{
170
2742
  return StepGenerator(d_interleaving.get());
171
}
172
173
}  // namespace nl
174
}  // namespace arith
175
}  // namespace theory
176
28796
}  // namespace CVC4