GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/tangent_plane_check.cpp Lines: 72 73 98.6 %
Date: 2021-03-22 Branches: 189 352 53.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tangent_plane_check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Andrew Reynolds, Tim King
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 tangent_plane check
13
 **/
14
15
#include "theory/arith/nl/ext/tangent_plane_check.h"
16
17
#include "expr/node.h"
18
#include "expr/proof.h"
19
#include "theory/arith/arith_msum.h"
20
#include "theory/arith/inference_manager.h"
21
#include "theory/arith/nl/nl_model.h"
22
#include "theory/arith/nl/ext/ext_state.h"
23
#include "theory/rewriter.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace arith {
28
namespace nl {
29
30
4389
TangentPlaneCheck::TangentPlaneCheck(ExtState* data) : d_data(data) {}
31
32
15
void TangentPlaneCheck::check(bool asWaitingLemmas)
33
{
34
15
  Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
35
15
  NodeManager* nm = NodeManager::currentNM();
36
  const std::map<Node, std::vector<Node> >& ccMap =
37
15
      d_data->d_mdb.getContainsChildrenMap();
38
15
  unsigned kstart = d_data->d_ms_vars.size();
39
78
  for (unsigned k = kstart; k < d_data->d_mterms.size(); k++)
40
  {
41
91
    Node t = d_data->d_mterms[k];
42
    // if this term requires a refinement
43
63
    if (d_data->d_tplane_refine.find(t) == d_data->d_tplane_refine.end())
44
    {
45
35
      continue;
46
    }
47
56
    Trace("nl-ext-tplanes")
48
28
        << "Look at monomial requiring refinement : " << t << std::endl;
49
    // get a decomposition
50
28
    std::map<Node, std::vector<Node> >::const_iterator it = ccMap.find(t);
51
28
    if (it == ccMap.end())
52
    {
53
      continue;
54
    }
55
56
    std::map<Node, std::map<Node, bool> > dproc;
56
94
    for (unsigned j = 0; j < it->second.size(); j++)
57
    {
58
132
      Node tc = it->second[j];
59
66
      if (tc != d_data->d_one)
60
      {
61
76
        Node tc_diff = d_data->d_mdb.getContainsDiffNl(tc, t);
62
38
        Assert(!tc_diff.isNull());
63
76
        Node a = tc < tc_diff ? tc : tc_diff;
64
76
        Node b = tc < tc_diff ? tc_diff : tc;
65
38
        if (dproc[a].find(b) == dproc[a].end())
66
        {
67
28
          dproc[a][b] = true;
68
56
          Trace("nl-ext-tplanes")
69
28
              << "  decomposable into : " << a << " * " << b << std::endl;
70
56
          Node a_v_c = d_data->d_model.computeAbstractModelValue(a);
71
56
          Node b_v_c = d_data->d_model.computeAbstractModelValue(b);
72
          // points we will add tangent planes for
73
56
          std::vector<Node> pts[2];
74
28
          pts[0].push_back(a_v_c);
75
28
          pts[1].push_back(b_v_c);
76
          // if previously refined
77
56
          bool prevRefine = d_tangent_val_bound[0][a].find(b)
78
84
                            != d_tangent_val_bound[0][a].end();
79
          // a_min, a_max, b_min, b_max
80
140
          for (unsigned p = 0; p < 4; p++)
81
          {
82
224
            Node curr_v = p <= 1 ? a_v_c : b_v_c;
83
112
            if (prevRefine)
84
            {
85
48
              Node pt_v = d_tangent_val_bound[p][a][b];
86
24
              Assert(!pt_v.isNull());
87
24
              if (curr_v != pt_v)
88
              {
89
                Node do_extend = nm->mkNode(
90
48
                    (p == 1 || p == 3) ? Kind::GT : Kind::LT, curr_v, pt_v);
91
24
                do_extend = Rewriter::rewrite(do_extend);
92
24
                if (do_extend == d_data->d_true)
93
                {
94
36
                  for (unsigned q = 0; q < 2; q++)
95
                  {
96
24
                    pts[p <= 1 ? 0 : 1].push_back(curr_v);
97
48
                    pts[p <= 1 ? 1 : 0].push_back(
98
24
                        d_tangent_val_bound[p <= 1 ? 2 + q : q][a][b]);
99
                  }
100
                }
101
              }
102
            }
103
            else
104
            {
105
88
              d_tangent_val_bound[p][a][b] = curr_v;
106
            }
107
          }
108
109
80
          for (unsigned p = 0; p < pts[0].size(); p++)
110
          {
111
104
            Node a_v = pts[0][p];
112
104
            Node b_v = pts[1][p];
113
114
            // tangent plane
115
            Node tplane = nm->mkNode(Kind::MINUS,
116
208
                                     nm->mkNode(Kind::PLUS,
117
104
                                                nm->mkNode(Kind::MULT, b_v, a),
118
104
                                                nm->mkNode(Kind::MULT, a_v, b)),
119
208
                                     nm->mkNode(Kind::MULT, a_v, b_v));
120
            // construct the following lemmas:
121
            // t <= tplane  <=>  ((a <= a_v ^ b >= b_v) v (a >= a_v ^ b <= b_v))
122
            // t >= tplane  <=>  ((a <= a_v ^ b <= b_v) v (a >= a_v ^ b >= b_v))
123
124
156
            for (unsigned d = 0; d < 2; d++)
125
            {
126
208
              Node b1 = nm->mkNode(d == 0 ? Kind::GEQ : Kind::LEQ, b, b_v);
127
208
              Node b2 = nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, b, b_v);
128
              Node tlem = nm->mkNode(
129
                  Kind::EQUAL,
130
208
                  nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, t, tplane),
131
416
                  nm->mkNode(
132
                      Kind::OR,
133
208
                      nm->mkNode(Kind::AND, nm->mkNode(Kind::LEQ, a, a_v), b1),
134
416
                      nm->mkNode(
135
624
                          Kind::AND, nm->mkNode(Kind::GEQ, a, a_v), b2)));
136
208
              Trace("nl-ext-tplanes")
137
104
                  << "Tangent plane lemma : " << tlem << std::endl;
138
104
              CDProof* proof = nullptr;
139
104
              if (d_data->isProofEnabled())
140
              {
141
14
                proof = d_data->getProof();
142
112
                proof->addStep(tlem,
143
                               PfRule::ARITH_MULT_TANGENT,
144
                               {},
145
                               {t,
146
                                a,
147
                                b,
148
                                a_v,
149
                                b_v,
150
112
                                nm->mkConst(Rational(d == 0 ? -1 : 1))});
151
              }
152
104
              d_data->d_im.addPendingLemma(tlem,
153
                                           InferenceId::ARITH_NL_TANGENT_PLANE,
154
                                           proof,
155
                                           asWaitingLemmas);
156
            }
157
          }
158
        }
159
      }
160
    }
161
  }
162
15
}
163
164
}  // namespace nl
165
}  // namespace arith
166
}  // namespace theory
167
26676
}  // namespace CVC4