diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 13:00:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-23 13:00:43 -0500 |
| commit | 085d6a91f0686d6680d15bb54f9435f30d53c331 (patch) | |
| tree | a5ffe08fecdcd1a66b5b40623a5b514284857cbe /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 996de9116150fb7214b3b9a56995e2492d3e5668 (diff) | |
Update dynamic splitting strategy for quantifiers (#3162)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index b72619392..7703f01fd 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -50,6 +50,13 @@ private: std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); + /** datatype expand + * + * If v occurs in args and has a datatype type whose index^th constructor is + * C, this method returns a node of the form C( x1, ..., xn ), removes v from + * args and adds x1...xn to args. + */ + static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args); //-------------------------------------variable elimination /** is variable elimination * |