GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/proof_checker.cpp Lines: 5 19 26.3 %
Date: 2021-03-23 Branches: 2 104 1.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner
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 bit-vectors proof checker
13
 **/
14
15
#include "theory/bv/proof_checker.h"
16
17
namespace CVC4 {
18
namespace theory {
19
namespace bv {
20
21
1
void BVProofRuleChecker::registerTo(ProofChecker* pc)
22
{
23
1
  pc->registerChecker(PfRule::BV_BITBLAST, this);
24
1
  pc->registerChecker(PfRule::BV_EAGER_ATOM, this);
25
1
}
26
27
Node BVProofRuleChecker::checkInternal(PfRule id,
28
                                       const std::vector<Node>& children,
29
                                       const std::vector<Node>& args)
30
{
31
  if (id == PfRule::BV_BITBLAST)
32
  {
33
    BBSimple bb(nullptr);
34
    Assert(children.empty());
35
    Assert(args.size() == 1);
36
    bb.bbAtom(args[0]);
37
    Node n = bb.getStoredBBAtom(args[0]);
38
    return args[0].eqNode(n);
39
  }
40
  else if (id == PfRule::BV_EAGER_ATOM)
41
  {
42
    Assert(children.empty());
43
    Assert(args.size() == 1);
44
    Assert(args[0].getKind() == kind::BITVECTOR_EAGER_ATOM);
45
    return args[0].eqNode(args[0][0]);
46
  }
47
  // no rule
48
  return Node::null();
49
}
50
51
}  // namespace bv
52
}  // namespace theory
53
26685
}  // namespace CVC4