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() {
#include "util/result.h"
#include "util/sexpr.h"
#include "util/datatype.h"
+#include "util/proof.h"
namespace CVC4 {
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;
| { 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
{ 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"); }
** Proof manager
**/
-#ifndef __CVC4__PROOF_H
-#define __CVC4__PROOF_H
+#ifndef __CVC4__PROOF__PROOF_H
+#define __CVC4__PROOF__PROOF_H
#include "util/options.h"
-#endif /* __CVC4__PROOF_H */
+#endif /* __CVC4__PROOF__PROOF_H */
**/
#include "proof/proof_manager.h"
+#include "util/proof.h"
#include "proof/sat_proof.h"
#include "proof/cnf_proof.h"
#include "util/Assert.h"
proofManager = new ProofManager();
isInitialized = true;
return proofManager;
- }
+ }
+}
+
+Proof* ProofManager::getProof() {
+ // for now, this is just the SAT proof
+ return getSatProof();
}
SatProof* ProofManager::getSatProof() {
#define __CVC4__PROOF_MANAGER_H
#include <iostream>
-#include "proof.h"
+#include "proof/proof.h"
// forward declarations
namespace Minisat {
namespace prop {
class CnfStream;
}
+class Proof;
class SatProof;
class CnfProof;
static void initSatProof(Minisat::Solver* solver);
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
+ static Proof* getProof();
static SatProof* getSatProof();
static CnfProof* getCnfProof();
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) {
res->addStep(lit, res_id, !sign(lit));
}
registerResolution(d_emptyClauseId, res);
- printProof();
}
/// CRef manager
}
-void LFSCSatProof::flush() {
- ostringstream out;
+void LFSCSatProof::flush(std::ostream& out) {
out << "(check \n";
d_paren <<")";
out << d_varSS.str();
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
printClauses();
printVariables();
- flush();
-
+ flush(out);
}
} /* CVC4 namespace */
}
#include "prop/minisat/core/SolverTypes.h"
+#include "util/proof.h"
namespace std {
using namespace __gnu_cxx;
void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
};
-class SatProof {
+class SatProof : public Proof {
protected:
::Minisat::Solver* d_solver;
// clauses
::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
void printVariables();
void printClauses();
- void flush();
+ void flush(std::ostream& out);
public:
LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
d_seenLemmas(),
d_seenInput()
{}
- void printProof();
+ virtual void toStream(std::ostream& out);
};
}
#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"
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() ||
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
Trace("smt") << "SMT getAssignment()" << endl;
+ NodeManagerScope nms(d_nodeManager);
if(Dump.isOn("benchmark")) {
Dump("benchmark") << GetAssignmentCommand() << endl;
}
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);
}
return SExpr();
}
- NodeManagerScope nms(d_nodeManager);
vector<SExpr> sexprs;
TypeNode boolType = d_nodeManager->booleanType();
for(AssignmentSet::const_iterator i = d_assignments->begin(),
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")) {
#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"
#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)
*/
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.
exception.h \
hash.h \
bool.h \
+ proof.h \
options.h \
options.cpp \
output.cpp \
--- /dev/null
+/********************* */
+/*! \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 */
# Regression tests for PL inputs
CVC_TESTS = \
+ boolean.cvc \
boolean-prec.cvc \
hole6.cvc \
ite.cvc \
ELSE FALSE
ENDIF;
QUERY a288;
-% EXIT: 20
% PROOF
+% EXIT: 20
QUERY FALSE;
-% EXIT: 20
% PROOF
+% EXIT: 20
% EXPECT: valid
QUERY a OR (a AND b) <=> a;
-% EXIT: 20
% PROOF
+% EXIT: 20
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: ,,'`
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"
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: ,,'`
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"
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: ,,'`
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
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
projects / cvc5.git / commitdiff