diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-20 18:18:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-20 18:18:35 -0500 |
commit | 278b60971f6209ffc0eb76a23548c081dc8c9c56 (patch) | |
tree | 3f51b8fe6ceebd24a4f77b7287f95dfa313ea700 /src/theory | |
parent | 78373c7f5fe93b7e8bbea10e3924f24d25a618ac (diff) |
SyGuS term size limit (#1262)
* Add option sygus-abort-size, which tells the enumerative SyGuS solver to abort when it reaches a given term size.
* Apply clang format.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 6 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 6 |
2 files changed, 10 insertions, 2 deletions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 5d48c1ce2..4999114eb 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -1347,6 +1347,12 @@ 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); + } Assert( !d_this.isNull() ); Node c = NodeManager::currentNM()->mkConst( Rational( s ) ); Node lit = NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND, d_this, c ); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index e7efba325..4b6a326cf 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1157,8 +1157,10 @@ void SortModel::allocateCardinality( OutputChannel* out ){ }while( increment ); //check for abort case - if( options::ufssAbortCardinality()==d_aloc_cardinality ){ - Message() << "Maximum cardinality reached." << std::endl; + if (options::ufssAbortCardinality() != -1 && + d_aloc_cardinality >= options::ufssAbortCardinality()) { + Message() << "Maximum cardinality (" << options::ufssAbortCardinality() + << ") for finite model finding exceeded." << std::endl; exit( 1 ); }else{ if( applyTotality( d_aloc_cardinality ) ){ |