GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/nl_lemma_utils.cpp Lines: 21 28 75.0 %
Date: 2021-03-23 Branches: 20 48 41.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file nl_lemma_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 the non-linear solver
13
 **/
14
15
#include "theory/arith/nl/nl_lemma_utils.h"
16
17
#include "theory/arith/nl/nl_model.h"
18
#include "theory/arith/nl/nonlinear_extension.h"
19
20
namespace CVC4 {
21
namespace theory {
22
namespace arith {
23
namespace nl {
24
25
TrustNode NlLemma::processLemma(LemmaProperty& p)
26
{
27
  if (d_nlext != nullptr)
28
  {
29
    d_nlext->processSideEffect(*this);
30
  }
31
  return SimpleTheoryLemma::processLemma(p);
32
}
33
34
std::ostream& operator<<(std::ostream& out, NlLemma& n)
35
{
36
  out << n.d_node;
37
  return out;
38
}
39
40
41420
bool SortNlModel::operator()(Node i, Node j)
41
{
42
41420
  int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute);
43
41420
  if (cv == 0)
44
  {
45
7102
    return i < j;
46
  }
47
34318
  return d_reverse_order ? cv < 0 : cv > 0;
48
}
49
50
7985
bool SortNonlinearDegree::operator()(Node i, Node j)
51
{
52
7985
  unsigned i_count = getDegree(i);
53
7985
  unsigned j_count = getDegree(j);
54
7985
  return i_count == j_count ? (i < j) : (i_count < j_count ? true : false);
55
}
56
57
15970
unsigned SortNonlinearDegree::getDegree(Node n) const
58
{
59
15970
  std::map<Node, unsigned>::const_iterator it = d_mdegree.find(n);
60
15970
  Assert(it != d_mdegree.end());
61
15970
  return it->second;
62
}
63
64
3765
Node ArgTrie::add(Node d, const std::vector<Node>& args)
65
{
66
3765
  ArgTrie* at = this;
67
7530
  for (const Node& a : args)
68
  {
69
3765
    at = &(at->d_children[a]);
70
  }
71
3765
  if (at->d_data.isNull())
72
  {
73
3439
    at->d_data = d;
74
  }
75
3765
  return at->d_data;
76
}
77
78
}  // namespace nl
79
}  // namespace arith
80
}  // namespace theory
81
26685
}  // namespace CVC4