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

6 files changed, 82 insertions, 73 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 8baaeb1e9..76ce1bda9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -23,7 +23,7 @@
 #include <utility>
 #include <vector>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index fbc1bb242..a73ec44f4 100644
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -19,6 +19,7 @@
 
 #include <ostream>
 
+#include "base/check.h"
 #include "options/open_ostream.h"
 #include "options/smt_options.h"
 #include "smt/update_ostream.h"
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index 168ded839..69cd2e7e6 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -89,10 +89,10 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions,
   }
   else
   {
-    Unreachable("Unknown model cores mode");
+    Unreachable() << "Unknown model cores mode";
   }
-  Assert(minimized,
-         "cannot compute model core, since model does not satisfy input!");
+  Assert(minimized)
+      << "cannot compute model core, since model does not satisfy input!";
   if (minimized)
   {
     m->setUsingModelCore();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 29c3f9092..b934617de 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -29,9 +29,9 @@
 #include <utility>
 #include <vector>
 
+#include "base/check.h"
 #include "base/configuration.h"
 #include "base/configuration_private.h"
-#include "base/cvc4_check.h"
 #include "base/exception.h"
 #include "base/listener.h"
 #include "base/modal_exception.h"
@@ -1002,9 +1002,9 @@ void SmtEngine::finalOptionsAreSet() {
   // finish initialization, create the prop engine, etc.
   finishInit();
 
-  AlwaysAssert( d_propEngine->getAssertionLevel() == 0,
-                "The PropEngine has pushed but the SmtEngine "
-                "hasn't finished initializing!" );
+  AlwaysAssert(d_propEngine->getAssertionLevel() == 0)
+      << "The PropEngine has pushed but the SmtEngine "
+         "hasn't finished initializing!";
 
   d_fullyInited = true;
   Assert(d_logic.isLocked());
@@ -1139,8 +1139,9 @@ void SmtEngine::setFilename(std::string filename) { d_filename = filename; }
 std::string SmtEngine::getFilename() const { return d_filename; }
 void SmtEngine::setLogicInternal()
 {
-  Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already"
-         " finished initializing for this run");
+  Assert(!d_fullyInited)
+      << "setting logic in SmtEngine but the engine has already"
+         " finished initializing for this run";
   d_logic.lock();
 }
 
@@ -2504,8 +2505,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
           "last result wasn't unknown!");
     }
   } else if(key == "assertion-stack-levels") {
-    AlwaysAssert(d_userLevels.size() <=
-                 std::numeric_limits<unsigned long int>::max());
+    AlwaysAssert(d_userLevels.size()
+                 <= std::numeric_limits<unsigned long int>::max());
     return SExpr(static_cast<unsigned long int>(d_userLevels.size()));
   } else if(key == "all-options") {
     // get the options, like all-statistics
@@ -3018,10 +3019,9 @@ bool SmtEnginePrivate::simplifyAssertions()
     // theory could still create a new expression that isn't
     // well-typed, and we don't want the C++ runtime to abort our
     // process without any error notice.
-    stringstream ss;
-    ss << "A bad expression was produced.  Original exception follows:\n"
-       << tcep;
-    InternalError(ss.str().c_str());
+    InternalError()
+        << "A bad expression was produced.  Original exception follows:\n"
+        << tcep;
   }
   return true;
 }
@@ -3357,16 +3357,17 @@ void SmtEnginePrivate::processAssertions() {
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
     if( options::fmfFunWellDefined() ){
       quantifiers::FunDefFmf fdf;
-      Assert( d_smt.d_fmfRecFunctionsDefined!=NULL );
+      Assert(d_smt.d_fmfRecFunctionsDefined != NULL);
       //must carry over current definitions (for incremental)
       for( context::CDList<Node>::const_iterator fit = d_smt.d_fmfRecFunctionsDefined->begin();
            fit != d_smt.d_fmfRecFunctionsDefined->end(); ++fit ) {
         Node f = (*fit);
-        Assert( d_smt.d_fmfRecFunctionsAbs.find( f )!=d_smt.d_fmfRecFunctionsAbs.end() );
+        Assert(d_smt.d_fmfRecFunctionsAbs.find(f)
+               != d_smt.d_fmfRecFunctionsAbs.end());
         TypeNode ft = d_smt.d_fmfRecFunctionsAbs[f];
         fdf.d_sorts[f] = ft;
         std::map< Node, std::vector< Node > >::iterator fcit = d_smt.d_fmfRecFunctionsConcrete.find( f );
-        Assert( fcit!=d_smt.d_fmfRecFunctionsConcrete.end() );
+        Assert(fcit != d_smt.d_fmfRecFunctionsConcrete.end());
         for( unsigned j=0; j<fcit->second.size(); j++ ){
           fdf.d_input_arg_inj[f].push_back( fcit->second[j] );
         }
@@ -4233,8 +4234,8 @@ Expr SmtEngine::getValue(const Expr& ex) const
   // Notice that lambdas have function type, which does not respect the subtype
   // relation, so we ignore them here.
   Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
-             || resultNode.getType().isSubtypeOf(expectedType),
-         "Run with -t smt for details.");
+         || resultNode.getType().isSubtypeOf(expectedType))
+      << "Run with -t smt for details.";
 
   // Ensure it's a constant, or a lambda (for uninterpreted functions), or
   // a choice (for approximate values).
@@ -4480,9 +4481,9 @@ std::pair<Expr, Expr> SmtEngine::getSepHeapAndNilExpr(void)
   {
     return std::make_pair(heap, nil);
   }
-  InternalError(
-      "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
-      "expressions from theory model.");
+  InternalError()
+      << "SmtEngine::getSepHeapAndNilExpr(): failed to obtain heap/nil "
+         "expressions from theory model.";
 }
 
 std::vector<Expr> SmtEngine::getExpandedAssertions()
@@ -4535,9 +4536,9 @@ void SmtEngine::checkProof()
   // lfscc_cleanup();
 
 #else  /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
-  Unreachable(
-      "This version of CVC4 was built without proof support; cannot check "
-      "proofs.");
+  Unreachable()
+      << "This version of CVC4 was built without proof support; cannot check "
+         "proofs.";
 #endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
 }
 
@@ -4566,7 +4567,8 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(options::unsatCores(), "cannot check unsat core if unsat cores are turned off");
+  Assert(options::unsatCores())
+      << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
   UnsatCore core = getUnsatCore();
@@ -4598,18 +4600,21 @@ void SmtEngine::checkUnsatCore() {
   }
   Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl;
   if(r.asSatisfiabilityResult().isUnknown()) {
-    InternalError("SmtEngine::checkUnsatCore(): could not check core result unknown.");
+    InternalError()
+        << "SmtEngine::checkUnsatCore(): could not check core result unknown.";
   }
 
   if(r.asSatisfiabilityResult().isSat()) {
-    InternalError("SmtEngine::checkUnsatCore(): produced core was satisfiable.");
+    InternalError()
+        << "SmtEngine::checkUnsatCore(): produced core was satisfiable.";
   }
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
   // --check-model implies --produce-assertions, which enables the
   // assertion list, so we should be ok.
-  Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()");
+  Assert(d_assertionList != NULL)
+      << "don't have an assertion list to check in SmtEngine::checkModel()";
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
 
@@ -4681,20 +4686,21 @@ void SmtEngine::checkModel(bool hardFailure) {
           }
           ss << "so " << func << " is defined in terms of itself." << endl
              << "Run with `--check-models -v' for additional diagnostics.";
-          InternalError(ss.str());
+          InternalError() << ss.str();
         }
       }
 
       // (2) check that the value is actually a value
       else if (!val.isConst()) {
         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl;
-        stringstream ss;
-        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
-           << "model value for " << func << endl
-           << "             is " << val << endl
-           << "and that is not a constant (.isConst() == false)." << endl
-           << "Run with `--check-models -v' for additional diagnostics.";
-        InternalError(ss.str());
+        InternalError()
+            << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
+               "MODEL:"
+            << endl
+            << "model value for " << func << endl
+            << "             is " << val << endl
+            << "and that is not a constant (.isConst() == false)." << endl
+            << "Run with `--check-models -v' for additional diagnostics.";
       }
 
       // (3) check that it's the correct (sub)type
@@ -4702,14 +4708,15 @@ void SmtEngine::checkModel(bool hardFailure) {
       // e.g. "1" is an INT, which isn't a subrange type [1..10] (etc.).
       else if(func.getType().isInteger() && !val.getType().isInteger()) {
         Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT CORRECT TYPE ***" << endl;
-        stringstream ss;
-        ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl
-           << "model value for " << func << endl
-           << "             is " << val << endl
-           << "value type is     " << val.getType() << endl
-           << "should be of type " << func.getType() << endl
-           << "Run with `--check-models -v' for additional diagnostics.";
-        InternalError(ss.str());
+        InternalError()
+            << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH "
+               "MODEL:"
+            << endl
+            << "model value for " << func << endl
+            << "             is " << val << endl
+            << "value type is     " << val.getType() << endl
+            << "should be of type " << func.getType() << endl
+            << "Run with `--check-models -v' for additional diagnostics.";
       }
 
       // (4) checks complete, add the substitution
@@ -4779,7 +4786,7 @@ void SmtEngine::checkModel(bool hardFailure) {
       // this is necessary until preprocessing passes explicitly record how they rewrite quantified formulas
       if( hardFailure && !n.isConst() && n.getKind() != kind::LAMBDA ){
         Notice() << "SmtEngine::checkModel(): -- relax check model wrt quantified formulas..." << endl;
-        AlwaysAssert( quantifiers::QuantifiersRewriter::containsQuantifiers( n ) );
+        AlwaysAssert(quantifiers::QuantifiersRewriter::containsQuantifiers(n));
         Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified assertion : " << n << endl;
         continue;
       }
@@ -4798,7 +4805,7 @@ void SmtEngine::checkModel(bool hardFailure) {
          << "expected `true'." << endl
          << "Run with `--check-models -v' for additional diagnostics.";
       if(hardFailure) {
-        InternalError(ss.str());
+        InternalError() << ss.str();
       } else {
         Warning() << ss.str() << endl;
       }
@@ -4901,15 +4908,15 @@ void SmtEngine::checkSynthSolution()
     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
     if (r.asSatisfiabilityResult().isUnknown())
     {
-      InternalError(
-          "SmtEngine::checkSynthSolution(): could not check solution, result "
-          "unknown.");
+      InternalError() << "SmtEngine::checkSynthSolution(): could not check "
+                         "solution, result "
+                         "unknown.";
     }
     else if (r.asSatisfiabilityResult().isSat())
     {
-      InternalError(
-          "SmtEngine::checkSynthSolution(): produced solution leads to "
-          "satisfiable negated conjecture.");
+      InternalError()
+          << "SmtEngine::checkSynthSolution(): produced solution leads to "
+             "satisfiable negated conjecture.";
     }
     solChecker.resetAssertions();
   }
@@ -4974,7 +4981,7 @@ void SmtEngine::checkAbduct(Expr a)
     // did we get an unexpected result?
     if (isError)
     {
-      InternalError(serr.str().c_str());
+      InternalError() << serr.str();
     }
   }
 }
@@ -5025,7 +5032,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   if( d_theoryEngine ){
     d_theoryEngine->printInstantiations( out );
   }else{
-    Assert( false );
+    Assert(false);
   }
   if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
     out << "% SZS output end Proof for " << d_filename.c_str() << std::endl;
@@ -5038,7 +5045,7 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
   if( d_theoryEngine ){
     d_theoryEngine->printSynthSolution( out );
   }else{
-    Assert( false );
+    Assert(false);
   }
 }
 
@@ -5083,23 +5090,23 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   e_children.push_back( n_attr );
   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
   Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
-  Assert( nn_e.getNumChildren()==3 );
+  Assert(nn_e.getNumChildren() == 3);
   Result r = checkSatisfiability(nn_e.toExpr(), true, true);
   Trace("smt-qe") << "Query returned " << r << std::endl;
   if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
     if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
-      stringstream ss;
-      ss << "While performing quantifier elimination, unexpected result : " << r << " for query.";
-      InternalError(ss.str().c_str());
+      InternalError()
+          << "While performing quantifier elimination, unexpected result : "
+          << r << " for query.";
     }
     std::vector< Node > inst_qs;
     d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
-    Assert( inst_qs.size()<=1 );
+    Assert(inst_qs.size() <= 1);
     Node ret_n;
     if( inst_qs.size()==1 ){
       Node top_q = inst_qs[0];
       //Node top_q = Rewriter::rewrite( nn_e ).negate();
-      Assert( top_q.getKind()==kind::FORALL );
+      Assert(top_q.getKind() == kind::FORALL);
       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
       ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
       Trace("smt-qe") << "Returned : " << ret_n << std::endl;
@@ -5252,7 +5259,7 @@ void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
       qs.push_back( qs_n[i].toExpr() );
     }
   }else{
-    Assert( false );
+    Assert(false);
   }
 }
 
@@ -5265,7 +5272,7 @@ void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
       insts.push_back( insts_n[i].toExpr() );
     }
   }else{
-    Assert( false );
+    Assert(false);
   }
 }
 
@@ -5283,7 +5290,7 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E
       tvecs.push_back( tvec );
     }
   }else{
-    Assert( false );
+    Assert(false);
   }
 }
 
@@ -5641,8 +5648,8 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 }
 
 void SmtEngine::setReplayStream(ExprStream* replayStream) {
-  AlwaysAssert(!d_fullyInited,
-               "Cannot set replay stream once fully initialized");
+  AlwaysAssert(!d_fullyInited)
+      << "Cannot set replay stream once fully initialized";
   d_replayStream = replayStream;
 }
 
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index c16278962..4b593f075 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -17,8 +17,8 @@
 
 #include "smt/smt_engine_scope.h"
 
+#include "base/check.h"
 #include "base/configuration_private.h"
-#include "base/cvc4_assert.h"
 #include "base/output.h"
 #include "proof/proof.h"
 #include "smt/smt_engine.h"
@@ -40,7 +40,8 @@ ProofManager* currentProofManager() {
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->d_proofManager;
 #else  /* IS_PROOFS_BUILD */
-  InternalError("proofs/unsat cores are not on, but ProofManager requested");
+  InternalError()
+      << "proofs/unsat cores are not on, but ProofManager requested";
   return NULL;
 #endif /* IS_PROOFS_BUILD */
 }
diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index 0427f4058..53d5e5ce0 100644
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -22,12 +22,12 @@
 
 #include <ostream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/set_language.h"
-#include "options/base_options.h"
 #include "smt/dump.h"
 
 namespace CVC4 {