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/quantifiers/quantifiers_rewriter.cpp | |
parent | d3e83102fde7d5e43f132efa80c651a43af5afa3 (diff) |
Variable elimination rewrite for quantified strings (#3071)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 83 |
1 files changed, 76 insertions, 7 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())); |