Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/pattern_term_selector.cpp	Lines:	335	360	93.1 %
Date:	2021-05-22	Branches:	769	1548	49.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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 pattern term selector class.
 */

#include "theory/quantifiers/ematching/pattern_term_selector.h"

#include "expr/node_algorithm.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {
namespace inst {

PatternTermSelector::PatternTermSelector(Node q,
                                         options::TriggerSelMode tstrt,
                                         const std::vector<Node>& exc,
                                         bool filterInst)
    : d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
{
}

PatternTermSelector::~PatternTermSelector() {}

bool PatternTermSelector::isUsable(Node n, Node q)
{
  if (quantifiers::TermUtil::getInstConstAttr(n) != q)
  {
    return true;
  }
  if (TriggerTermInfo::isAtomicTrigger(n))
  {
    for (const Node& nc : n)
    {
      if (!isUsable(nc, q))
      {
        return false;
      }
    }
    return true;
  }
  else if (n.getKind() == INST_CONSTANT)
  {
    return true;
  }
  std::map<Node, Node> coeffs;
  if (options::purifyTriggers())
  {
    Node x = getInversionVariable(n);
    if (!x.isNull())
    {
      return true;
    }
  }
  return false;
}

Node PatternTermSelector::getIsUsableEq(Node q, Node n)
{
  Assert(TriggerTermInfo::isRelationalTrigger(n));
  for (size_t i = 0; i < 2; i++)
  {
    if (isUsableEqTerms(q, n[i], n[1 - i]))
    {
      if (i == 1 && n.getKind() == EQUAL
          && !quantifiers::TermUtil::hasInstConstAttr(n[0]))
      {
        return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]);
      }
      else
      {
        return n;
      }
    }
  }
  return Node::null();
}

bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
{
  if (n1.getKind() == INST_CONSTANT)
  {
    if (options::relationalTriggers())
    {
      Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
      if (q1 != q)
      {
        // x is a variable from another quantified formula, fail
        return false;
      }
      Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
      if (q2.isNull())
      {
        // x = c
        return true;
      }
      if (n2.getKind() == INST_CONSTANT && q2 == q)
      {
        // x = y
        return true;
      }
      // we dont check x = f(y), which is handled symmetrically below
      // when n1 and n2 are swapped
    }
  }
  else if (isUsableAtomicTrigger(n1, q))
  {
    if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
        && quantifiers::TermUtil::getInstConstAttr(n2) == q
        && !expr::hasSubterm(n1, n2))
    {
      // f(x) = y
      return true;
    }
    else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
    {
      // f(x) = c
      return true;
    }
  }
  return false;
}

Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
{
  bool pol = true;
  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
  if (n.getKind() == NOT)
  {
    pol = !pol;
    n = n[0];
  }
  NodeManager* nm = NodeManager::currentNM();
  if (n.getKind() == INST_CONSTANT)
  {
    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
  }
  else if (TriggerTermInfo::isRelationalTrigger(n))
  {
    Node rtr = getIsUsableEq(q, n);
    if (rtr.isNull() && n[0].getType().isReal())
    {
      // try to solve relation
      std::map<Node, Node> m;
      if (ArithMSum::getMonomialSumLit(n, m))
      {
        for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
        {
          bool trySolve = false;
          if (!it->first.isNull())
          {
            if (it->first.getKind() == INST_CONSTANT)
            {
              trySolve = options::relationalTriggers();
            }
            else if (isUsableTrigger(it->first, q))
            {
              trySolve = true;
            }
          }
          if (trySolve)
          {
            Trace("trigger-debug")
                << "Try to solve for " << it->first << std::endl;
            Node veq;
            if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
            {
              rtr = getIsUsableEq(q, veq);
            }
            // either all solves will succeed or all solves will fail
            break;
          }
        }
      }
    }
    if (!rtr.isNull())
    {
      Trace("relational-trigger") << "Relational trigger : " << std::endl;
      Trace("relational-trigger")
          << "    " << rtr << " (from " << n << ")" << std::endl;
      Trace("relational-trigger") << "    in quantifier " << q << std::endl;
      Node rtr2 = pol ? rtr : rtr.negate();
      Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
      return rtr2;
    }
    return Node::null();
  }
  Trace("trigger-debug") << n << " usable : "
                         << (quantifiers::TermUtil::getInstConstAttr(n) == q)
                         << " " << TriggerTermInfo::isAtomicTrigger(n) << " "
                         << isUsable(n, q) << std::endl;
  if (isUsableAtomicTrigger(n, q))
  {
    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
  }
  return Node::null();
}

bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
{
  return quantifiers::TermUtil::getInstConstAttr(n) == q
         && TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
}

bool PatternTermSelector::isUsableTrigger(Node n, Node q)
{
  Node nu = getIsUsableTrigger(n, q);
  return !nu.isNull();
}

// store triggers in reqPol, indicating their polarity (if any) they must appear
// to falsify the quantified formula
void PatternTermSelector::collectTermsInternal(
    Node n,
    std::map<Node, std::vector<Node> >& visited,
    std::map<Node, TriggerTermInfo>& tinfo,
    options::TriggerSelMode tstrt,
    std::vector<Node>& added,
    bool pol,
    bool hasPol,
    bool epol,
    bool hasEPol,
    bool knowIsUsable)
{
  std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
  if (itv != visited.end())
  {
    // already visited
    for (const Node& t : itv->second)
    {
      if (std::find(added.begin(), added.end(), t) == added.end())
      {
        added.push_back(t);
      }
    }
    return;
  }
  visited[n].clear();
  Trace("auto-gen-trigger-debug2")
      << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
      << " " << hasEPol << std::endl;
  Kind nk = n.getKind();
  if (nk == FORALL || nk == INST_CONSTANT)
  {
    // do not traverse beneath quantified formulas
    return;
  }
  Node nu;
  bool nu_single = false;
  if (knowIsUsable)
  {
    nu = n;
  }
  else if (nk != NOT
           && std::find(d_excluded.begin(), d_excluded.end(), n)
                  == d_excluded.end())
  {
    nu = getIsUsableTrigger(n, d_quant);
    if (!nu.isNull() && nu != n)
    {
      collectTermsInternal(
          nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
      // copy to n
      visited[n].insert(visited[n].end(), added.begin(), added.end());
      return;
    }
  }
  if (!nu.isNull())
  {
    Assert(nu == n);
    Assert(nu.getKind() != NOT);
    Trace("auto-gen-trigger-debug2")
        << "...found usable trigger : " << nu << std::endl;
    Node reqEq;
    if (nu.getKind() == EQUAL)
    {
      if (TriggerTermInfo::isAtomicTrigger(nu[0])
          && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
      {
        if (hasPol)
        {
          reqEq = nu[1];
        }
        nu = nu[0];
      }
    }
    Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
    Assert(isUsableTrigger(nu, d_quant));
    Trace("auto-gen-trigger-debug2")
        << "...add usable trigger : " << nu << std::endl;
    tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
    nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
  }
  Node nrec = nu.isNull() ? n : nu;
  std::vector<Node> added2;
  for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
  {
    bool newHasPol, newPol;
    bool newHasEPol, newEPol;
    QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
    QuantPhaseReq::getEntailPolarity(
        nrec, i, hasEPol, epol, newHasEPol, newEPol);
    collectTermsInternal(nrec[i],
                         visited,
                         tinfo,
                         tstrt,
                         added2,
                         newPol,
                         newHasPol,
                         newEPol,
                         newHasEPol);
  }
  // if this is not a usable trigger, don't worry about caching the results,
  // since triggers do not contain non-usable subterms
  if (nu.isNull())
  {
    return;
  }
  bool rm_nu = false;
  for (size_t i = 0, asize = added2.size(); i < asize; i++)
  {
    Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
                                     << " : " << added2[i] << std::endl;
    Assert(added2[i] != nu);
    // if child was not already removed
    if (tinfo.find(added2[i]) != tinfo.end())
    {
      if (tstrt == options::TriggerSelMode::MAX
          || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
      {
        // discard all subterms
        // do not remove if it has smaller weight
        if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
        {
          Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
          visited[added2[i]].clear();
          tinfo.erase(added2[i]);
        }
      }
      else
      {
        if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
        {
          if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
          {
            // discard if we added a subterm as a trigger with all
            // variables that nu has
            Trace("auto-gen-trigger-debug2")
                << "......subsumes parent " << tinfo[nu].d_weight << " "
                << tinfo[added2[i]].d_weight << "." << std::endl;
            rm_nu = true;
          }
        }
        if (std::find(added.begin(), added.end(), added2[i]) == added.end())
        {
          added.push_back(added2[i]);
        }
      }
    }
  }
  if (rm_nu
      && (tstrt == options::TriggerSelMode::MIN
          || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
  {
    tinfo.erase(nu);
  }
  else
  {
    if (std::find(added.begin(), added.end(), nu) == added.end())
    {
      added.push_back(nu);
    }
  }
  visited[n].insert(visited[n].end(), added.begin(), added.end());
}

void PatternTermSelector::collect(Node n,
                                  std::vector<Node>& patTerms,
                                  std::map<Node, TriggerTermInfo>& tinfo)
{
  collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
}

void PatternTermSelector::collectInternal(
    Node n,
    std::vector<Node>& patTerms,
    std::map<Node, TriggerTermInfo>& tinfo,
    options::TriggerSelMode tstrt,
    bool filterInst)
{
  std::map<Node, std::vector<Node> > visited;
  if (filterInst)
  {
    // immediately do not consider any term t for which another term is an
    // instance of t
    std::vector<Node> patTerms2;
    std::map<Node, TriggerTermInfo> tinfo2;
    collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
    std::vector<Node> temp;
    temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
    filterInstances(temp);
    if (Trace.isOn("trigger-filter-instance"))
    {
      if (temp.size() != patTerms2.size())
      {
        Trace("trigger-filter-instance")
            << "Filtered an instance: " << std::endl;
        Trace("trigger-filter-instance") << "Old: ";
        for (unsigned i = 0; i < patTerms2.size(); i++)
        {
          Trace("trigger-filter-instance") << patTerms2[i] << " ";
        }
        Trace("trigger-filter-instance") << std::endl << "New: ";
        for (unsigned i = 0; i < temp.size(); i++)
        {
          Trace("trigger-filter-instance") << temp[i] << " ";
        }
        Trace("trigger-filter-instance") << std::endl;
      }
    }
    if (tstrt == options::TriggerSelMode::ALL)
    {
      for (const Node& t : temp)
      {
        // copy information
        tinfo[t].d_fv.insert(
            tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
        tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
        tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
        patTerms.push_back(t);
      }
      return;
    }
    // do not consider terms that have instances
    for (const Node& t : patTerms2)
    {
      if (std::find(temp.begin(), temp.end(), t) == temp.end())
      {
        visited[t].clear();
      }
    }
  }
  std::vector<Node> added;
  collectTermsInternal(
      n, visited, tinfo, tstrt, added, true, true, false, true);
  for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
  {
    patTerms.push_back(t.first);
  }
}

int PatternTermSelector::isInstanceOf(Node n1,
                                      Node n2,
                                      const std::vector<Node>& fv1,
                                      const std::vector<Node>& fv2)
{
  Assert(n1 != n2);
  int status = 0;
  std::unordered_set<TNode> subs_vars;
  std::unordered_set<
      std::pair<TNode, TNode>,
      PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>>
      visited;
  std::vector<std::pair<TNode, TNode> > visit;
  std::pair<TNode, TNode> cur;
  TNode cur1;
  TNode cur2;
  visit.push_back(std::pair<TNode, TNode>(n1, n2));
  do
  {
    cur = visit.back();
    visit.pop_back();
    if (visited.find(cur) != visited.end())
    {
      continue;
    }
    visited.insert(cur);
    cur1 = cur.first;
    cur2 = cur.second;
    Assert(cur1 != cur2);
    // recurse if they have the same operator
    if (cur1.hasOperator() && cur2.hasOperator()
        && cur1.getNumChildren() == cur2.getNumChildren()
        && cur1.getOperator() == cur2.getOperator()
        && cur1.getOperator().getKind() != INST_CONSTANT)
    {
      visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
      for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
      {
        if (cur1[i] != cur2[i])
        {
          visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
        }
        else if (cur1[i].getKind() == INST_CONSTANT)
        {
          if (subs_vars.find(cur1[i]) != subs_vars.end())
          {
            return 0;
          }
          // the variable must map to itself in the substitution
          subs_vars.insert(cur1[i]);
        }
      }
      continue;
    }
    bool success = false;
    // check if we are in a unifiable instance case
    // must be only this case
    for (unsigned r = 0; r < 2; r++)
    {
      if (status == 0 || ((status == 1) == (r == 0)))
      {
        TNode curi = r == 0 ? cur1 : cur2;
        if (curi.getKind() == INST_CONSTANT
            && subs_vars.find(curi) == subs_vars.end())
        {
          TNode curj = r == 0 ? cur2 : cur1;
          // RHS must be a simple trigger
          if (TriggerTermInfo::getTriggerWeight(curj) == 0)
          {
            // must occur in the free variables in the other
            const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
            if (std::find(free_vars.begin(), free_vars.end(), curi)
                != free_vars.end())
            {
              status = r == 0 ? 1 : -1;
              subs_vars.insert(curi);
              success = true;
              break;
            }
          }
        }
      }
    }
    if (!success)
    {
      return 0;
    }
  } while (!visit.empty());
  return status;
}

void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
{
  std::map<unsigned, std::vector<Node> > fvs;
  for (size_t i = 0, size = nodes.size(); i < size; i++)
  {
    quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
  }
  std::vector<bool> active;
  active.resize(nodes.size(), true);
  for (size_t i = 0, size = nodes.size(); i < size; i++)
  {
    std::vector<Node>& fvsi = fvs[i];
    if (!active[i])
    {
      continue;
    }
    for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
    {
      if (!active[j])
      {
        continue;
      }
      int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
      if (result == 1)
      {
        Trace("filter-instances")
            << nodes[j] << " is an instance of " << nodes[i] << std::endl;
        active[i] = false;
        break;
      }
      else if (result == -1)
      {
        Trace("filter-instances")
            << nodes[i] << " is an instance of " << nodes[j] << std::endl;
        active[j] = false;
      }
    }
  }
  std::vector<Node> temp;
  for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
  {
    if (active[i])
    {
      temp.push_back(nodes[i]);
    }
  }
  nodes.clear();
  nodes.insert(nodes.begin(), temp.begin(), temp.end());
}

Node PatternTermSelector::getInversionVariable(Node n)
{
  Kind nk = n.getKind();
  if (nk == INST_CONSTANT)
  {
    return n;
  }
  else if (nk == PLUS || nk == MULT)
  {
    Node ret;
    for (const Node& nc : n)
    {
      if (quantifiers::TermUtil::hasInstConstAttr(nc))
      {
        if (ret.isNull())
        {
          ret = getInversionVariable(nc);
          if (ret.isNull())
          {
            Trace("var-trigger-debug")
                << "No : multiple variables " << n << std::endl;
            return Node::null();
          }
        }
        else
        {
          return Node::null();
        }
      }
      else if (nk == MULT)
      {
        if (!nc.isConst())
        {
          Trace("var-trigger-debug")
              << "No : non-linear coefficient " << n << std::endl;
          return Node::null();
        }
      }
    }
    return ret;
  }
  Trace("var-trigger-debug")
      << "No : unsupported operator " << n << "." << std::endl;
  return Node::null();
}

Node PatternTermSelector::getInversion(Node n, Node x)
{
  Kind nk = n.getKind();
  if (nk == INST_CONSTANT)
  {
    return x;
  }
  else if (nk == PLUS || nk == MULT)
  {
    NodeManager* nm = NodeManager::currentNM();
    int cindex = -1;
    bool cindexSet = false;
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
    {
      Node nc = n[i];
      if (!quantifiers::TermUtil::hasInstConstAttr(nc))
      {
        if (nk == PLUS)
        {
          x = nm->mkNode(MINUS, x, nc);
        }
        else if (nk == MULT)
        {
          Assert(nc.isConst());
          if (x.getType().isInteger())
          {
            Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
            if (!nc.getConst<Rational>().abs().isOne())
            {
              x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
            }
            if (nc.getConst<Rational>().sgn() < 0)
            {
              x = nm->mkNode(UMINUS, x);
            }
          }
          else
          {
            Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
            x = nm->mkNode(MULT, x, coeff);
          }
        }
        x = Rewriter::rewrite(x);
      }
      else
      {
        Assert(!cindexSet);
        cindex = i;
        cindexSet = true;
      }
    }
    if (cindexSet)
    {
      return getInversion(n[cindex], x);
    }
  }
  return Node::null();
}

void PatternTermSelector::getTriggerVariables(Node n,
                                              Node q,
                                              std::vector<Node>& tvars)
{
  PatternTermSelector pts(q, options::TriggerSelMode::ALL);
  std::vector<Node> patTerms;
  std::map<Node, TriggerTermInfo> tinfo;
  // collect all patterns from n
  pts.collect(n, patTerms, tinfo);
  // collect all variables from all patterns in patTerms, add to tvars
  for (const Node& pat : patTerms)
  {
    quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
  }
}

}  // namespace inst
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, 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 pattern term selector class.
14		*/
15
16		#include "theory/quantifiers/ematching/pattern_term_selector.h"
17
18		#include "expr/node_algorithm.h"
19		#include "theory/arith/arith_msum.h"
20		#include "theory/quantifiers/quant_util.h"
21		#include "theory/quantifiers/term_util.h"
22		#include "theory/rewriter.h"
23
24		using namespace cvc5::kind;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29		namespace inst {
30
31	10781	PatternTermSelector::PatternTermSelector(Node q,
32		options::TriggerSelMode tstrt,
33		const std::vector<Node>& exc,
34	10781	bool filterInst)
35	10781	: d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
36		{
37	10781	}
38
39	10781	PatternTermSelector::~PatternTermSelector() {}
40
41	2163553	bool PatternTermSelector::isUsable(Node n, Node q)
42		{
43	2163553	if (quantifiers::TermUtil::getInstConstAttr(n) != q)
44		{
45	305202	return true;
46		}
47	1858351	if (TriggerTermInfo::isAtomicTrigger(n))
48		{
49	2541090	for (const Node& nc : n)
50		{
51	1697118	if (!isUsable(nc, q))
52		{
53	10814	return false;
54		}
55		}
56	843972	return true;
57		}
58	1003565	else if (n.getKind() == INST_CONSTANT)
59		{
60	972340	return true;
61		}
62	62450	std::map<Node, Node> coeffs;
63	31225	if (options::purifyTriggers())
64		{
65	204	Node x = getInversionVariable(n);
66	142	if (!x.isNull())
67		{
68	80	return true;
69		}
70		}
71	31145	return false;
72		}
73
74	37825	Node PatternTermSelector::getIsUsableEq(Node q, Node n)
75		{
76	37825	Assert(TriggerTermInfo::isRelationalTrigger(n));
77	99041	for (size_t i = 0; i < 2; i++)
78		{
79	72421	if (isUsableEqTerms(q, n[i], n[1 - i]))
80		{
81	19181	if (i == 1 && n.getKind() == EQUAL
82	19161	&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
83		{
84	7712	return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]);
85		}
86		else
87		{
88	3493	return n;
89		}
90		}
91		}
92	26620	return Node::null();
93		}
94
95	72421	bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
96		{
97	72421	if (n1.getKind() == INST_CONSTANT)
98		{
99	13555	if (options::relationalTriggers())
100		{
101	3075	Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
102	2465	if (q1 != q)
103		{
104		// x is a variable from another quantified formula, fail
105		return false;
106		}
107	3075	Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
108	2465	if (q2.isNull())
109		{
110		// x = c
111	1460	return true;
112		}
113	1005	if (n2.getKind() == INST_CONSTANT && q2 == q)
114		{
115		// x = y
116	395	return true;
117		}
118		// we dont check x = f(y), which is handled symmetrically below
119		// when n1 and n2 are swapped
120		}
121		}
122	58866	else if (isUsableAtomicTrigger(n1, q))
123		{
124	62230	if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
125	29868	&& quantifiers::TermUtil::getInstConstAttr(n2) == q
126	59150	&& !expr::hasSubterm(n1, n2))
127		{
128		// f(x) = y
129	244	return true;
130		}
131	29038	else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
132		{
133		// f(x) = c
134	9106	return true;
135		}
136		}
137	61216	return false;
138		}
139
140	286579	Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
141		{
142	286579	bool pol = true;
143	286579	Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
144	286579	if (n.getKind() == NOT)
145		{
146		pol = !pol;
147		n = n[0];
148		}
149	286579	NodeManager* nm = NodeManager::currentNM();
150	286579	if (n.getKind() == INST_CONSTANT)
151		{
152	12	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
153		}
154	286567	else if (TriggerTermInfo::isRelationalTrigger(n))
155		{
156	69330	Node rtr = getIsUsableEq(q, n);
157	34665	if (rtr.isNull() && n[0].getType().isReal())
158		{
159		// try to solve relation
160	18008	std::map<Node, Node> m;
161	9004	if (ArithMSum::getMonomialSumLit(n, m))
162		{
163	21668	for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
164		{
165	15836	bool trySolve = false;
166	15836	if (!it->first.isNull())
167		{
168	13942	if (it->first.getKind() == INST_CONSTANT)
169		{
170	7988	trySolve = options::relationalTriggers();
171		}
172	5954	else if (isUsableTrigger(it->first, q))
173		{
174	3148	trySolve = true;
175		}
176		}
177	15836	if (trySolve)
178		{
179	6344	Trace("trigger-debug")
180	3172	<< "Try to solve for " << it->first << std::endl;
181	6344	Node veq;
182	3172	if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
183		{
184	3160	rtr = getIsUsableEq(q, veq);
185		}
186		// either all solves will succeed or all solves will fail
187	3172	break;
188		}
189		}
190		}
191		}
192	34665	if (!rtr.isNull())
193		{
194	11205	Trace("relational-trigger") << "Relational trigger : " << std::endl;
195	22410	Trace("relational-trigger")
196	11205	<< " " << rtr << " (from " << n << ")" << std::endl;
197	11205	Trace("relational-trigger") << " in quantifier " << q << std::endl;
198	22410	Node rtr2 = pol ? rtr : rtr.negate();
199	11205	Trace("relational-trigger") << " return : " << rtr2 << std::endl;
200	11205	return rtr2;
201		}
202	23460	return Node::null();
203		}
204	503804	Trace("trigger-debug") << n << " usable : "
205	503804	<< (quantifiers::TermUtil::getInstConstAttr(n) == q)
206	503804	<< " " << TriggerTermInfo::isAtomicTrigger(n) << " "
207	251902	<< isUsable(n, q) << std::endl;
208	251902	if (isUsableAtomicTrigger(n, q))
209		{
210	181275	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
211		}
212	70627	return Node::null();
213		}
214
215	310768	bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
216		{
217	932304	return quantifiers::TermUtil::getInstConstAttr(n) == q
218	1243072	&& TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
219		}
220
221	98493	bool PatternTermSelector::isUsableTrigger(Node n, Node q)
222		{
223	196986	Node nu = getIsUsableTrigger(n, q);
224	196986	return !nu.isNull();
225		}
226
227		// store triggers in reqPol, indicating their polarity (if any) they must appear
228		// to falsify the quantified formula
229	456960	void PatternTermSelector::collectTermsInternal(
230		Node n,
231		std::map<Node, std::vector<Node> >& visited,
232		std::map<Node, TriggerTermInfo>& tinfo,
233		options::TriggerSelMode tstrt,
234		std::vector<Node>& added,
235		bool pol,
236		bool hasPol,
237		bool epol,
238		bool hasEPol,
239		bool knowIsUsable)
240		{
241	456960	std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
242	456960	if (itv != visited.end())
243		{
244		// already visited
245	198384	for (const Node& t : itv->second)
246		{
247	17914	if (std::find(added.begin(), added.end(), t) == added.end())
248		{
249	16301	added.push_back(t);
250		}
251		}
252	544891	return;
253		}
254	276490	visited[n].clear();
255	552980	Trace("auto-gen-trigger-debug2")
256	276490	<< "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
257	276490	<< " " << hasEPol << std::endl;
258	276490	Kind nk = n.getKind();
259	276490	if (nk == FORALL \|\| nk == INST_CONSTANT)
260		{
261		// do not traverse beneath quantified formulas
262	60857	return;
263		}
264	308172	Node nu;
265	215633	bool nu_single = false;
266	215633	if (knowIsUsable)
267		{
268	7728	nu = n;
269		}
270	207905	else if (nk != NOT
271	575495	&& std::find(d_excluded.begin(), d_excluded.end(), n)
272	575495	== d_excluded.end())
273		{
274	183795	nu = getIsUsableTrigger(n, d_quant);
275	183795	if (!nu.isNull() && nu != n)
276		{
277	7728	collectTermsInternal(
278		nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
279		// copy to n
280	7728	visited[n].insert(visited[n].end(), added.begin(), added.end());
281	7728	return;
282		}
283		}
284	207905	if (!nu.isNull())
285		{
286	92539	Assert(nu == n);
287	92539	Assert(nu.getKind() != NOT);
288	185078	Trace("auto-gen-trigger-debug2")
289	92539	<< "...found usable trigger : " << nu << std::endl;
290	185078	Node reqEq;
291	92539	if (nu.getKind() == EQUAL)
292		{
293	27492	if (TriggerTermInfo::isAtomicTrigger(nu[0])
294	27492	&& !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
295		{
296	8134	if (hasPol)
297		{
298	5232	reqEq = nu[1];
299		}
300	8134	nu = nu[0];
301		}
302		}
303	92539	Assert(reqEq.isNull() \|\| !quantifiers::TermUtil::hasInstConstAttr(reqEq));
304	92539	Assert(isUsableTrigger(nu, d_quant));
305	185078	Trace("auto-gen-trigger-debug2")
306	92539	<< "...add usable trigger : " << nu << std::endl;
307	92539	tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
308	92539	nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
309		}
310	300444	Node nrec = nu.isNull() ? n : nu;
311	300444	std::vector<Node> added2;
312	635585	for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
313		{
314		bool newHasPol, newPol;
315		bool newHasEPol, newEPol;
316	427680	QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
317	427680	QuantPhaseReq::getEntailPolarity(
318		nrec, i, hasEPol, epol, newHasEPol, newEPol);
319	427680	collectTermsInternal(nrec[i],
320		visited,
321		tinfo,
322		tstrt,
323		added2,
324		newPol,
325		newHasPol,
326		newEPol,
327		newHasEPol);
328		}
329		// if this is not a usable trigger, don't worry about caching the results,
330		// since triggers do not contain non-usable subterms
331	207905	if (nu.isNull())
332		{
333	115366	return;
334		}
335	92539	bool rm_nu = false;
336	188741	for (size_t i = 0, asize = added2.size(); i < asize; i++)
337		{
338	192404	Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
339	96202	<< " : " << added2[i] << std::endl;
340	96202	Assert(added2[i] != nu);
341		// if child was not already removed
342	96202	if (tinfo.find(added2[i]) != tinfo.end())
343		{
344	96202	if (tstrt == options::TriggerSelMode::MAX
345	96202	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
346		{
347		// discard all subterms
348		// do not remove if it has smaller weight
349		if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
350		{
351		Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
352		visited[added2[i]].clear();
353		tinfo.erase(added2[i]);
354		}
355		}
356		else
357		{
358	96202	if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
359		{
360	16549	if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
361		{
362		// discard if we added a subterm as a trigger with all
363		// variables that nu has
364	30478	Trace("auto-gen-trigger-debug2")
365	15239	<< "......subsumes parent " << tinfo[nu].d_weight << " "
366	15239	<< tinfo[added2[i]].d_weight << "." << std::endl;
367	15239	rm_nu = true;
368		}
369		}
370	96202	if (std::find(added.begin(), added.end(), added2[i]) == added.end())
371		{
372	89561	added.push_back(added2[i]);
373		}
374		}
375		}
376		}
377	92539	if (rm_nu
378	12918	&& (tstrt == options::TriggerSelMode::MIN
379	6750	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
380		{
381	6168	tinfo.erase(nu);
382		}
383		else
384		{
385	86371	if (std::find(added.begin(), added.end(), nu) == added.end())
386		{
387	86347	added.push_back(nu);
388		}
389		}
390	92539	visited[n].insert(visited[n].end(), added.begin(), added.end());
391		}
392
393	10781	void PatternTermSelector::collect(Node n,
394		std::vector<Node>& patTerms,
395		std::map<Node, TriggerTermInfo>& tinfo)
396		{
397	10781	collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
398	10781	}
399
400	21562	void PatternTermSelector::collectInternal(
401		Node n,
402		std::vector<Node>& patTerms,
403		std::map<Node, TriggerTermInfo>& tinfo,
404		options::TriggerSelMode tstrt,
405		bool filterInst)
406		{
407	43114	std::map<Node, std::vector<Node> > visited;
408	21562	if (filterInst)
409		{
410		// immediately do not consider any term t for which another term is an
411		// instance of t
412	21552	std::vector<Node> patTerms2;
413	21552	std::map<Node, TriggerTermInfo> tinfo2;
414	10781	collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
415	21552	std::vector<Node> temp;
416	10781	temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
417	10781	filterInstances(temp);
418	10781	if (Trace.isOn("trigger-filter-instance"))
419		{
420		if (temp.size() != patTerms2.size())
421		{
422		Trace("trigger-filter-instance")
423		<< "Filtered an instance: " << std::endl;
424		Trace("trigger-filter-instance") << "Old: ";
425		for (unsigned i = 0; i < patTerms2.size(); i++)
426		{
427		Trace("trigger-filter-instance") << patTerms2[i] << " ";
428		}
429		Trace("trigger-filter-instance") << std::endl << "New: ";
430		for (unsigned i = 0; i < temp.size(); i++)
431		{
432		Trace("trigger-filter-instance") << temp[i] << " ";
433		}
434		Trace("trigger-filter-instance") << std::endl;
435		}
436		}
437	10781	if (tstrt == options::TriggerSelMode::ALL)
438		{
439	14	for (const Node& t : temp)
440		{
441		// copy information
442	8	tinfo[t].d_fv.insert(
443	8	tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
444	4	tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
445	4	tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
446	4	patTerms.push_back(t);
447		}
448	10	return;
449		}
450		// do not consider terms that have instances
451	58536	for (const Node& t : patTerms2)
452		{
453	47765	if (std::find(temp.begin(), temp.end(), t) == temp.end())
454		{
455	3534	visited[t].clear();
456		}
457		}
458		}
459	43104	std::vector<Node> added;
460	21552	collectTermsInternal(
461		n, visited, tinfo, tstrt, added, true, true, false, true);
462	107521	for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
463		{
464	85969	patTerms.push_back(t.first);
465		}
466		}
467
468	160705	int PatternTermSelector::isInstanceOf(Node n1,
469		Node n2,
470		const std::vector<Node>& fv1,
471		const std::vector<Node>& fv2)
472		{
473	160705	Assert(n1 != n2);
474	160705	int status = 0;
475	321410	std::unordered_set<TNode> subs_vars;
476		std::unordered_set<
477		std::pair<TNode, TNode>,
478		PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>>
479	321410	visited;
480	321410	std::vector<std::pair<TNode, TNode> > visit;
481	321410	std::pair<TNode, TNode> cur;
482	321410	TNode cur1;
483	321410	TNode cur2;
484	160705	visit.push_back(std::pair<TNode, TNode>(n1, n2));
485	33551	do
486		{
487	194256	cur = visit.back();
488	194256	visit.pop_back();
489	194256	if (visited.find(cur) != visited.end())
490		{
491	4804	continue;
492		}
493	189452	visited.insert(cur);
494	189452	cur1 = cur.first;
495	189452	cur2 = cur.second;
496	189452	Assert(cur1 != cur2);
497		// recurse if they have the same operator
498	550100	if (cur1.hasOperator() && cur2.hasOperator()
499	168217	&& cur1.getNumChildren() == cur2.getNumChildren()
500	294441	&& cur1.getOperator() == cur2.getOperator()
501	405170	&& cur1.getOperator().getKind() != INST_CONSTANT)
502		{
503	26218	visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
504	78127	for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
505		{
506	51934	if (cur1[i] != cur2[i])
507		{
508	37388	visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
509		}
510	14546	else if (cur1[i].getKind() == INST_CONSTANT)
511		{
512	5338	if (subs_vars.find(cur1[i]) != subs_vars.end())
513		{
514	25	return 0;
515		}
516		// the variable must map to itself in the substitution
517	5313	subs_vars.insert(cur1[i]);
518		}
519		}
520	26193	continue;
521		}
522	163234	bool success = false;
523		// check if we are in a unifiable instance case
524		// must be only this case
525	479400	for (unsigned r = 0; r < 2; r++)
526		{
527	322254	if (status == 0 \|\| ((status == 1) == (r == 0)))
528		{
529	634058	TNode curi = r == 0 ? cur1 : cur2;
530	640146	if (curi.getKind() == INST_CONSTANT
531	320073	&& subs_vars.find(curi) == subs_vars.end())
532		{
533	50784	TNode curj = r == 0 ? cur2 : cur1;
534		// RHS must be a simple trigger
535	28436	if (TriggerTermInfo::getTriggerWeight(curj) == 0)
536		{
537		// must occur in the free variables in the other
538	7681	const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
539	23043	if (std::find(free_vars.begin(), free_vars.end(), curi)
540	23043	!= free_vars.end())
541		{
542	6088	status = r == 0 ? 1 : -1;
543	6088	subs_vars.insert(curi);
544	6088	success = true;
545	6088	break;
546		}
547		}
548		}
549		}
550		}
551	163234	if (!success)
552		{
553	157146	return 0;
554		}
555	37085	} while (!visit.empty());
556	3534	return status;
557		}
558
559	10781	void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
560		{
561	21562	std::map<unsigned, std::vector<Node> > fvs;
562	58550	for (size_t i = 0, size = nodes.size(); i < size; i++)
563		{
564	47769	quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
565		}
566	21562	std::vector<bool> active;
567	10781	active.resize(nodes.size(), true);
568	58550	for (size_t i = 0, size = nodes.size(); i < size; i++)
569		{
570	47769	std::vector<Node>& fvsi = fvs[i];
571	47769	if (!active[i])
572		{
573	1510	continue;
574		}
575	205990	for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
576		{
577	161755	if (!active[j])
578		{
579	1050	continue;
580		}
581	160705	int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
582	160705	if (result == 1)
583		{
584	4048	Trace("filter-instances")
585	2024	<< nodes[j] << " is an instance of " << nodes[i] << std::endl;
586	2024	active[i] = false;
587	2024	break;
588		}
589	158681	else if (result == -1)
590		{
591	3020	Trace("filter-instances")
592	1510	<< nodes[i] << " is an instance of " << nodes[j] << std::endl;
593	1510	active[j] = false;
594		}
595		}
596		}
597	21562	std::vector<Node> temp;
598	58550	for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
599		{
600	47769	if (active[i])
601		{
602	44235	temp.push_back(nodes[i]);
603		}
604		}
605	10781	nodes.clear();
606	10781	nodes.insert(nodes.begin(), temp.begin(), temp.end());
607	10781	}
608
609	335	Node PatternTermSelector::getInversionVariable(Node n)
610		{
611	335	Kind nk = n.getKind();
612	335	if (nk == INST_CONSTANT)
613		{
614	88	return n;
615		}
616	247	else if (nk == PLUS \|\| nk == MULT)
617		{
618	212	Node ret;
619	294	for (const Node& nc : n)
620		{
621	206	if (quantifiers::TermUtil::hasInstConstAttr(nc))
622		{
623	106	if (ret.isNull())
624		{
625	106	ret = getInversionVariable(nc);
626	106	if (ret.isNull())
627		{
628	36	Trace("var-trigger-debug")
629	18	<< "No : multiple variables " << n << std::endl;
630	18	return Node::null();
631		}
632		}
633		else
634		{
635		return Node::null();
636		}
637		}
638	100	else if (nk == MULT)
639		{
640	50	if (!nc.isConst())
641		{
642		Trace("var-trigger-debug")
643		<< "No : non-linear coefficient " << n << std::endl;
644		return Node::null();
645		}
646		}
647		}
648	88	return ret;
649		}
650	282	Trace("var-trigger-debug")
651	141	<< "No : unsupported operator " << n << "." << std::endl;
652	141	return Node::null();
653		}
654
655	16	Node PatternTermSelector::getInversion(Node n, Node x)
656		{
657	16	Kind nk = n.getKind();
658	16	if (nk == INST_CONSTANT)
659		{
660	8	return x;
661		}
662	8	else if (nk == PLUS \|\| nk == MULT)
663		{
664	8	NodeManager* nm = NodeManager::currentNM();
665	8	int cindex = -1;
666	8	bool cindexSet = false;
667	24	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
668		{
669	32	Node nc = n[i];
670	16	if (!quantifiers::TermUtil::hasInstConstAttr(nc))
671		{
672	8	if (nk == PLUS)
673		{
674	4	x = nm->mkNode(MINUS, x, nc);
675		}
676	4	else if (nk == MULT)
677		{
678	4	Assert(nc.isConst());
679	4	if (x.getType().isInteger())
680		{
681	8	Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
682	4	if (!nc.getConst<Rational>().abs().isOne())
683		{
684	4	x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
685		}
686	4	if (nc.getConst<Rational>().sgn() < 0)
687		{
688		x = nm->mkNode(UMINUS, x);
689		}
690		}
691		else
692		{
693		Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
694		x = nm->mkNode(MULT, x, coeff);
695		}
696		}
697	8	x = Rewriter::rewrite(x);
698		}
699		else
700		{
701	8	Assert(!cindexSet);
702	8	cindex = i;
703	8	cindexSet = true;
704		}
705		}
706	8	if (cindexSet)
707		{
708	8	return getInversion(n[cindex], x);
709		}
710		}
711		return Node::null();
712		}
713
714	10	void PatternTermSelector::getTriggerVariables(Node n,
715		Node q,
716		std::vector<Node>& tvars)
717		{
718	20	PatternTermSelector pts(q, options::TriggerSelMode::ALL);
719	20	std::vector<Node> patTerms;
720	20	std::map<Node, TriggerTermInfo> tinfo;
721		// collect all patterns from n
722	10	pts.collect(n, patTerms, tinfo);
723		// collect all variables from all patterns in patTerms, add to tvars
724	14	for (const Node& pat : patTerms)
725		{
726	4	quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
727		}
728	10	}
729
730		} // namespace inst
731		} // namespace quantifiers
732		} // namespace theory
733	28194	} // namespace cvc5