diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/datatypes_options | 2 | ||||
| -rw-r--r-- | src/options/uf_options | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/src/options/datatypes_options b/src/options/datatypes_options index d4d3e941c..5163cf35d 100644 --- a/src/options/datatypes_options +++ b/src/options/datatypes_options @@ -47,5 +47,7 @@ option sygusFair --sygus-fair=MODE CVC4::theory::SygusFairMode :default CVC4::th if and how to apply fairness for sygus option sygusFairMax --sygus-fair-max bool :default true use max instead of sum for multi-function sygus conjectures +option sygusAbortSize --sygus-abort-size=N int :default -1 + tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default) endmodule 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 |