diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 14:53:19 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 14:53:19 +0100 |
| commit | 97d43d56d74f3af68d1d022c66ee158a41b24757 (patch) | |
| tree | d8a4871505bf1b94558046d53f6280ac90d454d8 /src/theory/quantifiers/options_handlers.h | |
| parent | 7ff0098a91df9c912cbe98fb128fcf2cbc71e95c (diff) | |
CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied selectors.
Diffstat (limited to 'src/theory/quantifiers/options_handlers.h')
| -rw-r--r-- | src/theory/quantifiers/options_handlers.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9f85d454..fdfad21b9 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -184,6 +184,9 @@ uf-dt-size \n\ default | dt-size \n\ + Default, enforce fairness using size theory operator.\n\ \n\ +dt-height-bound \n\ ++ Enforce fairness by height bound predicate.\n\ +\n\ none \n\ + Do not enforce fairness. \n\ \n\ @@ -379,6 +382,8 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar return CEGQI_FAIR_UF_DT_SIZE; } else if(optarg == "default" || optarg == "dt-size") { return CEGQI_FAIR_DT_SIZE; + } else if(optarg == "dt-height-bound" ){ + return CEGQI_FAIR_DT_HEIGHT_PRED; } else if(optarg == "none") { return CEGQI_FAIR_NONE; } else if(optarg == "help") { |