1 /********************* */
2 /*! \file proof_checker.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Implementation of arithmetic proof checker
15 #include "theory/arith/proof_checker.h"
20 #include "expr/skolem_manager.h"
21 #include "theory/arith/arith_utilities.h"
22 #include "theory/arith/constraint.h"
23 #include "theory/arith/normal_form.h"
24 #include "theory/arith/operator_elim.h"
30 void ArithProofRuleChecker::registerTo(ProofChecker
* pc
)
32 pc
->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS
, this);
33 pc
->registerChecker(PfRule::ARITH_TRICHOTOMY
, this);
34 pc
->registerChecker(PfRule::INT_TIGHT_UB
, this);
35 pc
->registerChecker(PfRule::INT_TIGHT_LB
, this);
36 pc
->registerChecker(PfRule::INT_TRUST
, this);
37 pc
->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM
, this);
40 Node
ArithProofRuleChecker::checkInternal(PfRule id
,
41 const std::vector
<Node
>& children
,
42 const std::vector
<Node
>& args
)
44 if (Debug
.isOn("arith::pf::check"))
46 Debug("arith::pf::check") << "Arith PfRule:" << id
<< std::endl
;
47 Debug("arith::pf::check") << " children: " << std::endl
;
48 for (const auto& c
: children
)
50 Debug("arith::pf::check") << " * " << c
<< std::endl
;
52 Debug("arith::pf::check") << " args:" << std::endl
;
53 for (const auto& c
: args
)
55 Debug("arith::pf::check") << " * " << c
<< std::endl
;
60 case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS
:
62 // Children: (P1:l1, ..., Pn:ln)
63 // where each li is an ArithLiteral
64 // not(= ...) is dis-allowed!
66 // Arguments: (k1, ..., kn), non-zero reals
67 // ---------------------
68 // Conclusion: (>< (* k t1) (* k t2))
69 // where >< is the fusion of the combination of the ><i, (flipping each
70 // it its ki is negative). >< is always one of <, <= NB: this implies
71 // that lower bounds must have negative ki,
72 // and upper bounds must have positive ki.
73 // t1 is the sum of the polynomials.
74 // t2 is the sum of the constants.
75 Assert(children
.size() == args
.size());
76 if (children
.size() < 2)
81 // Whether a strict inequality is in the sum.
82 auto nm
= NodeManager::currentNM();
84 NodeBuilder
<> leftSum(Kind::PLUS
);
85 NodeBuilder
<> rightSum(Kind::PLUS
);
86 for (size_t i
= 0; i
< children
.size(); ++i
)
88 Rational scalar
= args
[i
].getConst
<Rational
>();
91 Debug("arith::pf::check") << "Error: zero scalar" << std::endl
;
96 switch (children
[i
].getKind())
112 Debug("arith::pf::check")
113 << "Bad kind: " << children
[i
].getKind() << std::endl
;
117 switch (children
[i
].getKind())
124 Debug("arith::pf::check")
125 << "Positive scalar for lower bound: " << scalar
<< " for "
126 << children
[i
] << std::endl
;
136 Debug("arith::pf::check")
137 << "Negative scalar for upper bound: " << scalar
<< " for "
138 << children
[i
] << std::endl
;
149 Debug("arith::pf::check")
150 << "Bad kind: " << children
[i
].getKind() << std::endl
;
153 leftSum
<< nm
->mkNode(
154 Kind::MULT
, children
[i
][0], nm
->mkConst
<Rational
>(scalar
));
155 rightSum
<< nm
->mkNode(
156 Kind::MULT
, children
[i
][1], nm
->mkConst
<Rational
>(scalar
));
158 Node r
= nm
->mkNode(strict
? Kind::LT
: Kind::LEQ
,
159 leftSum
.constructNode(),
160 rightSum
.constructNode());
163 case PfRule::INT_TIGHT_LB
:
165 // Children: (P:(> i c))
166 // where i has integer type.
168 // ---------------------
169 // Conclusion: (>= i leastIntGreaterThan(c)})
170 if (children
.size() != 1
171 || (children
[0].getKind() != Kind::GT
172 && children
[0].getKind() != Kind::GEQ
)
173 || !children
[0][0].getType().isInteger()
174 || children
[0][1].getKind() != Kind::CONST_RATIONAL
)
176 Debug("arith::pf::check") << "Illformed input: " << children
;
181 Rational originalBound
= children
[0][1].getConst
<Rational
>();
182 Rational newBound
= leastIntGreaterThan(originalBound
);
183 auto nm
= NodeManager::currentNM();
184 Node rational
= nm
->mkConst
<Rational
>(newBound
);
185 return nm
->mkNode(kind::GEQ
, children
[0][0], rational
);
188 case PfRule::INT_TIGHT_UB
:
190 // ======== Tightening Strict Integer Upper Bounds
191 // Children: (P:(< i c))
192 // where i has integer type.
194 // ---------------------
195 // Conclusion: (<= i greatestIntLessThan(c)})
196 if (children
.size() != 1
197 || (children
[0].getKind() != Kind::LT
198 && children
[0].getKind() != Kind::LEQ
)
199 || !children
[0][0].getType().isInteger()
200 || children
[0][1].getKind() != Kind::CONST_RATIONAL
)
202 Debug("arith::pf::check") << "Illformed input: " << children
;
207 Rational originalBound
= children
[0][1].getConst
<Rational
>();
208 Rational newBound
= greatestIntLessThan(originalBound
);
209 auto nm
= NodeManager::currentNM();
210 Node rational
= nm
->mkConst
<Rational
>(newBound
);
211 return nm
->mkNode(kind::LEQ
, children
[0][0], rational
);
214 case PfRule::ARITH_TRICHOTOMY
:
216 Node a
= negateProofLiteral(children
[0]);
217 Node b
= negateProofLiteral(children
[1]);
219 if (a
[0] == b
[0] && b
[0] == c
[0] && a
[1] == b
[1] && b
[1] == c
[1])
222 cmps
.insert(a
.getKind());
223 cmps
.insert(b
.getKind());
224 cmps
.insert(c
.getKind());
225 if (cmps
.count(Kind::EQUAL
) == 0)
227 Debug("arith::pf::check") << "Error: No = " << std::endl
;
230 if (cmps
.count(Kind::GT
) == 0)
232 Debug("arith::pf::check") << "Error: No > " << std::endl
;
235 if (cmps
.count(Kind::LT
) == 0)
237 Debug("arith::pf::check") << "Error: No < " << std::endl
;
244 Debug("arith::pf::check")
245 << "Error: Different polynomials / values" << std::endl
;
246 Debug("arith::pf::check") << " a: " << a
<< std::endl
;
247 Debug("arith::pf::check") << " b: " << b
<< std::endl
;
248 Debug("arith::pf::check") << " c: " << c
<< std::endl
;
251 // Check that all have the same constant:
253 case PfRule::INT_TRUST
:
255 Assert(args
.size() == 1);
258 case PfRule::ARITH_OP_ELIM_AXIOM
:
260 Assert(children
.empty());
261 Assert(args
.size() == 1);
262 return OperatorElim::getAxiomFor(args
[0]);
264 default: return Node::null();
268 } // namespace theory