diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-30 12:56:17 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-04-30 12:56:17 -0500 |
| commit | 2f4162877ad455c8c80f60a9bedf0b779b44ecaa (patch) | |
| tree | c2a17095f6b2a2523676773def22c59061e475de /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 2bce108ebe25f7a4b5996cf3fde5eda77564f52e (diff) | |
Add option in quantifiers for clause splitting
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 712967bd2..be3e333f3 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -50,6 +50,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 computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ COMPUTE_MINISCOPING = 0, @@ -60,6 +61,7 @@ private: COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, + COMPUTE_SPLIT, COMPUTE_LAST }; static Node computeOperation( Node f, int computeOption ); |