diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index ae7f75f34..f0c3b0414 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -80,22 +80,34 @@ class QuantifiersRewriter : public TheoryRewriter std::vector<Node>& args, std::vector<Node>& vars, std::vector<Node>& subs); + /** + * Get variable eliminate for an equality based on theory-specific reasoning. + */ + static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var); + /** variable eliminate for real equalities + * + * If this returns a non-null value ret, then var is updated to a member of + * args, lit is equivalent to ( var = ret ). + */ + static Node getVarElimEqReal(Node lit, + const std::vector<Node>& args, + Node& var); /** variable eliminate for bit-vector equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitBv(Node lit, - const std::vector<Node>& args, - Node& var); + static Node getVarElimEqBv(Node lit, + const std::vector<Node>& args, + Node& var); /** variable eliminate for string equalities * * If this returns a non-null value ret, then var is updated to a member of * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitString(Node lit, - const std::vector<Node>& args, - Node& var); + static Node getVarElimEqString(Node lit, + const std::vector<Node>& args, + Node& var); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds |