summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/cnf_proof.cpp14
-rw-r--r--src/proof/proof_manager.cpp19
-rw-r--r--src/proof/proof_manager.h15
-rw-r--r--src/proof/sat_proof.cpp6
-rw-r--r--src/proof/theory_proof.cpp2
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--test/regress/regress0/uf/Makefile.am3
-rw-r--r--test/regress/regress0/uf/proof00.smt221
-rwxr-xr-xtest/regress/run_regression16
9 files changed, 79 insertions, 20 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index cb22ca819..8e9c4cd21 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -33,7 +33,8 @@ CnfProof::CnfProof(CnfStream* stream)
Expr CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
- Expr atom = d_cnfStream->getNode(lit).toExpr();
+ Node node = d_cnfStream->getNode(lit);
+ Expr atom = node.toExpr();
return atom;
}
@@ -45,9 +46,16 @@ void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
for (;it != end; ++it) {
- Expr atom = getAtom(*it);
os << "(decl_atom ";
- LFSCTheoryProof::printFormula(atom, os);
+
+ if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
+ Expr atom = getAtom(*it);
+ LFSCTheoryProof::printFormula(atom, os);
+ } else {
+ // print fake atoms for all other logics
+ os << "true ";
+ }
+
os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
paren << ")))";
}
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 23ba0e4e7..110e6b79a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -21,6 +21,8 @@
#include "proof/cnf_proof.h"
#include "proof/theory_proof.h"
#include "util/cvc4_assert.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
namespace CVC4 {
@@ -68,12 +70,13 @@ ProofManager* ProofManager::currentPM() {
}
}
-Proof* ProofManager::getProof() {
+Proof* ProofManager::getProof(SmtEngine* smt) {
if (currentPM()->d_fullProof != NULL)
return currentPM()->d_fullProof;
Assert (currentPM()->d_format == LFSC);
- currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(),
+ currentPM()->d_fullProof = new LFSCProof(smt,
+ (LFSCSatProof*)getSatProof(),
(LFSCCnfProof*)getCnfProof(),
(LFSCTheoryProof*)getTheoryProof());
return currentPM()->d_fullProof;
@@ -138,19 +141,27 @@ void ProofManager::addAssertion(Expr formula) {
d_inputFormulas.insert(formula);
}
+void ProofManager::setLogic(const std::string& logic_string) {
+ d_logic = logic_string;
+}
+
-LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
+LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
: d_satProof(sat)
, d_cnfProof(cnf)
, d_theoryProof(theory)
+ , d_smtEngine(smtEngine)
{
d_satProof->constructProof();
}
void LFSCProof::toStream(std::ostream& out) {
+ smt::SmtScope scope(d_smtEngine);
std::ostringstream paren;
out << "(check \n";
- d_theoryProof->printAssertions(out, paren);
+ if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
+ d_theoryProof->printAssertions(out, paren);
+ }
out << "(: (holds cln) \n";
d_cnfProof->printAtomMapping(out, paren);
d_cnfProof->printClauses(out, paren);
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 7642ba776..82a1bd6be 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -36,6 +36,9 @@ namespace CVC4 {
namespace prop {
class CnfStream;
}
+
+class SmtEngine;
+
typedef int ClauseId;
class Proof;
@@ -91,6 +94,8 @@ class ProofManager {
static bool isInitialized;
ProofManager(ProofFormat format = LFSC);
~ProofManager();
+protected:
+ std::string d_logic;
public:
static ProofManager* currentPM();
// initialization
@@ -98,7 +103,7 @@ public:
static void initCnfProof(CVC4::prop::CnfStream* cnfStream);
static void initTheoryProof();
- static Proof* getProof();
+ static Proof* getProof(SmtEngine* smt);
static SatProof* getSatProof();
static CnfProof* getCnfProof();
static TheoryProof* getTheoryProof();
@@ -131,14 +136,18 @@ public:
static std::string getVarName(prop::SatVariable var);
static std::string getAtomName(prop::SatVariable var);
static std::string getLitName(prop::SatLiteral lit);
+
+ void setLogic(const std::string& logic_string);
+ const std::string getLogic() const { return d_logic; }
};/* class ProofManager */
class LFSCProof : public Proof {
LFSCSatProof* d_satProof;
LFSCCnfProof* d_cnfProof;
- LFSCTheoryProof* d_theoryProof;
+ LFSCTheoryProof* d_theoryProof;
+ SmtEngine* d_smtEngine;
public:
- LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
+ LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
virtual void toStream(std::ostream& out);
virtual ~LFSCProof() {}
};
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 2ac468b47..da9df0d42 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -579,9 +579,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
res->addStep(lit, res_id, !sign(lit));
}
registerResolution(d_emptyClauseId, res);
- // FIXME: massive hack
- Proof* proof = ProofManager::getProof();
- proof->toStream(std::cout);
+ // // FIXME: massive hack
+ // Proof* proof = ProofManager::getProof();
+ // proof->toStream(std::cout);
}
/// CRef manager
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 4ce804a74..696bd8309 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -167,7 +167,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
// declaring the terms
for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
Expr term = *it;
-
+
os << "(% " << term << " (term ";
paren <<")";
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 32d0d1703..0cfb674cf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -680,6 +680,7 @@ void SmtEngine::finishInit() {
if(options::cumulativeMillisecondLimit() != 0) {
setTimeLimit(options::cumulativeMillisecondLimit(), true);
}
+ PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
}
void SmtEngine::finalOptionsAreSet() {
@@ -3713,7 +3714,7 @@ Proof* SmtEngine::getProof() throw(ModalException) {
throw ModalException(msg);
}
- return ProofManager::getProof();
+ return ProofManager::getProof(this);
#else /* CVC4_PROOF */
throw ModalException("This build of CVC4 doesn't have proof support.");
#endif /* CVC4_PROOF */
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index bf9a36df1..19e673fea 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -42,7 +42,8 @@ TESTS = \
simple.01.cvc \
simple.02.cvc \
simple.03.cvc \
- simple.04.cvc
+ simple.04.cvc \
+ proof00.smt2
EXTRA_DIST = $(TESTS) \
mkpidgeon
diff --git a/test/regress/regress0/uf/proof00.smt2 b/test/regress/regress0/uf/proof00.smt2
new file mode 100644
index 000000000..1b7e7b8dd
--- /dev/null
+++ b/test/regress/regress0/uf/proof00.smt2
@@ -0,0 +1,21 @@
+; PROOF
+(set-logic QF_UF)
+(set-info :source |
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information.
+
+This benchmark was obtained by trying to find a finite model of a first-order
+formula (Albert Oliveras).
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun c3 () U)
+(declare-fun f1 (U U) U)
+(declare-fun f4 (U) U)
+(declare-fun c2 () U)
+(declare-fun c_0 () U)
+(declare-fun c_1 () U)
+(assert (let ((?v_1 (f1 c3 c_0))) (let ((?v_0 (f1 ?v_1 c_0)) (?v_2 (f1 c_0 c_0)) (?v_4 (f1 c_0 c_1)) (?v_3 (f1 ?v_1 c_1)) (?v_6 (f1 c3 c_1))) (let ((?v_5 (f1 ?v_6 c_0)) (?v_7 (f1 c_1 c_0)) (?v_9 (f1 c_1 c_1)) (?v_8 (f1 ?v_6 c_1)) (?v_10 (f4 c_0))) (let ((?v_11 (f1 c_0 ?v_10)) (?v_12 (f4 c_1))) (let ((?v_13 (f1 c_1 ?v_12)) (?v_15 (f1 c2 c_0))) (let ((?v_14 (f1 ?v_15 c_0)) (?v_16 (f1 ?v_15 c_1)) (?v_18 (f1 c2 c_1))) (let ((?v_17 (f1 ?v_18 c_0)) (?v_19 (f1 ?v_18 c_1))) (and (distinct c_0 c_1) (= (f1 ?v_0 c_0) (f1 c_0 ?v_2)) (= (f1 ?v_0 c_1) (f1 c_0 ?v_4)) (= (f1 ?v_3 c_0) (f1 c_1 ?v_2)) (= (f1 ?v_3 c_1) (f1 c_1 ?v_4)) (= (f1 ?v_5 c_0) (f1 c_0 ?v_7)) (= (f1 ?v_5 c_1) (f1 c_0 ?v_9)) (= (f1 ?v_8 c_0) (f1 c_1 ?v_7)) (= (f1 ?v_8 c_1) (f1 c_1 ?v_9)) (not (= ?v_11 (f1 ?v_10 ?v_11))) (not (= ?v_13 (f1 ?v_12 ?v_13))) (= (f1 ?v_14 c_0) (f1 (f1 ?v_2 c_0) c_0)) (= (f1 ?v_14 c_1) (f1 (f1 ?v_4 c_0) c_1)) (= (f1 ?v_16 c_0) (f1 (f1 ?v_2 c_1) c_0)) (= (f1 ?v_16 c_1) (f1 (f1 ?v_4 c_1) c_1)) (= (f1 ?v_17 c_0) (f1 (f1 ?v_7 c_0) c_0)) (= (f1 ?v_17 c_1) (f1 (f1 ?v_9 c_0) c_1)) (= (f1 ?v_19 c_0) (f1 (f1 ?v_7 c_1) c_0)) (= (f1 ?v_19 c_1) (f1 (f1 ?v_9 c_1) c_1)) (or (= ?v_2 c_0) (= ?v_2 c_1)) (or (= ?v_4 c_0) (= ?v_4 c_1)) (or (= ?v_7 c_0) (= ?v_7 c_1)) (or (= ?v_9 c_0) (= ?v_9 c_1)) (or (= ?v_10 c_0) (= ?v_10 c_1)) (or (= ?v_12 c_0) (= ?v_12 c_1)) (or (= c3 c_0) (= c3 c_1)) (or (= c2 c_0) (= c2 c_1)))))))))))
+(check-sat)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index e9c17a3af..44517cc0c 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -112,7 +112,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
proof_command='(get-proof)'
lang=smt2
if test -e "$benchmark.expect"; then
- expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes`
+ expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes`
expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -140,7 +140,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
expected_exit_status=10
command_line=
elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then
- expected_proof=
+ expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes`
expected_output=unsat
expected_exit_status=20
command_line=
@@ -276,8 +276,15 @@ fi
if [ "$proof" = yes -a "$expected_proof" = yes ]; then
gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX
- cp "$benchmark" "$pfbenchmark";
- echo "$proof_command" >>"$pfbenchmark";
+ # remove exit command to add proof command for smt2 benchmarks
+ if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
+ head -n -0 "$benchmark" > "$pfbenchmark";
+ echo "$proof_command" >>"$pfbenchmark";
+ echo "(exit)" >> "$pfbenchmark";
+ else
+ cp $benchmark $pfbenchmark
+ echo "$proof_command" >>"$pfbenchmark";
+ fi
echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
time ( :; \
( cd `dirname "$pfbenchmark"`;
@@ -286,6 +293,7 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then
) > "$outfile" 2> "$errfile" )
gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX
+
diff --unchanged-group-format='' \
--old-group-format='' \
--new-group-format='%>' \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback