1 /********************* */
2 /*! \file arith_proof_recorder.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 A class for recording the skeletons of arithmetic proofs at solve
13 ** time so they can later be used during proof-production time.
16 #include "proof/arith_proof_recorder.h"
21 #include "base/map_util.h"
26 ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients()
30 void ArithProofRecorder::saveFarkasCoefficients(
31 Node conflict
, theory::arith::RationalVectorCP farkasCoefficients
)
33 // Verify that the conflict is a conjuction of (possibly negated) real bounds
34 // Verify that the conflict is a conjunciton ...
35 Assert(conflict
.getKind() == kind::AND
);
36 Assert(conflict
.getNumChildren() == farkasCoefficients
->size());
37 for (size_t i
= 0, nchildren
= conflict
.getNumChildren(); i
< nchildren
; ++i
)
39 const Node
& child
= conflict
[i
];
40 // ... of possibly negated ...
41 const Node
& nonNegativeChild
=
42 child
.getKind() == kind::NOT
? child
[0] : child
;
44 Assert(nonNegativeChild
.getType().isBoolean()
45 && nonNegativeChild
[0].getType().isReal());
47 Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl
;
48 if (Debug
.isOn("pf::arith"))
50 for (size_t i
= 0, nchildren
= conflict
.getNumChildren(); i
< nchildren
;
53 const Node
& child
= conflict
[i
];
54 const Rational
& r
= (*farkasCoefficients
)[i
];
55 Debug("pf::arith") << " " << std::setw(8) << r
;
56 Debug("pf::arith") << " " << child
<< std::endl
;
62 conflict
.begin(), conflict
.end(), std::inserter(lits
, lits
.begin()));
64 d_lemmasToFarkasCoefficients
[lits
] =
65 std::make_pair(std::move(conflict
), *farkasCoefficients
);
68 bool ArithProofRecorder::hasFarkasCoefficients(
69 const std::set
<Node
>& conflict
) const
71 return d_lemmasToFarkasCoefficients
.find(conflict
)
72 != d_lemmasToFarkasCoefficients
.end();
75 std::pair
<Node
, theory::arith::RationalVectorCP
>
76 ArithProofRecorder::getFarkasCoefficients(const std::set
<Node
>& conflict
) const
78 if (auto *p
= FindOrNull(d_lemmasToFarkasCoefficients
, conflict
))
80 return std::make_pair(p
->first
, &p
->second
);
84 return std::make_pair(Node(), theory::arith::RationalVectorCPSentinel
);