summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/cnf_stream.cpp179
-rw-r--r--src/prop/cnf_stream.h20
-rw-r--r--src/prop/proof_cnf_stream.h1
-rw-r--r--test/api/CMakeLists.txt1
-rw-r--r--test/api/issue6111.cpp58
5 files changed, 166 insertions, 93 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index f8a34ec42..40853b33a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -292,7 +292,7 @@ SatLiteral CnfStream::getLiteral(TNode node) {
return literal;
}
-SatLiteral CnfStream::handleXor(TNode xorNode)
+void CnfStream::handleXor(TNode xorNode)
{
Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!";
@@ -300,8 +300,8 @@ SatLiteral CnfStream::handleXor(TNode xorNode)
Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
- SatLiteral a = toCNF(xorNode[0]);
- SatLiteral b = toCNF(xorNode[1]);
+ SatLiteral a = getLiteral(xorNode[0]);
+ SatLiteral b = getLiteral(xorNode[1]);
SatLiteral xorLit = newLiteral(xorNode);
@@ -309,11 +309,9 @@ SatLiteral CnfStream::handleXor(TNode xorNode)
assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
assertClause(xorNode, a, ~b, xorLit);
assertClause(xorNode, ~a, b, xorLit);
-
- return xorLit;
}
-SatLiteral CnfStream::handleOr(TNode orNode)
+void CnfStream::handleOr(TNode orNode)
{
Assert(!hasLiteral(orNode)) << "Atom already mapped!";
Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!";
@@ -322,37 +320,31 @@ SatLiteral CnfStream::handleOr(TNode orNode)
Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
// Number of children
- unsigned n_children = orNode.getNumChildren();
-
- // Transform all the children first
- TNode::const_iterator node_it = orNode.begin();
- TNode::const_iterator node_it_end = orNode.end();
- SatClause clause(n_children + 1);
- for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
- clause[i] = toCNF(*node_it);
- }
+ size_t numChildren = orNode.getNumChildren();
// Get the literal for this node
SatLiteral orLit = newLiteral(orNode);
- // lit <- (a_1 | a_2 | a_3 | ... | a_n)
- // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
- // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
- for(unsigned i = 0; i < n_children; ++i) {
+ // Transform all the children first
+ SatClause clause(numChildren + 1);
+ for (size_t i = 0; i < numChildren; ++i)
+ {
+ clause[i] = getLiteral(orNode[i]);
+
+ // lit <- (a_1 | a_2 | a_3 | ... | a_n)
+ // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
+ // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
assertClause(orNode, orLit, ~clause[i]);
}
// lit -> (a_1 | a_2 | a_3 | ... | a_n)
// ~lit | a_1 | a_2 | a_3 | ... | a_n
- clause[n_children] = ~orLit;
+ clause[numChildren] = ~orLit;
// This needs to go last, as the clause might get modified by the SAT solver
assertClause(orNode.negate(), clause);
-
- // Return the literal
- return orLit;
}
-SatLiteral CnfStream::handleAnd(TNode andNode)
+void CnfStream::handleAnd(TNode andNode)
{
Assert(!hasLiteral(andNode)) << "Atom already mapped!";
Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!";
@@ -361,37 +353,32 @@ SatLiteral CnfStream::handleAnd(TNode andNode)
Trace("cnf") << "handleAnd(" << andNode << ")\n";
// Number of children
- unsigned n_children = andNode.getNumChildren();
-
- // Transform all the children first (remembering the negation)
- TNode::const_iterator node_it = andNode.begin();
- TNode::const_iterator node_it_end = andNode.end();
- SatClause clause(n_children + 1);
- for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
- clause[i] = ~toCNF(*node_it);
- }
+ size_t numChildren = andNode.getNumChildren();
// Get the literal for this node
SatLiteral andLit = newLiteral(andNode);
- // lit -> (a_1 & a_2 & a_3 & ... & a_n)
- // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
- // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
- for(unsigned i = 0; i < n_children; ++i) {
+ // Transform all the children first (remembering the negation)
+ SatClause clause(numChildren + 1);
+ for (size_t i = 0; i < numChildren; ++i)
+ {
+ clause[i] = ~getLiteral(andNode[i]);
+
+ // lit -> (a_1 & a_2 & a_3 & ... & a_n)
+ // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
+ // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
assertClause(andNode.negate(), ~andLit, ~clause[i]);
}
// lit <- (a_1 & a_2 & a_3 & ... a_n)
// lit | ~(a_1 & a_2 & a_3 & ... & a_n)
// lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
- clause[n_children] = andLit;
+ clause[numChildren] = andLit;
// This needs to go last, as the clause might get modified by the SAT solver
assertClause(andNode, clause);
-
- return andLit;
}
-SatLiteral CnfStream::handleImplies(TNode impliesNode)
+void CnfStream::handleImplies(TNode impliesNode)
{
Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
Assert(impliesNode.getKind() == kind::IMPLIES)
@@ -401,8 +388,8 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode)
Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
// Convert the children to cnf
- SatLiteral a = toCNF(impliesNode[0]);
- SatLiteral b = toCNF(impliesNode[1]);
+ SatLiteral a = getLiteral(impliesNode[0]);
+ SatLiteral b = getLiteral(impliesNode[1]);
SatLiteral impliesLit = newLiteral(impliesNode);
@@ -415,11 +402,9 @@ SatLiteral CnfStream::handleImplies(TNode impliesNode)
// (a | l) & (~b | l)
assertClause(impliesNode, a, impliesLit);
assertClause(impliesNode, ~b, impliesLit);
-
- return impliesLit;
}
-SatLiteral CnfStream::handleIff(TNode iffNode)
+void CnfStream::handleIff(TNode iffNode)
{
Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
@@ -428,8 +413,8 @@ SatLiteral CnfStream::handleIff(TNode iffNode)
Trace("cnf") << "handleIff(" << iffNode << ")\n";
// Convert the children to CNF
- SatLiteral a = toCNF(iffNode[0]);
- SatLiteral b = toCNF(iffNode[1]);
+ SatLiteral a = getLiteral(iffNode[0]);
+ SatLiteral b = getLiteral(iffNode[1]);
// Get the now literal
SatLiteral iffLit = newLiteral(iffNode);
@@ -447,11 +432,9 @@ SatLiteral CnfStream::handleIff(TNode iffNode)
// (~a | ~b | lit) & (a | b | lit)
assertClause(iffNode, ~a, ~b, iffLit);
assertClause(iffNode, a, b, iffLit);
-
- return iffLit;
}
-SatLiteral CnfStream::handleIte(TNode iteNode)
+void CnfStream::handleIte(TNode iteNode)
{
Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
Assert(iteNode.getKind() == kind::ITE);
@@ -460,9 +443,9 @@ SatLiteral CnfStream::handleIte(TNode iteNode)
Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
<< iteNode[2] << ")\n";
- SatLiteral condLit = toCNF(iteNode[0]);
- SatLiteral thenLit = toCNF(iteNode[1]);
- SatLiteral elseLit = toCNF(iteNode[2]);
+ SatLiteral condLit = getLiteral(iteNode[0]);
+ SatLiteral thenLit = getLiteral(iteNode[1]);
+ SatLiteral elseLit = getLiteral(iteNode[2]);
SatLiteral iteLit = newLiteral(iteNode);
@@ -485,47 +468,79 @@ SatLiteral CnfStream::handleIte(TNode iteNode)
assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
assertClause(iteNode, iteLit, ~condLit, ~thenLit);
assertClause(iteNode, iteLit, condLit, ~elseLit);
-
- return iteLit;
}
SatLiteral CnfStream::toCNF(TNode node, bool negated)
{
Trace("cnf") << "toCNF(" << node
<< ", negated = " << (negated ? "true" : "false") << ")\n";
+
+ TNode cur;
SatLiteral nodeLit;
- Node negatedNode = node.notNode();
-
- // If the non-negated node has already been translated, get the translation
- if(hasLiteral(node)) {
- Trace("cnf") << "toCNF(): already translated\n";
- nodeLit = getLiteral(node);
- // Return the (maybe negated) literal
- return !negated ? nodeLit : ~nodeLit;
- }
- // Handle each Boolean operator case
- switch (node.getKind())
+ std::vector<TNode> visit;
+ std::unordered_map<TNode, bool> cache;
+
+ visit.push_back(node);
+ while (!visit.empty())
{
- case kind::NOT: nodeLit = ~toCNF(node[0]); break;
- case kind::XOR: nodeLit = handleXor(node); break;
- case kind::ITE: nodeLit = handleIte(node); break;
- case kind::IMPLIES: nodeLit = handleImplies(node); break;
- case kind::OR: nodeLit = handleOr(node); break;
- case kind::AND: nodeLit = handleAnd(node); break;
- case kind::EQUAL:
- nodeLit =
- node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node);
- break;
- default:
+ cur = visit.back();
+ Assert(cur.getType().isBoolean());
+
+ if (hasLiteral(cur))
{
- nodeLit = convertAtom(node);
+ visit.pop_back();
+ continue;
}
- break;
+
+ const auto& it = cache.find(cur);
+ if (it == cache.end())
+ {
+ cache.emplace(cur, false);
+ Kind k = cur.getKind();
+ // Only traverse Boolean nodes
+ if (k == kind::NOT || k == kind::XOR || k == kind::ITE
+ || k == kind::IMPLIES || k == kind::OR || k == kind::AND
+ || (k == kind::EQUAL && cur[0].getType().isBoolean()))
+ {
+ // Preserve the order of the recursive version
+ for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
+ {
+ visit.push_back(cur[size - 1 - i]);
+ }
+ }
+ continue;
+ }
+ else if (!it->second)
+ {
+ it->second = true;
+ Kind k = cur.getKind();
+ switch (k)
+ {
+ case kind::NOT: Assert(hasLiteral(cur[0])); break;
+ case kind::XOR: handleXor(cur); break;
+ case kind::ITE: handleIte(cur); break;
+ case kind::IMPLIES: handleImplies(cur); break;
+ case kind::OR: handleOr(cur); break;
+ case kind::AND: handleAnd(cur); break;
+ default:
+ if (k == kind::EQUAL && cur[0].getType().isBoolean())
+ {
+ handleIff(cur);
+ }
+ else
+ {
+ convertAtom(cur);
+ }
+ break;
+ }
+ }
+ visit.pop_back();
}
- // Return the (maybe negated) literal
+
+ nodeLit = getLiteral(node);
Trace("cnf") << "toCNF(): resulting literal: "
<< (!negated ? nodeLit : ~nodeLit) << "\n";
- return !negated ? nodeLit : ~nodeLit;
+ return negated ? ~nodeLit : nodeLit;
}
void CnfStream::convertAndAssertAnd(TNode node, bool negated)
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 264e26777..2959ae726 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -191,16 +191,16 @@ class CnfStream {
*/
SatLiteral toCNF(TNode node, bool negated = false);
- /** Specific clausifiers, based on the formula kinds, that clausify a formula,
- * by calling toCNF into each of the formula's children under the respective
- * kind, and introduce a literal definitionally equal to it. */
- SatLiteral handleNot(TNode node);
- SatLiteral handleXor(TNode node);
- SatLiteral handleImplies(TNode node);
- SatLiteral handleIff(TNode node);
- SatLiteral handleIte(TNode node);
- SatLiteral handleAnd(TNode node);
- SatLiteral handleOr(TNode node);
+ /**
+ * Specific clausifiers that clausify a formula based on the given formula
+ * kind and introduce a literal definitionally equal to it.
+ */
+ void handleXor(TNode node);
+ void handleImplies(TNode node);
+ void handleIff(TNode node);
+ void handleIte(TNode node);
+ void handleAnd(TNode node);
+ void handleOr(TNode node);
/** Stores the literal of the given node in d_literalToNodeMap.
*
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 9972581c0..af131c2c3 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -133,7 +133,6 @@ class ProofCnfStream : public ProofGenerator
* Specific clausifiers, based on the formula kinds, that clausify a formula,
* by calling toCNF into each of the formula's children under the respective
* kind, and introduce a literal definitionally equal to it. */
- SatLiteral handleNot(TNode node);
SatLiteral handleXor(TNode node);
SatLiteral handleImplies(TNode node);
SatLiteral handleIff(TNode node);
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index e9fd47261..4811cca1b 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance)
cvc5_add_api_test(two_solvers)
cvc5_add_api_test(issue5074)
cvc5_add_api_test(issue4889)
+cvc5_add_api_test(issue6111)
# if we've built using libedit, then we want the interactive shell tests
if (USE_EDITLINE)
diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp
new file mode 100644
index 000000000..bd7be2ad0
--- /dev/null
+++ b/test/api/issue6111.cpp
@@ -0,0 +1,58 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Mathias Preiner
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Test for issue #6111
+ *
+ */
+#include <iostream>
+#include <vector>
+
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+using namespace std;
+
+int main()
+{
+ Solver solver;
+ solver.setLogic("QF_BV");
+ Sort bvsort12979 = solver.mkBitVectorSort(12979);
+ Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1");
+ Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10);
+
+ vector<Term> args1;
+ args1.push_back(zero);
+ args1.push_back(input2_1);
+ Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1);
+ solver.assertFormula(bvult_res);
+
+ Sort bvsort4 = solver.mkBitVectorSort(4);
+ Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42");
+ Sort bvsort8 = solver.mkBitVectorSort(8);
+ Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43");
+
+ vector<Term> args2;
+ args2.push_back(concat_result_42);
+ args2.push_back(
+ solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43}));
+ solver.assertFormula(solver.mkTerm(EQUAL, args2));
+
+ vector<Term> args3;
+ args3.push_back(concat_result_42);
+ args3.push_back(
+ solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43}));
+ solver.assertFormula(solver.mkTerm(EQUAL, args3));
+
+ cout << solver.checkSat() << endl;
+
+ return 0;
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback