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/uf | |
| 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/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
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 ) ){ |