better proof support for bools and formulas

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index fa89a457f2aa479481077749a1b23fc9539a0fbb..6d04c3004c1dc8038ef920bee2a532f6e4a665c9 100644 (file)
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -20,13 +20,13 @@
        (! f1 formula
        (! f2 formula
           formula)))
-       
+
 (define formula_op3
        (! f1 formula
        (! f2 formula
        (! f3 formula
           formula))))
-          
+
 (declare not formula_op1)
 (declare and formula_op2)
 (declare or formula_op2)
@@ -76,6 +76,10 @@
  (! u (th_holds (not (p_app x)))
    (th_holds (= Bool x t_false)))))
 
+(declare f_to_b
+  (! f formula
+    (term Bool)))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
 ; CNF Clausification
@@ -107,8 +111,8 @@
        (! vbv (bvatom v bv_v)
          (holds cln))))))
     (holds cln))))
-    
-    
+
+
 ; clausify a formula directly
 (declare clausify_form
   (! f formula
@@ -116,14 +120,14 @@
   (! a (atom v f)
   (! u (th_holds f)
     (holds (clc (pos v) cln)))))))
-    
+
 (declare clausify_form_not
   (! f formula
   (! v var
   (! a (atom v f)
   (! u (th_holds (not f))
     (holds (clc (neg v) cln)))))))
-    
+
 (declare clausify_false
   (! u (th_holds false)
     (holds cln)))
@@ -134,7 +138,7 @@
   (! u2 (! v (th_holds f) (holds cln))
     (holds cln)))))
 
-  
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
 ; Natural deduction rules : used for CNF
@@ -191,7 +195,7 @@
   (! f2 formula
   (! u2 (th_holds (not (or f1 f2)))
     (th_holds (and (not f1) (not f2)))))))
-    
+
 ;; and elimination
 
 (declare and_elim_1
@@ -211,7 +215,7 @@
   (! f2 formula
   (! u2 (th_holds (not (and f1 f2)))
     (th_holds (or (not f1) (not f2)))))))
-    
+
 ;; impl elimination
 
 (declare impl_intro (! f1 formula
@@ -231,7 +235,7 @@
   (! f2 formula
   (! u (th_holds (not (impl f1 f2)))
     (th_holds (and f1 (not f2)))))))
-    
+
 ;; iff elimination
 
 (declare iff_elim_1
@@ -358,10 +362,10 @@
   (! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof
          (holds C))
     (holds (clc (pos v) C))))))))))
-    
+
 (declare bv_ast
   (! v var
-  (! bv_v var  
+  (! bv_v var
   (! f formula
   (! C clause
   (! r (atom v f)       ; this is specified
@@ -397,7 +401,7 @@
 ;;     ...
 ;;      (or_elim_1 _ _ l2
 ;;     (or_elim_1 _ _ l1 A))))) ln)
-;;     
+;;
 ;;))))))) (\ C
 ;;
 ;; We now have the free variable C, which should be the clause (v1 V ... V vn).
@@ -415,9 +419,7 @@
 ;;   (contra _ l3
 ;;      (or_elim_1 _ _ l2
 ;;     (or_elim_1 _ _ (not_not_intro l1) A))))
-;;     
+;;
 ;;))))))) (\ C
 ;;
 ;; C should be the clause (~v1 V v2 V ~v3 )
-
-

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index cc60d8c07417b21b97d65ce8c364178cfc85f1be..af158f37b788dc7ea05b9b914e112265c99171d4 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1197,8 +1197,11 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
   Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE));
 
   switch (term.getKind()) {
-  case kind::SELECT:
+  case kind::SELECT: {
     Assert(term.getNumChildren() == 2);
+
+    bool convertToBool = (term[1].getType().isBoolean() && !d_proofEngine->printsAsBool(term[1]));
+
     os << "(apply _ _ (apply _ _ (read ";
     printSort(ArrayType(term[0].getType()).getIndexType(), os);
     os << " ";
@@ -1206,9 +1209,12 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
     os << ") ";
     printTerm(term[0], os, map);
     os << ") ";
+    if (convertToBool) os << "(f_to_b ";
     printTerm(term[1], os, map);
+    if (convertToBool) os << ")";
     os << ") ";
     return;
+  }
 
   case kind::PARTIAL_SELECT_0:
     Assert(term.getNumChildren() == 1);
@@ -1381,7 +1387,15 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
 }
 
 void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
-    // Nothing to do here at this point.
+  // Nothing to do here at this point.
+}
+
+bool LFSCArrayProof::printsAsBool(const Node &n)
+{
+  if (n.getKind() == kind::SELECT)
+    return true;
+
+  return false;
 }
 
 } /* CVC4  namespace */

diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 61f168a163ab584cf4b08d75c90a6726c70d2193..eaf2f47fb8a645e4f3fbc8eed33d824ceb6c14a3 100644 (file)
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -125,6 +125,8 @@ public:
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+
+  bool printsAsBool(const Node &n);
 };
 
 

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 69b613f28b589240189e37e57a1aece6082c9cd3..d1a228ecb80c494df08b99adb0195fa96fe8104a 100644 (file)
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -350,8 +350,9 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
     prop::SatVariable var = getLiteral(atom).getSatVariable();
     //FIXME hideous
     LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
-    // pe->printLetTerm(atom.toExpr(), os);
+    if (pe->printsAsBool(atom.toExpr())) os << "(p_app ";
     pe->printBoundTerm(atom.toExpr(), os, letMap);
+    if (pe->printsAsBool(atom.toExpr())) os << ")";
 
     os << " (\\ " << ProofManager::getVarName(var, d_name);
     os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5ce615366716901134481a2f965360e351b4fe77..ddd2029fbaba008d5bebb1624bd7357876fa9052 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -565,6 +565,7 @@ void LFSCProof::toStream(std::ostream& out) {
     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 
   std::set<Node> atoms;
+
   NodePairSet rewrites;
   // collects the atoms in the clauses
   d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
@@ -779,7 +780,9 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
       //TODO
       os << "(trust_f ";
+      if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app ";
       ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
+      if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")";
       os << ") ";
 
       os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 156c90e472c7fb04319b34ff0a01cb1a280f2cbf..65f66ce29980bf44ff7d368c67eb43eb6b03d2a0 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -299,14 +299,6 @@ void LFSCTheoryProofEngine::performExtraRegistrations() {
   }
 }
 
-void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
-  TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
-  TheoryProofTable::const_iterator end = d_theoryProofTable.end();
-  for (; it != end; ++it) {
-    it->second->treatBoolsAsFormulas(value);
-  }
-}
-
 void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
@@ -330,7 +322,11 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
 
     // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
     ProofLetMap dummyMap;
+
+    bool convertFromBool = (it->getType().isBoolean() && printsAsBool(*it));
+    if (convertFromBool) os << "(p_app ";
     printBoundTerm(*it, os, dummyMap);
+    if (convertFromBool) os << ")";
 
     os << ")\n";
     paren << ")";
@@ -843,31 +839,47 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
   Kind k = term.getKind();
 
   switch(k) {
-  case kind::ITE:
+  case kind::ITE: {
     os << (term.getType().isBoolean() ? "(ifte ": "(ite _ ");
 
+    bool booleanCase = term[0].getType().isBoolean();
+    if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
     printBoundTerm(term[0], os, map);
+    if (booleanCase && printsAsBool(term[0])) os << ")";
+
     os << " ";
     printBoundTerm(term[1], os, map);
     os << " ";
     printBoundTerm(term[2], os, map);
     os << ")";
     return;
+  }
+
+  case kind::EQUAL: {
+    bool booleanCase = term[0].getType().isBoolean();
 
-  case kind::EQUAL:
     os << "(";
-    if( term[0].getType().isBoolean() ){
+    if (booleanCase) {
       os << "iff ";
-    }else{
+    } else {
       os << "= ";
       printSort(term[0].getType(), os);
       os << " ";
     }
+
+    if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
     printBoundTerm(term[0], os, map);
+    if (booleanCase && printsAsBool(term[0])) os << ")";
+
     os << " ";
+
+    if (booleanCase && printsAsBool(term[1])) os << "(p_app ";
     printBoundTerm(term[1], os, map);
+    if (booleanCase && printsAsBool(term[1])) os << ") ";
     os << ")";
+
     return;
+  }
 
   case kind::DISTINCT:
     // Distinct nodes can have any number of chidlren.
@@ -917,9 +929,11 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
     // arguments, so we have to flatten chained operators, like =.
     Kind op = term.getOperator().getConst<Chain>().getOperator();
     std::string op_str;
-    if( op==kind::EQUAL && term[0].getType().isBoolean() ){
+    bool booleanCase;
+    if (op==kind::EQUAL && term[0].getType().isBoolean()) {
+      booleanCase = term[0].getType().isBoolean();
       op_str = "iff";
-    }else{
+    } else {
       op_str = utils::toLFSCKind(op);
     }
     size_t n = term.getNumChildren();
@@ -930,9 +944,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
         paren << ")";
       }
       os << "(" << op_str << " ";
+      if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app ";
       printBoundTerm(term[i - 1], os, map);
+      if (booleanCase && printsAsBool(term[i - 1])) os << ")";
       os << " ";
+      if (booleanCase && printsAsBool(term[i])) os << "(p_app ";
       printBoundTerm(term[i], os, map);
+      if (booleanCase && printsAsBool(term[i])) os << ")";
       os << ")";
       if(i + 1 < n) {
         os << " ";
@@ -1049,6 +1067,15 @@ bool TheoryProofEngine::supportedTheory(theory::TheoryId id) {
           id == theory::THEORY_BOOL);
 }
 
+bool TheoryProofEngine::printsAsBool(const Node &n) {
+  if (!n.getType().isBoolean()) {
+    return false;
+  }
+
+  theory::TheoryId theory_id = theory::Theory::theoryOf(n);
+  return getTheoryProof(theory_id)->printsAsBool(n);
+}
+
 BooleanProof::BooleanProof(TheoryProofEngine* proofEngine)
   : TheoryProof(NULL, proofEngine)
 {}
@@ -1068,10 +1095,7 @@ void BooleanProof::registerTerm(Expr term) {
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
-    if (d_treatBoolsAsFormulas)
-      os << "(p_app " << ProofManager::sanitize(term) <<")";
-    else
-      os << ProofManager::sanitize(term);
+    os << ProofManager::sanitize(term);
     return;
   }
 
@@ -1116,7 +1140,11 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
       std::ostringstream paren;
       os << " ";
       for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+
+        if (printsAsBool(term[i])) os << "(p_app ";
         d_proofEngine->printBoundTerm(term[i], os, map);
+        if (printsAsBool(term[i])) os << ")";
+
         os << " ";
         if(i < term.getNumChildren() - 2) {
           os << "(" << utils::toLFSCKind(k) << " ";
@@ -1128,17 +1156,16 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
       // this is for binary and unary operators
       for (unsigned i = 0; i < term.getNumChildren(); ++i) {
         os << " ";
+        if (printsAsBool(term[i])) os << "(p_app ";
         d_proofEngine->printBoundTerm(term[i], os, map);
+        if (printsAsBool(term[i])) os << ")";
       }
       os << ")";
     }
     return;
 
   case kind::CONST_BOOLEAN:
-    if (d_treatBoolsAsFormulas)
-      os << (term.getConst<bool>() ? "true" : "false");
-    else
-      os << (term.getConst<bool>() ? "t_true" : "t_false");
+    os << (term.getConst<bool>() ? "true" : "false");
     return;
 
   default:
@@ -1182,6 +1209,19 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
   Unreachable("No boolean lemmas yet!");
 }
 
+bool LFSCBooleanProof::printsAsBool(const Node &n)
+{
+  Kind k = n.getKind();
+  switch (k) {
+  case kind::BOOLEAN_TERM_VARIABLE:
+  case kind::VARIABLE:
+    return true;
+
+  default:
+    return false;
+  }
+}
+
 void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
   // By default, we just print a trust statement. Specific theories can implement
   // better proofs.

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 34248f7ebdc05d4f8e1d1d60d35b971eb00e949f..bbdb7d6d7c161f797cfa262aa96d54ec6b4fcf40 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -151,9 +151,9 @@ public:
 
   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 
-  virtual void treatBoolsAsFormulas(bool value) {};
-
   virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
+
+  bool printsAsBool(const Node &n);
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -182,7 +182,6 @@ public:
 
   void performExtraRegistrations();
 
-  void treatBoolsAsFormulas(bool value);
   void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
 
 private:
@@ -294,7 +293,11 @@ public:
    */
   virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 
-  virtual void treatBoolsAsFormulas(bool value) {}
+  // Return true if node prints as bool, false if it prints as a formula.
+  virtual bool printsAsBool(const Node &n) {
+    // Most nodes print as formulas, so this is the default.
+    return false;
+  }
 };
 
 class BooleanProof : public TheoryProof {
@@ -318,7 +321,7 @@ public:
 class LFSCBooleanProof : public BooleanProof {
 public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
-    : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
+    : BooleanProof(proofEngine)
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
@@ -328,12 +331,7 @@ public:
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 
-  void treatBoolsAsFormulas(bool value) {
-    d_treatBoolsAsFormulas = value;
-  }
-
-private:
-  bool d_treatBoolsAsFormulas;
+  bool printsAsBool(const Node &n);
 };
 
 } /* CVC4 namespace */

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 41262051c518a058b4830789f71cf965eb71c64d..d3da2bcdbb18b55eebe533a5eee6f33577e184a4 100644 (file)
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -701,17 +701,13 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
 
   if (term.getKind() == kind::VARIABLE ||
-      term.getKind() == kind::SKOLEM) {
+      term.getKind() == kind::SKOLEM ||
+      term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
     os << term;
     return;
   }
-  if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
-    os << "(p_app " << term << ")";
-    return;
-  }
 
   Assert (term.getKind() == kind::APPLY_UF);
-  d_proofEngine->treatBoolsAsFormulas(false);
 
   if(term.getType().isBoolean()) {
     os << "(p_app ";
@@ -722,13 +718,15 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
   }
   os << func << " ";
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
+    if (convertToBool) os << "(f_to_b ";
     d_proofEngine->printBoundTerm(term[i], os, map);
+    if (convertToBool) os << ")";
     os << ")";
   }
   if(term.getType().isBoolean()) {
     os << ")";
   }
-  d_proofEngine->treatBoolsAsFormulas(true);
 }
 
 void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
@@ -803,4 +801,13 @@ void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& pare
   // Nothing to do here at this point.
 }
 
+bool LFSCUFProof::printsAsBool(const Node &n)
+{
+  Debug("gk::temp") << "\nUF printsAsBool: " << n << std::endl;
+  if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+    return true;
+
+  return false;
+}
+
 } /* namespace CVC4 */

diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index ff0f9a8799d27cccee86d5cc8c11b234701a9319..221a50f4305c32ec5fb254a35fc215f1d44b991d 100644 (file)
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -71,6 +71,8 @@ public:
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+
+  bool printsAsBool(const Node &n);
 };
 
 

diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2
index cd3e1137e4344e97aa35af41c5d3ebf6f8ecab39..51780654283d8f8a19f06d6d382f0bfd302d27a5 100644 (file)
--- a/test/regress/regress0/bt-test-00.smt2
+++ b/test/regress/regress0/bt-test-00.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :smt-lib-version 2.0)

diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2
index 918dcf9ecaa0aea5165068136f91c36f7ed754a5..e17bd2d7a97fa06587586c10134cc402c513a0fe 100644 (file)
--- a/test/regress/regress0/bt-test-01.smt2
+++ b/test/regress/regress0/bt-test-01.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :smt-lib-version 2.0)

diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 34cfcad330c26bb2167b1225ec5c2cf1bcfce94b..4d2e828b56582e17b5f8fe0eaf8a7504e7070b33 100644 (file)
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)