src/smt/smt_engine_check_proof.cpp

   1 /*********************                                                        */
   2 /*! \file smt_engine_check_proof.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Guy Katz, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__)
  19 #include <io.h>
  20 #endif
  21 #include <sys/types.h>
  22 #include <sys/stat.h>
  23 #include <fcntl.h>
  24 #include <unistd.h>
  25
  26 #include <cstdlib>
  27 #include <cstring>
  28 #include <fstream>
  29 #include <string>
  30
  31 #include "base/configuration_private.h"
  32 #include "base/cvc4_assert.h"
  33 #include "base/output.h"
  34 #include "smt/smt_engine.h"
  35 #include "util/proof.h"
  36 #include "util/statistics_registry.h"
  37
  38 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
  39 #include "lfscc.h"
  40 #endif
  41
  42 using namespace CVC4;
  43 using namespace std;
  44
  45 namespace CVC4 {
  46
  47 namespace proof {
  48   extern const char *const plf_signatures;
  49 }/* CVC4::proof namespace */
  50
  51 namespace smt {
  52
  53 class UnlinkProofFile {
  54   string d_filename;
  55 public:
  56   UnlinkProofFile(const char* filename) : d_filename(filename) {}
  57   ~UnlinkProofFile() { unlink(d_filename.c_str()); }
  58 };/* class UnlinkProofFile */
  59
  60 }/* CVC4::smt namespace */
  61
  62 }/* CVC4 namespace */
  63
  64 void SmtEngine::checkProof() {
  65
  66 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
  67
  68   Chat() << "generating proof..." << endl;
  69
  70   const Proof& pf = getProof();
  71
  72   Chat() << "checking proof..." << endl;
  73
  74   std::string logicString = d_logic.getLogicString();
  75
  76   if (!(
  77         // Pure logics
  78         logicString == "QF_UF" ||
  79         logicString == "QF_AX" ||
  80         logicString == "QF_BV" ||
  81         // Non-pure logics
  82         logicString == "QF_AUF" ||
  83         logicString == "QF_UFBV" ||
  84         logicString == "QF_ABV" ||
  85         logicString == "QF_AUFBV"
  86         )) {
  87     // This logic is not yet supported
  88     Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl;
  89     return;
  90   }
  91
  92   char *pfFile = tempnam(NULL, "cvc4_");
  93   if (!pfFile) {
  94     Notice() << "Error: couldn't get path from tempnam() during proof checking" << endl;
  95     return;
  96   }
  97 #if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__)
  98   int fd = _open(pfFile,
  99                  _O_CREAT | _O_EXCL | _O_SHORT_LIVED | _O_RDWR,
 100                  _S_IREAD | _S_IWRITE);
 101 #else
 102   mode_t openmode = S_IRUSR | S_IWUSR;
 103   int fd = open(pfFile, O_CREAT | O_EXCL | O_RDWR, openmode);
 104 #endif
 105   if (fd == -1) {
 106     free(pfFile);
 107     Notice() << "Error: failed to open temporary file during proof checking" << endl;
 108     return;
 109   }
 110
 111   // ensure this temp file is removed after
 112   smt::UnlinkProofFile unlinker(pfFile);
 113
 114   ofstream pfStream(pfFile);
 115   pfStream << proof::plf_signatures << endl;
 116   pf.toStream(pfStream);
 117   pfStream.close();
 118   lfscc_init();
 119   lfscc_check_file(pfFile, false, false, false, false, false, false, false);
 120   // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
 121   // segfaults on regress0/bv/core/bitvec7.smt
 122   //lfscc_cleanup();
 123   free(pfFile);
 124   close(fd);
 125
 126 #else /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
 127   Unreachable("This version of CVC4 was built without proof support; cannot check proofs.");
 128 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
 129 }