summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-08-26 16:27:57 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-08-26 16:27:57 -0500
commit9ac5255577a07e3bef123908d55003f89dea7619 (patch)
tree81a74251576a2bdcb58a010a8d0eb83c57b71a9d /src/options
parent2e7ec13174e165cccc74159b5c6590d12894a674 (diff)
Basic support for EPR+CBQI. Minor cleanup.
Diffstat (limited to 'src/options')
-rw-r--r--src/options/quantifiers_options3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index cb4f292c1..9f8f088de 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -306,6 +306,9 @@ option cbqiLitDepend --cbqi-lit-dep bool :default false
option cbqiInnermost --cbqi-innermost bool :default false
only process innermost quantified formulas in counterexample-based quantifier instantiation
+option quantEpr --quant-epr bool :default false
+ infer whether in effectively propositional fragment, use for cbqi
+
### local theory extensions options
option localTheoryExt --local-t-ext bool :default false
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback