summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-04-09 13:07:11 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-04-09 13:07:11 -0500
commit67623ee1e6d62b36cb598c28ad9b871b6957a9dd (patch)
tree3ea7e16b6b1f8e2073ad9265741fa7853b63c0df /src/options
parent59b935c1af18ec51efacf87b0e45d9134d3aaa1e (diff)
Minor refactoring of entailment tests and quantifiers util. Initial draft of instantiation propagator.
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 8ed4f24c0..c27b21e23 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -174,6 +174,9 @@ option qcfAllConflict --qcf-all-conflict bool :read-write :default false
option instNoEntail --inst-no-entail bool :read-write :default true
do not consider instances of quantified formulas that are currently entailed
+
+option instPropagate --inst-propagate bool :read-write :default false
+ internal propagation for instantiations for selecting relevant instances
### rewrite rules options
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback