1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Implementation of bit-vectors proof checker. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/bv/proof_checker.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
namespace theory { |
20 |
|
namespace bv { |
21 |
|
|
22 |
3747 |
void BVProofRuleChecker::registerTo(ProofChecker* pc) |
23 |
|
{ |
24 |
3747 |
pc->registerChecker(PfRule::BV_BITBLAST, this); |
25 |
3747 |
pc->registerChecker(PfRule::BV_BITBLAST_STEP, this); |
26 |
3747 |
pc->registerChecker(PfRule::BV_EAGER_ATOM, this); |
27 |
3747 |
} |
28 |
|
|
29 |
15237 |
Node BVProofRuleChecker::checkInternal(PfRule id, |
30 |
|
const std::vector<Node>& children, |
31 |
|
const std::vector<Node>& args) |
32 |
|
{ |
33 |
15237 |
if (id == PfRule::BV_BITBLAST) |
34 |
|
{ |
35 |
3968 |
Assert(children.empty()); |
36 |
3968 |
Assert(args.size() == 1); |
37 |
3968 |
Assert(args[0].getKind() == kind::EQUAL); |
38 |
3968 |
return args[0]; |
39 |
|
} |
40 |
11269 |
else if (id == PfRule::BV_BITBLAST_STEP) |
41 |
|
{ |
42 |
11216 |
Assert(children.empty()); |
43 |
11216 |
Assert(args.size() == 1); |
44 |
11216 |
Assert(args[0].getKind() == kind::EQUAL); |
45 |
11216 |
return args[0]; |
46 |
|
} |
47 |
53 |
else if (id == PfRule::BV_EAGER_ATOM) |
48 |
|
{ |
49 |
53 |
Assert(children.empty()); |
50 |
53 |
Assert(args.size() == 1); |
51 |
53 |
Assert(args[0].getKind() == kind::BITVECTOR_EAGER_ATOM); |
52 |
53 |
return args[0].eqNode(args[0][0]); |
53 |
|
} |
54 |
|
// no rule |
55 |
|
return Node::null(); |
56 |
|
} |
57 |
|
|
58 |
|
} // namespace bv |
59 |
|
} // namespace theory |
60 |
29322 |
} // namespace cvc5 |