Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/proof_checker.cpp	Lines:	247	295	83.7 %
Date:	2021-09-07	Branches:	643	1826	35.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 rule
  pc->registerTrustedChecker(PfRule::STRING_INFERENCE, 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_INFERENCE)
  {
    Assert(args.size() >= 3);
    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	3786	void StringProofRuleChecker::registerTo(ProofChecker* pc)
36		{
37	3786	pc->registerChecker(PfRule::CONCAT_EQ, this);
38	3786	pc->registerChecker(PfRule::CONCAT_UNIFY, this);
39	3786	pc->registerChecker(PfRule::CONCAT_CONFLICT, this);
40	3786	pc->registerChecker(PfRule::CONCAT_SPLIT, this);
41	3786	pc->registerChecker(PfRule::CONCAT_CSPLIT, this);
42	3786	pc->registerChecker(PfRule::CONCAT_LPROP, this);
43	3786	pc->registerChecker(PfRule::CONCAT_CPROP, this);
44	3786	pc->registerChecker(PfRule::STRING_DECOMPOSE, this);
45	3786	pc->registerChecker(PfRule::STRING_LENGTH_POS, this);
46	3786	pc->registerChecker(PfRule::STRING_LENGTH_NON_EMPTY, this);
47	3786	pc->registerChecker(PfRule::STRING_REDUCTION, this);
48	3786	pc->registerChecker(PfRule::STRING_EAGER_REDUCTION, this);
49	3786	pc->registerChecker(PfRule::RE_INTER, this);
50	3786	pc->registerChecker(PfRule::RE_UNFOLD_POS, this);
51	3786	pc->registerChecker(PfRule::RE_UNFOLD_NEG, this);
52	3786	pc->registerChecker(PfRule::RE_UNFOLD_NEG_CONCAT_FIXED, this);
53	3786	pc->registerChecker(PfRule::RE_ELIM, this);
54	3786	pc->registerChecker(PfRule::STRING_CODE_INJ, this);
55	3786	pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
56		// trusted rule
57	3786	pc->registerTrustedChecker(PfRule::STRING_INFERENCE, this, 2);
58	3786	}
59
60	2760	Node StringProofRuleChecker::checkInternal(PfRule id,
61		const std::vector<Node>& children,
62		const std::vector<Node>& args)
63		{
64	2760	NodeManager* nm = NodeManager::currentNM();
65		// core rules for word equations
66	2760	if (id == PfRule::CONCAT_EQ \|\| id == PfRule::CONCAT_UNIFY
67	1639	\|\| id == PfRule::CONCAT_CONFLICT \|\| id == PfRule::CONCAT_SPLIT
68	1605	\|\| id == PfRule::CONCAT_CSPLIT \|\| id == PfRule::CONCAT_LPROP
69	1182	\|\| id == PfRule::CONCAT_CPROP)
70		{
71	1605	Trace("strings-pfcheck") << "Checking id " << id << std::endl;
72	1605	Assert(children.size() >= 1);
73	1605	Assert(args.size() == 1);
74		// all rules have an equality
75	1605	if (children[0].getKind() != EQUAL)
76		{
77		return Node::null();
78		}
79		// convert to concatenation form
80	3210	std::vector<Node> tvec;
81	3210	std::vector<Node> svec;
82	1605	utils::getConcat(children[0][0], tvec);
83	1605	utils::getConcat(children[0][1], svec);
84	1605	size_t nchildt = tvec.size();
85	1605	size_t nchilds = svec.size();
86	3210	TypeNode stringType = children[0][0].getType();
87		// extract the Boolean corresponding to whether the rule is reversed
88		bool isRev;
89	1605	if (!getBool(args[0], isRev))
90		{
91		return Node::null();
92		}
93	1605	if (id == PfRule::CONCAT_EQ)
94		{
95	759	Assert(children.size() == 1);
96	759	size_t index = 0;
97	1518	std::vector<Node> tremVec;
98	1518	std::vector<Node> sremVec;
99		// scan the concatenation until we exhaust child proofs
100	1855	while (index < nchilds && index < nchildt)
101		{
102	1855	Node currT = tvec[isRev ? (nchildt - 1 - index) : index];
103	1855	Node currS = svec[isRev ? (nchilds - 1 - index) : index];
104	1307	if (currT != currS)
105		{
106	759	if (currT.isConst() && currS.isConst())
107		{
108		size_t sindex;
109		// get the equal prefix/suffix, strip and add the remainders
110	370	Node currR = Word::splitConstant(currT, currS, sindex, isRev);
111	185	if (!currR.isNull())
112		{
113		// add the constant to remainder vec
114	179	std::vector<Node>& rem = sindex == 0 ? tremVec : sremVec;
115	179	rem.push_back(currR);
116		// ignore the current component
117	179	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	759	break;
128		}
129	548	index++;
130		}
131	759	Assert(index <= nchildt);
132	759	Assert(index <= nchilds);
133		// the remainders are equal
134	2277	tremVec.insert(isRev ? tremVec.begin() : tremVec.end(),
135	1518	tvec.begin() + (isRev ? 0 : index),
136	3795	tvec.begin() + nchildt - (isRev ? index : 0));
137	2277	sremVec.insert(isRev ? sremVec.begin() : sremVec.end(),
138	1518	svec.begin() + (isRev ? 0 : index),
139	3795	svec.begin() + nchilds - (isRev ? index : 0));
140		// convert back to node
141	1518	Node trem = utils::mkConcat(tremVec, stringType);
142	1518	Node srem = utils::mkConcat(sremVec, stringType);
143	759	return trem.eqNode(srem);
144		}
145		// all remaining rules do something with the first child of each side
146	1692	Node t0 = tvec[isRev ? nchildt - 1 : 0];
147	1692	Node s0 = svec[isRev ? nchilds - 1 : 0];
148	846	if (id == PfRule::CONCAT_UNIFY)
149		{
150	362	Assert(children.size() == 2);
151	362	if (children[1].getKind() != EQUAL)
152		{
153		return Node::null();
154		}
155	1084	for (size_t i = 0; i < 2; i++)
156		{
157	733	Node l = children[1][i];
158	723	if (l.getKind() != STRING_LENGTH)
159		{
160		return Node::null();
161		}
162	733	Node term = i == 0 ? t0 : s0;
163	723	if (l[0] == term)
164		{
165	712	continue;
166		}
167		// could be a spliced constant
168	11	bool success = false;
169	11	if (term.isConst() && l[0].isConst())
170		{
171	10	size_t lenL = Word::getLength(l[0]);
172	20	success = (isRev && l[0] == Word::suffix(term, lenL))
173	30	\|\| (!isRev && l[0] == Word::prefix(term, lenL));
174		}
175	11	if (!success)
176		{
177	1	return Node::null();
178		}
179		}
180	361	return children[1][0][0].eqNode(children[1][1][0]);
181		}
182	484	else if (id == PfRule::CONCAT_CONFLICT)
183		{
184	10	Assert(children.size() == 1);
185	10	if (!t0.isConst() \|\| !s0.isConst())
186		{
187		// not constants
188		return Node::null();
189		}
190		size_t sindex;
191	20	Node r0 = Word::splitConstant(t0, s0, sindex, isRev);
192	10	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	10	return nm->mkConst(false);
199		}
200	474	else if (id == PfRule::CONCAT_SPLIT)
201		{
202	24	Assert(children.size() == 2);
203	72	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
204	48	\|\| children[1][0][0].getKind() != STRING_LENGTH
205	48	\|\| children[1][0][0][0] != t0
206	48	\|\| children[1][0][1].getKind() != STRING_LENGTH
207	72	\|\| children[1][0][1][0] != s0)
208		{
209		return Node::null();
210		}
211		}
212	450	else if (id == PfRule::CONCAT_CSPLIT)
213		{
214	309	Assert(children.size() == 2);
215	618	Node zero = nm->mkConst(Rational(0));
216	618	Node one = nm->mkConst(Rational(1));
217	927	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
218	618	\|\| children[1][0][0].getKind() != STRING_LENGTH
219	927	\|\| children[1][0][0][0] != t0 \|\| children[1][0][1] != zero)
220		{
221		return Node::null();
222		}
223	309	if (!s0.isConst() \|\| !s0.getType().isStringLike() \|\| Word::isEmpty(s0))
224		{
225		return Node::null();
226		}
227		}
228	141	else if (id == PfRule::CONCAT_LPROP)
229		{
230	114	Assert(children.size() == 2);
231	228	if (children[1].getKind() != GT
232	228	\|\| children[1][0].getKind() != STRING_LENGTH
233	228	\|\| children[1][0][0] != t0
234	228	\|\| children[1][1].getKind() != STRING_LENGTH
235	342	\|\| children[1][1][0] != s0)
236		{
237		return Node::null();
238		}
239		}
240	27	else if (id == PfRule::CONCAT_CPROP)
241		{
242	27	Assert(children.size() == 2);
243	54	Node zero = nm->mkConst(Rational(0));
244
245	54	Trace("pfcheck-strings-cprop")
246	27	<< "CONCAT_PROP, isRev=" << isRev << std::endl;
247	81	if (children[1].getKind() != NOT \|\| children[1][0].getKind() != EQUAL
248	54	\|\| children[1][0][0].getKind() != STRING_LENGTH
249	81	\|\| 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	27	if (tvec.size() <= 1)
256		{
257		Trace("pfcheck-strings-cprop")
258		<< "...failed adjacent constant" << std::endl;
259		return Node::null();
260		}
261	54	Node w1 = tvec[isRev ? nchildt - 2 : 1];
262	27	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	54	Node w2 = s0;
269	27	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	27	t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
276		}
277		// use skolem cache
278	948	SkolemCache skc(false);
279	948	std::vector<Node> newSkolems;
280	948	Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems);
281	474	return conc;
282		}
283	1155	else if (id == PfRule::STRING_DECOMPOSE)
284		{
285		Assert(children.size() == 1);
286		Assert(args.size() == 1);
287		bool isRev;
288		if (!getBool(args[0], isRev))
289		{
290		return Node::null();
291		}
292		Node atom = children[0];
293		if (atom.getKind() != GEQ \|\| atom[0].getKind() != STRING_LENGTH)
294		{
295		return Node::null();
296		}
297		SkolemCache sc(false);
298		std::vector<Node> newSkolems;
299		Node conc = CoreSolver::getConclusion(
300		atom[0][0], atom[1], id, isRev, &sc, newSkolems);
301		return conc;
302		}
303	1155	else if (id == PfRule::STRING_REDUCTION
304	730	\|\| id == PfRule::STRING_EAGER_REDUCTION
305	650	\|\| id == PfRule::STRING_LENGTH_POS)
306		{
307	710	Assert(children.empty());
308	710	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	1420	Node t = args[0];
313	1420	Node ret;
314	710	if (id == PfRule::STRING_REDUCTION)
315		{
316	425	Assert(args.size() == 1);
317		// we do not use optimizations
318	850	SkolemCache skc(false);
319	850	std::vector<Node> conj;
320	425	ret = StringsPreprocess::reduce(t, conj, &skc);
321	425	conj.push_back(t.eqNode(ret));
322	425	ret = nm->mkAnd(conj);
323		}
324	285	else if (id == PfRule::STRING_EAGER_REDUCTION)
325		{
326	80	Assert(args.size() == 1);
327	160	SkolemCache skc(false);
328	80	ret = TermRegistry::eagerReduce(t, &skc);
329		}
330	205	else if (id == PfRule::STRING_LENGTH_POS)
331		{
332	205	Assert(args.size() == 1);
333	205	ret = TermRegistry::lengthPositive(t);
334		}
335	710	if (ret.isNull())
336		{
337		return Node::null();
338		}
339	710	return ret;
340		}
341	445	else if (id == PfRule::STRING_LENGTH_NON_EMPTY)
342		{
343	183	Assert(children.size() == 1);
344	183	Assert(args.empty());
345	366	Node nemp = children[0];
346	543	if (nemp.getKind() != NOT \|\| nemp[0].getKind() != EQUAL
347	530	\|\| !nemp[0][1].isConst() \|\| !nemp[0][1].getType().isStringLike())
348		{
349	29	return Node::null();
350		}
351	154	if (!Word::isEmpty(nemp[0][1]))
352		{
353		return Node::null();
354		}
355	308	Node zero = nm->mkConst(Rational(0));
356	308	Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
357	154	return clen.eqNode(zero).notNode();
358		}
359	262	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	251	else if (id == PfRule::RE_UNFOLD_POS \|\| id == PfRule::RE_UNFOLD_NEG
393	189	\|\| id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
394		{
395	80	Assert(children.size() == 1);
396	80	Assert(args.empty());
397	160	Node skChild = children[0];
398	80	if (id == PfRule::RE_UNFOLD_NEG \|\| id == PfRule::RE_UNFOLD_NEG_CONCAT_FIXED)
399		{
400	40	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	60	else if (skChild.getKind() != STRING_IN_REGEXP)
407		{
408		Trace("strings-pfcheck") << "...fail, non-pos member" << std::endl;
409		return Node::null();
410		}
411	160	Node conc;
412	80	if (id == PfRule::RE_UNFOLD_POS)
413		{
414	120	std::vector<Node> newSkolems;
415	120	SkolemCache sc;
416	60	conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems);
417		}
418	20	else if (id == PfRule::RE_UNFOLD_NEG)
419		{
420	2	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	80	return conc;
439		}
440	171	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	167	else if (id == PfRule::STRING_CODE_INJ)
458		{
459	69	Assert(children.empty());
460	69	Assert(args.size() == 2);
461	69	Assert(args[0].getType().isStringLike()
462		&& args[1].getType().isStringLike());
463	138	Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
464	138	Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
465	138	Node eqNegOne = c1.eqNode(nm->mkConst(Rational(-1)));
466	138	Node deq = c1.eqNode(c2).negate();
467	138	Node eqn = args[0].eqNode(args[1]);
468	69	return nm->mkNode(kind::OR, eqNegOne, deq, eqn);
469		}
470	98	else if (id == PfRule::STRING_SEQ_UNIT_INJ)
471		{
472	5	Assert(children.size() == 1);
473	5	Assert(args.empty());
474	5	if (children[0].getKind() != EQUAL)
475		{
476		return Node::null();
477		}
478	10	Node t[2];
479	15	for (size_t i = 0; i < 2; i++)
480		{
481	10	if (children[0][i].getKind() == SEQ_UNIT)
482		{
483	9	t[i] = children[0][i][0];
484		}
485	1	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	1	const Sequence& sx = children[0][i].getConst<Sequence>();
491	1	const std::vector<Node>& vec = sx.getVec();
492	1	if (vec.size() == 1)
493		{
494		// the character of the single character sequence
495	1	t[i] = vec[0];
496		}
497		}
498	10	if (t[i].isNull())
499		{
500		return Node::null();
501		}
502		}
503	10	Trace("strings-pfcheck-debug")
504	5	<< "STRING_SEQ_UNIT_INJ: " << children[0] << " => " << t[0]
505	5	<< " == " << t[1] << std::endl;
506	5	AlwaysAssert(t[0].getType() == t[1].getType());
507	5	return t[0].eqNode(t[1]);
508		}
509	93	else if (id == PfRule::STRING_INFERENCE)
510		{
511	93	Assert(args.size() >= 3);
512	93	return args[0];
513		}
514		return Node::null();
515		}
516
517		} // namespace strings
518		} // namespace theory
519	29502	} // namespace cvc5