Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/term_registry.cpp	Lines:	286	311	92.0 %
Date:	2021-09-07	Branches:	687	1420	48.4 %


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

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_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, nm->mkConst(Rational(-1)).eqNode(t), 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 == 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_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);
    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		#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		struct StringsProxyVarAttributeId
38		{
39		};
40		typedef expr::Attribute<StringsProxyVarAttributeId, bool>
41		StringsProxyVarAttribute;
42
43	9926	TermRegistry::TermRegistry(SolverState& s,
44		SequencesStatistics& statistics,
45	9926	ProofNodeManager* pnm)
46		: d_state(s),
47		d_im(nullptr),
48		d_statistics(statistics),
49		d_hasStrCode(false),
50		d_functionsTerms(s.getSatContext()),
51	9926	d_inputVars(s.getUserContext()),
52		d_preregisteredTerms(s.getSatContext()),
53	9926	d_registeredTerms(s.getUserContext()),
54	9926	d_registeredTypes(s.getUserContext()),
55	9926	d_proxyVar(s.getUserContext()),
56	9926	d_lengthLemmaTermsCache(s.getUserContext()),
57		d_epg(pnm ? new EagerProofGenerator(
58		pnm,
59	1243	s.getUserContext(),
60	1243	"strings::TermRegistry::EagerProofGenerator")
61	62042	: nullptr)
62		{
63	9926	NodeManager* nm = NodeManager::currentNM();
64	9926	d_zero = nm->mkConst(Rational(0));
65	9926	d_one = nm->mkConst(Rational(1));
66	9926	d_negOne = NodeManager::currentNM()->mkConst(Rational(-1));
67	9926	d_cardSize = utils::getAlphabetCardinality();
68	9926	}
69
70	9923	TermRegistry::~TermRegistry() {}
71
72	9926	void TermRegistry::finishInit(InferenceManager* im) { d_im = im; }
73
74	30558	Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
75		{
76	30558	NodeManager* nm = NodeManager::currentNM();
77	30558	Node lemma;
78	30558	Kind tk = t.getKind();
79	30558	if (tk == STRING_TO_CODE)
80		{
81		// ite( str.len(s)==1, 0 <= str.code(s) < \|A\|, str.code(s)=-1 )
82	3322	Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConst(Rational(1)));
83	3322	Node code_eq_neg1 = t.eqNode(nm->mkConst(Rational(-1)));
84		Node code_range = nm->mkNode(
85		AND,
86	3322	nm->mkNode(GEQ, t, nm->mkConst(Rational(0))),
87	3322	nm->mkNode(
88	9966	LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
89	1661	lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
90		}
91	28897	else if (tk == STRING_INDEXOF \|\| tk == STRING_INDEXOF_RE)
92		{
93		// (and
94		// (or (= (f x y n) (- 1)) (>= (f x y n) n))
95		// (<= (f x y n) (str.len x)))
96		//
97		// where f in { str.indexof, str.indexof_re }
98	628	Node l = nm->mkNode(STRING_LENGTH, t[0]);
99	942	lemma = nm->mkNode(
100		AND,
101	1256	nm->mkNode(
102	1256	OR, nm->mkConst(Rational(-1)).eqNode(t), nm->mkNode(GEQ, t, t[2])),
103	942	nm->mkNode(LEQ, t, l));
104		}
105	28583	else if (tk == STRING_STOI)
106		{
107		// (>= (str.to_int x) (- 1))
108	91	lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
109		}
110	28492	else if (tk == STRING_CONTAINS)
111		{
112		// ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
113		Node sk1 =
114	8268	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1");
115		Node sk2 =
116	8268	sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2");
117	4134	lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2));
118	4134	lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode());
119		}
120	30558	return lemma;
121		}
122
123	11263	Node TermRegistry::lengthPositive(Node t)
124		{
125	11263	NodeManager* nm = NodeManager::currentNM();
126	22526	Node zero = nm->mkConst(Rational(0));
127	22526	Node emp = Word::mkEmptyWord(t.getType());
128	22526	Node tlen = nm->mkNode(STRING_LENGTH, t);
129	22526	Node tlenEqZero = tlen.eqNode(zero);
130	22526	Node tEqEmp = t.eqNode(emp);
131	22526	Node caseEmpty = nm->mkNode(AND, tlenEqZero, tEqEmp);
132	22526	Node caseNEmpty = nm->mkNode(GT, tlen, zero);
133		// (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
134	22526	return nm->mkNode(OR, caseEmpty, caseNEmpty);
135		}
136
137	158451	void TermRegistry::preRegisterTerm(TNode n)
138		{
139	158451	if (d_preregisteredTerms.find(n) != d_preregisteredTerms.end())
140		{
141	65046	return;
142		}
143	157519	eq::EqualityEngine* ee = d_state.getEqualityEngine();
144	157519	d_preregisteredTerms.insert(n);
145	315038	Trace("strings-preregister")
146	157519	<< "TheoryString::preregister : " << n << std::endl;
147		// check for logic exceptions
148	157519	Kind k = n.getKind();
149	157519	if (!options::stringExp())
150		{
151	4103	if (k == STRING_INDEXOF \|\| k == STRING_INDEXOF_RE \|\| k == STRING_ITOS
152	4103	\|\| k == STRING_STOI \|\| k == STRING_REPLACE \|\| k == STRING_SUBSTR
153	4103	\|\| k == STRING_REPLACE_ALL \|\| k == SEQ_NTH \|\| k == STRING_REPLACE_RE
154	4103	\|\| k == STRING_REPLACE_RE_ALL \|\| k == STRING_CONTAINS \|\| k == STRING_LEQ
155	4103	\|\| k == STRING_TOLOWER \|\| k == STRING_TOUPPER \|\| k == STRING_REV
156	4103	\|\| k == STRING_UPDATE)
157		{
158		std::stringstream ss;
159		ss << "Term of kind " << k
160		<< " not supported in default mode, try --strings-exp";
161		throw LogicException(ss.str());
162		}
163		}
164	157519	if (k == EQUAL)
165		{
166	60017	if (n[0].getType().isRegExp())
167		{
168		std::stringstream ss;
169		ss << "Equality between regular expressions is not supported";
170		throw LogicException(ss.str());
171		}
172	60017	ee->addTriggerPredicate(n);
173	60017	return;
174		}
175	97502	else if (k == STRING_IN_REGEXP)
176		{
177	3165	d_im->requirePhase(n, true);
178	3165	ee->addTriggerPredicate(n);
179	3165	ee->addTerm(n[0]);
180	3165	ee->addTerm(n[1]);
181	3165	return;
182		}
183	94337	else if (k == STRING_TO_CODE)
184		{
185	2953	d_hasStrCode = true;
186		}
187	91384	else if (k == REGEXP_RANGE)
188		{
189	255	for (const Node& nc : n)
190		{
191	170	if (!nc.isConst())
192		{
193		throw LogicException(
194		"expecting a constant string term in regexp range");
195		}
196	170	if (nc.getConst<String>().size() != 1)
197		{
198		throw LogicException(
199		"expecting a single constant string term in regexp range");
200		}
201		}
202		}
203	94337	registerTerm(n, 0);
204	188674	TypeNode tn = n.getType();
205	94337	if (tn.isRegExp() && n.isVar())
206		{
207		std::stringstream ss;
208		ss << "Regular expression variables are not supported.";
209		throw LogicException(ss.str());
210		}
211	94337	if (tn.isString()) // string-only
212		{
213		// all characters of constants should fall in the alphabet
214	47818	if (n.isConst())
215		{
216	8158	std::vector<unsigned> vec = n.getConst<String>().getVec();
217	17746	for (unsigned u : vec)
218		{
219	13667	if (u >= d_cardSize)
220		{
221		std::stringstream ss;
222		ss << "Characters in string \"" << n
223		<< "\" are outside of the given alphabet.";
224		throw LogicException(ss.str());
225		}
226		}
227		}
228	47818	ee->addTerm(n);
229		}
230	46519	else if (tn.isBoolean())
231		{
232		// All kinds that we do congruence over that may return a Boolean go here
233	1883	if (k == STRING_CONTAINS \|\| k == STRING_LEQ \|\| k == SEQ_NTH)
234		{
235		// Get triggered for both equal and dis-equal
236	1877	ee->addTriggerPredicate(n);
237		}
238		}
239		else
240		{
241		// Function applications/predicates
242	44636	ee->addTerm(n);
243		}
244		// Set d_functionsTerms stores all function applications that are
245		// relevant to theory combination. Notice that this is a subset of
246		// the applications whose kinds are function kinds in the equality
247		// engine. This means it does not include applications of operators
248		// like re.++, which is not a function kind in the equality engine.
249		// Concatenation terms do not need to be considered here because
250		// their arguments have string type and do not introduce any shared
251		// terms.
252	246808	if (n.hasOperator() && ee->isFunctionKind(k)
253	148869	&& kindToTheoryId(k) == THEORY_STRINGS && k != STRING_CONCAT)
254		{
255	43606	d_functionsTerms.push_back(n);
256		}
257	94337	if (options::stringFMF())
258		{
259	15158	if (tn.isStringLike())
260		{
261		// Our decision strategy will minimize the length of this term if it is a
262		// variable but not an internally generated Skolem, or a term that does
263		// not belong to this theory.
264	11096	if (n.isVar() ? !d_skCache.isSkolem(n)
265	3230	: kindToTheoryId(k) != THEORY_STRINGS)
266		{
267	518	d_inputVars.insert(n);
268	518	Trace("strings-preregister") << "input variable: " << n << std::endl;
269		}
270		}
271		}
272		}
273
274	206763	void TermRegistry::registerTerm(Node n, int effort)
275		{
276	413526	Trace("strings-register") << "TheoryStrings::registerTerm() " << n
277	206763	<< ", effort = " << effort << std::endl;
278	206763	if (d_registeredTerms.find(n) != d_registeredTerms.end())
279		{
280	149556	Trace("strings-register") << "...already registered" << std::endl;
281	299112	return;
282		}
283	57207	bool do_register = true;
284	114414	TypeNode tn = n.getType();
285	57207	if (!tn.isStringLike())
286		{
287	27437	if (options::stringEagerLen())
288		{
289	27437	do_register = effort == 0;
290		}
291		else
292		{
293		do_register = effort > 0 \|\| n.getKind() != STRING_CONCAT;
294		}
295		}
296	57207	if (!do_register)
297		{
298		Trace("strings-register") << "...do not register" << std::endl;
299		return;
300		}
301	57207	Trace("strings-register") << "...register" << std::endl;
302	57207	d_registeredTerms.insert(n);
303		// ensure the type is registered
304	57207	registerType(tn);
305	114414	TrustNode regTermLem;
306	57207	if (tn.isStringLike())
307		{
308		// register length information:
309		// for variables, split on empty vs positive length
310		// for concat/const/replace, introduce proxy var and state length relation
311	29770	regTermLem = getRegisterTermLemma(n);
312		}
313	27437	else if (n.getKind() != STRING_CONTAINS)
314		{
315		// we don't send out eager reduction lemma for str.contains currently
316	52742	Node eagerRedLemma = eagerReduce(n, &d_skCache);
317	26371	if (!eagerRedLemma.isNull())
318		{
319		// if there was an eager reduction, we make the trust node for it
320	2013	if (d_epg != nullptr)
321		{
322	624	regTermLem = d_epg->mkTrustNode(
323	312	eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {}, {n});
324		}
325		else
326		{
327	1701	regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr);
328		}
329		}
330		}
331	57207	if (!regTermLem.isNull())
332		{
333	22894	Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
334	11447	<< std::endl;
335	22894	Trace("strings-assert")
336	11447	<< "(assert " << regTermLem.getNode() << ")" << std::endl;
337	11447	d_im->trustedLemma(regTermLem, InferenceId::STRINGS_REGISTER_TERM);
338		}
339		}
340
341	57207	void TermRegistry::registerType(TypeNode tn)
342		{
343	57207	if (d_registeredTypes.find(tn) != d_registeredTypes.end())
344		{
345	54855	return;
346		}
347	2352	d_registeredTypes.insert(tn);
348	2352	if (tn.isStringLike())
349		{
350		// preregister the empty word for the type
351	1864	Node emp = Word::mkEmptyWord(tn);
352	932	if (!d_state.hasTerm(emp))
353		{
354	932	preRegisterTerm(emp);
355		}
356		}
357		}
358
359	29770	TrustNode TermRegistry::getRegisterTermLemma(Node n)
360		{
361	29770	Assert(n.getType().isStringLike());
362	29770	NodeManager* nm = NodeManager::currentNM();
363		// register length information:
364		// for variables, split on empty vs positive length
365		// for concat/const/replace, introduce proxy var and state length relation
366	59540	Node lsum;
367	29770	if (n.getKind() != STRING_CONCAT && !n.isConst())
368		{
369	20648	Node lsumb = nm->mkNode(STRING_LENGTH, n);
370	20492	lsum = Rewriter::rewrite(lsumb);
371		// can register length term if it does not rewrite
372	20492	if (lsum == lsumb)
373		{
374	20336	registerTermAtomic(n, LENGTH_SPLIT);
375	20336	return TrustNode::null();
376		}
377		}
378	18868	Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
379		StringsProxyVarAttribute spva;
380	9434	sk.setAttribute(spva, true);
381	18868	Node eq = Rewriter::rewrite(sk.eqNode(n));
382	9434	d_proxyVar[n] = sk;
383		// If we are introducing a proxy for a constant or concat term, we do not
384		// need to send lemmas about its length, since its length is already
385		// implied.
386	9434	if (n.isConst() \|\| n.getKind() == STRING_CONCAT)
387		{
388		// do not send length lemma for sk.
389	9278	registerTermAtomic(sk, LENGTH_IGNORE);
390		}
391	18868	Node skl = nm->mkNode(STRING_LENGTH, sk);
392	9434	if (n.getKind() == STRING_CONCAT)
393		{
394	11720	std::vector<Node> nodeVec;
395	19952	for (const Node& nc : n)
396		{
397	14092	if (nc.getAttribute(StringsProxyVarAttribute()))
398		{
399	60	Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end());
400	60	nodeVec.push_back(d_proxyVarToLength[nc]);
401		}
402		else
403		{
404	28064	Node lni = nm->mkNode(STRING_LENGTH, nc);
405	14032	nodeVec.push_back(lni);
406		}
407		}
408	5860	lsum = nm->mkNode(PLUS, nodeVec);
409	5860	lsum = Rewriter::rewrite(lsum);
410		}
411	3574	else if (n.isConst())
412		{
413	3418	lsum = nm->mkConst(Rational(Word::getLength(n)));
414		}
415	9434	Assert(!lsum.isNull());
416	9434	d_proxyVarToLength[sk] = lsum;
417	18868	Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
418
419	18868	Node ret = nm->mkNode(AND, eq, ceq);
420
421		// it is a simple rewrite to justify this
422	9434	if (d_epg != nullptr)
423		{
424	1280	return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {}, {ret});
425		}
426	8154	return TrustNode::mkTrustLemma(ret, nullptr);
427		}
428
429	31037	void TermRegistry::registerTermAtomic(Node n, LengthStatus s)
430		{
431	31037	if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
432		{
433	30656	return;
434		}
435	20340	d_lengthLemmaTermsCache.insert(n);
436
437	20340	if (s == LENGTH_IGNORE)
438		{
439		// ignore it
440	9262	return;
441		}
442	22156	std::map<Node, bool> reqPhase;
443	22156	TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
444	11078	if (!lenLem.isNull())
445		{
446	22148	Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
447	11074	<< std::endl;
448	22148	Trace("strings-assert")
449	11074	<< "(assert " << lenLem.getNode() << ")" << std::endl;
450	11074	d_im->trustedLemma(lenLem, InferenceId::STRINGS_REGISTER_TERM_ATOMIC);
451		}
452	33194	for (const std::pair<const Node, bool>& rp : reqPhase)
453		{
454	22116	d_im->requirePhase(rp.first, rp.second);
455		}
456		}
457
458	35354	SkolemCache* TermRegistry::getSkolemCache() { return &d_skCache; }
459
460	7226	const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
461		{
462	7226	return d_functionsTerms;
463		}
464
465	78	const context::CDHashSet<Node>& TermRegistry::getInputVars() const
466		{
467	78	return d_inputVars;
468		}
469
470	12149	bool TermRegistry::hasStringCode() const { return d_hasStrCode; }
471
472	11078	TrustNode TermRegistry::getRegisterTermAtomicLemma(
473		Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
474		{
475	11078	if (n.isConst())
476		{
477		// No need to send length for constant terms. This case may be triggered
478		// for cases where the skolem cache automatically replaces a skolem by
479		// a constant.
480	4	return TrustNode::null();
481		}
482	11074	Assert(n.getType().isStringLike());
483	11074	NodeManager* nm = NodeManager::currentNM();
484	22148	Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
485	22148	Node emp = Word::mkEmptyWord(n.getType());
486	11074	if (s == LENGTH_GEQ_ONE)
487		{
488	32	Node neq_empty = n.eqNode(emp).negate();
489	32	Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero);
490	32	Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z);
491	32	Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
492	16	<< std::endl;
493	16	Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
494	16	return TrustNode::mkTrustLemma(len_geq_one, nullptr);
495		}
496
497	11058	if (s == LENGTH_ONE)
498		{
499		Node len_one = n_len.eqNode(d_one);
500		Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
501		<< std::endl;
502		Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
503		return TrustNode::mkTrustLemma(len_one, nullptr);
504		}
505	11058	Assert(s == LENGTH_SPLIT);
506
507		// get the positive length lemma
508	22116	Node lenLemma = lengthPositive(n);
509		// split whether the string is empty
510	22116	Node n_len_eq_z = n_len.eqNode(d_zero);
511	22116	Node n_len_eq_z_2 = n.eqNode(emp);
512	22116	Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
513	22116	Node case_emptyr = Rewriter::rewrite(case_empty);
514	11058	if (!case_emptyr.isConst())
515		{
516		// prefer trying the empty case first
517		// notice that requirePhase must only be called on rewritten literals that
518		// occur in the CNF stream.
519	11058	n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
520	11058	Assert(!n_len_eq_z.isConst());
521	11058	reqPhase[n_len_eq_z] = true;
522	11058	n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
523	11058	Assert(!n_len_eq_z_2.isConst());
524	11058	reqPhase[n_len_eq_z_2] = true;
525		}
526		else
527		{
528		// If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
529		// n ---> "". Since this method is only called on non-constants n, it must
530		// be that n = "" ^ len( n ) = 0 does not rewrite to true.
531		Assert(!case_emptyr.getConst<bool>());
532		}
533
534	11058	if (d_epg != nullptr)
535		{
536	1470	return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {}, {n});
537		}
538	9588	return TrustNode::mkTrustLemma(lenLemma, nullptr);
539		}
540
541	411763	Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
542		{
543	411763	if (n.getNumChildren() == 0)
544		{
545	366780	Node pn = getProxyVariableFor(n);
546	183390	if (pn.isNull())
547		{
548	20057	return Node::null();
549		}
550	326666	Node eq = n.eqNode(pn);
551	163333	eq = Rewriter::rewrite(eq);
552	163333	if (std::find(exp.begin(), exp.end(), eq) == exp.end())
553		{
554	159997	exp.push_back(eq);
555		}
556	163333	return pn;
557		}
558	456746	std::vector<Node> children;
559	228373	if (n.getMetaKind() == metakind::PARAMETERIZED)
560		{
561	42	children.push_back(n.getOperator());
562		}
563	604955	for (const Node& nc : n)
564		{
565	404487	if (n.getType().isRegExp())
566		{
567	142814	children.push_back(nc);
568		}
569		else
570		{
571	495441	Node ns = getSymbolicDefinition(nc, exp);
572	261673	if (ns.isNull())
573		{
574	27905	return Node::null();
575		}
576		else
577		{
578	233768	children.push_back(ns);
579		}
580		}
581		}
582	200468	return NodeManager::currentNM()->mkNode(n.getKind(), children);
583		}
584
585	191268	Node TermRegistry::getProxyVariableFor(Node n) const
586		{
587	191268	NodeNodeMap::const_iterator it = d_proxyVar.find(n);
588	191268	if (it != d_proxyVar.end())
589		{
590	170901	return (*it).second;
591		}
592	20367	return Node::null();
593		}
594
595	7552	Node TermRegistry::ensureProxyVariableFor(Node n)
596		{
597	7552	Node proxy = getProxyVariableFor(n);
598	7552	if (proxy.isNull())
599		{
600	294	registerTerm(n, 0);
601	294	proxy = getProxyVariableFor(n);
602		}
603	7552	Assert(!proxy.isNull());
604	7552	return proxy;
605		}
606
607	89978	void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const
608		{
609	89978	if (n.getKind() == AND)
610		{
611	2821	for (const Node& nc : n)
612		{
613	2232	removeProxyEqs(nc, unproc);
614		}
615	1194	return;
616		}
617	89389	Trace("strings-subs-proxy") << "Input : " << n << std::endl;
618	178762	Node ns = Rewriter::rewrite(n);
619	89389	if (ns.getKind() == EQUAL)
620		{
621	267443	for (size_t i = 0; i < 2; i++)
622		{
623		// determine whether this side has a proxy variable
624	178306	if (ns[i].getAttribute(StringsProxyVarAttribute()))
625		{
626	32	if (getProxyVariableFor(ns[1 - i]) == ns[i])
627		{
628	32	Trace("strings-subs-proxy")
629	16	<< "...trivial definition via " << ns[i] << std::endl;
630		// it is a trivial equality, e.g. between a proxy variable
631		// and its definition
632	16	return;
633		}
634		}
635		}
636		}
637	89373	if (!n.isConst() \|\| !n.getConst<bool>())
638		{
639	89363	Trace("strings-subs-proxy") << "...unprocessed" << std::endl;
640	89363	unproc.push_back(n);
641		}
642		}
643
644		} // namespace strings
645		} // namespace theory
646	29502	} // namespace cvc5