diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-05 19:56:42 +0200 |
| commit | ba56661b4a49d4b470c6298d3531324b3bf15005 (patch) | |
| tree | 6dee0cde13ab4e86a6bde22bf130e1d3f70c2a6f /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 69769dae4886621f82c2905b82db727bf2e8cf3f (diff) | |
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching. Avoid unecessary delta lemmas. Update casc scripts.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 201a03737..d01677171 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -51,6 +51,7 @@ private: static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computeElimTaut( Node body ); static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ @@ -61,6 +62,7 @@ private: COMPUTE_PROCESS_ITE, COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, + COMPUTE_ELIM_TAUT, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, |