Cleanup various exit calls (#1692)

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 3c90bc448cab3f3c88bc187d732748b3d15b94f7..7fe403526f48e2bfc893020e321cd5da1c093d08 100644 (file)
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1290,11 +1290,13 @@ Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDat
   if( options::sygusFair()!=SYGUS_FAIR_NONE ){
     std::map< unsigned, Node >::iterator it = d_lits.find( s );
     if( it==d_lits.end() ){
-      if (options::sygusAbortSize() != -1 &&
-          static_cast<int>(s) > options::sygusAbortSize()) {
-        Message() << "Maximum term size (" << options::sygusAbortSize()
-                  << ") for enumerative SyGuS exceeded." << std::endl;
-        exit(1);
+      if (options::sygusAbortSize() != -1
+          && static_cast<int>(s) > options::sygusAbortSize())
+      {
+        std::stringstream ss;
+        ss << "Maximum term size (" << options::sygusAbortSize()
+           << ") for enumerative SyGuS exceeded." << std::endl;
+        throw LogicException(ss.str());
       }
       Assert( !d_this.isNull() );
       Node c = NodeManager::currentNM()->mkConst( Rational( s ) );

diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
index 6bb73f8a92dfe385819222bd561a8960e8ca6d96..cedd2a2ed2a0c6da5cdfdd9f365bf7365fc2beae 100644 (file)
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp
@@ -605,10 +605,6 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
       construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def );
     }
     Assert( is_normalized() );
-    //if( !is_normalized() ){
-    //  std::cout << "NON NORMALIZED DEFINITION" << std::endl;
-    //  exit( 10 );
-    //}
     return true;
   }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){
     Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b1e9c2a341fba209b73416699d973d3368c0b43c..d96fb4e05368743ebb92967c3927cae989bb073e 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -91,7 +91,7 @@ void BoundedIntegers::IntRangeModel::assertNode(Node n) {
     }
   }else{
     Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
-    exit(0);
+    AlwaysAssert(false);
   }
 }
 

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index d6957b21057d81278ddbef381f55a10d4d081687..0ec8b00b22f8b075745ce38ddf6f8133befe45ba 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -101,10 +101,6 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>
     int minIndex = -1;
     if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){
       for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
-        //if( !m->isInterval( it->first ) ){
-        //  std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
-        //  exit( 11 );
-        //}
         //check if it is in the range
         if( m->isInRange(inst[index], it->first )  ){
           int gindex = it->second.getGeneralizationIndex(m, inst, index+1);
@@ -678,8 +674,9 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
               if (Trace.isOn("fmc-test-inst")) {
                 Node ev = d_quant_models[f].evaluate(fmfmc, inst);
                 if( ev==d_true ){
-                  std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
-                  exit(0);
+                  Message() << "WARNING: instantiation was true! " << f << " "
+                            << d_quant_models[f].d_cond[i] << std::endl;
+                  AlwaysAssert(false);
                 }else{
                   Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
                 }

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 356e95d1b4d8ea408a395fbaba0a177f64395a87..49a19aedac4e51de819b692e254c048bcfd08a49 100644 (file)
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -42,7 +42,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
       //check if already defined, if so, throw error
       if( d_sorts.find( f )!=d_sorts.end() ){
         Message() << "Cannot define function " << f << " more than once." << std::endl;
-        exit( 0 );
+        AlwaysAssert(false);
       }
 
       Node bd = QuantAttributes::getFunDefBody( assertions[i] );

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index a951ec867cb2564f471fbed2909c1872cc209127..3e48c11b28299a49dd5099ce3d9539eb123dee0c 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -323,9 +323,11 @@ void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) {
   }else{
     d_single_inv = Node::null();
     Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
-    if( options::cegqiSingleInvAbort() ){
-      Notice() << "Property is not single invocation." << std::endl;
-      exit( 1 );
+    if (options::cegqiSingleInvAbort())
+    {
+      std::stringstream ss;
+      ss << "Property is not single invocation." << std::endl;
+      throw LogicException(ss.str());
     }
   }
 }
@@ -582,11 +584,9 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
 
   if( Trace.isOn("csi-sol") ){
     //debug solution
-    if( !d_sol->debugSolution( d_solution ) ){
+    if (!d_sol->debugSolution(d_solution))
+    {
       Trace("csi-sol") << "WARNING : solution " << d_solution << " contains free constants." << std::endl;
-      //exit( 47 );
-    }else{
-      //exit( 49 );
     }
   }
   if( Trace.isOn("cegqi-stats") ){

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8827959ead09d8bddeca68f8822292c0a395fe79..59b2e8ea07d0ab9f521628fb3a8b37fe42ee9399 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2807,8 +2807,9 @@ bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms
 bool TheoryStrings::processLoop( std::vector< std::vector< Node > > &normal_forms, std::vector< Node > &normal_form_src,
                                  int i, int j, int loop_n_index, int other_n_index, int loop_index, int index, InferInfo& info ){
   if( options::stringAbortLoop() ){
-    Message() << "Looping word equation encountered." << std::endl;
-    exit( 1 );
+    std::stringstream ss;
+    ss << "Looping word equation encountered." << std::endl;
+    throw LogicException(ss.str());
   }
   NodeManager* nm = NodeManager::currentNM();
   Node conc;

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index b32a50eb4077f50372d79dcf4115a923b6eb2b35..76cb95867c2141cb56a2d2097e024f0dab73f9fb 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1147,9 +1147,10 @@ void SortModel::allocateCardinality( OutputChannel* out ){
   //check for abort case
   if (options::ufssAbortCardinality() != -1 &&
       d_aloc_cardinality >= options::ufssAbortCardinality()) {
-    Message() << "Maximum cardinality (" << options::ufssAbortCardinality()
-              << ")  for finite model finding exceeded." << std::endl;
-    exit( 1 );
+    std::stringstream ss;
+    ss << "Maximum cardinality (" << options::ufssAbortCardinality()
+       << ")  for finite model finding exceeded." << std::endl;
+    throw LogicException(ss.str());
   }else{
     if( applyTotality( d_aloc_cardinality ) ){
       //must generate new cardinality lemma term
@@ -1231,7 +1232,7 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
       }
       if( ss==b_t ){
         Message() << "Bad split " << s << std::endl;
-        exit( 16 );
+        AlwaysAssert(false);
       }
     }
     if( options::sortInference()) {