Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/proof_checker.cpp	Lines:	257	296	86.8 %
Date:	2021-08-06	Branches:	668	1846	36.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of strings proof checker.
 */

#include "theory/strings/proof_checker.h"

#include "expr/sequence.h"
#include "options/strings_options.h"
#include "theory/rewriter.h"
#include "theory/strings/core_solver.h"
#include "theory/strings/regexp_elim.h"
#include "theory/strings/regexp_operation.h"
#include "theory/strings/term_registry.h"
#include "theory/strings/theory_strings_preprocess.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

void StringProofRuleChecker::registerTo(ProofChecker* pc)
{
  pc->registerChecker(PfRule::CONCAT_EQ, this);
  pc->registerChecker(PfRule::CONCAT_UNIFY, this);
  pc->registerChecker(PfRule::CONCAT_CONFLICT, this);
  pc->registerChecker(PfRule::CONCAT_SPLIT, this);
  pc->registerChecker(PfRule::CONCAT_CSPLIT, this);
  pc->registerChecker(PfRule::CONCAT_LPROP, this);
  pc->registerChecker(PfRule::CONCAT_CPROP, this);
  pc->registerChecker(PfRule::STRING_DECOMPOSE, this);
  pc->registerChecker(PfRule::STRING_LENGTH_POS, this);
  pc->registerChecker(PfRule::STRING_LENGTH_NON_EMPTY, this);
  pc->registerChecker(PfRule::STRING_REDUCTION, this);
  pc->registerChecker(PfRule::STRING_EAGER_REDUCTION, this);
  pc->registerChecker(PfRule::RE_INTER, this);
  pc->registerChecker(PfRule::RE_UNFOLD_POS, this);
  pc->registerChecker(PfRule::RE_UNFOLD_NEG, this);
  pc->registerChecker(PfRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
  pc->registerChecker(PfRule::RE_ELIM, this);
  pc->registerChecker(PfRule::STRING_CODE_INJ, this);
  pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
  // trusted rules
  pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
}

Node StringProofRuleChecker::checkInternal(PfRule id,
                                           const std::vector<Node>& children,
                                           const std::vector<Node>& args)
{
  NodeManager* nm = NodeManager::currentNM();
  // core rules for word equations
  if (id == PfRule::CONCAT_EQ || id == PfRule::CONCAT_UNIFY
      || id == PfRule::CONCAT_CONFLICT || id == PfRule::CONCAT_SPLIT
      || id == PfRule::CONCAT_CSPLIT || id == PfRule::CONCAT_LPROP
      || id == PfRule::CONCAT_CPROP)
  {
    Trace("strings-pfcheck") << "Checking id " << id << std::endl;
    Assert(children.size() >= 1);
    Assert(args.size() == 1);
    // all rules have an equality
    if (children[0].getKind() != EQUAL)
    {
      return Node::null();
    }
    // convert to concatenation form
    std::vector<Node> tvec;
    std::vector<Node> svec;
    utils::getConcat(children[0][0], tvec);
    utils::getConcat(children[0][1], svec);
    size_t nchildt = tvec.size();
    size_t nchilds = svec.size();
    TypeNode stringType = children[0][0].getType();
    // extract the Boolean corresponding to whether the rule is reversed
    bool isRev;
    if (!getBool(args[0], isRev))
    {
      return Node::null();
    }
    if (id == PfRule::CONCAT_EQ)
    {
      Assert(children.size() == 1);
      size_t index = 0;
      std::vector<Node> tremVec;
      std::vector<Node> sremVec;
      // scan the concatenation until we exhaust child proofs
      while (index < nchilds && index < nchildt)
      {
        Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
        Node currS = svec[isRev ? (nchilds - 1 - index) : index];
        if (currT != currS)
        {
          if (currT.isConst() && currS.isConst())
          {
            size_t sindex;
            // get the equal prefix/suffix, strip and add the remainders
            Node currR = Word::splitConstant(currT, currS, sindex, isRev);
            if (!currR.isNull())
            {
              // add the constant to remainder vec
              std::vector<Node>& rem = sindex == 0 ? tremVec : sremVec;
              rem.push_back(currR);
              // ignore the current component
              index++;
              // In other words, if we have (currS,currT) = ("ab","abc"), then
              // we proceed to the next component and add currR = "c" to
              // tremVec.
            }
            // otherwise if we are not the same prefix, then both will be added
            // Notice that we do not add maximal prefixes, in other words,
            // ("abc", "abd") may be added to the remainder vectors, and not
            // ("c", "d").
          }
          break;
        }
        index++;
      }
      Assert(index <= nchildt);
      Assert(index <= nchilds);
      // the remainders are equal
      tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
                     tvec.begin() + (isRev ? 0 : index),
                     tvec.begin() + nchildt - (isRev ? index : 0));
      sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
                     svec.begin() + (isRev ? 0 : index),
                     svec.begin() + nchilds - (isRev ? index : 0));
      // convert back to node
      Node trem = utils::mkConcat(tremVec, stringType);
      Node srem = utils::mkConcat(sremVec, stringType);
      return trem.eqNode(srem);
    }
    // all remaining rules do something with the first child of each side
    Node t0 = tvec[isRev ? nchildt - 1 : 0];
    Node s0 = svec[isRev ? nchilds - 1 : 0];
    if (id == PfRule::CONCAT_UNIFY)
    {
      Assert(children.size() == 2);
      if (children[1].getKind() != EQUAL)
      {
        return Node::null();
      }
      for (size_t i = 0; i < 2; i++)
      {
        Node l = children[1][i];
        if (l.getKind() != STRING_LENGTH)
        {
          return Node::null();
        }
        Node term = i == 0 ? t0 : s0;
        if (l[0] == term)
        {
          continue;
        }
        // could be a spliced constant
        bool success = false;
        if (term.isConst() && l[0].isConst())
        {
          size_t lenL = Word::getLength(l[0]);
          success = (isRev && l[0] == Word::suffix(term, lenL))
                    || (!isRev && l[0] == Word::prefix(term, lenL));
        }
        if (!success)
        {
          return Node::null();
        }
      }
      return children[1][0][0].eqNode(children[1][1][0]);
    }
    else if (id == PfRule::CONCAT_CONFLICT)
    {
      Assert(children.size() == 1);
      if (!t0.isConst() || !s0.isConst())
      {
        // not constants
        return Node::null();
      }
      size_t sindex;
      Node r0 = Word::splitConstant(t0, s0, sindex, isRev);
      if (!r0.isNull())
      {
        // Not a conflict due to constants, i.e. s0 is a prefix of t0 or vice
        // versa.
        return Node::null();
      }
      return nm->mkConst(false);
    }
    else if (id == PfRule::CONCAT_SPLIT)
    {
      Assert(children.size() == 2);
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
          || children[1][0][0].getKind() != STRING_LENGTH
          || children[1][0][0][0] != t0
          || children[1][0][1].getKind() != STRING_LENGTH
          || children[1][0][1][0] != s0)
      {
        return Node::null();
      }
    }
    else if (id == PfRule::CONCAT_CSPLIT)
    {
      Assert(children.size() == 2);
      Node zero = nm->mkConst(Rational(0));
      Node one = nm->mkConst(Rational(1));
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
          || children[1][0][0].getKind() != STRING_LENGTH
          || children[1][0][0][0] != t0 || children[1][0][1] != zero)
      {
        return Node::null();
      }
      if (!s0.isConst() || !s0.getType().isStringLike() || Word::isEmpty(s0))
      {
        return Node::null();
      }
    }
    else if (id == PfRule::CONCAT_LPROP)
    {
      Assert(children.size() == 2);
      if (children[1].getKind() != GT
          || children[1][0].getKind() != STRING_LENGTH
          || children[1][0][0] != t0
          || children[1][1].getKind() != STRING_LENGTH
          || children[1][1][0] != s0)
      {
        return Node::null();
      }
    }
    else if (id == PfRule::CONCAT_CPROP)
    {
      Assert(children.size() == 2);
      Node zero = nm->mkConst(Rational(0));

      Trace("pfcheck-strings-cprop")
          << "CONCAT_PROP, isRev=" << isRev << std::endl;
      if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
          || children[1][0][0].getKind() != STRING_LENGTH
          || children[1][0][0][0] != t0 || children[1][0][1] != zero)
      {
        Trace("pfcheck-strings-cprop")
            << "...failed pattern match" << std::endl;
        return Node::null();
      }
      if (tvec.size() <= 1)
      {
        Trace("pfcheck-strings-cprop")
            << "...failed adjacent constant" << std::endl;
        return Node::null();
      }
      Node w1 = tvec[isRev ? nchildt - 2 : 1];
      if (!w1.isConst() || !w1.getType().isStringLike() || Word::isEmpty(w1))
      {
        Trace("pfcheck-strings-cprop")
            << "...failed adjacent constant content" << std::endl;
        return Node::null();
      }
      Node w2 = s0;
      if (!w2.isConst() || !w2.getType().isStringLike() || Word::isEmpty(w2))
      {
        Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl;
        return Node::null();
      }
      // getConclusion expects the adjacent constant to be included
      t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
    }
    // use skolem cache
    SkolemCache skc(false);
    std::vector<Node> newSkolems;
    Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems);
    return conc;
  }
  else if (id == PfRule::STRING_DECOMPOSE)
  {
    Assert(children.size() == 1);
    Assert(args.size() == 1);
    bool isRev;
    if (!getBool(args[0], isRev))
    {
      return Node::null();
    }
    Node atom = children[0];
    if (atom.getKind() != GEQ || atom[0].getKind() != STRING_LENGTH)
    {
      return Node::null();
    }
    SkolemCache sc(false);
    std::vector<Node> newSkolems;
    Node conc = CoreSolver::getConclusion(
        atom[0][0], atom[1], id, isRev, &sc, newSkolems);
    return conc;
  }
  else if (id == PfRule::STRING_REDUCTION
           || id == PfRule::STRING_EAGER_REDUCTION
           || id == PfRule::STRING_LENGTH_POS)
  {
    Assert(children.empty());
    Assert(args.size() >= 1);
    // These rules are based on calling a C++ method for returning a valid
    // lemma involving a single argument term.
    // Must convert to skolem form.
    Node t = args[0];
    Node ret;
    if (id == PfRule::STRING_REDUCTION)
    {
      Assert(args.size() == 1);
      // we do not use optimizations
      SkolemCache skc(false);
      std::vector<Node> conj;
      ret = StringsPreprocess::reduce(t, conj, &skc);
      conj.push_back(t.eqNode(ret));
      ret = nm->mkAnd(conj);
    }
    else if (id == PfRule::STRING_EAGER_REDUCTION)
    {
      Assert(args.size() == 1);
      SkolemCache skc(false);
      ret = TermRegistry::eagerReduce(t, &skc);
    }
    else if (id == PfRule::STRING_LENGTH_POS)
    {
      Assert(args.size() == 1);
      ret = TermRegistry::lengthPositive(t);
    }
    if (ret.isNull())
    {
      return Node::null();
    }
    return ret;
  }
  else if (id == PfRule::STRING_LENGTH_NON_EMPTY)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    Node nemp = children[0];
    if (nemp.getKind() != NOT || nemp[0].getKind() != EQUAL
        || !nemp[0][1].isConst() || !nemp[0][1].getType().isStringLike())
    {
      return Node::null();
    }
    if (!Word::isEmpty(nemp[0][1]))
    {
      return Node::null();
    }
    Node zero = nm->mkConst(Rational(0));
    Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
    return clen.eqNode(zero).notNode();
  }
  else if (id == PfRule::RE_INTER)
  {
    Assert(children.size() >= 1);
    Assert(args.empty());
    std::vector<Node> reis;
    Node x;
    // make the regular expression intersection that summarizes all
    // memberships in the explanation
    for (const Node& c : children)
    {
      bool polarity = c.getKind() != NOT;
      Node catom = polarity ? c : c[0];
      if (catom.getKind() != STRING_IN_REGEXP)
      {
        return Node::null();
      }
      if (x.isNull())
      {
        x = catom[0];
      }
      else if (x != catom[0])
      {
        // different LHS
        return Node::null();
      }
      Node xcurr = catom[0];
      Node rcurr =
          polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]);
      reis.push_back(rcurr);
    }
    Node rei = reis.size() == 1 ? reis[0] : nm->mkNode(REGEXP_INTER, reis);
    return nm->mkNode(STRING_IN_REGEXP, x, rei);
  }
  else if (id == PfRule::RE_UNFOLD_POS || id == PfRule::RE_UNFOLD_NEG
           || id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    Node skChild = children[0];
    if (id == PfRule::RE_UNFOLD_NEG || id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
    {
      if (skChild.getKind() != NOT || skChild[0].getKind() != STRING_IN_REGEXP)
      {
        Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl;
        return Node::null();
      }
    }
    else if (skChild.getKind() != STRING_IN_REGEXP)
    {
      Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
      return Node::null();
    }
    Node conc;
    if (id == PfRule::RE_UNFOLD_POS)
    {
      std::vector<Node> newSkolems;
      SkolemCache sc;
      conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems);
    }
    else if (id == PfRule::RE_UNFOLD_NEG)
    {
      conc = RegExpOpr::reduceRegExpNeg(skChild);
    }
    else if (id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
    {
      if (skChild[0][1].getKind() != REGEXP_CONCAT)
      {
        Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl;
        return Node::null();
      }
      size_t index;
      Node reLen = RegExpOpr::getRegExpConcatFixed(skChild[0][1], index);
      if (reLen.isNull())
      {
        Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl;
        return Node::null();
      }
      conc = RegExpOpr::reduceRegExpNegConcatFixed(skChild, reLen, index);
    }
    return conc;
  }
  else if (id == PfRule::RE_ELIM)
  {
    Assert(children.empty());
    Assert(args.size() == 2);
    bool isAgg;
    if (!getBool(args[1], isAgg))
    {
      return Node::null();
    }
    Node ea = RegExpElimination::eliminate(args[0], isAgg);
    // if we didn't eliminate, then this trivially proves the reflexive equality
    if (ea.isNull())
    {
      ea = args[0];
    }
    return args[0].eqNode(ea);
  }
  else if (id == PfRule::STRING_CODE_INJ)
  {
    Assert(children.empty());
    Assert(args.size() == 2);
    Assert(args[0].getType().isStringLike()
           && args[1].getType().isStringLike());
    Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
    Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
    Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1)));
    Node deq = c1.eqNode(c2).negate();
    Node eqn = args[0].eqNode(args[1]);
    return nm->mkNode(kind::OR, eqNegOne, deq, eqn);
  }
  else if (id == PfRule::STRING_SEQ_UNIT_INJ)
  {
    Assert(children.size() == 1);
    Assert(args.empty());
    if (children[0].getKind() != EQUAL)
    {
      return Node::null();
    }
    Node t[2];
    for (size_t i = 0; i < 2; i++)
    {
      if (children[0][i].getKind() == SEQ_UNIT)
      {
        t[i] = children[0][i][0];
      }
      else if (children[0][i].isConst())
      {
        // notice that Word::getChars is not the right call here, since it
        // gets a vector of sequences of length one. We actually need to
        // extract the character, which is a sequence-specific operation.
        const Sequence& sx = children[0][i].getConst<Sequence>();
        const std::vector<Node>& vec = sx.getVec();
        if (vec.size() == 1)
        {
          // the character of the single character sequence
          t[i] = vec[0];
        }
      }
      if (t[i].isNull())
      {
        return Node::null();
      }
    }
    Trace("strings-pfcheck-debug")
        << "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
        << " == " << t[1] << std::endl;
    AlwaysAssert(t[0].getType() == t[1].getType());
    return t[0].eqNode(t[1]);
  }
  else if (id == PfRule::STRING_TRUST)
  {
    // "trusted" rules
    Assert(!args.empty());
    Assert(args[0].getType().isBoolean());
    return args[0];
  }
  return Node::null();
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of strings proof checker.
14		*/
15
16		#include "theory/strings/proof_checker.h"
17
18		#include "expr/sequence.h"
19		#include "options/strings_options.h"
20		#include "theory/rewriter.h"
21		#include "theory/strings/core_solver.h"
22		#include "theory/strings/regexp_elim.h"
23		#include "theory/strings/regexp_operation.h"
24		#include "theory/strings/term_registry.h"
25		#include "theory/strings/theory_strings_preprocess.h"
26		#include "theory/strings/theory_strings_utils.h"
27		#include "theory/strings/word.h"
28
29		using namespace cvc5::kind;
30
31		namespace cvc5 {
32		namespace theory {
33		namespace strings {
34
35	3768	void StringProofRuleChecker::registerTo(ProofChecker* pc)
36		{
37	3768	pc->registerChecker(PfRule::CONCAT_EQ, this);
38	3768	pc->registerChecker(PfRule::CONCAT_UNIFY, this);
39	3768	pc->registerChecker(PfRule::CONCAT_CONFLICT, this);
40	3768	pc->registerChecker(PfRule::CONCAT_SPLIT, this);
41	3768	pc->registerChecker(PfRule::CONCAT_CSPLIT, this);
42	3768	pc->registerChecker(PfRule::CONCAT_LPROP, this);
43	3768	pc->registerChecker(PfRule::CONCAT_CPROP, this);
44	3768	pc->registerChecker(PfRule::STRING_DECOMPOSE, this);
45	3768	pc->registerChecker(PfRule::STRING_LENGTH_POS, this);
46	3768	pc->registerChecker(PfRule::STRING_LENGTH_NON_EMPTY, this);
47	3768	pc->registerChecker(PfRule::STRING_REDUCTION, this);
48	3768	pc->registerChecker(PfRule::STRING_EAGER_REDUCTION, this);
49	3768	pc->registerChecker(PfRule::RE_INTER, this);
50	3768	pc->registerChecker(PfRule::RE_UNFOLD_POS, this);
51	3768	pc->registerChecker(PfRule::RE_UNFOLD_NEG, this);
52	3768	pc->registerChecker(PfRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
53	3768	pc->registerChecker(PfRule::RE_ELIM, this);
54	3768	pc->registerChecker(PfRule::STRING_CODE_INJ, this);
55	3768	pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
56		// trusted rules
57	3768	pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
58	3768	}
59
60	5875	Node StringProofRuleChecker::checkInternal(PfRule id,
61		const std::vector<Node>& children,
62		const std::vector<Node>& args)
63		{
64	5875	NodeManager* nm = NodeManager::currentNM();
65		// core rules for word equations
66	5875	if (id == PfRule::CONCAT_EQ \|\| id == PfRule::CONCAT_UNIFY
67	3980	\|\| id == PfRule::CONCAT_CONFLICT \|\| id == PfRule::CONCAT_SPLIT
68	3929	\|\| id == PfRule::CONCAT_CSPLIT \|\| id == PfRule::CONCAT_LPROP
69	3492	\|\| id == PfRule::CONCAT_CPROP)
70		{
71	2417	Trace("strings-pfcheck") << "Checking id " << id << std::endl;
72	2417	Assert(children.size() >= 1);
73	2417	Assert(args.size() == 1);
74		// all rules have an equality
75	2417	if (children[0].getKind() != EQUAL)
76		{
77		return Node::null();
78		}
79		// convert to concatenation form
80	4834	std::vector<Node> tvec;
81	4834	std::vector<Node> svec;
82	2417	utils::getConcat(children[0][0], tvec);
83	2417	utils::getConcat(children[0][1], svec);
84	2417	size_t nchildt = tvec.size();
85	2417	size_t nchilds = svec.size();
86	4834	TypeNode stringType = children[0][0].getType();
87		// extract the Boolean corresponding to whether the rule is reversed
88		bool isRev;
89	2417	if (!getBool(args[0], isRev))
90		{
91		return Node::null();
92		}
93	2417	if (id == PfRule::CONCAT_EQ)
94		{
95	1317	Assert(children.size() == 1);
96	1317	size_t index = 0;
97	2634	std::vector<Node> tremVec;
98	2634	std::vector<Node> sremVec;
99		// scan the concatenation until we exhaust child proofs
100	3139	while (index < nchilds && index < nchildt)
101		{
102	3139	Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
103	3139	Node currS = svec[isRev ? (nchilds - 1 - index) : index];
104	2228	if (currT != currS)
105		{
106	1317	if (currT.isConst() && currS.isConst())
107		{
108		size_t sindex;
109		// get the equal prefix/suffix, strip and add the remainders
110	802	Node currR = Word::splitConstant(currT, currS, sindex, isRev);
111	401	if (!currR.isNull())
112		{
113		// add the constant to remainder vec
114	375	std::vector<Node>& rem = sindex == 0 ? tremVec : sremVec;
115	375	rem.push_back(currR);
116		// ignore the current component
117	375	index++;
118		// In other words, if we have (currS,currT) = ("ab","abc"), then
119		// we proceed to the next component and add currR = "c" to
120		// tremVec.
121		}
122		// otherwise if we are not the same prefix, then both will be added
123		// Notice that we do not add maximal prefixes, in other words,
124		// ("abc", "abd") may be added to the remainder vectors, and not
125		// ("c", "d").
126		}
127	1317	break;
128		}
129	911	index++;
130		}
131	1317	Assert(index <= nchildt);
132	1317	Assert(index <= nchilds);
133		// the remainders are equal
134	3951	tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
135	2634	tvec.begin() + (isRev ? 0 : index),
136	6585	tvec.begin() + nchildt - (isRev ? index : 0));
137	3951	sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
138	2634	svec.begin() + (isRev ? 0 : index),
139	6585	svec.begin() + nchilds - (isRev ? index : 0));
140		// convert back to node
141	2634	Node trem = utils::mkConcat(tremVec, stringType);
142	2634	Node srem = utils::mkConcat(sremVec, stringType);
143	1317	return trem.eqNode(srem);
144		}
145		// all remaining rules do something with the first child of each side
146	2200	Node t0 = tvec[isRev ? nchildt - 1 : 0];
147	2200	Node s0 = svec[isRev ? nchilds - 1 : 0];
148	1100	if (id == PfRule::CONCAT_UNIFY)
149		{
150	578	Assert(children.size() == 2);
151	578	if (children[1].getKind() != EQUAL)
152		{
153		return Node::null();
154		}
155	1732	for (size_t i = 0; i < 2; i++)
156		{
157	1173	Node l = children[1][i];
158	1155	if (l.getKind() != STRING_LENGTH)
159		{
160		return Node::null();
161		}
162	1173	Node term = i == 0 ? t0 : s0;
163	1155	if (l[0] == term)
164		{
165	1136	continue;
166		}
167		// could be a spliced constant
168	19	bool success = false;
169	19	if (term.isConst() && l[0].isConst())
170		{
171	18	size_t lenL = Word::getLength(l[0]);
172	36	success = (isRev && l[0] == Word::suffix(term, lenL))
173	54	\|\| (!isRev && l[0] == Word::prefix(term, lenL));
174		}
175	19	if (!success)
176		{
177	1	return Node::null();
178		}
179		}
180	577	return children[1][0][0].eqNode(children[1][1][0]);
181		}
182	522	else if (id == PfRule::CONCAT_CONFLICT)
183		{
184	34	Assert(children.size() == 1);
185	34	if (!t0.isConst() \|\| !s0.isConst())
186		{
187		// not constants
188		return Node::null();
189		}
190		size_t sindex;
191	68	Node r0 = Word::splitConstant(t0, s0, sindex, isRev);
192	34	if (!r0.isNull())
193		{
194		// Not a conflict due to constants, i.e. s0 is a prefix of t0 or vice
195		// versa.
196		return Node::null();
197		}
198	34	return nm->mkConst(false);
199		}
200	488	else if (id == PfRule::CONCAT_SPLIT)
201		{
202	17	Assert(children.size() == 2);
203	51	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
204	34	\|\| children[1][0][0].getKind() != STRING_LENGTH
205	34	\|\| children[1][0][0][0] != t0
206	34	\|\| children[1][0][1].getKind() != STRING_LENGTH
207	51	\|\| children[1][0][1][0] != s0)
208		{
209		return Node::null();
210		}
211		}
212	471	else if (id == PfRule::CONCAT_CSPLIT)
213		{
214	340	Assert(children.size() == 2);
215	680	Node zero = nm->mkConst(Rational(0));
216	680	Node one = nm->mkConst(Rational(1));
217	1020	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
218	680	\|\| children[1][0][0].getKind() != STRING_LENGTH
219	1020	\|\| children[1][0][0][0] != t0 \|\| children[1][0][1] != zero)
220		{
221		return Node::null();
222		}
223	340	if (!s0.isConst() \|\| !s0.getType().isStringLike() \|\| Word::isEmpty(s0))
224		{
225		return Node::null();
226		}
227		}
228	131	else if (id == PfRule::CONCAT_LPROP)
229		{
230	97	Assert(children.size() == 2);
231	194	if (children[1].getKind() != GT
232	194	\|\| children[1][0].getKind() != STRING_LENGTH
233	194	\|\| children[1][0][0] != t0
234	194	\|\| children[1][1].getKind() != STRING_LENGTH
235	291	\|\| children[1][1][0] != s0)
236		{
237		return Node::null();
238		}
239		}
240	34	else if (id == PfRule::CONCAT_CPROP)
241		{
242	34	Assert(children.size() == 2);
243	68	Node zero = nm->mkConst(Rational(0));
244
245	68	Trace("pfcheck-strings-cprop")
246	34	<< "CONCAT_PROP, isRev=" << isRev << std::endl;
247	102	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
248	68	\|\| children[1][0][0].getKind() != STRING_LENGTH
249	102	\|\| children[1][0][0][0] != t0 \|\| children[1][0][1] != zero)
250		{
251		Trace("pfcheck-strings-cprop")
252		<< "...failed pattern match" << std::endl;
253		return Node::null();
254		}
255	34	if (tvec.size() <= 1)
256		{
257		Trace("pfcheck-strings-cprop")
258		<< "...failed adjacent constant" << std::endl;
259		return Node::null();
260		}
261	68	Node w1 = tvec[isRev ? nchildt - 2 : 1];
262	34	if (!w1.isConst() \|\| !w1.getType().isStringLike() \|\| Word::isEmpty(w1))
263		{
264		Trace("pfcheck-strings-cprop")
265		<< "...failed adjacent constant content" << std::endl;
266		return Node::null();
267		}
268	68	Node w2 = s0;
269	34	if (!w2.isConst() \|\| !w2.getType().isStringLike() \|\| Word::isEmpty(w2))
270		{
271		Trace("pfcheck-strings-cprop") << "...failed constant" << std::endl;
272		return Node::null();
273		}
274		// getConclusion expects the adjacent constant to be included
275	34	t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
276		}
277		// use skolem cache
278	976	SkolemCache skc(false);
279	976	std::vector<Node> newSkolems;
280	976	Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems);
281	488	return conc;
282		}
283	3458	else if (id == PfRule::STRING_DECOMPOSE)
284		{
285	2	Assert(children.size() == 1);
286	2	Assert(args.size() == 1);
287		bool isRev;
288	2	if (!getBool(args[0], isRev))
289		{
290		return Node::null();
291		}
292	4	Node atom = children[0];
293	2	if (atom.getKind() != GEQ \|\| atom[0].getKind() != STRING_LENGTH)
294		{
295		return Node::null();
296		}
297	4	SkolemCache sc(false);
298	4	std::vector<Node> newSkolems;
299		Node conc = CoreSolver::getConclusion(
300	4	atom[0][0], atom[1], id, isRev, &sc, newSkolems);
301	2	return conc;
302		}
303	3456	else if (id == PfRule::STRING_REDUCTION
304	2916	\|\| id == PfRule::STRING_EAGER_REDUCTION
305	1840	\|\| id == PfRule::STRING_LENGTH_POS)
306		{
307	2722	Assert(children.empty());
308	2722	Assert(args.size() >= 1);
309		// These rules are based on calling a C++ method for returning a valid
310		// lemma involving a single argument term.
311		// Must convert to skolem form.
312	5444	Node t = args[0];
313	5444	Node ret;
314	2722	if (id == PfRule::STRING_REDUCTION)
315		{
316	540	Assert(args.size() == 1);
317		// we do not use optimizations
318	1080	SkolemCache skc(false);
319	1080	std::vector<Node> conj;
320	540	ret = StringsPreprocess::reduce(t, conj, &skc);
321	540	conj.push_back(t.eqNode(ret));
322	540	ret = nm->mkAnd(conj);
323		}
324	2182	else if (id == PfRule::STRING_EAGER_REDUCTION)
325		{
326	1076	Assert(args.size() == 1);
327	2152	SkolemCache skc(false);
328	1076	ret = TermRegistry::eagerReduce(t, &skc);
329		}
330	1106	else if (id == PfRule::STRING_LENGTH_POS)
331		{
332	1106	Assert(args.size() == 1);
333	1106	ret = TermRegistry::lengthPositive(t);
334		}
335	2722	if (ret.isNull())
336		{
337		return Node::null();
338		}
339	2722	return ret;
340		}
341	734	else if (id == PfRule::STRING_LENGTH_NON_EMPTY)
342		{
343	264	Assert(children.size() == 1);
344	264	Assert(args.empty());
345	528	Node nemp = children[0];
346	785	if (nemp.getKind() != NOT \|\| nemp[0].getKind() != EQUAL
347	767	\|\| !nemp[0][1].isConst() \|\| !nemp[0][1].getType().isStringLike())
348		{
349	40	return Node::null();
350		}
351	224	if (!Word::isEmpty(nemp[0][1]))
352		{
353		return Node::null();
354		}
355	448	Node zero = nm->mkConst(Rational(0));
356	448	Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
357	224	return clen.eqNode(zero).notNode();
358		}
359	470	else if (id == PfRule::RE_INTER)
360		{
361	11	Assert(children.size() >= 1);
362	11	Assert(args.empty());
363	22	std::vector<Node> reis;
364	22	Node x;
365		// make the regular expression intersection that summarizes all
366		// memberships in the explanation
367	31	for (const Node& c : children)
368		{
369	22	bool polarity = c.getKind() != NOT;
370	42	Node catom = polarity ? c : c[0];
371	22	if (catom.getKind() != STRING_IN_REGEXP)
372		{
373		return Node::null();
374		}
375	22	if (x.isNull())
376		{
377	11	x = catom[0];
378		}
379	11	else if (x != catom[0])
380		{
381		// different LHS
382	2	return Node::null();
383		}
384	40	Node xcurr = catom[0];
385		Node rcurr =
386	40	polarity ? catom[1] : nm->mkNode(REGEXP_COMPLEMENT, catom[1]);
387	20	reis.push_back(rcurr);
388		}
389	18	Node rei = reis.size() == 1 ? reis[0] : nm->mkNode(REGEXP_INTER, reis);
390	9	return nm->mkNode(STRING_IN_REGEXP, x, rei);
391		}
392	459	else if (id == PfRule::RE_UNFOLD_POS \|\| id == PfRule::RE_UNFOLD_NEG
393	359	\|\| id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
394		{
395	118	Assert(children.size() == 1);
396	118	Assert(args.empty());
397	236	Node skChild = children[0];
398	118	if (id == PfRule::RE_UNFOLD_NEG \|\| id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
399		{
400	48	if (skChild.getKind() != NOT \|\| skChild[0].getKind() != STRING_IN_REGEXP)
401		{
402		Trace("strings-pfcheck") << "...fail, non-neg member" << std::endl;
403		return Node::null();
404		}
405		}
406	94	else if (skChild.getKind() != STRING_IN_REGEXP)
407		{
408		Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
409		return Node::null();
410		}
411	236	Node conc;
412	118	if (id == PfRule::RE_UNFOLD_POS)
413		{
414	188	std::vector<Node> newSkolems;
415	188	SkolemCache sc;
416	94	conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems);
417		}
418	24	else if (id == PfRule::RE_UNFOLD_NEG)
419		{
420	6	conc = RegExpOpr::reduceRegExpNeg(skChild);
421		}
422	18	else if (id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
423		{
424	18	if (skChild[0][1].getKind() != REGEXP_CONCAT)
425		{
426		Trace("strings-pfcheck") << "...fail, no concat regexp" << std::endl;
427		return Node::null();
428		}
429		size_t index;
430	36	Node reLen = RegExpOpr::getRegExpConcatFixed(skChild[0][1], index);
431	18	if (reLen.isNull())
432		{
433		Trace("strings-pfcheck") << "...fail, non-fixed lengths" << std::endl;
434		return Node::null();
435		}
436	18	conc = RegExpOpr::reduceRegExpNegConcatFixed(skChild, reLen, index);
437		}
438	118	return conc;
439		}
440	341	else if (id == PfRule::RE_ELIM)
441		{
442	4	Assert(children.empty());
443	4	Assert(args.size() == 2);
444		bool isAgg;
445	4	if (!getBool(args[1], isAgg))
446		{
447		return Node::null();
448		}
449	8	Node ea = RegExpElimination::eliminate(args[0], isAgg);
450		// if we didn't eliminate, then this trivially proves the reflexive equality
451	4	if (ea.isNull())
452		{
453		ea = args[0];
454		}
455	4	return args[0].eqNode(ea);
456		}
457	337	else if (id == PfRule::STRING_CODE_INJ)
458		{
459	165	Assert(children.empty());
460	165	Assert(args.size() == 2);
461	165	Assert(args[0].getType().isStringLike()
462		&& args[1].getType().isStringLike());
463	330	Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
464	330	Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
465	330	Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1)));
466	330	Node deq = c1.eqNode(c2).negate();
467	330	Node eqn = args[0].eqNode(args[1]);
468	165	return nm->mkNode(kind::OR, eqNegOne, deq, eqn);
469		}
470	172	else if (id == PfRule::STRING_SEQ_UNIT_INJ)
471		{
472	12	Assert(children.size() == 1);
473	12	Assert(args.empty());
474	12	if (children[0].getKind() != EQUAL)
475		{
476		return Node::null();
477		}
478	24	Node t[2];
479	36	for (size_t i = 0; i < 2; i++)
480		{
481	24	if (children[0][i].getKind() == SEQ_UNIT)
482		{
483	20	t[i] = children[0][i][0];
484		}
485	4	else if (children[0][i].isConst())
486		{
487		// notice that Word::getChars is not the right call here, since it
488		// gets a vector of sequences of length one. We actually need to
489		// extract the character, which is a sequence-specific operation.
490	4	const Sequence& sx = children[0][i].getConst<Sequence>();
491	4	const std::vector<Node>& vec = sx.getVec();
492	4	if (vec.size() == 1)
493		{
494		// the character of the single character sequence
495	4	t[i] = vec[0];
496		}
497		}
498	24	if (t[i].isNull())
499		{
500		return Node::null();
501		}
502		}
503	24	Trace("strings-pfcheck-debug")
504	12	<< "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
505	12	<< " == " << t[1] << std::endl;
506	12	AlwaysAssert(t[0].getType() == t[1].getType());
507	12	return t[0].eqNode(t[1]);
508		}
509	160	else if (id == PfRule::STRING_TRUST)
510		{
511		// "trusted" rules
512	160	Assert(!args.empty());
513	160	Assert(args[0].getType().isBoolean());
514	160	return args[0];
515		}
516		return Node::null();
517		}
518
519		} // namespace strings
520		} // namespace theory
521	29322	} // namespace cvc5