Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

1 files changed, 40 insertions, 38 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index dc4722fa1..7df5fb492 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -19,7 +19,7 @@
 
 #include <queue>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/node.h"
@@ -138,12 +138,14 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
     return;
   }
 
-  AlwaysAssertArgument(n.getType().isBoolean(), n,
-                       "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
-                       "got node: %s\n"
-                       "its type: %s\n",
-                       n.toString().c_str(),
-                       n.getType().toString().c_str());
+  AlwaysAssertArgument(
+      n.getType().isBoolean(),
+      n,
+      "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
+      "got node: %s\n"
+      "its type: %s\n",
+      n.toString().c_str(),
+      n.getType().toString().c_str());
 
   bool negated CVC4_UNUSED = false;
   SatLiteral lit;
@@ -231,14 +233,14 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
 }
 
 void CnfStream::setProof(CnfProof* proof) {
-  Assert (d_cnfProof == NULL);
+  Assert(d_cnfProof == NULL);
   d_cnfProof = proof;
 }
 
 SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
-  Assert(!hasLiteral(node), "atom already mapped!");
+  Assert(!hasLiteral(node)) << "atom already mapped!";
 
   bool theoryLiteral = false;
   bool canEliminate = true;
@@ -260,11 +262,10 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
 }
 
 SatLiteral CnfStream::getLiteral(TNode node) {
-  Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
+  Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
 
-  Assert(d_nodeToLiteralMap.contains(node),
-         "Literal not in the CNF Cache: %s\n",
-         node.toString().c_str());
+  Assert(d_nodeToLiteralMap.contains(node))
+      << "Literal not in the CNF Cache: " << node << "\n";
 
   SatLiteral literal = d_nodeToLiteralMap[node];
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
@@ -272,10 +273,10 @@ SatLiteral CnfStream::getLiteral(TNode node) {
 }
 
 SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
-  Assert(!hasLiteral(xorNode), "Atom already mapped!");
-  Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
-  Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
-  Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+  Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
+  Assert(xorNode.getKind() == XOR) << "Expecting an XOR expression!";
+  Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 
   SatLiteral a = toCNF(xorNode[0]);
   SatLiteral b = toCNF(xorNode[1]);
@@ -291,10 +292,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 }
 
 SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
-  Assert(!hasLiteral(orNode), "Atom already mapped!");
-  Assert(orNode.getKind() == OR, "Expecting an OR expression!");
-  Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
-  Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+  Assert(!hasLiteral(orNode)) << "Atom already mapped!";
+  Assert(orNode.getKind() == OR) << "Expecting an OR expression!";
+  Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 
   // Number of children
   unsigned n_children = orNode.getNumChildren();
@@ -328,10 +329,10 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
 }
 
 SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
-  Assert(!hasLiteral(andNode), "Atom already mapped!");
-  Assert(andNode.getKind() == AND, "Expecting an AND expression!");
-  Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
-  Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+  Assert(!hasLiteral(andNode)) << "Atom already mapped!";
+  Assert(andNode.getKind() == AND) << "Expecting an AND expression!";
+  Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 
   // Number of children
   unsigned n_children = andNode.getNumChildren();
@@ -365,10 +366,11 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
 }
 
 SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
-  Assert(!hasLiteral(impliesNode), "Atom already mapped!");
-  Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
-  Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
-  Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+  Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
+  Assert(impliesNode.getKind() == IMPLIES)
+      << "Expecting an IMPLIES expression!";
+  Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 
   // Convert the children to cnf
   SatLiteral a = toCNF(impliesNode[0]);
@@ -391,9 +393,9 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
 
 SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
-  Assert(!hasLiteral(iffNode), "Atom already mapped!");
-  Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!");
-  Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
+  Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
+  Assert(iffNode.getKind() == EQUAL) << "Expecting an EQUAL expression!";
+  Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
 
   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
 
@@ -423,9 +425,9 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
 
 
 SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
-  Assert(!hasLiteral(notNode), "Atom already mapped!");
-  Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
-  Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!");
+  Assert(!hasLiteral(notNode)) << "Atom already mapped!";
+  Assert(notNode.getKind() == NOT) << "Expecting a NOT expression!";
+  Assert(notNode.getNumChildren() == 1) << "Expecting exactly 1 child!";
 
   SatLiteral notLit = ~toCNF(notNode[0]);
 
@@ -435,7 +437,7 @@ SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
 SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   Assert(iteNode.getKind() == ITE);
   Assert(iteNode.getNumChildren() == 3);
-  Assert(!d_removable, "Removable clauses can not contain Boolean structure");
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 
   Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
 
@@ -539,7 +541,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
     SatClause clause(nChildren);
     TNode::const_iterator disjunct = node.begin();
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
-      Assert( disjunct != node.end() );
+      Assert(disjunct != node.end());
       clause[i] = toCNF(*disjunct, true);
     }
     Assert(disjunct == node.end());
@@ -555,7 +557,7 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
     SatClause clause(nChildren);
     TNode::const_iterator disjunct = node.begin();
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
-      Assert( disjunct != node.end() );
+      Assert(disjunct != node.end());
       clause[i] = toCNF(*disjunct, false);
     }
     Assert(disjunct == node.end());