summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/command.cpp17
-rw-r--r--src/expr/command.h11
-rw-r--r--src/parser/cvc/Cvc.g6
-rw-r--r--src/parser/smt2/Smt2.g2
-rw-r--r--src/proof/proof.h6
-rw-r--r--src/proof/proof_manager.cpp8
-rw-r--r--src/proof/proof_manager.h4
-rw-r--r--src/proof/sat_proof.cpp15
-rw-r--r--src/proof/sat_proof.h11
-rw-r--r--src/smt/smt_engine.cpp35
-rw-r--r--src/smt/smt_engine.h9
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/proof.h36
-rw-r--r--test/regress/regress0/Makefile.am1
-rw-r--r--test/regress/regress0/boolean.cvc2
-rw-r--r--test/regress/regress0/hole6.cvc2
-rw-r--r--test/regress/regress0/wiki.05.cvc2
-rwxr-xr-xtest/regress/run_regression34
18 files changed, 163 insertions, 39 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 61702561a..345d7f956 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -423,6 +423,23 @@ void GetAssignmentCommand::printResult(std::ostream& out) const {
out << d_result << endl;
}
+/* class GetProofCommand */
+
+GetProofCommand::GetProofCommand() {
+}
+
+void GetProofCommand::invoke(SmtEngine* smtEngine) {
+ d_result = smtEngine->getProof();
+}
+
+Proof* GetProofCommand::getResult() const {
+ return d_result;
+}
+
+void GetProofCommand::printResult(std::ostream& out) const {
+ d_result->toStream(out);
+}
+
/* class GetAssertionsCommand */
GetAssertionsCommand::GetAssertionsCommand() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 5cf4f6fa0..b686025fe 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -35,6 +35,7 @@
#include "util/result.h"
#include "util/sexpr.h"
#include "util/datatype.h"
+#include "util/proof.h"
namespace CVC4 {
@@ -232,6 +233,16 @@ public:
void printResult(std::ostream& out) const;
};/* class GetAssignmentCommand */
+class CVC4_PUBLIC GetProofCommand : public Command {
+protected:
+ Proof* d_result;
+public:
+ GetProofCommand();
+ void invoke(SmtEngine* smtEngine);
+ Proof* getResult() const;
+ void printResult(std::ostream& out) const;
+};/* class GetProofCommand */
+
class CVC4_PUBLIC GetAssertionsCommand : public Command {
protected:
std::string d_result;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 96c0933d8..22cf368eb 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -705,8 +705,10 @@ mainCommand[CVC4::Command*& cmd]
| { PARSER_STATE->parseError("No filename given to INCLUDE command"); }
)
- | ( DUMP_PROOF_TOK
- | DUMP_ASSUMPTIONS_TOK
+ | DUMP_PROOF_TOK
+ { cmd = new GetProofCommand(); }
+
+ | ( DUMP_ASSUMPTIONS_TOK
| DUMP_SIG_TOK
| DUMP_TCC_TOK
| DUMP_TCC_ASSUMPTIONS_TOK
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7fb671bb0..974de29b2 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -297,7 +297,7 @@ command returns [CVC4::Command* cmd = NULL]
{ cmd = new GetAssertionsCommand; }
| /* get-proof */
GET_PROOF_TOK
- { UNSUPPORTED("get-proof command not yet supported"); }
+ { cmd = new GetProofCommand; }
| /* get-unsat-core */
GET_UNSAT_CORE_TOK
{ UNSUPPORTED("unsat cores not yet supported"); }
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 3e5b54cc7..a3270c4c0 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -16,8 +16,8 @@
** Proof manager
**/
-#ifndef __CVC4__PROOF_H
-#define __CVC4__PROOF_H
+#ifndef __CVC4__PROOF__PROOF_H
+#define __CVC4__PROOF__PROOF_H
#include "util/options.h"
@@ -33,4 +33,4 @@
-#endif /* __CVC4__PROOF_H */
+#endif /* __CVC4__PROOF__PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 2d7432cbc..4191d1046 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -18,6 +18,7 @@
**/
#include "proof/proof_manager.h"
+#include "util/proof.h"
#include "proof/sat_proof.h"
#include "proof/cnf_proof.h"
#include "util/Assert.h"
@@ -40,7 +41,12 @@ ProofManager* ProofManager::currentPM() {
proofManager = new ProofManager();
isInitialized = true;
return proofManager;
- }
+ }
+}
+
+Proof* ProofManager::getProof() {
+ // for now, this is just the SAT proof
+ return getSatProof();
}
SatProof* ProofManager::getSatProof() {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c79d26fed..e23fbd600 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -22,7 +22,7 @@
#define __CVC4__PROOF_MANAGER_H
#include <iostream>
-#include "proof.h"
+#include "proof/proof.h"
// forward declarations
namespace Minisat {
@@ -33,6 +33,7 @@ namespace CVC4 {
namespace prop {
class CnfStream;
}
+class Proof;
class SatProof;
class CnfProof;
@@ -56,6 +57,7 @@ public:
static void initSatProof(Minisat::Solver* solver);
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
+ static Proof* getProof();
static SatProof* getSatProof();
static CnfProof* getCnfProof();
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 57bb96513..37a3a9706 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -524,8 +524,9 @@ ClauseId SatProof::resolveUnit(Lit lit) {
return unit_id;
}
-void SatProof::printProof() {
+void SatProof::toStream(std::ostream& out) {
Debug("proof:sat") << "SatProof::printProof\n";
+ Unimplemented("native proof printing not supported yet");
}
void SatProof::finalizeProof(CRef conflict_ref) {
@@ -543,7 +544,6 @@ void SatProof::finalizeProof(CRef conflict_ref) {
res->addStep(lit, res_id, !sign(lit));
}
registerResolution(d_emptyClauseId, res);
- printProof();
}
/// CRef manager
@@ -693,8 +693,7 @@ void LFSCSatProof::printVariables() {
}
-void LFSCSatProof::flush() {
- ostringstream out;
+void LFSCSatProof::flush(std::ostream& out) {
out << "(check \n";
d_paren <<")";
out << d_varSS.str();
@@ -703,11 +702,10 @@ void LFSCSatProof::flush() {
out << d_lemmaSS.str();
d_paren << "))";
out << d_paren.str();
- out << ";"; //to comment out the solver's answer
- std::cout << out.str();
+ out << "\n";
}
-void LFSCSatProof::printProof() {
+void LFSCSatProof::toStream(std::ostream& out) {
Debug("proof:sat") << " LFSCSatProof::printProof \n";
// first collect lemmas to print in reverse order
@@ -722,8 +720,7 @@ void LFSCSatProof::printProof() {
printClauses();
printVariables();
- flush();
-
+ flush(out);
}
} /* CVC4 namespace */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 4641ea4cc..051266df8 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -32,6 +32,7 @@ typedef uint32_t CRef;
}
#include "prop/minisat/core/SolverTypes.h"
+#include "util/proof.h"
namespace std {
using namespace __gnu_cxx;
@@ -99,7 +100,7 @@ public:
void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
};
-class SatProof {
+class SatProof : public Proof {
protected:
::Minisat::Solver* d_solver;
// clauses
@@ -144,8 +145,8 @@ protected:
::Minisat::Lit getUnit(ClauseId id);
ClauseId getUnitId(::Minisat::Lit lit);
::Minisat::Clause& getClause(ClauseId id);
- virtual void printProof();
-
+ virtual void toStream(std::ostream& out);
+
bool checkResolution(ClauseId id);
/**
* Constructs a resolution tree that proves lit
@@ -237,7 +238,7 @@ private:
void printVariables();
void printClauses();
- void flush();
+ void flush(std::ostream& out);
public:
LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
@@ -249,7 +250,7 @@ public:
d_seenLemmas(),
d_seenInput()
{}
- void printProof();
+ virtual void toStream(std::ostream& out);
};
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 96ee5b59b..7ea22ce8f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,6 +34,8 @@
#include "smt/no_such_function_exception.h"
#include "smt/smt_engine.h"
#include "theory/theory_engine.h"
+#include "proof/proof_manager.h"
+#include "util/proof.h"
#include "util/boolean_simplification.h"
#include "util/configuration.h"
#include "util/exception.h"
@@ -987,7 +989,7 @@ Expr SmtEngine::getValue(const Expr& e)
d_status.asSatisfiabilityResult() != Result::SAT ||
d_problemExtended) {
const char* msg =
- "Cannot get value unless immediately proceded by SAT/INVALID response.";
+ "Cannot get value unless immediately preceded by SAT/INVALID response.";
throw ModalException(msg);
}
if(type.isFunction() || type.isPredicate() ||
@@ -1040,6 +1042,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getAssignment()" << endl;
+ NodeManagerScope nms(d_nodeManager);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand() << endl;
}
@@ -1053,7 +1056,8 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
d_status.asSatisfiabilityResult() != Result::SAT ||
d_problemExtended) {
const char* msg =
- "Cannot get value unless immediately proceded by SAT/INVALID response.";
+ "Cannot get the current assignment unless immediately "
+ "preceded by SAT/INVALID response.";
throw ModalException(msg);
}
@@ -1061,7 +1065,6 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
return SExpr();
}
- NodeManagerScope nms(d_nodeManager);
vector<SExpr> sexprs;
TypeNode boolType = d_nodeManager->booleanType();
for(AssignmentSet::const_iterator i = d_assignments->begin(),
@@ -1093,6 +1096,32 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
return SExpr(sexprs);
}
+Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
+ Trace("smt") << "SMT getProof()" << endl;
+ NodeManagerScope nms(d_nodeManager);
+ if(Dump.isOn("benchmark")) {
+ Dump("benchmark") << GetProofCommand() << endl;
+ }
+#ifdef CVC4_PROOF
+ if(!Options::current()->proof) {
+ const char* msg =
+ "Cannot get a proof when produce-proofs option is off.";
+ throw ModalException(msg);
+ }
+ if(d_status.isNull() ||
+ d_status.asSatisfiabilityResult() != Result::UNSAT ||
+ d_problemExtended) {
+ const char* msg =
+ "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
+ throw ModalException(msg);
+ }
+
+ return ProofManager::getProof();
+#else /* CVC4_PROOF */
+ throw ModalException("This build of CVC4 doesn't have proof support.");
+#endif /* CVC4_PROOF */
+}
+
vector<Expr> SmtEngine::getAssertions()
throw(ModalException, AssertionException) {
if(Dump.isOn("benchmark")) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5d8f31d3c..90593569b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,6 +28,7 @@
#include "context/cdset_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
+#include "util/proof.h"
#include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
#include "smt/no_such_function_exception.h"
@@ -36,7 +37,6 @@
#include "util/result.h"
#include "util/sexpr.h"
#include "util/stats.h"
-#include "proof/proof_manager.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
@@ -319,6 +319,13 @@ public:
SExpr getAssignment() throw(ModalException, AssertionException);
/**
+ * Get the last proof (only if immediately preceded by an UNSAT
+ * or VALID query). Only permitted if CVC4 was built with proof
+ * support and produce-proofs is on.
+ */
+ Proof* getProof() throw(ModalException, AssertionException);
+
+ /**
* Get the current set of assertions. Only permitted if the
* SmtEngine is set to operate interactively.
*/
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e915fe483..c5a20cd5d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -28,6 +28,7 @@ libutil_la_SOURCES = \
exception.h \
hash.h \
bool.h \
+ proof.h \
options.h \
options.cpp \
output.cpp \
diff --git a/src/util/proof.h b/src/util/proof.h
new file mode 100644
index 000000000..be833e33c
--- /dev/null
+++ b/src/util/proof.h
@@ -0,0 +1,36 @@
+/********************* */
+/*! \file proof.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PROOF_H
+#define __CVC4__PROOF_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Proof {
+public:
+ virtual void toStream(std::ostream& out) = 0;
+};/* class Proof */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PROOF_H */
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3a4583805..e564b567a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -45,6 +45,7 @@ SMT2_TESTS = \
# Regression tests for PL inputs
CVC_TESTS = \
+ boolean.cvc \
boolean-prec.cvc \
hole6.cvc \
ite.cvc \
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index d6f428bdb..2d0eb59b2 100644
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -804,5 +804,5 @@ a288 : BOOLEAN =
ELSE FALSE
ENDIF;
QUERY a288;
-% EXIT: 20
% PROOF
+% EXIT: 20
diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index 31204a6c1..ece29e17c 100644
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -177,5 +177,5 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
QUERY FALSE;
-% EXIT: 20
% PROOF
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index 1aedcbe2b..04c7dafe0 100644
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -2,5 +2,5 @@ a, b, c : BOOLEAN;
% EXPECT: valid
QUERY a OR (a AND b) <=> a;
-% EXIT: 20
% PROOF
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index b836b39f6..6c06175d2 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -52,6 +52,8 @@ function gettemp {
tmpbenchmark=
if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
+ proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1
+ lang=smt
if test -e "$benchmark.expect"; then
expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
@@ -68,9 +70,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
# old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
- # this frustrates our auto-language-detection, so add explicit --lang
+ # this frustrates our auto-language-detection
gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
- command_line="${command_line:+$command_line }--lang=smt"
grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
@@ -90,6 +91,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
error "cannot determine status of \`$benchmark'"
fi
elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
+ proof_command='(get-proof)'
+ lang=smt2
if test -e "$benchmark.expect"; then
expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
@@ -106,9 +109,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
# old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
- # this frustrates our auto-language-detection, so add explicit --lang
+ # this frustrates our auto-language-detection
gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
- command_line="${command_line:+$command_line }--lang=smt2"
grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
@@ -128,6 +130,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
error "cannot determine status of \`$benchmark'"
fi
elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
+ proof_command='DUMP_PROOF;'
+ lang=cvc4
expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
expected_output=$(grep '^% EXPECT: ' "$benchmark")
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
@@ -145,6 +149,8 @@ else
error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
fi
+command_line="${command_line:+$command_line }--lang=$lang"
+
gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX
gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX
gettemp outfile cvc4_stdout.$$.XXXXXXXXXX
@@ -203,19 +209,27 @@ if [ "$exit_status" != "$expected_exit_status" ]; then
fi
if [ "$proof" = yes -a "$expected_proof" = yes ]; then
- echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
- ( cd `dirname "$benchmark"`;
- "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`;
+ gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX
+ cp "$benchmark" "$pfbenchmark";
+ echo "$proof_command" >>"$pfbenchmark";
+ echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
+ ( cd `dirname "$pfbenchmark"`;
+ "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`;
echo $? >"$exitstatusfile"
) > "$outfile" 2> "$errfile"
- if [ ! -s "$outfile" ]; then
+ gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX
+ diff --unchanged-group-format='' \
+ --old-group-format='' \
+ --new-group-format='%>' \
+ "$expoutfile" "$outfile" > "$pfoutfile"
+ if [ ! -s "$pfoutfile" ]; then
echo "$prog: error: proof generation failed with empty output (stderr follows)"
cat "$errfile"
exitcode=1
else
- echo running $LFSC "$outfile" [from working dir `dirname "$benchmark"`]
- if ! $LFSC "$outfile" &> "$errfile"; then
+ echo running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`]
+ if ! $LFSC "$pfoutfile" &> "$errfile"; then
echo "$prog: error: proof checker failed (output follows)"
cat "$errfile"
exitcode=1
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback