GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/ext/constraint.cpp Lines: 53 55 96.4 %
Date: 2021-03-22 Branches: 87 180 48.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file constraint.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 utilities for non-linear constraints
13
 **/
14
15
#include "theory/arith/nl/ext/constraint.h"
16
17
#include "theory/arith/arith_msum.h"
18
#include "theory/arith/arith_utilities.h"
19
#include "theory/arith/nl/ext/monomial.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace arith {
26
namespace nl {
27
28
4389
ConstraintDb::ConstraintDb(MonomialDb& mdb) : d_mdb(mdb) {}
29
30
34933
void ConstraintDb::registerConstraint(Node atom)
31
{
32
104799
  if (std::find(d_constraints.begin(), d_constraints.end(), atom)
33
104799
      != d_constraints.end())
34
  {
35
23886
    return;
36
  }
37
11047
  d_constraints.push_back(atom);
38
11047
  Trace("nl-ext-debug") << "Register constraint : " << atom << std::endl;
39
22094
  std::map<Node, Node> msum;
40
11047
  if (ArithMSum::getMonomialSumLit(atom, msum))
41
  {
42
11047
    Trace("nl-ext-debug") << "got monomial sum: " << std::endl;
43
11047
    if (Trace.isOn("nl-ext-debug"))
44
    {
45
      ArithMSum::debugPrintMonomialSum(msum, "nl-ext-debug");
46
    }
47
11047
    unsigned max_degree = 0;
48
22094
    std::vector<Node> all_m;
49
22094
    std::vector<Node> max_deg_m;
50
34803
    for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
51
         ++itm)
52
    {
53
23756
      if (!itm->first.isNull())
54
      {
55
19612
        all_m.push_back(itm->first);
56
19612
        d_mdb.registerMonomial(itm->first);
57
39224
        Trace("nl-ext-debug2")
58
19612
            << "...process monomial " << itm->first << std::endl;
59
19612
        unsigned d = d_mdb.getDegree(itm->first);
60
19612
        if (d > max_degree)
61
        {
62
13483
          max_degree = d;
63
13483
          max_deg_m.clear();
64
        }
65
19612
        if (d >= max_degree)
66
        {
67
19471
          max_deg_m.push_back(itm->first);
68
        }
69
      }
70
    }
71
    // isolate for each maximal degree monomial
72
30659
    for (unsigned i = 0; i < all_m.size(); i++)
73
    {
74
39224
      Node m = all_m[i];
75
39224
      Node rhs, coeff;
76
19612
      int res = ArithMSum::isolate(m, msum, coeff, rhs, atom.getKind());
77
19612
      if (res != 0)
78
      {
79
19612
        Kind type = atom.getKind();
80
19612
        if (res == -1)
81
        {
82
5280
          type = reverseRelationKind(type);
83
        }
84
19612
        Trace("nl-ext-constraint") << "Constraint : " << atom << " <=> ";
85
19612
        if (!coeff.isNull())
86
        {
87
516
          Trace("nl-ext-constraint") << coeff << " * ";
88
        }
89
39224
        Trace("nl-ext-constraint")
90
19612
            << m << " " << type << " " << rhs << std::endl;
91
19612
        ConstraintInfo& ci = d_c_info[atom][m];
92
19612
        ci.d_rhs = rhs;
93
19612
        ci.d_coeff = coeff;
94
19612
        ci.d_type = type;
95
      }
96
    }
97
27592
    for (unsigned i = 0; i < max_deg_m.size(); i++)
98
    {
99
33090
      Node m = max_deg_m[i];
100
16545
      d_c_info_maxm[atom][m] = true;
101
    }
102
  }
103
  else
104
  {
105
    Trace("nl-ext-debug") << "...failed to get monomial sum." << std::endl;
106
  }
107
}
108
109
const std::map<Node, std::map<Node, ConstraintInfo> >&
110
520
ConstraintDb::getConstraints()
111
{
112
520
  return d_c_info;
113
}
114
115
63577
bool ConstraintDb::isMaximal(Node atom, Node x) const
116
{
117
  std::map<Node, std::map<Node, bool> >::const_iterator itcm =
118
63577
      d_c_info_maxm.find(atom);
119
63577
  Assert(itcm != d_c_info_maxm.end());
120
63577
  return itcm->second.find(x) != itcm->second.end();
121
}
122
123
}  // namespace nl
124
}  // namespace arith
125
}  // namespace theory
126
26676
}  // namespace CVC4