(! 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)))
(! 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
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 \
**/
-#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 <stack>
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);
pf->debug_print("mgd", 0, &d_proofPrinter);
std::stack<const theory::eq::EqProof*> 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 ||
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) {
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;
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
return litName;
}
+bool ProofManager::hasLitName(TNode lit) {
+ return currentPM()->d_cnfProof->hasLiteral(lit);
+}
+
std::string ProofManager::sanitize(TNode node) {
Assert (node.isVar() || node.isConst());
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();
}
out << std::endl << std::endl;
}
+void ProofManager::ensureLiteral(Node node) {
+ d_cnfProof->ensureLiteral(node);
+}
+
} /* CVC4 namespace */
return d_inputFormulas.find(assertion) != d_inputFormulas.end();
}
+ void ensureLiteral(Node node);
+
//---from Morgan---
Node mkOp(TNode n);
Node lookupOp(TNode n) const;
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);
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);
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
}
}
+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()) {
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 */
/********************* */
/*! \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 <stack>
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;
}
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");
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<theory::eq::EqProof *> orderedEqualities;
-
// Insert target clause first.
if (targetAppearsBefore) {
orderedEqualities.push_back(pf->d_children[i - 1]);
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) {
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; }
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]) {
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;
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();
}
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;
}
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) {
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;
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 {
// 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]);
} 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]);
ss << ")";
}
-
out << ss.str();
Debug("pf::uf") << "\n++ trans proof done, have proven " << n1 << std::endl;
return n1;
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
}
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);
// 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 */
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);
};
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
; EXPECT: unsat
(set-logic QF_AX)
(set-info :status unsat)
(assert (= (select a true) (select a false)))
(check-sat)
-
projects / cvc5.git / commitdiff