fixed proof regression script and added a new uf test case

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index cb22ca819924e7e7f2bd93784bf9351d386cab26..8e9c4cd214febcadf5272eed340331914b8e7b43 100644 (file)
--- 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 23ba0e4e710e7bc7d133a99cd01305050a779999..110e6b79af1bfbc0b88cdad948ab9edcb6e889d6 100644 (file)
--- 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 7642ba776e520bcb9612cfd6c0e1707d3334fd30..82a1bd6be3690d70db02a567fca1fa9b31579d66 100644 (file)
--- 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 2ac468b47c25b38b24f3179d9b1f2758f661858b..da9df0d424a8f1f8a995caa7227836ebc01cc70c 100644 (file)
--- 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 4ce804a74fec9e13bf0fd78ea288f44c20ae7ed2..696bd8309ca3e743fae7230c899505d6f855fb83 100644 (file)
--- 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 32d0d1703746916a22c74e0938bf562604d5d931..0cfb674cf549582aaabf33e662b3a6d28b270fd7 100644 (file)
--- 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 bf9a36df1186d2413e45cd13b59ebeaed8dbb1dd..19e673fea858697a7e140fe98a6b19c06354f7ed 100644 (file)
--- 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 (file)
index 0000000..1b7e7b8
--- /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 e9c17a3af2aeafe4836d73234cdd18e18306129f..44517cc0c2dd6e8dbcbe3199f5f13b658793ae21 100755 (executable)
--- 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='%>' \