Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/term_registry.cpp	Lines:	286	327	87.5 %
Date:	2021-11-05	Branches:	689	1488	46.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Morgan Deters
 *
 * 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 term registry for the theory of strings.
 */

#include "theory/strings/term_registry.h"

#include "expr/attribute.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "smt/logic_exception.h"
#include "theory/rewriter.h"
#include "theory/strings/inference_manager.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
#include "util/rational.h"
#include "util/string.h"

using namespace std;
using namespace cvc5::context;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

TermRegistry::TermRegistry(Env& env,
                           SolverState& s,
                           SequencesStatistics& statistics,
                           ProofNodeManager* pnm)
    : EnvObj(env),
      d_state(s),
      d_im(nullptr),
      d_statistics(statistics),
      d_hasStrCode(false),
      d_hasSeqUpdate(false),
      d_skCache(env.getRewriter()),
      d_aent(env.getRewriter()),
      d_functionsTerms(context()),
      d_inputVars(userContext()),
      d_preregisteredTerms(context()),
      d_registeredTerms(userContext()),
      d_registeredTypes(userContext()),
      d_proxyVar(userContext()),
      d_proxyVarToLength(userContext()),
      d_lengthLemmaTermsCache(userContext()),
      d_epg(
          pnm ? new EagerProofGenerator(
              pnm, userContext(), "strings::TermRegistry::EagerProofGenerator")
              : nullptr)
{
  NodeManager* nm = NodeManager::currentNM();
  d_zero = nm->mkConst(Rational(0));
  d_one = nm->mkConst(Rational(1));
  d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
  Assert(options().strings.stringsAlphaCard <= String::num_codes());
  d_alphaCard = options().strings.stringsAlphaCard;
}

TermRegistry::~TermRegistry() {}

uint32_t TermRegistry::getAlphabetCardinality() const { return d_alphaCard; }

void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }

Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
{
  NodeManager* nm = NodeManager::currentNM();
  Node lemma;
  Kind tk = t.getKind();
  if (tk == STRING_TO_CODE)
  {
    // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
    Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
    Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
    Node code_range =
        nm->mkNode(AND,
                   nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
                   nm->mkNode(LT, t, nm->mkConst(Rational(alphaCard))));
    lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
  }
  else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
  {
    // (and
    //   (or (= (f x y n) (- 1)) (>= (f x y n) n))
    //   (<= (f x y n) (str.len x)))
    //
    // where f in { str.indexof, str.indexof_re }
    Node l = nm->mkNode(STRING_LENGTH, t[0]);
    lemma = nm->mkNode(
        AND,
        nm->mkNode(
            OR, t.eqNode(nm->mkConst(Rational(-1))), nm->mkNode(GEQ, t, t[2])),
        nm->mkNode(LEQ, t, l));
  }
  else if (tk == STRING_STOI)
  {
    // (>= (str.to_int x) (- 1))
    lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
  }
  else if (tk == STRING_CONTAINS)
  {
    // ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
    Node sk1 =
        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
    Node sk2 =
        sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
    lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
    lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
  }
  return lemma;
}

Node TermRegistry::lengthPositive(Node t)
{
  NodeManager* nm = NodeManager::currentNM();
  Node zero = nm->mkConst(Rational(0));
  Node emp = Word::mkEmptyWord(t.getType());
  Node tlen = nm->mkNode(STRING_LENGTH, t);
  Node tlenEqZero = tlen.eqNode(zero);
  Node tEqEmp = t.eqNode(emp);
  Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
  Node caseNEmpty = nm->mkNode(GT, tlen, zero);
  // (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
  return nm->mkNode(OR, caseEmpty, caseNEmpty);
}

void TermRegistry::preRegisterTerm(TNode n)
{
  if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
  {
    return;
  }
  eq::EqualityEngine* ee = d_state.getEqualityEngine();
  d_preregisteredTerms.insert(n);
  Trace("strings-preregister")
      << "TheoryString::preregister : " << n << std::endl;
  // check for logic exceptions
  Kind k = n.getKind();
  if (!options::stringExp())
  {
    if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
        || k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR
        || k == STRING_REPLACE_ALL || k == SEQ_NTH || k == STRING_REPLACE_RE
        || k == STRING_REPLACE_RE_ALL || k == STRING_CONTAINS || k == STRING_LEQ
        || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV
        || k == STRING_UPDATE)
    {
      std::stringstream ss;
      ss << "Term of kind " << k
         << " not supported in default mode, try --strings-exp";
      throw LogicException(ss.str());
    }
  }
  if (k == EQUAL)
  {
    if (n[0].getType().isRegExp())
    {
      std::stringstream ss;
      ss << "Equality between regular expressions is not supported";
      throw LogicException(ss.str());
    }
    ee->addTriggerPredicate(n);
    return;
  }
  else if (k == STRING_IN_REGEXP)
  {
    d_im->requirePhase(n, true);
    ee->addTriggerPredicate(n);
    ee->addTerm(n[0]);
    ee->addTerm(n[1]);
    return;
  }
  else if (k == STRING_TO_CODE)
  {
    d_hasStrCode = true;
  }
  else if (k == SEQ_NTH || k == STRING_UPDATE)
  {
    d_hasSeqUpdate = true;
  }
  else if (k == REGEXP_RANGE)
  {
    for (const Node& nc : n)
    {
      if (!nc.isConst())
      {
        throw LogicException(
            "expecting a constant string term in regexp range");
      }
      if (nc.getConst<String>().size() != 1)
      {
        throw LogicException(
            "expecting a single constant string term in regexp range");
      }
    }
  }
  registerTerm(n, 0);
  TypeNode tn = n.getType();
  if (tn.isRegExp() && n.isVar())
  {
    std::stringstream ss;
    ss << "Regular expression variables are not supported.";
    throw LogicException(ss.str());
  }
  if (tn.isString())  // string-only
  {
    // all characters of constants should fall in the alphabet
    if (n.isConst())
    {
      std::vector<unsigned> vec = n.getConst<String>().getVec();
      for (unsigned u : vec)
      {
        if (u >= d_alphaCard)
        {
          std::stringstream ss;
          ss << "Characters in string \"" << n
             << "\" are outside of the given alphabet.";
          throw LogicException(ss.str());
        }
      }
    }
    ee->addTerm(n);
  }
  else if (tn.isBoolean())
  {
    // All kinds that we do congruence over that may return a Boolean go here
    if (k == STRING_CONTAINS || k == STRING_LEQ || k == SEQ_NTH)
    {
      // Get triggered for both equal and dis-equal
      ee->addTriggerPredicate(n);
    }
  }
  else
  {
    // Function applications/predicates
    ee->addTerm(n);
  }
  // Set d_functionsTerms stores all function applications that are
  // relevant to theory combination. Notice that this is a subset of
  // the applications whose kinds are function kinds in the equality
  // engine. This means it does not include applications of operators
  // like re.++, which is not a function kind in the equality engine.
  // Concatenation terms do not need to be considered here because
  // their arguments have string type and do not introduce any shared
  // terms.
  if (n.hasOperator() && ee->isFunctionKind(k)
      && kindToTheoryId(k) == THEORY_STRINGS && k != STRING_CONCAT)
  {
    d_functionsTerms.push_back(n);
  }
  if (options::stringFMF())
  {
    if (tn.isStringLike())
    {
      // Our decision strategy will minimize the length of this term if it is a
      // variable but not an internally generated Skolem, or a term that does
      // not belong to this theory.
      if (n.isVar() ? !d_skCache.isSkolem(n)
                    : kindToTheoryId(k) != THEORY_STRINGS)
      {
        d_inputVars.insert(n);
        Trace("strings-preregister") << "input variable: " << n << std::endl;
      }
    }
  }
}

void TermRegistry::registerTerm(Node n, int effort)
{
  Trace("strings-register") << "TheoryStrings::registerTerm() " << n
                            << ", effort = " << effort << std::endl;
  if (d_registeredTerms.find(n) != d_registeredTerms.end())
  {
    Trace("strings-register") << "...already registered" << std::endl;
    return;
  }
  bool do_register = true;
  TypeNode tn = n.getType();
  if (!tn.isStringLike())
  {
    if (options::stringEagerLen())
    {
      do_register = effort == 0;
    }
    else
    {
      do_register = effort > 0 || n.getKind() != STRING_CONCAT;
    }
  }
  if (!do_register)
  {
    Trace("strings-register") << "...do not register" << std::endl;
    return;
  }
  Trace("strings-register") << "...register" << std::endl;
  d_registeredTerms.insert(n);
  // ensure the type is registered
  registerType(tn);
  TrustNode regTermLem;
  if (tn.isStringLike())
  {
    // register length information:
    //  for variables, split on empty vs positive length
    //  for concat/const/replace, introduce proxy var and state length relation
    regTermLem = getRegisterTermLemma(n);
  }
  else if (n.getKind() != STRING_CONTAINS)
  {
    // we don't send out eager reduction lemma for str.contains currently
    Node eagerRedLemma = eagerReduce(n, &d_skCache, d_alphaCard);
    if (!eagerRedLemma.isNull())
    {
      // if there was an eager reduction, we make the trust node for it
      if (d_epg != nullptr)
      {
        regTermLem = d_epg->mkTrustNode(
            eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
      }
      else
      {
        regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
      }
    }
  }
  if (!regTermLem.isNull())
  {
    Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
                           << std::endl;
    Trace("strings-assert")
        << "(assert " << regTermLem.getNode() << ")" << std::endl;
    d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
  }
}

void TermRegistry::registerType(TypeNode tn)
{
  if (d_registeredTypes.find(tn) != d_registeredTypes.end())
  {
    return;
  }
  d_registeredTypes.insert(tn);
  if (tn.isStringLike())
  {
    // preregister the empty word for the type
    Node emp = Word::mkEmptyWord(tn);
    if (!d_state.hasTerm(emp))
    {
      preRegisterTerm(emp);
    }
  }
}

TrustNode TermRegistry::getRegisterTermLemma(Node n)
{
  Assert(n.getType().isStringLike());
  NodeManager* nm = NodeManager::currentNM();
  // register length information:
  //  for variables, split on empty vs positive length
  //  for concat/const/replace, introduce proxy var and state length relation
  Node lsum;
  if (n.getKind() != STRING_CONCAT && !n.isConst())
  {
    Node lsumb = nm->mkNode(STRING_LENGTH, n);
    lsum = Rewriter::rewrite(lsumb);
    // can register length term if it does not rewrite
    if (lsum == lsumb)
    {
      registerTermAtomic(n, LENGTH_SPLIT);
      return TrustNode::null();
    }
  }
  Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
  Node eq = Rewriter::rewrite(sk.eqNode(n));
  d_proxyVar[n] = sk;
  // If we are introducing a proxy for a constant or concat term, we do not
  // need to send lemmas about its length, since its length is already
  // implied.
  if (n.isConst() || n.getKind() == STRING_CONCAT)
  {
    // do not send length lemma for sk.
    registerTermAtomic(sk, LENGTH_IGNORE);
  }
  Node skl = nm->mkNode(STRING_LENGTH, sk);
  if (n.getKind() == STRING_CONCAT)
  {
    std::vector<Node> nodeVec;
    NodeNodeMap::const_iterator itl;
    for (const Node& nc : n)
    {
      itl = d_proxyVarToLength.find(nc);
      if (itl != d_proxyVarToLength.end())
      {
        nodeVec.push_back(itl->second);
      }
      else
      {
        Node lni = nm->mkNode(STRING_LENGTH, nc);
        nodeVec.push_back(lni);
      }
    }
    lsum = nm->mkNode(PLUS, nodeVec);
    lsum = Rewriter::rewrite(lsum);
  }
  else if (n.isConst())
  {
    lsum = nm->mkConst(Rational(Word::getLength(n)));
  }
  Assert(!lsum.isNull());
  d_proxyVarToLength[sk] = lsum;
  Node ceq = Rewriter::rewrite(skl.eqNode(lsum));

  Node ret = nm->mkNode(AND, eq, ceq);

  // it is a simple rewrite to justify this
  if (d_epg != nullptr)
  {
    return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
  }
  return TrustNode::mkTrustLemma(ret, nullptr);
}

void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
{
  if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
  {
    return;
  }
  d_lengthLemmaTermsCache.insert(n);

  if (s == LENGTH_IGNORE)
  {
    // ignore it
    return;
  }
  std::map<Node, bool> reqPhase;
  TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
  if (!lenLem.isNull())
  {
    Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
                           << std::endl;
    Trace("strings-assert")
        << "(assert " << lenLem.getNode() << ")" << std::endl;
    d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
  }
  for (const std::pair<const Node, bool>& rp : reqPhase)
  {
    d_im->requirePhase(rp.first, rp.second);
  }
}

SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }

const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
{
  return d_functionsTerms;
}

const context::CDHashSet<Node>& TermRegistry::getInputVars() const
{
  return d_inputVars;
}

bool TermRegistry::hasStringCode() const { return d_hasStrCode; }

bool TermRegistry::hasSeqUpdate() const { return d_hasSeqUpdate; }

bool TermRegistry::isHandledUpdate(Node n)
{
  Assert(n.getKind() == STRING_UPDATE || n.getKind() == STRING_SUBSTR);
  NodeManager* nm = NodeManager::currentNM();
  Node lenN = n[2];
  if (n.getKind() == STRING_UPDATE)
  {
    lenN = nm->mkNode(STRING_LENGTH, n[2]);
  }
  Node one = nm->mkConst(Rational(1));
  return d_aent.checkEq(lenN, one);
}

Node TermRegistry::getUpdateBase(Node n)
{
  while (n.getKind() == STRING_UPDATE)
  {
    n = n[0];
  }
  return n;
}

TrustNode TermRegistry::getRegisterTermAtomicLemma(
    Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
{
  if (n.isConst())
  {
    // No need to send length for constant terms. This case may be triggered
    // for cases where the skolem cache automatically replaces a skolem by
    // a constant.
    return TrustNode::null();
  }
  Assert(n.getType().isStringLike());
  NodeManager* nm = NodeManager::currentNM();
  Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
  Node emp = Word::mkEmptyWord(n.getType());
  if (s == LENGTH_GEQ_ONE)
  {
    Node neq_empty = n.eqNode(emp).negate();
    Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
    Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
    Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
                           << std::endl;
    Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
    return TrustNode::mkTrustLemma(len_geq_one, nullptr);
  }

  if (s == LENGTH_ONE)
  {
    Node len_one = n_len.eqNode(d_one);
    Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
                           << std::endl;
    Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
    return TrustNode::mkTrustLemma(len_one, nullptr);
  }
  Assert(s == LENGTH_SPLIT);

  // get the positive length lemma
  Node lenLemma = lengthPositive(n);
  // split whether the string is empty
  Node n_len_eq_z = n_len.eqNode(d_zero);
  Node n_len_eq_z_2 = n.eqNode(emp);
  Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
  Node case_emptyr = Rewriter::rewrite(case_empty);
  if (!case_emptyr.isConst())
  {
    // prefer trying the empty case first
    // notice that requirePhase must only be called on rewritten literals that
    // occur in the CNF stream.
    n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
    Assert(!n_len_eq_z.isConst());
    reqPhase[n_len_eq_z] = true;
    n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
    Assert(!n_len_eq_z_2.isConst());
    reqPhase[n_len_eq_z_2] = true;
  }
  else
  {
    // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
    // n ---> "". Since this method is only called on non-constants n, it must
    // be that n = "" ^ len( n ) = 0 does not rewrite to true.
    Assert(!case_emptyr.getConst<bool>());
  }

  if (d_epg != nullptr)
  {
    return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
  }
  return TrustNode::mkTrustLemma(lenLemma, nullptr);
}

Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
{
  if (n.getNumChildren() == 0)
  {
    Node pn = getProxyVariableFor(n);
    if (pn.isNull())
    {
      return Node::null();
    }
    Node eq = n.eqNode(pn);
    eq = Rewriter::rewrite(eq);
    if (std::find(exp.begin(), exp.end(), eq) == exp.end())
    {
      exp.push_back(eq);
    }
    return pn;
  }
  std::vector<Node> children;
  if (n.getMetaKind() == metakind::PARAMETERIZED)
  {
    children.push_back(n.getOperator());
  }
  for (const Node& nc : n)
  {
    if (n.getType().isRegExp())
    {
      children.push_back(nc);
    }
    else
    {
      Node ns = getSymbolicDefinition(nc, exp);
      if (ns.isNull())
      {
        return Node::null();
      }
      else
      {
        children.push_back(ns);
      }
    }
  }
  return NodeManager::currentNM()->mkNode(n.getKind(), children);
}

Node TermRegistry::getProxyVariableFor(Node n) const
{
  NodeNodeMap::const_iterator it = d_proxyVar.find(n);
  if (it != d_proxyVar.end())
  {
    return (*it).second;
  }
  return Node::null();
}

Node TermRegistry::ensureProxyVariableFor(Node n)
{
  Node proxy = getProxyVariableFor(n);
  if (proxy.isNull())
  {
    registerTerm(n, 0);
    proxy = getProxyVariableFor(n);
  }
  Assert(!proxy.isNull());
  return proxy;
}

void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
{
  if (n.getKind() == AND)
  {
    for (const Node& nc : n)
    {
      removeProxyEqs(nc, unproc);
    }
    return;
  }
  Trace("strings-subs-proxy") << "Input : " << n << std::endl;
  Node ns = Rewriter::rewrite(n);
  if (ns.getKind() == EQUAL)
  {
    for (size_t i = 0; i < 2; i++)
    {
      // determine whether this side has a proxy variable
      if (d_proxyVar.find(ns[i]) != d_proxyVar.end())
      {
        if (getProxyVariableFor(ns[1 - i]) == ns[i])
        {
          Trace("strings-subs-proxy")
              << "...trivial definition via " << ns[i] << std::endl;
          // it is a trivial equality, e.g. between a proxy variable
          // and its definition
          return;
        }
      }
    }
  }
  if (!n.isConst() || !n.getConst<bool>())
  {
    Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
    unproc.push_back(n);
  }
}

}  // 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, Andres Noetzli, Morgan Deters
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 term registry for the theory of strings.
14		*/
15
16		#include "theory/strings/term_registry.h"
17
18		#include "expr/attribute.h"
19		#include "options/smt_options.h"
20		#include "options/strings_options.h"
21		#include "smt/logic_exception.h"
22		#include "theory/rewriter.h"
23		#include "theory/strings/inference_manager.h"
24		#include "theory/strings/theory_strings_utils.h"
25		#include "theory/strings/word.h"
26		#include "util/rational.h"
27		#include "util/string.h"
28
29		using namespace std;
30		using namespace cvc5::context;
31		using namespace cvc5::kind;
32
33		namespace cvc5 {
34		namespace theory {
35		namespace strings {
36
37	15271	TermRegistry::TermRegistry(Env& env,
38		SolverState& s,
39		SequencesStatistics& statistics,
40	15271	ProofNodeManager* pnm)
41		: EnvObj(env),
42		d_state(s),
43		d_im(nullptr),
44		d_statistics(statistics),
45		d_hasStrCode(false),
46		d_hasSeqUpdate(false),
47		d_skCache(env.getRewriter()),
48		d_aent(env.getRewriter()),
49		d_functionsTerms(context()),
50	15271	d_inputVars(userContext()),
51		d_preregisteredTerms(context()),
52	15271	d_registeredTerms(userContext()),
53	15271	d_registeredTypes(userContext()),
54	15271	d_proxyVar(userContext()),
55	15271	d_proxyVarToLength(userContext()),
56	15271	d_lengthLemmaTermsCache(userContext()),
57		d_epg(
58		pnm ? new EagerProofGenerator(
59	10744	pnm, userContext(), "strings::TermRegistry::EagerProofGenerator")
60	117641	: nullptr)
61		{
62	15271	NodeManager* nm = NodeManager::currentNM();
63	15271	d_zero = nm->mkConst(Rational(0));
64	15271	d_one = nm->mkConst(Rational(1));
65	15271	d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
66	15271	Assert(options().strings.stringsAlphaCard <= String::num_codes());
67	15271	d_alphaCard = options().strings.stringsAlphaCard;
68	15271	}
69
70	15266	TermRegistry::~TermRegistry() {}
71
72	36086	uint32_t TermRegistry::getAlphabetCardinality() const { return d_alphaCard; }
73
74	15271	void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
75
76	31892	Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
77		{
78	31892	NodeManager* nm = NodeManager::currentNM();
79	31892	Node lemma;
80	31892	Kind tk = t.getKind();
81	31892	if (tk == STRING_TO_CODE)
82		{
83		// ite( str.len(s)==1, 0 <= str.code(s) < \|A\|, str.code(s)=-1 )
84	3360	Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
85	3360	Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
86		Node code_range =
87		nm->mkNode(AND,
88	3360	nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
89	6720	nm->mkNode(LT, t, nm->mkConst(Rational(alphaCard))));
90	1680	lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
91		}
92	30212	else if (tk == STRING_INDEXOF \|\| tk == STRING_INDEXOF_RE)
93		{
94		// (and
95		// (or (= (f x y n) (- 1)) (>= (f x y n) n))
96		// (<= (f x y n) (str.len x)))
97		//
98		// where f in { str.indexof, str.indexof_re }
99	644	Node l = nm->mkNode(STRING_LENGTH, t[0]);
100	966	lemma = nm->mkNode(
101		AND,
102	1288	nm->mkNode(
103	1288	OR, t.eqNode(nm->mkConst(Rational(-1))), nm->mkNode(GEQ, t, t[2])),
104	966	nm->mkNode(LEQ, t, l));
105		}
106	29890	else if (tk == STRING_STOI)
107		{
108		// (>= (str.to_int x) (- 1))
109	91	lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
110		}
111	29799	else if (tk == STRING_CONTAINS)
112		{
113		// ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
114		Node sk1 =
115	8206	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
116		Node sk2 =
117	8206	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
118	4103	lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
119	4103	lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
120		}
121	31892	return lemma;
122		}
123
124	12077	Node TermRegistry::lengthPositive(Node t)
125		{
126	12077	NodeManager* nm = NodeManager::currentNM();
127	24154	Node zero = nm->mkConst(Rational(0));
128	24154	Node emp = Word::mkEmptyWord(t.getType());
129	24154	Node tlen = nm->mkNode(STRING_LENGTH, t);
130	24154	Node tlenEqZero = tlen.eqNode(zero);
131	24154	Node tEqEmp = t.eqNode(emp);
132	24154	Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
133	24154	Node caseNEmpty = nm->mkNode(GT, tlen, zero);
134		// (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
135	24154	return nm->mkNode(OR, caseEmpty, caseNEmpty);
136		}
137
138	189309	void TermRegistry::preRegisterTerm(TNode n)
139		{
140	189309	if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
141		{
142	92216	return;
143		}
144	188316	eq::EqualityEngine* ee = d_state.getEqualityEngine();
145	188316	d_preregisteredTerms.insert(n);
146	376632	Trace("strings-preregister")
147	188316	<< "TheoryString::preregister : " << n << std::endl;
148		// check for logic exceptions
149	188316	Kind k = n.getKind();
150	188316	if (!options::stringExp())
151		{
152	5489	if (k == STRING_INDEXOF \|\| k == STRING_INDEXOF_RE \|\| k == STRING_ITOS
153	5489	\|\| k == STRING_STOI \|\| k == STRING_REPLACE \|\| k == STRING_SUBSTR
154	5489	\|\| k == STRING_REPLACE_ALL \|\| k == SEQ_NTH \|\| k == STRING_REPLACE_RE
155	5489	\|\| k == STRING_REPLACE_RE_ALL \|\| k == STRING_CONTAINS \|\| k == STRING_LEQ
156	5489	\|\| k == STRING_TOLOWER \|\| k == STRING_TOUPPER \|\| k == STRING_REV
157	5489	\|\| k == STRING_UPDATE)
158		{
159		std::stringstream ss;
160		ss << "Term of kind " << k
161		<< " not supported in default mode, try --strings-exp";
162		throw LogicException(ss.str());
163		}
164		}
165	188316	if (k == EQUAL)
166		{
167	86948	if (n[0].getType().isRegExp())
168		{
169		std::stringstream ss;
170		ss << "Equality between regular expressions is not supported";
171		throw LogicException(ss.str());
172		}
173	86948	ee->addTriggerPredicate(n);
174	86948	return;
175		}
176	101368	else if (k == STRING_IN_REGEXP)
177		{
178	3282	d_im->requirePhase(n, true);
179	3282	ee->addTriggerPredicate(n);
180	3282	ee->addTerm(n[0]);
181	3282	ee->addTerm(n[1]);
182	3282	return;
183		}
184	98086	else if (k == STRING_TO_CODE)
185		{
186	2978	d_hasStrCode = true;
187		}
188	95108	else if (k == SEQ_NTH \|\| k == STRING_UPDATE)
189		{
190	94	d_hasSeqUpdate = true;
191		}
192	95014	else if (k == REGEXP_RANGE)
193		{
194	255	for (const Node& nc : n)
195		{
196	170	if (!nc.isConst())
197		{
198		throw LogicException(
199		"expecting a constant string term in regexp range");
200		}
201	170	if (nc.getConst<String>().size() != 1)
202		{
203		throw LogicException(
204		"expecting a single constant string term in regexp range");
205		}
206		}
207		}
208	98086	registerTerm(n, 0);
209	196172	TypeNode tn = n.getType();
210	98086	if (tn.isRegExp() && n.isVar())
211		{
212		std::stringstream ss;
213		ss << "Regular expression variables are not supported.";
214		throw LogicException(ss.str());
215		}
216	98086	if (tn.isString()) // string-only
217		{
218		// all characters of constants should fall in the alphabet
219	49686	if (n.isConst())
220		{
221	8576	std::vector<unsigned> vec = n.getConst<String>().getVec();
222	18258	for (unsigned u : vec)
223		{
224	13970	if (u >= d_alphaCard)
225		{
226		std::stringstream ss;
227		ss << "Characters in string \"" << n
228		<< "\" are outside of the given alphabet.";
229		throw LogicException(ss.str());
230		}
231		}
232		}
233	49686	ee->addTerm(n);
234		}
235	48400	else if (tn.isBoolean())
236		{
237		// All kinds that we do congruence over that may return a Boolean go here
238	1933	if (k == STRING_CONTAINS \|\| k == STRING_LEQ \|\| k == SEQ_NTH)
239		{
240		// Get triggered for both equal and dis-equal
241	1927	ee->addTriggerPredicate(n);
242		}
243		}
244		else
245		{
246		// Function applications/predicates
247	46467	ee->addTerm(n);
248		}
249		// Set d_functionsTerms stores all function applications that are
250		// relevant to theory combination. Notice that this is a subset of
251		// the applications whose kinds are function kinds in the equality
252		// engine. This means it does not include applications of operators
253		// like re.++, which is not a function kind in the equality engine.
254		// Concatenation terms do not need to be considered here because
255		// their arguments have string type and do not introduce any shared
256		// terms.
257	256463	if (n.hasOperator() && ee->isFunctionKind(k)
258	154502	&& kindToTheoryId(k) == THEORY_STRINGS && k != STRING_CONCAT)
259		{
260	45274	d_functionsTerms.push_back(n);
261		}
262	98086	if (options::stringFMF())
263		{
264	15190	if (tn.isStringLike())
265		{
266		// Our decision strategy will minimize the length of this term if it is a
267		// variable but not an internally generated Skolem, or a term that does
268		// not belong to this theory.
269	11124	if (n.isVar() ? !d_skCache.isSkolem(n)
270	3238	: kindToTheoryId(k) != THEORY_STRINGS)
271		{
272	518	d_inputVars.insert(n);
273	518	Trace("strings-preregister") << "input variable: " << n << std::endl;
274		}
275		}
276		}
277		}
278
279	211560	void TermRegistry::registerTerm(Node n, int effort)
280		{
281	423120	Trace("strings-register") << "TheoryStrings::registerTerm() " << n
282	211560	<< ", effort = " << effort << std::endl;
283	211560	if (d_registeredTerms.find(n) != d_registeredTerms.end())
284		{
285	151569	Trace("strings-register") << "...already registered" << std::endl;
286	303138	return;
287		}
288	59991	bool do_register = true;
289	119982	TypeNode tn = n.getType();
290	59991	if (!tn.isStringLike())
291		{
292	28820	if (options::stringEagerLen())
293		{
294	28820	do_register = effort == 0;
295		}
296		else
297		{
298		do_register = effort > 0 \|\| n.getKind() != STRING_CONCAT;
299		}
300		}
301	59991	if (!do_register)
302		{
303		Trace("strings-register") << "...do not register" << std::endl;
304		return;
305		}
306	59991	Trace("strings-register") << "...register" << std::endl;
307	59991	d_registeredTerms.insert(n);
308		// ensure the type is registered
309	59991	registerType(tn);
310	119982	TrustNode regTermLem;
311	59991	if (tn.isStringLike())
312		{
313		// register length information:
314		// for variables, split on empty vs positive length
315		// for concat/const/replace, introduce proxy var and state length relation
316	31171	regTermLem = getRegisterTermLemma(n);
317		}
318	28820	else if (n.getKind() != STRING_CONTAINS)
319		{
320		// we don't send out eager reduction lemma for str.contains currently
321	55460	Node eagerRedLemma = eagerReduce(n, &d_skCache, d_alphaCard);
322	27730	if (!eagerRedLemma.isNull())
323		{
324		// if there was an eager reduction, we make the trust node for it
325	2034	if (d_epg != nullptr)
326		{
327	664	regTermLem = d_epg->mkTrustNode(
328	332	eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
329		}
330		else
331		{
332	1702	regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
333		}
334		}
335		}
336	59991	if (!regTermLem.isNull())
337		{
338	23576	Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
339	11788	<< std::endl;
340	23576	Trace("strings-assert")
341	11788	<< "(assert " << regTermLem.getNode() << ")" << std::endl;
342	11788	d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
343		}
344		}
345
346	59991	void TermRegistry::registerType(TypeNode tn)
347		{
348	59991	if (d_registeredTypes.find(tn) != d_registeredTypes.end())
349		{
350	57489	return;
351		}
352	2502	d_registeredTypes.insert(tn);
353	2502	if (tn.isStringLike())
354		{
355		// preregister the empty word for the type
356	1986	Node emp = Word::mkEmptyWord(tn);
357	993	if (!d_state.hasTerm(emp))
358		{
359	993	preRegisterTerm(emp);
360		}
361		}
362		}
363
364	31171	TrustNode TermRegistry::getRegisterTermLemma(Node n)
365		{
366	31171	Assert(n.getType().isStringLike());
367	31171	NodeManager* nm = NodeManager::currentNM();
368		// register length information:
369		// for variables, split on empty vs positive length
370		// for concat/const/replace, introduce proxy var and state length relation
371	62342	Node lsum;
372	31171	if (n.getKind() != STRING_CONCAT && !n.isConst())
373		{
374	21757	Node lsumb = nm->mkNode(STRING_LENGTH, n);
375	21587	lsum = Rewriter::rewrite(lsumb);
376		// can register length term if it does not rewrite
377	21587	if (lsum == lsumb)
378		{
379	21417	registerTermAtomic(n, LENGTH_SPLIT);
380	21417	return TrustNode::null();
381		}
382		}
383	19508	Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
384	19508	Node eq = Rewriter::rewrite(sk.eqNode(n));
385	9754	d_proxyVar[n] = sk;
386		// If we are introducing a proxy for a constant or concat term, we do not
387		// need to send lemmas about its length, since its length is already
388		// implied.
389	9754	if (n.isConst() \|\| n.getKind() == STRING_CONCAT)
390		{
391		// do not send length lemma for sk.
392	9584	registerTermAtomic(sk, LENGTH_IGNORE);
393		}
394	19508	Node skl = nm->mkNode(STRING_LENGTH, sk);
395	9754	if (n.getKind() == STRING_CONCAT)
396		{
397	11972	std::vector<Node> nodeVec;
398	5986	NodeNodeMap::const_iterator itl;
399	20511	for (const Node& nc : n)
400		{
401	14525	itl = d_proxyVarToLength.find(nc);
402	14525	if (itl != d_proxyVarToLength.end())
403		{
404	64	nodeVec.push_back(itl->second);
405		}
406		else
407		{
408	28922	Node lni = nm->mkNode(STRING_LENGTH, nc);
409	14461	nodeVec.push_back(lni);
410		}
411		}
412	5986	lsum = nm->mkNode(PLUS, nodeVec);
413	5986	lsum = Rewriter::rewrite(lsum);
414		}
415	3768	else if (n.isConst())
416		{
417	3598	lsum = nm->mkConst(Rational(Word::getLength(n)));
418		}
419	9754	Assert(!lsum.isNull());
420	9754	d_proxyVarToLength[sk] = lsum;
421	19508	Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
422
423	19508	Node ret = nm->mkNode(AND, eq, ceq);
424
425		// it is a simple rewrite to justify this
426	9754	if (d_epg != nullptr)
427		{
428	1357	return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
429		}
430	8397	return TrustNode::mkTrustLemma(ret, nullptr);
431		}
432
433	32426	void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
434		{
435	32426	if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
436		{
437	31570	return;
438		}
439	21421	d_lengthLemmaTermsCache.insert(n);
440
441	21421	if (s == LENGTH_IGNORE)
442		{
443		// ignore it
444	9560	return;
445		}
446	23722	std::map<Node, bool> reqPhase;
447	23722	TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
448	11861	if (!lenLem.isNull())
449		{
450	23714	Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
451	11857	<< std::endl;
452	23714	Trace("strings-assert")
453	11857	<< "(assert " << lenLem.getNode() << ")" << std::endl;
454	11857	d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
455		}
456	35543	for (const std::pair<const Node, bool>& rp : reqPhase)
457		{
458	23682	d_im->requirePhase(rp.first, rp.second);
459		}
460		}
461
462	46179	SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
463
464	9452	const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
465		{
466	9452	return d_functionsTerms;
467		}
468
469	78	const context::CDHashSet<Node>& TermRegistry::getInputVars() const
470		{
471	78	return d_inputVars;
472		}
473
474	14502	bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
475
476		bool TermRegistry::hasSeqUpdate() const { return d_hasSeqUpdate; }
477
478		bool TermRegistry::isHandledUpdate(Node n)
479		{
480		Assert(n.getKind() == STRING_UPDATE \|\| n.getKind() == STRING_SUBSTR);
481		NodeManager* nm = NodeManager::currentNM();
482		Node lenN = n[2];
483		if (n.getKind() == STRING_UPDATE)
484		{
485		lenN = nm->mkNode(STRING_LENGTH, n[2]);
486		}
487		Node one = nm->mkConst(Rational(1));
488		return d_aent.checkEq(lenN, one);
489		}
490
491		Node TermRegistry::getUpdateBase(Node n)
492		{
493		while (n.getKind() == STRING_UPDATE)
494		{
495		n = n[0];
496		}
497		return n;
498		}
499
500	11861	TrustNode TermRegistry::getRegisterTermAtomicLemma(
501		Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
502		{
503	11861	if (n.isConst())
504		{
505		// No need to send length for constant terms. This case may be triggered
506		// for cases where the skolem cache automatically replaces a skolem by
507		// a constant.
508	4	return TrustNode::null();
509		}
510	11857	Assert(n.getType().isStringLike());
511	11857	NodeManager* nm = NodeManager::currentNM();
512	23714	Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
513	23714	Node emp = Word::mkEmptyWord(n.getType());
514	11857	if (s == LENGTH_GEQ_ONE)
515		{
516	32	Node neq_empty = n.eqNode(emp).negate();
517	32	Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
518	32	Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
519	32	Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
520	16	<< std::endl;
521	16	Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
522	16	return TrustNode::mkTrustLemma(len_geq_one, nullptr);
523		}
524
525	11841	if (s == LENGTH_ONE)
526		{
527		Node len_one = n_len.eqNode(d_one);
528		Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
529		<< std::endl;
530		Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
531		return TrustNode::mkTrustLemma(len_one, nullptr);
532		}
533	11841	Assert(s == LENGTH_SPLIT);
534
535		// get the positive length lemma
536	23682	Node lenLemma = lengthPositive(n);
537		// split whether the string is empty
538	23682	Node n_len_eq_z = n_len.eqNode(d_zero);
539	23682	Node n_len_eq_z_2 = n.eqNode(emp);
540	23682	Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
541	23682	Node case_emptyr = Rewriter::rewrite(case_empty);
542	11841	if (!case_emptyr.isConst())
543		{
544		// prefer trying the empty case first
545		// notice that requirePhase must only be called on rewritten literals that
546		// occur in the CNF stream.
547	11841	n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
548	11841	Assert(!n_len_eq_z.isConst());
549	11841	reqPhase[n_len_eq_z] = true;
550	11841	n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
551	11841	Assert(!n_len_eq_z_2.isConst());
552	11841	reqPhase[n_len_eq_z_2] = true;
553		}
554		else
555		{
556		// If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
557		// n ---> "". Since this method is only called on non-constants n, it must
558		// be that n = "" ^ len( n ) = 0 does not rewrite to true.
559		Assert(!case_emptyr.getConst<bool>());
560		}
561
562	11841	if (d_epg != nullptr)
563		{
564	1594	return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
565		}
566	10247	return TrustNode::mkTrustLemma(lenLemma, nullptr);
567		}
568
569	390716	Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
570		{
571	390716	if (n.getNumChildren() == 0)
572		{
573	352078	Node pn = getProxyVariableFor(n);
574	176039	if (pn.isNull())
575		{
576	19727	return Node::null();
577		}
578	312624	Node eq = n.eqNode(pn);
579	156312	eq = Rewriter::rewrite(eq);
580	156312	if (std::find(exp.begin(), exp.end(), eq) == exp.end())
581		{
582	152975	exp.push_back(eq);
583		}
584	156312	return pn;
585		}
586	429354	std::vector<Node> children;
587	214677	if (n.getMetaKind() == metakind::PARAMETERIZED)
588		{
589	42	children.push_back(n.getOperator());
590		}
591	566474	for (const Node& nc : n)
592		{
593	379188	if (n.getType().isRegExp())
594		{
595	131242	children.push_back(nc);
596		}
597		else
598		{
599	468501	Node ns = getSymbolicDefinition(nc, exp);
600	247946	if (ns.isNull())
601		{
602	27391	return Node::null();
603		}
604		else
605		{
606	220555	children.push_back(ns);
607		}
608		}
609		}
610	187286	return NodeManager::currentNM()->mkNode(n.getKind(), children);
611		}
612
613	268922	Node TermRegistry::getProxyVariableFor(Node n) const
614		{
615	268922	NodeNodeMap::const_iterator it = d_proxyVar.find(n);
616	268922	if (it != d_proxyVar.end())
617		{
618	195160	return (*it).second;
619		}
620	73762	return Node::null();
621		}
622
623	7624	Node TermRegistry::ensureProxyVariableFor(Node n)
624		{
625	7624	Node proxy = getProxyVariableFor(n);
626	7624	if (proxy.isNull())
627		{
628	292	registerTerm(n, 0);
629	292	proxy = getProxyVariableFor(n);
630		}
631	7624	Assert(!proxy.isNull());
632	7624	return proxy;
633		}
634
635	89888	void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
636		{
637	89888	if (n.getKind() == AND)
638		{
639	2846	for (const Node& nc : n)
640		{
641	2255	removeProxyEqs(nc, unproc);
642		}
643	1182	return;
644		}
645	89297	Trace("strings-subs-proxy") << "Input : " << n << std::endl;
646	178594	Node ns = Rewriter::rewrite(n);
647	89297	if (ns.getKind() == EQUAL)
648		{
649	267249	for (size_t i = 0; i < 2; i++)
650		{
651		// determine whether this side has a proxy variable
652	178166	if (d_proxyVar.find(ns[i]) != d_proxyVar.end())
653		{
654	84967	if (getProxyVariableFor(ns[1 - i]) == ns[i])
655		{
656		Trace("strings-subs-proxy")
657		<< "...trivial definition via " << ns[i] << std::endl;
658		// it is a trivial equality, e.g. between a proxy variable
659		// and its definition
660		return;
661		}
662		}
663		}
664		}
665	89297	if (!n.isConst() \|\| !n.getConst<bool>())
666		{
667	89287	Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
668	89287	unproc.push_back(n);
669		}
670		}
671
672		} // namespace strings
673		} // namespace theory
674	31125	} // namespace cvc5