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/options/uf_options | |
| 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/options/uf_options')
| -rw-r--r-- | src/options/uf_options | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/uf_options b/src/options/uf_options index 7e1cbdb17..c93ccf864 100644 --- a/src/options/uf_options +++ b/src/options/uf_options @@ -22,7 +22,7 @@ option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false apply symmetry breaking for totality axioms option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 - tells the uf strong solver a cardinality to abort at (-1 == no limit, default) + tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default) option ufssExplainedCliques --uf-ss-explained-cliques bool :default false use explained clique lemmas for uf strong solver option ufssSimpleCliques --uf-ss-simple-cliques bool :default true |