diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-27 13:51:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-27 13:51:40 -0500 |
commit | 0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5 (patch) | |
tree | 623913335ab967b83c240a457c963aa9fb1a6ef7 /src/theory | |
parent | d3e83102fde7d5e43f132efa80c651a43af5afa3 (diff) |
Variable elimination rewrite for quantified strings (#3071)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 83 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 30 |
2 files changed, 100 insertions, 13 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 015bf9c5a..ec52bf990 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/strings/theory_strings_rewriter.h" using namespace std; using namespace CVC4::kind; @@ -64,7 +65,11 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ } } -void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ){ +void QuantifiersRewriter::computeArgs(const std::vector<Node>& args, + std::map<Node, bool>& activeMap, + Node n, + std::map<Node, bool>& visited) +{ if( visited.find( n )==visited.end() ){ visited[n] = true; if( n.getKind()==BOUND_VARIABLE ){ @@ -83,7 +88,10 @@ void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node } } -void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) { +void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n) +{ Assert( activeArgs.empty() ); std::map< Node, bool > activeMap; std::map< Node, bool > visited; @@ -97,7 +105,11 @@ void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< } } -void QuantifiersRewriter::computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ) { +void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n, + Node ipl) +{ Assert( activeArgs.empty() ); std::map< Node, bool > activeMap; std::map< Node, bool > visited; @@ -880,7 +892,7 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s) } Node QuantifiersRewriter::getVarElimLitBv(Node lit, - std::vector<Node>& args, + const std::vector<Node>& args, Node& var) { if (Trace.isOn("quant-velim-bv")) @@ -930,6 +942,54 @@ Node QuantifiersRewriter::getVarElimLitBv(Node lit, return Node::null(); } +Node QuantifiersRewriter::getVarElimLitString(Node lit, + const std::vector<Node>& args, + Node& var) +{ + Assert(lit.getKind() == EQUAL); + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < 2; i++) + { + if (lit[i].getKind() == STRING_CONCAT) + { + for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren; + j++) + { + if (std::find(args.begin(), args.end(), lit[i][j]) != args.end()) + { + var = lit[i][j]; + Node slv = lit[1 - i]; + std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j); + std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end()); + Node tpre = + strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, preL); + Node tpost = + strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, postL); + Node slvL = nm->mkNode(STRING_LENGTH, slv); + Node tpreL = nm->mkNode(STRING_LENGTH, tpre); + Node tpostL = nm->mkNode(STRING_LENGTH, tpost); + slv = nm->mkNode( + STRING_SUBSTR, + slv, + tpreL, + nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL))); + // forall x. r ++ x ++ t = s => P( x ) + // is equivalent to + // r ++ s' ++ t = s => P( s' ) where + // s' = substr( s, |r|, |s|-(|t|+|r|) ). + // We apply this only if r,t,s do not contain free variables. + if (!expr::hasFreeVar(slv)) + { + return slv; + } + } + } + } + } + + return Node::null(); +} + bool QuantifiersRewriter::getVarElimLit(Node lit, bool pol, std::vector<Node>& args, @@ -1058,10 +1118,19 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, } } } - if (lit.getKind() == EQUAL && lit[0].getType().isBitVector() && pol) + if (lit.getKind() == EQUAL && pol) { Node var; - Node slv = getVarElimLitBv(lit, args, var); + Node slv; + TypeNode tt = lit[0].getType(); + if (tt.isBitVector()) + { + slv = getVarElimLitBv(lit, args, var); + } + else if (tt.isString()) + { + slv = getVarElimLitString(lit, args, var); + } if (!slv.isNull()) { Assert(!var.isNull()); @@ -1069,7 +1138,7 @@ bool QuantifiersRewriter::getVarElimLit(Node lit, std::find(args.begin(), args.end(), var); Assert(ita != args.end()); Trace("var-elim-quant") - << "Variable eliminate based on bit-vector inversion : " << var + << "Variable eliminate based on theory-specific solving : " << var << " -> " << slv << std::endl; Assert(!expr::hasSubterm(slv, var)); Assert(slv.getType().isSubtypeOf(var.getType())); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 09f26b65b..f91630097 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -36,9 +36,17 @@ public: private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); - static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); - static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); + static void computeArgs(const std::vector<Node>& args, + std::map<Node, bool>& activeMap, + Node n, + std::map<Node, bool>& visited); + static void computeArgVec(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n); + static void computeArgVec2(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n, + Node ipl); static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ); @@ -62,12 +70,22 @@ private: std::vector<Node>& args, std::vector<Node>& vars, std::vector<Node>& subs); - /** variable eliminate for bit-vector literals + /** 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 ), and var is removed from args. + * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitBv(Node lit, std::vector<Node>& args, Node& var); + static Node getVarElimLitBv(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); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds |