diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-08 13:21:29 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-08 13:21:29 -0600 |
commit | 36bdf14e005556c3834fc280e134a1ec440da14b (patch) | |
tree | 9512264802b1eb454930d55dd20951fcf2691f30 /src/theory/quantifiers/quantifiers_rewriter.h | |
parent | e72f41bb9d64724d62894989f3369f97877d6782 (diff) |
Improvements to quant+BV/Bool variable elimination (#1495)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index b179110e7..149380b84 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -52,7 +52,16 @@ private: static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); -public: + /** variable eliminate for bit-vector literals + * + * If this returns a non-null value ret, then var is updated to a member of + * args, and lit is equivalent to ( var = ret ). + */ + static Node computeVariableElimLitBv(Node lit, + std::vector<Node>& args, + Node& var); + + public: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); |