summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/options
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-11-12 16:46:51 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-11-12 16:46:51 +0000
commit0ba075e240b2083163ab35a3580547cae6927b6c (patch)
tree47be765d608aff213ee58749adab458f315fcf89 /src/theory/quantifiers/options
parent341794b1cbd5693010c78b9f5bfe232ee90404b0 (diff)
minor bug fixes for quantifiers, added sort inference module (not ready to be used yet), added new totality lemma option for uf strong solver
Diffstat (limited to 'src/theory/quantifiers/options')
-rw-r--r--src/theory/quantifiers/options1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 5802a05cd..2c36520e4 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -91,4 +91,5 @@ option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :defau
option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
policy for instantiating axioms
+
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback