GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext_theory_callback.cpp Lines: 45 49 91.8 %
Date: 2021-03-23 Branches: 93 194 47.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ext_theory_callback.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Tianyi Liang
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 extended theory callback for non-linear arithmetic
13
 **/
14
15
#include "theory/arith/nl/ext_theory_callback.h"
16
17
#include "theory/arith/arith_utilities.h"
18
#include "theory/uf/equality_engine.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
namespace nl {
26
27
4391
NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee)
28
{
29
4391
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
30
4391
}
31
32
3893
bool NlExtTheoryCallback::getCurrentSubstitution(
33
    int effort,
34
    const std::vector<Node>& vars,
35
    std::vector<Node>& subs,
36
    std::map<Node, std::vector<Node>>& exp)
37
{
38
  // get the constant equivalence classes
39
7786
  std::map<Node, std::vector<int>> rep_to_subs_index;
40
41
3893
  bool retVal = false;
42
24910
  for (unsigned i = 0; i < vars.size(); i++)
43
  {
44
42034
    Node n = vars[i];
45
21017
    if (d_ee->hasTerm(n))
46
    {
47
29706
      Node nr = d_ee->getRepresentative(n);
48
14853
      if (nr.isConst())
49
      {
50
2823
        subs.push_back(nr);
51
5646
        Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr
52
2823
                         << std::endl;
53
2823
        exp[n].push_back(n.eqNode(nr));
54
2823
        retVal = true;
55
      }
56
      else
57
      {
58
12030
        rep_to_subs_index[nr].push_back(i);
59
12030
        subs.push_back(n);
60
      }
61
    }
62
    else
63
    {
64
6164
      subs.push_back(n);
65
    }
66
  }
67
68
  // return true if the substitution is non-trivial
69
7786
  return retVal;
70
}
71
72
4596
bool NlExtTheoryCallback::isExtfReduced(int effort,
73
                                        Node n,
74
                                        Node on,
75
                                        std::vector<Node>& exp)
76
{
77
4596
  if (n != d_zero)
78
  {
79
2892
    Kind k = n.getKind();
80
2892
    return k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND;
81
  }
82
1704
  Assert(n == d_zero);
83
1704
  if (on.getKind() == NONLINEAR_MULT)
84
  {
85
3088
    Trace("nl-ext-zero-exp")
86
1544
        << "Infer zero : " << on << " == " << n << std::endl;
87
    // minimize explanation if a substitution+rewrite results in zero
88
1544
    const std::set<Node> vars(on.begin(), on.end());
89
90
1724
    for (unsigned i = 0, size = exp.size(); i < size; i++)
91
    {
92
3448
      Trace("nl-ext-zero-exp")
93
1724
          << "  exp[" << i << "] = " << exp[i] << std::endl;
94
1904
      std::vector<Node> eqs;
95
1724
      if (exp[i].getKind() == EQUAL)
96
      {
97
1724
        eqs.push_back(exp[i]);
98
      }
99
      else if (exp[i].getKind() == AND)
100
      {
101
        for (const Node& ec : exp[i])
102
        {
103
          if (ec.getKind() == EQUAL)
104
          {
105
            eqs.push_back(ec);
106
          }
107
        }
108
      }
109
110
1904
      for (unsigned j = 0; j < eqs.size(); j++)
111
      {
112
3628
        for (unsigned r = 0; r < 2; r++)
113
        {
114
3448
          if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end())
115
          {
116
3088
            Trace("nl-ext-zero-exp")
117
1544
                << "...single exp : " << eqs[j] << std::endl;
118
1544
            exp.clear();
119
1544
            exp.push_back(eqs[j]);
120
1544
            return true;
121
          }
122
        }
123
      }
124
    }
125
  }
126
160
  return true;
127
}
128
129
}  // namespace nl
130
}  // namespace arith
131
}  // namespace theory
132
26685
}  // namespace CVC4