GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/arith_preprocess.cpp Lines: 7 28 25.0 %
Date: 2021-03-23 Branches: 6 82 7.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_preprocess.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 Arithmetic preprocess
13
 **/
14
15
#include "theory/arith/arith_preprocess.h"
16
17
#include "theory/arith/arith_state.h"
18
#include "theory/arith/inference_manager.h"
19
#include "theory/skolem_lemma.h"
20
21
namespace CVC4 {
22
namespace theory {
23
namespace arith {
24
25
8997
ArithPreprocess::ArithPreprocess(ArithState& state,
26
                                 InferenceManager& im,
27
                                 ProofNodeManager* pnm,
28
8997
                                 const LogicInfo& info)
29
8997
    : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
30
{
31
8997
}
32
698058
TrustNode ArithPreprocess::eliminate(TNode n,
33
                                     std::vector<SkolemLemma>& lems,
34
                                     bool partialOnly)
35
{
36
698058
  return d_opElim.eliminate(n, lems, partialOnly);
37
}
38
39
bool ArithPreprocess::reduceAssertion(TNode atom)
40
{
41
  context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
42
      d_reduced.find(atom);
43
  if (it != d_reduced.end())
44
  {
45
    // already computed
46
    return (*it).second;
47
  }
48
  std::vector<SkolemLemma> lems;
49
  TrustNode tn = eliminate(atom, lems);
50
  for (const SkolemLemma& lem : lems)
51
  {
52
    d_im.trustedLemma(lem.d_lemma, InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA);
53
  }
54
  if (tn.isNull())
55
  {
56
    // did not reduce
57
    d_reduced[atom] = false;
58
    return false;
59
  }
60
  Assert(tn.getKind() == TrustNodeKind::REWRITE);
61
  // tn is of kind REWRITE, turn this into a LEMMA here
62
  TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
63
  // send the trusted lemma
64
  d_im.trustedLemma(tlem, InferenceId::ARITH_PP_ELIM_OPERATORS);
65
  // mark the atom as reduced
66
  d_reduced[atom] = true;
67
  return true;
68
}
69
70
bool ArithPreprocess::isReduced(TNode atom) const
71
{
72
  context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
73
      d_reduced.find(atom);
74
  if (it == d_reduced.end())
75
  {
76
    return false;
77
  }
78
  return (*it).second;
79
}
80
81
}  // namespace arith
82
}  // namespace theory
83
26685
}  // namespace CVC4