diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 10:50:56 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 10:50:56 -0600 |
| commit | 21f8e233e46fae32eaa6d2d4d5b4d0f36c36ba7f (patch) | |
| tree | 610112b7b9f621466e478f29997a8fe2d5a62ccb /src/theory/quantifiers/options | |
| parent | 841b7951f41f399859afab13a81e04599308da61 (diff) | |
Add stats to quantifiers conflict find. Added option for qcf. Working on handling non-APPLY_UF terms.
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 652526cc9..dc016be3f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -120,6 +120,9 @@ option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode policy for instantiating axioms option quantConflictFind --quant-cf bool :default false - enable eager conflict find mechanism for quantifiers + enable conflict find mechanism for quantifiers +option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" + when to invoke conflict find mechanism for quantifiers + endmodule |