From 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 Oct 2019 15:27:10 -0700
Subject: Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

---
 src/theory/arith/arith_rewriter.cpp | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'src/theory/arith/arith_rewriter.cpp')

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 86e5b3195..c8a03fab1 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -50,7 +50,7 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){
 }
 
 RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
-  Assert(t.getKind()== kind::MINUS);
+  Assert(t.getKind() == kind::MINUS);
 
   if(pre){
     if(t[0] == t[1]){
@@ -70,7 +70,7 @@ RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
 }
 
 RewriteResponse ArithRewriter::rewriteUMinus(TNode t, bool pre){
-  Assert(t.getKind()== kind::UMINUS);
+  Assert(t.getKind() == kind::UMINUS);
 
   if(t[0].getKind() == kind::CONST_RATIONAL){
     Rational neg = -(t[0].getConst<Rational>());
@@ -143,8 +143,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       return RewriteResponse(REWRITE_DONE, t);
     case kind::PI:
       return RewriteResponse(REWRITE_DONE, t);
-    default:
-      Unhandled(k);
+    default: Unhandled() << k;
     }
   }
 }
@@ -263,7 +262,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
 
 
 RewriteResponse ArithRewriter::preRewriteMult(TNode t){
-  Assert(t.getKind()== kind::MULT || t.getKind()== kind::NONLINEAR_MULT);
+  Assert(t.getKind() == kind::MULT || t.getKind() == kind::NONLINEAR_MULT);
 
   if(t.getNumChildren() == 2){
     if(t[0].getKind() == kind::CONST_RATIONAL
@@ -321,7 +320,7 @@ static Node flatten(Kind k, TNode t){
 }
 
 RewriteResponse ArithRewriter::preRewritePlus(TNode t){
-  Assert(t.getKind()== kind::PLUS);
+  Assert(t.getKind() == kind::PLUS);
 
   if(canFlatten(kind::PLUS, t)){
     return RewriteResponse(REWRITE_DONE, flatten(kind::PLUS, t));
@@ -331,7 +330,7 @@ RewriteResponse ArithRewriter::preRewritePlus(TNode t){
 }
 
 RewriteResponse ArithRewriter::postRewritePlus(TNode t){
-  Assert(t.getKind()== kind::PLUS);
+  Assert(t.getKind() == kind::PLUS);
 
   std::vector<Monomial> monomials;
   std::vector<Polynomial> polynomials;
@@ -357,7 +356,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t){
 }
 
 RewriteResponse ArithRewriter::postRewriteMult(TNode t){
-  Assert(t.getKind()== kind::MULT || t.getKind()==kind::NONLINEAR_MULT);
+  Assert(t.getKind() == kind::MULT || t.getKind() == kind::NONLINEAR_MULT);
 
   Polynomial res = Polynomial::mkOne();
 
@@ -462,7 +461,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
                            pi_factor,
                            nm->mkNode(kind::MULT, ntwo, ra_div_two));
           }else{
-            Assert( r.sgn()==-1 );
+            Assert(r.sgn() == -1);
             new_pi_factor =
                 nm->mkNode(kind::PLUS,
                            pi_factor,
@@ -671,7 +670,7 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
 }
 
 RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){
-  Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind()== kind::DIVISION);
+  Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION);
 
   Node left = t[0];
   Node right = t[1];
-- 
cgit v1.2.3