summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp12
-rw-r--r--src/theory/quantifiers/fmf/ambqi_builder.cpp4
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp2
-rw-r--r--src/theory/quantifiers/fmf/full_model_check.cpp9
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp2
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.cpp14
-rw-r--r--src/theory/strings/theory_strings.cpp5
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp9
8 files changed, 27 insertions, 30 deletions
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<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 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<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 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()) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback