From: Andrew Reynolds Date: Sun, 25 Mar 2018 16:47:38 +0000 (-0500) Subject: Cleanup various exit calls (#1692) X-Git-Tag: cvc5-1.0.0~5213 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c03e15c1b4ef6ec62209f2a4906cce5843e80c46;p=cvc5.git Cleanup various exit calls (#1692) --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 3c90bc448..7fe403526 100644 --- 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(s) > options::sygusAbortSize()) { - Message() << "Maximum term size (" << options::sygusAbortSize() - << ") for enumerative SyGuS exceeded." << std::endl; - exit(1); + if (options::sygusAbortSize() != -1 + && static_cast(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 6bb73f8a9..cedd2a2ed 100644 --- 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 b1e9c2a34..d96fb4e05 100644 --- 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 d6957b210..0ec8b00b2 100644 --- 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 int minIndex = -1; if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){ for( std::map::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 356e95d1b..49a19aeda 100644 --- 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 a951ec867..3e48c11b2 100644 --- 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 8827959ea..59b2e8ea0 100644 --- 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 b32a50eb4..76cb95867 100644 --- 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()) {