src/proof/arith_proof_recorder.cpp

   1 /*********************                                                        */
   2 /*! \file arith_proof_recorder.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Alex Ozdemir
   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
  11  **
  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.
  14  **/
  15
  16 #include "proof/arith_proof_recorder.h"
  17
  18 #include <algorithm>
  19 #include <vector>
  20
  21 #include "base/map_util.h"
  22
  23 namespace CVC4 {
  24 namespace proof {
  25
  26 ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients()
  27 {
  28   // Nothing else
  29 }
  30 void ArithProofRecorder::saveFarkasCoefficients(
  31     Node conflict, theory::arith::RationalVectorCP farkasCoefficients)
  32 {
  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)
  38   {
  39     const Node& child = conflict[i];
  40     // ... of possibly negated ...
  41     const Node& nonNegativeChild =
  42         child.getKind() == kind::NOT ? child[0] : child;
  43     // ... real bounds
  44     Assert(nonNegativeChild.getType().isBoolean()
  45            && nonNegativeChild[0].getType().isReal());
  46   }
  47   Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl;
  48   if (Debug.isOn("pf::arith"))
  49   {
  50     for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren;
  51          ++i)
  52     {
  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;
  57     }
  58   }
  59
  60   std::set<Node> lits;
  61   std::copy(
  62       conflict.begin(), conflict.end(), std::inserter(lits, lits.begin()));
  63
  64   d_lemmasToFarkasCoefficients[lits] =
  65       std::make_pair(std::move(conflict), *farkasCoefficients);
  66 }
  67
  68 bool ArithProofRecorder::hasFarkasCoefficients(
  69     const std::set<Node>& conflict) const
  70 {
  71   return d_lemmasToFarkasCoefficients.find(conflict)
  72          != d_lemmasToFarkasCoefficients.end();
  73 }
  74
  75 std::pair<Node, theory::arith::RationalVectorCP>
  76 ArithProofRecorder::getFarkasCoefficients(const std::set<Node>& conflict) const
  77 {
  78   if (auto *p = FindOrNull(d_lemmasToFarkasCoefficients, conflict))
  79   {
  80     return std::make_pair(p->first, &p->second);
  81   }
  82   else
  83   {
  84     return std::make_pair(Node(), theory::arith::RationalVectorCPSentinel);
  85   }
  86 }
  87
  88 }  // namespace proof
  89 }  // namespace CVC4