Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/term_registry.cpp	Lines:	279	308	90.6 %
Date:	2021-05-24	Branches:	670	1418	47.2 %


/******************************************************************************
 * 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"

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

namespace cvc5 {
namespace theory {
namespace strings {

struct StringsProxyVarAttributeId
{
};
typedef expr::Attribute<StringsProxyVarAttributeId, bool>
    StringsProxyVarAttribute;

TermRegistry::TermRegistry(SolverState& s,
                           SequencesStatistics& statistics,
                           ProofNodeManager* pnm)
    : d_state(s),
      d_im(nullptr),
      d_statistics(statistics),
      d_hasStrCode(false),
      d_functionsTerms(s.getSatContext()),
      d_inputVars(s.getUserContext()),
      d_preregisteredTerms(s.getSatContext()),
      d_registeredTerms(s.getUserContext()),
      d_registeredTypes(s.getUserContext()),
      d_proxyVar(s.getUserContext()),
      d_lengthLemmaTermsCache(s.getUserContext()),
      d_epg(pnm ? new EagerProofGenerator(
                      pnm,
                      s.getUserContext(),
                      "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));
  d_cardSize = utils::getAlphabetCardinality();
}

TermRegistry::~TermRegistry() {}

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

Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
{
  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(utils::getAlphabetCardinality()))));
    lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
  }
  else if (tk == STRING_STRIDOF)
  {
    // (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len
    // x)))
    Node l = nm->mkNode(STRING_LENGTH, t[0]);
    lemma = nm->mkNode(AND,
                       nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
                       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_STRCTN)
  {
    // 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_STRIDOF || k == STRING_ITOS || k == STRING_STOI
        || k == STRING_STRREPL || k == STRING_SUBSTR || k == STRING_STRREPLALL
        || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL
        || k == STRING_STRCTN || 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 == 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_cardSize)
        {
          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_STRCTN || 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) && 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_STRCTN)
  {
    // we don't send out eager reduction lemma for str.contains currently
    Node eagerRedLemma = eagerReduce(n, &d_skCache);
    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");
  StringsProxyVarAttribute spva;
  sk.setAttribute(spva, true);
  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;
    for (const Node& nc : n)
    {
      if (nc.getAttribute(StringsProxyVarAttribute()))
      {
        Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end());
        nodeVec.push_back(d_proxyVarToLength[nc]);
      }
      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; }

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 (ns[i].getAttribute(StringsProxyVarAttribute()))
      {
        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
27		using namespace std;
28		using namespace cvc5::context;
29		using namespace cvc5::kind;
30
31		namespace cvc5 {
32		namespace theory {
33		namespace strings {
34
35		struct StringsProxyVarAttributeId
36		{
37		};
38		typedef expr::Attribute<StringsProxyVarAttributeId, bool>
39		StringsProxyVarAttribute;
40
41	9459	TermRegistry::TermRegistry(SolverState& s,
42		SequencesStatistics& statistics,
43	9459	ProofNodeManager* pnm)
44		: d_state(s),
45		d_im(nullptr),
46		d_statistics(statistics),
47		d_hasStrCode(false),
48		d_functionsTerms(s.getSatContext()),
49	9459	d_inputVars(s.getUserContext()),
50		d_preregisteredTerms(s.getSatContext()),
51	9459	d_registeredTerms(s.getUserContext()),
52	9459	d_registeredTypes(s.getUserContext()),
53	9459	d_proxyVar(s.getUserContext()),
54	9459	d_lengthLemmaTermsCache(s.getUserContext()),
55		d_epg(pnm ? new EagerProofGenerator(
56		pnm,
57	1192	s.getUserContext(),
58	1192	"strings::TermRegistry::EagerProofGenerator")
59	59138	: nullptr)
60		{
61	9459	NodeManager* nm = NodeManager::currentNM();
62	9459	d_zero = nm->mkConst(Rational(0));
63	9459	d_one = nm->mkConst(Rational(1));
64	9459	d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
65	9459	d_cardSize = utils::getAlphabetCardinality();
66	9459	}
67
68	9459	TermRegistry::~TermRegistry() {}
69
70	9459	void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
71
72	20302	Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
73		{
74	20302	NodeManager* nm = NodeManager::currentNM();
75	20302	Node lemma;
76	20302	Kind tk = t.getKind();
77	20302	if (tk == STRING_TO_CODE)
78		{
79		// ite( str.len(s)==1, 0 <= str.code(s) < \|A\|, str.code(s)=-1 )
80	2384	Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
81	2384	Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
82		Node code_range = nm->mkNode(
83		AND,
84	2384	nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
85	2384	nm->mkNode(
86	7152	LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
87	1192	lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
88		}
89	19110	else if (tk == STRING_STRIDOF)
90		{
91		// (and (>= (str.indexof x y n) (- 1)) (<= (str.indexof x y n) (str.len
92		// x)))
93	320	Node l = nm->mkNode(STRING_LENGTH, t[0]);
94	480	lemma = nm->mkNode(AND,
95	320	nm->mkNode(GEQ, t, nm->mkConst(Rational(-1))),
96	320	nm->mkNode(LEQ, t, l));
97		}
98	18950	else if (tk == STRING_STOI)
99		{
100		// (>= (str.to_int x) (- 1))
101	53	lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
102		}
103	18897	else if (tk == STRING_STRCTN)
104		{
105		// ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
106		Node sk1 =
107	3914	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
108		Node sk2 =
109	3914	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
110	1957	lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
111	1957	lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
112		}
113	20302	return lemma;
114		}
115
116	8445	Node TermRegistry::lengthPositive(Node t)
117		{
118	8445	NodeManager* nm = NodeManager::currentNM();
119	16890	Node zero = nm->mkConst(Rational(0));
120	16890	Node emp = Word::mkEmptyWord(t.getType());
121	16890	Node tlen = nm->mkNode(STRING_LENGTH, t);
122	16890	Node tlenEqZero = tlen.eqNode(zero);
123	16890	Node tEqEmp = t.eqNode(emp);
124	16890	Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
125	16890	Node caseNEmpty = nm->mkNode(GT, tlen, zero);
126		// (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
127	16890	return nm->mkNode(OR, caseEmpty, caseNEmpty);
128		}
129
130	105323	void TermRegistry::preRegisterTerm(TNode n)
131		{
132	105323	if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
133		{
134	42780	return;
135		}
136	104554	eq::EqualityEngine* ee = d_state.getEqualityEngine();
137	104554	d_preregisteredTerms.insert(n);
138	209108	Trace("strings-preregister")
139	104554	<< "TheoryString::preregister : " << n << std::endl;
140		// check for logic exceptions
141	104554	Kind k = n.getKind();
142	104554	if (!options::stringExp())
143		{
144	2818	if (k == STRING_STRIDOF \|\| k == STRING_ITOS \|\| k == STRING_STOI
145	2818	\|\| k == STRING_STRREPL \|\| k == STRING_SUBSTR \|\| k == STRING_STRREPLALL
146	2818	\|\| k == SEQ_NTH \|\| k == STRING_REPLACE_RE \|\| k == STRING_REPLACE_RE_ALL
147	2818	\|\| k == STRING_STRCTN \|\| k == STRING_LEQ \|\| k == STRING_TOLOWER
148	2818	\|\| k == STRING_TOUPPER \|\| k == STRING_REV \|\| k == STRING_UPDATE)
149		{
150		std::stringstream ss;
151		ss << "Term of kind " << k
152		<< " not supported in default mode, try --strings-exp";
153		throw LogicException(ss.str());
154		}
155		}
156	104554	if (k == EQUAL)
157		{
158	39176	if (n[0].getType().isRegExp())
159		{
160		std::stringstream ss;
161		ss << "Equality between regular expressions is not supported";
162		throw LogicException(ss.str());
163		}
164	39176	ee->addTriggerPredicate(n);
165	39176	return;
166		}
167	65378	else if (k == STRING_IN_REGEXP)
168		{
169	2066	d_im->requirePhase(n, true);
170	2066	ee->addTriggerPredicate(n);
171	2066	ee->addTerm(n[0]);
172	2066	ee->addTerm(n[1]);
173	2066	return;
174		}
175	63312	else if (k == STRING_TO_CODE)
176		{
177	1930	d_hasStrCode = true;
178		}
179	61382	else if (k == REGEXP_RANGE)
180		{
181	180	for (const Node& nc : n)
182		{
183	120	if (!nc.isConst())
184		{
185		throw LogicException(
186		"expecting a constant string term in regexp range");
187		}
188	120	if (nc.getConst<String>().size() != 1)
189		{
190		throw LogicException(
191		"expecting a single constant string term in regexp range");
192		}
193		}
194		}
195	63312	registerTerm(n, 0);
196	126624	TypeNode tn = n.getType();
197	63312	if (tn.isRegExp() && n.isVar())
198		{
199		std::stringstream ss;
200		ss << "Regular expression variables are not supported.";
201		throw LogicException(ss.str());
202		}
203	63312	if (tn.isString()) // string-only
204		{
205		// all characters of constants should fall in the alphabet
206	31713	if (n.isConst())
207		{
208	6434	std::vector<unsigned> vec = n.getConst<String>().getVec();
209	11359	for (unsigned u : vec)
210		{
211	8142	if (u >= d_cardSize)
212		{
213		std::stringstream ss;
214		ss << "Characters in string \"" << n
215		<< "\" are outside of the given alphabet.";
216		throw LogicException(ss.str());
217		}
218		}
219		}
220	31713	ee->addTerm(n);
221		}
222	31599	else if (tn.isBoolean())
223		{
224		// All kinds that we do congruence over that may return a Boolean go here
225	1740	if (k==STRING_STRCTN \|\| k == STRING_LEQ \|\| k == SEQ_NTH)
226		{
227		// Get triggered for both equal and dis-equal
228	1734	ee->addTriggerPredicate(n);
229		}
230		}
231		else
232		{
233		// Function applications/predicates
234	29859	ee->addTerm(n);
235		}
236		// Set d_functionsTerms stores all function applications that are
237		// relevant to theory combination. Notice that this is a subset of
238		// the applications whose kinds are function kinds in the equality
239		// engine. This means it does not include applications of operators
240		// like re.++, which is not a function kind in the equality engine.
241		// Concatenation terms do not need to be considered here because
242		// their arguments have string type and do not introduce any shared
243		// terms.
244	63312	if (n.hasOperator() && ee->isFunctionKind(k) && k != STRING_CONCAT)
245		{
246	29475	d_functionsTerms.push_back(n);
247		}
248	63312	if (options::stringFMF())
249		{
250	12382	if (tn.isStringLike())
251		{
252		// Our decision strategy will minimize the length of this term if it is a
253		// variable but not an internally generated Skolem, or a term that does
254		// not belong to this theory.
255	9080	if (n.isVar() ? !d_skCache.isSkolem(n)
256	2610	: kindToTheoryId(k) != THEORY_STRINGS)
257		{
258	332	d_inputVars.insert(n);
259	332	Trace("strings-preregister") << "input variable: " << n << std::endl;
260		}
261		}
262		}
263		}
264
265	111640	void TermRegistry::registerTerm(Node n, int effort)
266		{
267	223280	Trace("strings-register") << "TheoryStrings::registerTerm() " << n
268	111640	<< ", effort = " << effort << std::endl;
269	111640	if (d_registeredTerms.find(n) != d_registeredTerms.end())
270		{
271	71558	Trace("strings-register") << "...already registered" << std::endl;
272	143116	return;
273		}
274	40082	bool do_register = true;
275	80164	TypeNode tn = n.getType();
276	40082	if (!tn.isStringLike())
277		{
278	19203	if (options::stringEagerLen())
279		{
280	19203	do_register = effort == 0;
281		}
282		else
283		{
284		do_register = effort > 0 \|\| n.getKind() != STRING_CONCAT;
285		}
286		}
287	40082	if (!do_register)
288		{
289		Trace("strings-register") << "...do not register" << std::endl;
290		return;
291		}
292	40082	Trace("strings-register") << "...register" << std::endl;
293	40082	d_registeredTerms.insert(n);
294		// ensure the type is registered
295	40082	registerType(tn);
296	80164	TrustNode regTermLem;
297	40082	if (tn.isStringLike())
298		{
299		// register length information:
300		// for variables, split on empty vs positive length
301		// for concat/const/replace, introduce proxy var and state length relation
302	20879	regTermLem = getRegisterTermLemma(n);
303		}
304	19203	else if (n.getKind() != STRING_STRCTN)
305		{
306		// we don't send out eager reduction lemma for str.contains currently
307	36454	Node eagerRedLemma = eagerReduce(n, &d_skCache);
308	18227	if (!eagerRedLemma.isNull())
309		{
310		// if there was an eager reduction, we make the trust node for it
311	1287	if (d_epg != nullptr)
312		{
313	236	regTermLem = d_epg->mkTrustNode(
314	118	eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
315		}
316		else
317		{
318	1169	regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
319		}
320		}
321		}
322	40082	if (!regTermLem.isNull())
323		{
324	15870	Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
325	7935	<< std::endl;
326	15870	Trace("strings-assert")
327	7935	<< "(assert " << regTermLem.getNode() << ")" << std::endl;
328	7935	d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
329		}
330		}
331
332	40082	void TermRegistry::registerType(TypeNode tn)
333		{
334	40082	if (d_registeredTypes.find(tn) != d_registeredTypes.end())
335		{
336	38168	return;
337		}
338	1914	d_registeredTypes.insert(tn);
339	1914	if (tn.isStringLike())
340		{
341		// preregister the empty word for the type
342	1538	Node emp = Word::mkEmptyWord(tn);
343	769	if (!d_state.hasTerm(emp))
344		{
345	769	preRegisterTerm(emp);
346		}
347		}
348		}
349
350	20879	TrustNode TermRegistry::getRegisterTermLemma(Node n)
351		{
352	20879	Assert(n.getType().isStringLike());
353	20879	NodeManager* nm = NodeManager::currentNM();
354		// register length information:
355		// for variables, split on empty vs positive length
356		// for concat/const/replace, introduce proxy var and state length relation
357	41758	Node lsum;
358	20879	if (n.getKind() != STRING_CONCAT && !n.isConst())
359		{
360	14499	Node lsumb = nm->mkNode(STRING_LENGTH, n);
361	14365	lsum = Rewriter::rewrite(lsumb);
362		// can register length term if it does not rewrite
363	14365	if (lsum == lsumb)
364		{
365	14231	registerTermAtomic(n, LENGTH_SPLIT);
366	14231	return TrustNode::null();
367		}
368		}
369	13296	Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
370		StringsProxyVarAttribute spva;
371	6648	sk.setAttribute(spva, true);
372	13296	Node eq = Rewriter::rewrite(sk.eqNode(n));
373	6648	d_proxyVar[n] = sk;
374		// If we are introducing a proxy for a constant or concat term, we do not
375		// need to send lemmas about its length, since its length is already
376		// implied.
377	6648	if (n.isConst() \|\| n.getKind() == STRING_CONCAT)
378		{
379		// do not send length lemma for sk.
380	6514	registerTermAtomic(sk, LENGTH_IGNORE);
381		}
382	13296	Node skl = nm->mkNode(STRING_LENGTH, sk);
383	6648	if (n.getKind() == STRING_CONCAT)
384		{
385	7470	std::vector<Node> nodeVec;
386	12684	for (const Node& nc : n)
387		{
388	8949	if (nc.getAttribute(StringsProxyVarAttribute()))
389		{
390		Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end());
391		nodeVec.push_back(d_proxyVarToLength[nc]);
392		}
393		else
394		{
395	17898	Node lni = nm->mkNode(STRING_LENGTH, nc);
396	8949	nodeVec.push_back(lni);
397		}
398		}
399	3735	lsum = nm->mkNode(PLUS, nodeVec);
400	3735	lsum = Rewriter::rewrite(lsum);
401		}
402	2913	else if (n.isConst())
403		{
404	2779	lsum = nm->mkConst(Rational(Word::getLength(n)));
405		}
406	6648	Assert(!lsum.isNull());
407	6648	d_proxyVarToLength[sk] = lsum;
408	13296	Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
409
410	13296	Node ret = nm->mkNode(AND, eq, ceq);
411
412		// it is a simple rewrite to justify this
413	6648	if (d_epg != nullptr)
414		{
415	659	return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
416		}
417	5989	return TrustNode::mkTrustLemma(ret, nullptr);
418		}
419
420	21575	void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
421		{
422	21575	if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
423		{
424	21192	return;
425		}
426	14235	d_lengthLemmaTermsCache.insert(n);
427
428	14235	if (s == LENGTH_IGNORE)
429		{
430		// ignore it
431	6512	return;
432		}
433	15446	std::map<Node, bool> reqPhase;
434	15446	TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
435	7723	if (!lenLem.isNull())
436		{
437	15438	Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
438	7719	<< std::endl;
439	15438	Trace("strings-assert")
440	7719	<< "(assert " << lenLem.getNode() << ")" << std::endl;
441	7719	d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
442		}
443	22973	for (const std::pair<const Node, bool>& rp : reqPhase)
444		{
445	15250	d_im->requirePhase(rp.first, rp.second);
446		}
447		}
448
449	27656	SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
450
451	6484	const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
452		{
453	6484	return d_functionsTerms;
454		}
455
456	74	const context::CDHashSet<Node>& TermRegistry::getInputVars() const
457		{
458	74	return d_inputVars;
459		}
460
461	10105	bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
462
463	7723	TrustNode TermRegistry::getRegisterTermAtomicLemma(
464		Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
465		{
466	7723	if (n.isConst())
467		{
468		// No need to send length for constant terms. This case may be triggered
469		// for cases where the skolem cache automatically replaces a skolem by
470		// a constant.
471	4	return TrustNode::null();
472		}
473	7719	Assert(n.getType().isStringLike());
474	7719	NodeManager* nm = NodeManager::currentNM();
475	15438	Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
476	15438	Node emp = Word::mkEmptyWord(n.getType());
477	7719	if (s == LENGTH_GEQ_ONE)
478		{
479	16	Node neq_empty = n.eqNode(emp).negate();
480	16	Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
481	16	Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
482	16	Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
483	8	<< std::endl;
484	8	Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
485	8	return TrustNode::mkTrustLemma(len_geq_one, nullptr);
486		}
487
488	7711	if (s == LENGTH_ONE)
489		{
490		Node len_one = n_len.eqNode(d_one);
491		Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
492		<< std::endl;
493		Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
494		return TrustNode::mkTrustLemma(len_one, nullptr);
495		}
496	7711	Assert(s == LENGTH_SPLIT);
497
498		// get the positive length lemma
499	15422	Node lenLemma = lengthPositive(n);
500		// split whether the string is empty
501	15422	Node n_len_eq_z = n_len.eqNode(d_zero);
502	15422	Node n_len_eq_z_2 = n.eqNode(emp);
503	15422	Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
504	15422	Node case_emptyr = Rewriter::rewrite(case_empty);
505	7711	if (!case_emptyr.isConst())
506		{
507		// prefer trying the empty case first
508		// notice that requirePhase must only be called on rewritten literals that
509		// occur in the CNF stream.
510	7625	n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
511	7625	Assert(!n_len_eq_z.isConst());
512	7625	reqPhase[n_len_eq_z] = true;
513	7625	n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
514	7625	Assert(!n_len_eq_z_2.isConst());
515	7625	reqPhase[n_len_eq_z_2] = true;
516		}
517		else
518		{
519		// If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
520		// n ---> "". Since this method is only called on non-constants n, it must
521		// be that n = "" ^ len( n ) = 0 does not rewrite to true.
522	86	Assert(!case_emptyr.getConst<bool>());
523		}
524
525	7711	if (d_epg != nullptr)
526		{
527	734	return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
528		}
529	6977	return TrustNode::mkTrustLemma(lenLemma, nullptr);
530		}
531
532	167754	Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
533		{
534	167754	if (n.getNumChildren() == 0)
535		{
536	167044	Node pn = getProxyVariableFor(n);
537	83522	if (pn.isNull())
538		{
539	10804	return Node::null();
540		}
541	145436	Node eq = n.eqNode(pn);
542	72718	eq = Rewriter::rewrite(eq);
543	72718	if (std::find(exp.begin(), exp.end(), eq) == exp.end())
544		{
545	70623	exp.push_back(eq);
546		}
547	72718	return pn;
548		}
549	168464	std::vector<Node> children;
550	84232	if (n.getMetaKind() == metakind::PARAMETERIZED)
551		{
552	36	children.push_back(n.getOperator());
553		}
554	202562	for (const Node& nc : n)
555		{
556	132175	if (n.getType().isRegExp())
557		{
558	27475	children.push_back(nc);
559		}
560		else
561		{
562	195555	Node ns = getSymbolicDefinition(nc, exp);
563	104700	if (ns.isNull())
564		{
565	13845	return Node::null();
566		}
567		else
568		{
569	90855	children.push_back(ns);
570		}
571		}
572		}
573	70387	return NodeManager::currentNM()->mkNode(n.getKind(), children);
574		}
575
576	88040	Node TermRegistry::getProxyVariableFor(Node n) const
577		{
578	88040	NodeNodeMap::const_iterator it = d_proxyVar.find(n);
579	88040	if (it != d_proxyVar.end())
580		{
581	77062	return (*it).second;
582		}
583	10978	return Node::null();
584		}
585
586	4342	Node TermRegistry::ensureProxyVariableFor(Node n)
587		{
588	4342	Node proxy = getProxyVariableFor(n);
589	4342	if (proxy.isNull())
590		{
591	174	registerTerm(n, 0);
592	174	proxy = getProxyVariableFor(n);
593		}
594	4342	Assert(!proxy.isNull());
595	4342	return proxy;
596		}
597
598	39393	void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
599		{
600	39393	if (n.getKind() == AND)
601		{
602	650	for (const Node& nc : n)
603		{
604	484	removeProxyEqs(nc, unproc);
605		}
606	332	return;
607		}
608	39227	Trace("strings-subs-proxy") << "Input : " << n << std::endl;
609	78454	Node ns = Rewriter::rewrite(n);
610	39227	if (ns.getKind() == EQUAL)
611		{
612	117507	for (size_t i = 0; i < 2; i++)
613		{
614		// determine whether this side has a proxy variable
615	78338	if (ns[i].getAttribute(StringsProxyVarAttribute()))
616		{
617	2	if (getProxyVariableFor(ns[1 - i]) == ns[i])
618		{
619		Trace("strings-subs-proxy")
620		<< "...trivial definition via " << ns[i] << std::endl;
621		// it is a trivial equality, e.g. between a proxy variable
622		// and its definition
623		return;
624		}
625		}
626		}
627		}
628	39227	if (!n.isConst() \|\| !n.getConst<bool>())
629		{
630	39213	Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
631	39213	unproc.push_back(n);
632		}
633		}
634
635		} // namespace strings
636		} // namespace theory
637	28191	} // namespace cvc5