From 768534c0973788cab0097c6485e5113da1d406da Mon Sep 17 00:00:00 2001 From: guykatzz Date: Fri, 17 Mar 2017 14:11:41 -0700 Subject: [PATCH] better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes --- proofs/signatures/smt.plf | 41 +++++ src/Makefile.am | 2 + src/proof/array_proof.cpp | 27 ++- src/proof/proof_manager.cpp | 13 ++ src/proof/proof_manager.h | 4 + src/proof/simplify_boolean_node.cpp | 183 +++++++++++++++++++ src/proof/simplify_boolean_node.h | 27 +++ src/proof/theory_proof.cpp | 14 ++ src/proof/theory_proof.h | 1 + src/proof/uf_proof.cpp | 109 +++++++---- src/proof/uf_proof.h | 2 + test/regress/regress0/arrays/bool-array.smt2 | 2 - 12 files changed, 383 insertions(+), 42 deletions(-) create mode 100644 src/proof/simplify_boolean_node.cpp create mode 100644 src/proof/simplify_boolean_node.h diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 38428dd1e..06dc16153 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -71,6 +71,7 @@ (! x (term Bool) (! u (th_holds (p_app x)) (th_holds (= Bool x t_true))))) + (declare pred_eq_f (! x (term Bool) (! u (th_holds (not (p_app x))) @@ -104,6 +105,46 @@ (! u1 (th_holds (not (p_app x1))) (th_holds (= Bool x1 x1))))) +(declare pred_not_iff_f + (! x (term Bool) + (! u (th_holds (not (iff false (p_app x)))) + (th_holds (= Bool t_true x))))) + +(declare pred_not_iff_f_2 + (! x (term Bool) + (! u (th_holds (not (iff (p_app x) false))) + (th_holds (= Bool x t_true))))) + +(declare pred_not_iff_t + (! x (term Bool) + (! u (th_holds (not (iff true (p_app x)))) + (th_holds (= Bool t_false x))))) + +(declare pred_not_iff_t_2 + (! x (term Bool) + (! u (th_holds (not (iff (p_app x) true))) + (th_holds (= Bool x t_false))))) + +(declare pred_iff_f + (! x (term Bool) + (! u (th_holds (iff false (p_app x))) + (th_holds (= Bool t_false x))))) + +(declare pred_iff_f_2 + (! x (term Bool) + (! u (th_holds (iff (p_app x) false)) + (th_holds (= Bool x t_false))))) + +(declare pred_iff_t + (! x (term Bool) + (! u (th_holds (iff true (p_app x))) + (th_holds (= Bool t_true x))))) + +(declare pred_iff_t_2 + (! x (term Bool) + (! u (th_holds (iff (p_app x) true)) + (th_holds (= Bool x t_true))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; ; CNF Clausification diff --git a/src/Makefile.am b/src/Makefile.am index c05065c35..85cf3548d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -104,6 +104,8 @@ libcvc4_la_SOURCES = \ proof/unsat_core.h \ proof/proof_output_channel.cpp \ proof/proof_output_channel.h \ + proof/simplify_boolean_node.cpp \ + proof/simplify_boolean_node.h \ prop/cnf_stream.cpp \ prop/cnf_stream.h \ prop/prop_engine.cpp \ diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index af158f37b..6d1bd567d 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -15,9 +15,10 @@ **/ -#include "proof/theory_proof.h" -#include "proof/proof_manager.h" #include "proof/array_proof.h" +#include "proof/proof_manager.h" +#include "proof/simplify_boolean_node.h" +#include "proof/theory_proof.h" #include "theory/arrays/theory_arrays.h" #include @@ -147,6 +148,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, size_t i = 0; while (i < pf->d_children.size()) { + if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + // Look for the negative clause, with which we will form a contradiction. if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { Assert(neg < 0); @@ -318,6 +322,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf->debug_print("mgd", 0, &d_proofPrinter); std::stack stk; for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) { + Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl; + Assert(!pf2->d_node.isNull()); Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || @@ -601,6 +607,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\ndoing trans proof[[\n"; pf->debug_print("mgd", 0, &d_proofPrinter); Debug("mgd") << "\n"; + + pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { @@ -617,6 +626,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, std::stringstream ss1(ss.str()), ss2; ss.str(""); + // In congruences, we can have something like a[x] - it's important to keep these, + // and not turn them into (a[x]=true), because that will mess up the congruence application + // later. + + if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE) + pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + // It is possible that we've already converted the i'th child to stream. If so, // use previously stored result. Otherwise, convert and store. Node n2; @@ -1166,6 +1182,13 @@ void ArrayProof::registerTerm(Expr term) { d_declarations.insert(term); } + if (term.getKind() == kind::SELECT && term.getType().isBoolean()) { + // Ensure cnf literals + Node asNode(term); + ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true))); + ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false))); + } + // recursively declare all other terms for (unsigned i = 0; i < term.getNumChildren(); ++i) { // could belong to other theories diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index ddd2029fb..d8eefdcf0 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -243,6 +243,10 @@ std::string ProofManager::getLitName(TNode lit, return litName; } +bool ProofManager::hasLitName(TNode lit) { + return currentPM()->d_cnfProof->hasLiteral(lit); +} + std::string ProofManager::sanitize(TNode node) { Assert (node.isVar() || node.isConst()); @@ -875,6 +879,11 @@ void ProofManager::addRewriteFilter(const std::string &original, const std::stri d_rewriteFilters[original] = substitute; } +bool ProofManager::haveRewriteFilter(TNode lit) { + std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit)); + return d_rewriteFilters.find(litName) != d_rewriteFilters.end(); +} + void ProofManager::clearRewriteFilters() { d_rewriteFilters.clear(); } @@ -1002,4 +1011,8 @@ void ProofManager::printGlobalLetMap(std::set& atoms, out << std::endl << std::endl; } +void ProofManager::ensureLiteral(Node node) { + d_cnfProof->ensureLiteral(node); +} + } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index fa7224d72..19215589f 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -206,6 +206,8 @@ public: return d_inputFormulas.find(assertion) != d_inputFormulas.end(); } + void ensureLiteral(Node node); + //---from Morgan--- Node mkOp(TNode n); Node lookupOp(TNode n) const; @@ -230,6 +232,7 @@ public: static std::string getAtomName(TNode atom, const std::string& prefix = ""); static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = ""); static std::string getLitName(TNode lit, const std::string& prefix = ""); + static bool hasLitName(TNode lit); // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); @@ -265,6 +268,7 @@ public: void addRewriteFilter(const std::string &original, const std::string &substitute); void clearRewriteFilters(); + bool haveRewriteFilter(TNode lit); void addAssertionFilter(const Node& node, const std::string& rewritten); diff --git a/src/proof/simplify_boolean_node.cpp b/src/proof/simplify_boolean_node.cpp new file mode 100644 index 000000000..34c3f526d --- /dev/null +++ b/src/proof/simplify_boolean_node.cpp @@ -0,0 +1,183 @@ +/********************* */ +/*! \file simplify_boolean_node.h + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simplifying a boolean node, needed for constructing LFSC proofs. + ** + **/ + +#include "cvc4_private.h" + +#include "proof_manager.h" + +namespace CVC4 { + +inline static Node eqNode(TNode n1, TNode n2) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); +} + +Node simplifyBooleanNode(const Node &n) { + if (n.isNull()) + return n; + + // Only simplify boolean nodes + if (!n.getType().isBoolean()) + return n; + + // Sometimes we get sent intermediate nodes that we shouldn't simplify. + // If a node doesn't have a literal, it's clearly intermediate - ignore. + if (!ProofManager::hasLitName(n)) + return n; + + // If we already simplified the node, ignore. + if (ProofManager::currentPM()->haveRewriteFilter(n.negate())) + return n; + + + std::string litName = ProofManager::getLitName(n.negate()); + Node falseNode = NodeManager::currentNM()->mkConst(false); + Node trueNode = NodeManager::currentNM()->mkConst(true); + Node simplified = n; + + // (not (= false b)), (not (= true b))) + if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::EQUAL) && + (n[0][0].getKind() == kind::BOOLEAN_TERM_VARIABLE || n[0][1].getKind() == kind::BOOLEAN_TERM_VARIABLE)) { + Node lhs = n[0][0]; + Node rhs = n[0][1]; + + if (lhs == falseNode) { + Assert(rhs != falseNode); + Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (not (= false b)) --> true = b + + simplified = eqNode(trueNode, rhs); + + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_not_iff_f _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if (rhs == falseNode) { + Assert(lhs != falseNode); + Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (not (= b false)) --> b = true + + simplified = eqNode(lhs, trueNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_not_iff_f_2 _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if (lhs == trueNode) { + Assert(rhs != trueNode); + Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (not (= true b)) --> b = false + + simplified = eqNode(falseNode, rhs); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_not_iff_t _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if (rhs == trueNode) { + Assert(lhs != trueNode); + Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (not (= b true)) --> b = false + + simplified = eqNode(lhs, falseNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_not_iff_t_2 _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + } + + } else if ((n.getKind() == kind::EQUAL) && + (n[0].getKind() == kind::BOOLEAN_TERM_VARIABLE || n[1].getKind() == kind::BOOLEAN_TERM_VARIABLE)) { + Node lhs = n[0]; + Node rhs = n[1]; + + if (lhs == falseNode) { + Assert(rhs != falseNode); + Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (= false b) + + std::stringstream newLitName; + newLitName << "(pred_iff_f _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); + + } else if (rhs == falseNode) { + Assert(lhs != falseNode); + Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (= b false)) + + std::stringstream newLitName; + newLitName << "(pred_iff_f_2 _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); + + } else if (lhs == trueNode) { + Assert(rhs != trueNode); + Assert(rhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (= true b) + + std::stringstream newLitName; + newLitName << "(pred_iff_t _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); + + } else if (rhs == trueNode) { + Assert(lhs != trueNode); + Assert(lhs.getKind() == kind::BOOLEAN_TERM_VARIABLE); + // (= b true) + + + std::stringstream newLitName; + newLitName << "(pred_iff_t_2 _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(litName, newLitName.str()); + } + + } else if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::BOOLEAN_TERM_VARIABLE)) { + // (not b) --> b = false + simplified = eqNode(n[0], falseNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_eq_f _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE) { + // (b) --> b = true + simplified = eqNode(n, trueNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_eq_t _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if ((n.getKind() == kind::NOT) && (n[0].getKind() == kind::SELECT)) { + // not(a[x]) --> a[x] = false + simplified = eqNode(n[0], falseNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_eq_f _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + + } else if (n.getKind() == kind::SELECT) { + // a[x] --> a[x] = true + simplified = eqNode(n, trueNode); + std::string simplifiedLitName = ProofManager::getLitName(simplified.negate()); + std::stringstream newLitName; + newLitName << "(pred_eq_t _ " << litName << ")"; + ProofManager::currentPM()->addRewriteFilter(simplifiedLitName, newLitName.str()); + } + + if (simplified != n) + Debug("pf::simplify") << "simplifyBooleanNode: " << n << " --> " << simplified << std::endl; + + return simplified; +} + +}/* CVC4 namespace */ diff --git a/src/proof/simplify_boolean_node.h b/src/proof/simplify_boolean_node.h new file mode 100644 index 000000000..dcf7e93db --- /dev/null +++ b/src/proof/simplify_boolean_node.h @@ -0,0 +1,27 @@ +/********************* */ +/*! \file simplify_boolean_node.h + ** \verbatim + ** Top contributors (to current version): + ** Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simplifying a boolean node, needed for constructing LFSC proofs. + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H +#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H + +namespace CVC4 { + +Node simplifyBooleanNode(const Node &n); + +}/* CVC4 namespace */ + +#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index e245117fd..c684aa6bc 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1092,6 +1092,20 @@ void BooleanProof::registerTerm(Expr term) { } } +void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { + Node falseNode = NodeManager::currentNM()->mkConst(false); + Node trueNode = NodeManager::currentNM()->mkConst(true); + + Assert(c1 == falseNode.toExpr() || c1 == trueNode.toExpr()); + Assert(c2 == falseNode.toExpr() || c2 == trueNode.toExpr()); + Assert(c1 != c2); + + if (c1 == trueNode.toExpr()) + os << "t_t_neq_f"; + else + os << "(negsymm _ _ _ t_t_neq_f)"; +} + void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index bbdb7d6d7..b9fb33406 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -332,6 +332,7 @@ public: virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); bool printsAsBool(const Node &n); + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); }; } /* CVC4 namespace */ diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index c38fa1403..cea873b6d 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -1,22 +1,23 @@ /********************* */ /*! \file uf_proof.cpp - ** \verbatim - ** Top contributors (to current version): - ** Liana Hadarean, Guy Katz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** [[ Add lengthier description here ]] - - ** \todo document this file +** \verbatim +** Top contributors (to current version): +** Liana Hadarean, Guy Katz +** This file is part of the CVC4 project. +** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file COPYING in the top-level source +** directory for licensing information.\endverbatim +** +** [[ Add lengthier description here ]] + +** \todo document this file **/ -#include "proof/theory_proof.h" #include "proof/proof_manager.h" +#include "proof/simplify_boolean_node.h" +#include "proof/theory_proof.h" #include "proof/uf_proof.h" #include "theory/uf/theory_uf.h" #include @@ -110,10 +111,14 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E subTrans.d_node = pf->d_node; size_t i = 0; + while (i < pf->d_children.size()) { + pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + // Look for the negative clause, with which we will form a contradiction. if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) { Assert(neg < 0); + Node node = pf->d_children[i]->d_node[0]; neg = i; ++i; } @@ -128,8 +133,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "Collecting congruence sequence" << std::endl; for (count = 0; i + count < pf->d_children.size() && - pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && - pf->d_children[i + count]->d_node.isNull(); + pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && + pf->d_children[i + count]->d_node.isNull(); ++count) { Debug("pf::uf") << "Found a congruence: " << std::endl; pf->d_children[i+count]->debug_print("pf::uf"); @@ -154,13 +159,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E targetAppearsAfter = false; } - // Assert that we have precisely one target clause. - Assert(targetAppearsBefore != targetAppearsAfter); + // Assert that we have precisely at least one possible clause. + Assert(targetAppearsBefore || targetAppearsAfter); + + // If both are valid, assume the one after the sequence is correct + if (targetAppearsAfter && targetAppearsBefore) + targetAppearsBefore = false; // Begin breaking up the congruences and ordering the equalities correctly. std::vector orderedEqualities; - // Insert target clause first. if (targetAppearsBefore) { orderedEqualities.push_back(pf->d_children[i - 1]); @@ -176,7 +184,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]); if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY) - orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); + orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]); } } else { for (unsigned j = 0; j < count; ++j) { @@ -231,6 +239,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E if (disequalityFound) { Node n2 = pf->d_children[neg]->d_node; Assert(n2.getKind() == kind::NOT); + Debug("pf::uf") << "n2 is " << n2[0] << std::endl; if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; } @@ -248,6 +257,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << ss.str(); } out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl; + } else if (n2[0].getKind() == kind::BOOLEAN_TERM_VARIABLE) { + out << ss.str() << " " << ProofManager::getLitName(n2[0]) << "))"; } else { Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1])); if(n1[1] == n2[0][0]) { @@ -308,8 +319,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "SIDE IS 1\n"; //} if(!match(pf2->d_node, n1[1])) { - Debug("pf::uf") << "IN BAD CASE, our first subproof is\n"; - pf2->d_children[0]->debug_print("pf::uf"); + Debug("pf::uf") << "IN BAD CASE, our first subproof is\n"; + pf2->d_children[0]->debug_print("pf::uf"); } Assert(match(pf2->d_node, n1[1])); side = 1; @@ -352,7 +363,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E out << ")"; while(!stk.empty()) { if(tb == 1) { - Debug("pf::uf") << "\nMORE TO DO\n"; + Debug("pf::uf") << "\nMORE TO DO\n"; } pf2 = stk.top(); stk.pop(); @@ -410,7 +421,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } Node n = (side == 0 ? eqNode(n1, n2) : eqNode(n2, n1)); if(tb == 1) { - Debug("pf::uf") << "\ncong proved: " << n << "\n"; + Debug("pf::uf") << "\ncong proved: " << n << "\n"; } return n; } @@ -436,6 +447,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "\ndoing trans proof[[\n"; pf->debug_print("pf::uf"); Debug("pf::uf") << "\n"; + + pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node); + Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map); Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { @@ -452,6 +466,8 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E std::stringstream ss1(ss.str()), ss2; ss.str(""); + pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node); + // It is possible that we've already converted the i'th child to stream. If so, // use previously stored result. Otherwise, convert and store. Node n2; @@ -524,7 +540,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ss << " (symm _ _ _ " << ss1.str() << ")" << ss1.str(); } else { Debug("pf::uf") << "Error: identical equalities over, but hands don't match what we're proving." - << std::endl; + << std::endl; Assert(false); } } else { @@ -595,18 +611,18 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { - if(tb == 1) { Debug("pf::uf") << "case 1\n"; } - n1 = eqNode(n1[1], n2[1]); - ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); + if(tb == 1) { Debug("pf::uf") << "case 1\n"; } + n1 = eqNode(n1[1], n2[1]); + ss << "(symm _ _ _ " << ss1.str() << ") " << ss2.str(); } else if(n1[1] == n2[1]) { if(tb == 1) { Debug("pf::uf") << "case 2\n"; } n1 = eqNode(n1[0], n2[0]); ss << ss1.str() << " (symm _ _ _ " << ss2.str() << ")"; } else if(n1[0] == n2[1]) { - if(tb == 1) { Debug("pf::uf") << "case 3\n"; } - n1 = eqNode(n2[0], n1[1]); - ss << ss2.str() << " " << ss1.str(); - if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; } + if(tb == 1) { Debug("pf::uf") << "case 3\n"; } + n1 = eqNode(n2[0], n1[1]); + ss << ss2.str() << " " << ss1.str(); + if(tb == 1) { Debug("pf::uf") << "++ proved " << n1 << "\n"; } } else if(n1[1] == n2[0]) { if(tb == 1) { Debug("pf::uf") << "case 4\n"; } n1 = eqNode(n1[0], n2[1]); @@ -646,9 +662,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else { // Both n1 and n2 are predicates. // We want to prove b1 = b2, and we know that ((b1), (b2)) or ((not b1), (not b2)) - Debug("gk::temp") << "Two-predicate case. pf->d_node = " << pf->d_node - << ", n1 = " << n1 << ", n2 = " << n2 << std::endl; - if (n1.getKind() == kind::NOT) { Assert(n2.getKind() == kind::NOT); Assert(pf->d_node[0] == n1[0] || pf->d_node[0] == n2[0]); @@ -687,7 +700,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E ss << ")"; } - out << ss.str(); Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl; return n1; @@ -724,6 +736,14 @@ void UFProof::registerTerm(Expr term) { if (term.isVariable()) { d_declarations.insert(term); + + + if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { + // Ensure cnf literals + Node asNode(term); + ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(true))); + ProofManager::currentPM()->ensureLiteral(eqNode(term, NodeManager::currentNM()->mkConst(false))); + } } // recursively declare all other terms @@ -756,6 +776,7 @@ 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); @@ -839,13 +860,25 @@ 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; +bool LFSCUFProof::printsAsBool(const Node &n) { if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE) return true; return false; } +void LFSCUFProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { + Node falseNode = NodeManager::currentNM()->mkConst(false); + Node trueNode = NodeManager::currentNM()->mkConst(true); + + Assert(c1 == falseNode.toExpr() || c1 == trueNode.toExpr()); + Assert(c2 == falseNode.toExpr() || c2 == trueNode.toExpr()); + Assert(c1 != c2); + + if (c1 == trueNode.toExpr()) + os << "t_t_neq_f"; + else + os << "(symm _ _ _ t_t_neq_f)"; +} + } /* namespace CVC4 */ diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index 221a50f43..c4bd28dc5 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -73,6 +73,8 @@ public: virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap); bool printsAsBool(const Node &n); + + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); }; diff --git a/test/regress/regress0/arrays/bool-array.smt2 b/test/regress/regress0/arrays/bool-array.smt2 index f05d0266b..0e5920384 100644 --- a/test/regress/regress0/arrays/bool-array.smt2 +++ b/test/regress/regress0/arrays/bool-array.smt2 @@ -1,4 +1,3 @@ -; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores ; EXPECT: unsat (set-logic QF_AX) (set-info :status unsat) @@ -10,4 +9,3 @@ (assert (= (select a true) (select a false))) (check-sat) - -- 2.30.2