1 /********************* */
2 /*! \file smt_engine_check_proof.cpp
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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__)
21 #include <sys/types.h>
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"
38 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
48 extern const char *const plf_signatures
;
49 }/* CVC4::proof namespace */
53 class UnlinkProofFile
{
56 UnlinkProofFile(const char* filename
) : d_filename(filename
) {}
57 ~UnlinkProofFile() { unlink(d_filename
.c_str()); }
58 };/* class UnlinkProofFile */
60 }/* CVC4::smt namespace */
64 void SmtEngine::checkProof() {
66 #if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
68 Chat() << "generating proof..." << endl
;
70 const Proof
& pf
= getProof();
72 Chat() << "checking proof..." << endl
;
74 std::string logicString
= d_logic
.getLogicString();
78 logicString
== "QF_UF" ||
79 logicString
== "QF_AX" ||
80 logicString
== "QF_BV" ||
82 logicString
== "QF_AUF" ||
83 logicString
== "QF_UFBV" ||
84 logicString
== "QF_ABV" ||
85 logicString
== "QF_AUFBV"
87 // This logic is not yet supported
88 Notice() << "Notice: no proof-checking for " << logicString
<< " proofs yet" << endl
;
92 char *pfFile
= tempnam(NULL
, "cvc4_");
94 Notice() << "Error: couldn't get path from tempnam() during proof checking" << endl
;
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
);
102 mode_t openmode
= S_IRUSR
| S_IWUSR
;
103 int fd
= open(pfFile
, O_CREAT
| O_EXCL
| O_RDWR
, openmode
);
107 Notice() << "Error: failed to open temporary file during proof checking" << endl
;
111 // ensure this temp file is removed after
112 smt::UnlinkProofFile
unlinker(pfFile
);
114 ofstream
pfStream(pfFile
);
115 pfStream
<< proof::plf_signatures
<< endl
;
116 pf
.toStream(pfStream
);
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
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) */