diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:49:51 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-29 13:50:08 -0500 |
| commit | fa5df1aad69f8ad62686b9418070a1baf74b4a77 (patch) | |
| tree | ad780365050498223b2a3fceb703556713cb49d0 /src/options | |
| parent | 599329b76da2e95f18479a19c1bbbc3e3228b100 (diff) | |
Add quantifiers options related to model and master equality engine.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index e5f2922a7..f4bce5518 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -108,6 +108,8 @@ option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen option instWhenTcFirst --inst-when-tc-first bool :default true :read-write allow theory combination to happen once initially, before quantifier strategies are run +option quantModelEe --quant-model-ee bool :default false + use equality engine of model for last call effort option instMaxLevel --inst-max-level=N int :read-write :default -1 maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) @@ -187,6 +189,8 @@ option qcfVoExp --qcf-vo-exp bool :default false option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed +option instNoModelTrue --inst-no-model-true bool :read-write :default false + do not consider instances of quantified formulas that are currently true in model, if it is available option instPropagate --inst-prop bool :read-write :default false internal propagation for instantiations for selecting relevant instances |