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 |
3 |
void BVProofRuleChecker::registerTo(ProofChecker* pc) |
23 |
|
{ |
24 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST, this); |
25 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_CONST, this); |
26 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_VAR, this); |
27 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_EQUAL, this); |
28 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ULT, this); |
29 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ULE, this); |
30 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_UGT, this); |
31 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_UGE, this); |
32 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SLT, this); |
33 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SLE, this); |
34 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SGT, this); |
35 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SGE, this); |
36 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_NOT, this); |
37 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_CONCAT, this); |
38 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_AND, this); |
39 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_OR, this); |
40 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_XOR, this); |
41 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_XNOR, this); |
42 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_NAND, this); |
43 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_NOR, this); |
44 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_COMP, this); |
45 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_MULT, this); |
46 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ADD, this); |
47 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SUB, this); |
48 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_NEG, this); |
49 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_UDIV, this); |
50 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_UREM, this); |
51 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SDIV, this); |
52 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SREM, this); |
53 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SMOD, this); |
54 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SHL, this); |
55 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_LSHR, this); |
56 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ASHR, this); |
57 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ULTBV, this); |
58 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SLTBV, this); |
59 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ITE, this); |
60 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_EXTRACT, this); |
61 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_REPEAT, this); |
62 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ZERO_EXTEND, this); |
63 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_SIGN_EXTEND, this); |
64 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_RIGHT, this); |
65 |
3 |
pc->registerChecker(PfRule::BV_BITBLAST_ROTATE_LEFT, this); |
66 |
3 |
pc->registerChecker(PfRule::BV_EAGER_ATOM, this); |
67 |
3 |
} |
68 |
|
|
69 |
|
Node BVProofRuleChecker::checkInternal(PfRule id, |
70 |
|
const std::vector<Node>& children, |
71 |
|
const std::vector<Node>& args) |
72 |
|
{ |
73 |
|
if (id == PfRule::BV_BITBLAST) |
74 |
|
{ |
75 |
|
BBSimple bb(nullptr); |
76 |
|
Assert(children.empty()); |
77 |
|
Assert(args.size() == 1); |
78 |
|
bb.bbAtom(args[0]); |
79 |
|
Node n = bb.getStoredBBAtom(args[0]); |
80 |
|
return args[0].eqNode(n); |
81 |
|
} |
82 |
|
else if (id == PfRule::BV_BITBLAST_CONST || id == PfRule::BV_BITBLAST_VAR |
83 |
|
|| id == PfRule::BV_BITBLAST_EQUAL || id == PfRule::BV_BITBLAST_ULT |
84 |
|
|| id == PfRule::BV_BITBLAST_ULE || id == PfRule::BV_BITBLAST_UGT |
85 |
|
|| id == PfRule::BV_BITBLAST_UGE || id == PfRule::BV_BITBLAST_SLT |
86 |
|
|| id == PfRule::BV_BITBLAST_SLE || id == PfRule::BV_BITBLAST_SGT |
87 |
|
|| id == PfRule::BV_BITBLAST_SGE || id == PfRule::BV_BITBLAST_NOT |
88 |
|
|| id == PfRule::BV_BITBLAST_CONCAT || id == PfRule::BV_BITBLAST_AND |
89 |
|
|| id == PfRule::BV_BITBLAST_OR || id == PfRule::BV_BITBLAST_XOR |
90 |
|
|| id == PfRule::BV_BITBLAST_XNOR || id == PfRule::BV_BITBLAST_NAND |
91 |
|
|| id == PfRule::BV_BITBLAST_NOR || id == PfRule::BV_BITBLAST_COMP |
92 |
|
|| id == PfRule::BV_BITBLAST_MULT || id == PfRule::BV_BITBLAST_ADD |
93 |
|
|| id == PfRule::BV_BITBLAST_SUB || id == PfRule::BV_BITBLAST_NEG |
94 |
|
|| id == PfRule::BV_BITBLAST_UDIV || id == PfRule::BV_BITBLAST_UREM |
95 |
|
|| id == PfRule::BV_BITBLAST_SDIV || id == PfRule::BV_BITBLAST_SREM |
96 |
|
|| id == PfRule::BV_BITBLAST_SMOD || id == PfRule::BV_BITBLAST_SHL |
97 |
|
|| id == PfRule::BV_BITBLAST_LSHR || id == PfRule::BV_BITBLAST_ASHR |
98 |
|
|| id == PfRule::BV_BITBLAST_ULTBV || id == PfRule::BV_BITBLAST_SLTBV |
99 |
|
|| id == PfRule::BV_BITBLAST_ITE || id == PfRule::BV_BITBLAST_EXTRACT |
100 |
|
|| id == PfRule::BV_BITBLAST_REPEAT |
101 |
|
|| id == PfRule::BV_BITBLAST_ZERO_EXTEND |
102 |
|
|| id == PfRule::BV_BITBLAST_SIGN_EXTEND |
103 |
|
|| id == PfRule::BV_BITBLAST_ROTATE_RIGHT |
104 |
|
|| id == PfRule::BV_BITBLAST_ROTATE_LEFT) |
105 |
|
{ |
106 |
|
return args[0]; |
107 |
|
} |
108 |
|
else if (id == PfRule::BV_EAGER_ATOM) |
109 |
|
{ |
110 |
|
Assert(children.empty()); |
111 |
|
Assert(args.size() == 1); |
112 |
|
Assert(args[0].getKind() == kind::BITVECTOR_EAGER_ATOM); |
113 |
|
return args[0].eqNode(args[0][0]); |
114 |
|
} |
115 |
|
// no rule |
116 |
|
return Node::null(); |
117 |
|
} |
118 |
|
|
119 |
|
} // namespace bv |
120 |
|
} // namespace theory |
121 |
28191 |
} // namespace cvc5 |