From: Andrew Reynolds Date: Thu, 27 Jun 2019 18:51:40 +0000 (-0500) Subject: Variable elimination rewrite for quantified strings (#3071) X-Git-Tag: cvc5-1.0.0~4102 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a936446c8e2d95e5c7d39f2f3f0740fb5b717a5;p=cvc5.git Variable elimination rewrite for quantified strings (#3071) --- 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& args, + std::map& activeMap, + Node n, + std::map& 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& args, + std::vector& 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& args, + std::vector& 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& args, + const std::vector& 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& 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 preL(lit[i].begin(), lit[i].begin() + j); + std::vector 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& 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& args, + std::map& activeMap, + Node n, + std::map& visited); + static void computeArgVec(const std::vector& args, + std::vector& activeArgs, + Node n); + static void computeArgVec2(const std::vector& args, + std::vector& 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& args, std::vector& vars, std::vector& 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& args, Node& var); + static Node getVarElimLitBv(Node lit, + const std::vector& 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& args, + Node& var); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3c5d82fa8..f7760a504 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1352,6 +1352,7 @@ set(regress_1_tests regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 regress1/quantifiers/is-even.smt2 regress1/quantifiers/isaplanner-goal20.smt2 + regress1/quantifiers/issue2970-string-var-elim.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 regress1/quantifiers/mix-coeff.smt2 diff --git a/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 new file mode 100644 index 000000000..31a57fc8b --- /dev/null +++ b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun s () String) +(declare-fun t () String) +(assert (! + (forall ((t1 String) (t2 String)) + (=> (= (str.++ t1 t2) t) (= (= t1 s) false)) + ) + :named a1)) +(assert (! + (not (= (str.prefixof s t) false)) :named a0)) + + +(check-sat)