GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/nl/cad/proof_checker.cpp Lines: 1 16 6.3 %
Date: 2021-03-22 Branches: 2 64 3.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 CAD proof checker
13
 **/
14
15
#include "theory/arith/nl/cad/proof_checker.h"
16
17
#include "expr/sequence.h"
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
namespace nl {
26
namespace cad {
27
28
void CADProofRuleChecker::registerTo(ProofChecker* pc)
29
{
30
  // trusted rules
31
  pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_DIRECT, this, 2);
32
  pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_RECURSIVE, this, 2);
33
}
34
35
Node CADProofRuleChecker::checkInternal(PfRule id,
36
                                        const std::vector<Node>& children,
37
                                        const std::vector<Node>& args)
38
{
39
  Trace("nl-cad-checker") << "Checking " << id << std::endl;
40
  for (const auto& c : children)
41
  {
42
    Trace("nl-cad-checker") << "\t" << c << std::endl;
43
  }
44
  if (id == PfRule::ARITH_NL_CAD_DIRECT)
45
  {
46
    Assert(args.size() == 1);
47
    return args[0];
48
  }
49
  if (id == PfRule::ARITH_NL_CAD_RECURSIVE)
50
  {
51
    Assert(args.size() == 1);
52
    return args[0];
53
  }
54
  return Node::null();
55
}
56
57
}  // namespace cad
58
}  // namespace nl
59
}  // namespace arith
60
}  // namespace theory
61
26676
}  // namespace CVC4