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-09-07	Branches:	766	1534	49.9 %


/******************************************************************************
 * 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"
#include "util/rational.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		#include "util/rational.h"
24
25		using namespace cvc5::kind;
26
27		namespace cvc5 {
28		namespace theory {
29		namespace quantifiers {
30		namespace inst {
31
32	10659	PatternTermSelector::PatternTermSelector(Node q,
33		options::TriggerSelMode tstrt,
34		const std::vector<Node>& exc,
35	10659	bool filterInst)
36	10659	: d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
37		{
38	10659	}
39
40	10659	PatternTermSelector::~PatternTermSelector() {}
41
42	2117693	bool PatternTermSelector::isUsable(Node n, Node q)
43		{
44	2117693	if (quantifiers::TermUtil::getInstConstAttr(n) != q)
45		{
46	277884	return true;
47		}
48	1839809	if (TriggerTermInfo::isAtomicTrigger(n))
49		{
50	2488144	for (const Node& nc : n)
51		{
52	1659432	if (!isUsable(nc, q))
53		{
54	8576	return false;
55		}
56		}
57	828712	return true;
58		}
59	1002521	else if (n.getKind() == INST_CONSTANT)
60		{
61	972370	return true;
62		}
63	60302	std::map<Node, Node> coeffs;
64	30151	if (options::purifyTriggers())
65		{
66	204	Node x = getInversionVariable(n);
67	142	if (!x.isNull())
68		{
69	80	return true;
70		}
71		}
72	30071	return false;
73		}
74
75	38321	Node PatternTermSelector::getIsUsableEq(Node q, Node n)
76		{
77	38321	Assert(TriggerTermInfo::isRelationalTrigger(n));
78	99803	for (size_t i = 0; i < 2; i++)
79		{
80	73245	if (isUsableEqTerms(q, n[i], n[1 - i]))
81		{
82	20129	if (i == 1 && n.getKind() == EQUAL
83	20101	&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
84		{
85	8094	return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]);
86		}
87		else
88		{
89	3669	return n;
90		}
91		}
92		}
93	26558	return Node::null();
94		}
95
96	73245	bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
97		{
98	73245	if (n1.getKind() == INST_CONSTANT)
99		{
100	13585	if (options::relationalTriggers())
101		{
102	3075	Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
103	2465	if (q1 != q)
104		{
105		// x is a variable from another quantified formula, fail
106		return false;
107		}
108	3075	Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
109	2465	if (q2.isNull())
110		{
111		// x = c
112	1460	return true;
113		}
114	1005	if (n2.getKind() == INST_CONSTANT && q2 == q)
115		{
116		// x = y
117	395	return true;
118		}
119		// we dont check x = f(y), which is handled symmetrically below
120		// when n1 and n2 are swapped
121		}
122		}
123	59660	else if (isUsableAtomicTrigger(n1, q))
124		{
125	65358	if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
126	31432	&& quantifiers::TermUtil::getInstConstAttr(n2) == q
127	62278	&& !expr::hasSubterm(n1, n2))
128		{
129		// f(x) = y
130	244	return true;
131		}
132	30602	else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
133		{
134		// f(x) = c
135	9664	return true;
136		}
137		}
138	61482	return false;
139		}
140
141	279450	Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
142		{
143	279450	bool pol = true;
144	279450	Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
145	279450	if (n.getKind() == NOT)
146		{
147		pol = !pol;
148		n = n[0];
149		}
150	279450	NodeManager* nm = NodeManager::currentNM();
151	279450	if (n.getKind() == INST_CONSTANT)
152		{
153	12	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
154		}
155	279438	else if (TriggerTermInfo::isRelationalTrigger(n))
156		{
157	69270	Node rtr = getIsUsableEq(q, n);
158	34635	if (rtr.isNull() && n[0].getType().isReal())
159		{
160		// try to solve relation
161	18964	std::map<Node, Node> m;
162	9482	if (ArithMSum::getMonomialSumLit(n, m))
163		{
164	22114	for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
165		{
166	16330	bool trySolve = false;
167	16330	if (!it->first.isNull())
168		{
169	14468	if (it->first.getKind() == INST_CONSTANT)
170		{
171	8214	trySolve = options::relationalTriggers();
172		}
173	6254	else if (isUsableTrigger(it->first, q))
174		{
175	3674	trySolve = true;
176		}
177		}
178	16330	if (trySolve)
179		{
180	7396	Trace("trigger-debug")
181	3698	<< "Try to solve for " << it->first << std::endl;
182	7396	Node veq;
183	3698	if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
184		{
185	3686	rtr = getIsUsableEq(q, veq);
186		}
187		// either all solves will succeed or all solves will fail
188	3698	break;
189		}
190		}
191		}
192		}
193	34635	if (!rtr.isNull())
194		{
195	11763	Trace("relational-trigger") << "Relational trigger : " << std::endl;
196	23526	Trace("relational-trigger")
197	11763	<< " " << rtr << " (from " << n << ")" << std::endl;
198	11763	Trace("relational-trigger") << " in quantifier " << q << std::endl;
199	23526	Node rtr2 = pol ? rtr : rtr.negate();
200	11763	Trace("relational-trigger") << " return : " << rtr2 << std::endl;
201	11763	return rtr2;
202		}
203	22872	return Node::null();
204		}
205	489606	Trace("trigger-debug") << n << " usable : "
206	489606	<< (quantifiers::TermUtil::getInstConstAttr(n) == q)
207	489606	<< " " << TriggerTermInfo::isAtomicTrigger(n) << " "
208	244803	<< isUsable(n, q) << std::endl;
209	244803	if (isUsableAtomicTrigger(n, q))
210		{
211	179248	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
212		}
213	65555	return Node::null();
214		}
215
216	304463	bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
217		{
218	913389	return quantifiers::TermUtil::getInstConstAttr(n) == q
219	1217852	&& TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
220		}
221
222	97864	bool PatternTermSelector::isUsableTrigger(Node n, Node q)
223		{
224	195728	Node nu = getIsUsableTrigger(n, q);
225	195728	return !nu.isNull();
226		}
227
228		// store triggers in reqPol, indicating their polarity (if any) they must appear
229		// to falsify the quantified formula
230	450744	void PatternTermSelector::collectTermsInternal(
231		Node n,
232		std::map<Node, std::vector<Node> >& visited,
233		std::map<Node, TriggerTermInfo>& tinfo,
234		options::TriggerSelMode tstrt,
235		std::vector<Node>& added,
236		bool pol,
237		bool hasPol,
238		bool epol,
239		bool hasEPol,
240		bool knowIsUsable)
241		{
242	450744	std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
243	450744	if (itv != visited.end())
244		{
245		// already visited
246	198417	for (const Node& t : itv->second)
247		{
248	18452	if (std::find(added.begin(), added.end(), t) == added.end())
249		{
250	16791	added.push_back(t);
251		}
252		}
253	539099	return;
254		}
255	270779	visited[n].clear();
256	541558	Trace("auto-gen-trigger-debug2")
257	270779	<< "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
258	270779	<< " " << hasEPol << std::endl;
259	270779	Kind nk = n.getKind();
260	270779	if (nk == FORALL \|\| nk == INST_CONSTANT)
261		{
262		// do not traverse beneath quantified formulas
263	60999	return;
264		}
265	301390	Node nu;
266	209780	bool nu_single = false;
267	209780	if (knowIsUsable)
268		{
269	8118	nu = n;
270		}
271	201662	else if (nk != NOT
272	556530	&& std::find(d_excluded.begin(), d_excluded.end(), n)
273	556530	== d_excluded.end())
274		{
275	177434	nu = getIsUsableTrigger(n, d_quant);
276	177434	if (!nu.isNull() && nu != n)
277		{
278	8118	collectTermsInternal(
279		nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
280		// copy to n
281	8118	visited[n].insert(visited[n].end(), added.begin(), added.end());
282	8118	return;
283		}
284		}
285	201662	if (!nu.isNull())
286		{
287	91610	Assert(nu == n);
288	91610	Assert(nu.getKind() != NOT);
289	183220	Trace("auto-gen-trigger-debug2")
290	91610	<< "...found usable trigger : " << nu << std::endl;
291	183220	Node reqEq;
292	91610	if (nu.getKind() == EQUAL)
293		{
294	28782	if (TriggerTermInfo::isAtomicTrigger(nu[0])
295	28782	&& !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
296		{
297	8564	if (hasPol)
298		{
299	5730	reqEq = nu[1];
300		}
301	8564	nu = nu[0];
302		}
303		}
304	91610	Assert(reqEq.isNull() \|\| !quantifiers::TermUtil::hasInstConstAttr(reqEq));
305	91610	Assert(isUsableTrigger(nu, d_quant));
306	183220	Trace("auto-gen-trigger-debug2")
307	91610	<< "...add usable trigger : " << nu << std::endl;
308	91610	tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
309	91610	nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
310		}
311	293272	Node nrec = nu.isNull() ? n : nu;
312	293272	std::vector<Node> added2;
313	622980	for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
314		{
315		bool newHasPol, newPol;
316		bool newHasEPol, newEPol;
317	421318	QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
318	421318	QuantPhaseReq::getEntailPolarity(
319		nrec, i, hasEPol, epol, newHasEPol, newEPol);
320	421318	collectTermsInternal(nrec[i],
321		visited,
322		tinfo,
323		tstrt,
324		added2,
325		newPol,
326		newHasPol,
327		newEPol,
328		newHasEPol);
329		}
330		// if this is not a usable trigger, don't worry about caching the results,
331		// since triggers do not contain non-usable subterms
332	201662	if (nu.isNull())
333		{
334	110052	return;
335		}
336	91610	bool rm_nu = false;
337	186370	for (size_t i = 0, asize = added2.size(); i < asize; i++)
338		{
339	189520	Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
340	94760	<< " : " << added2[i] << std::endl;
341	94760	Assert(added2[i] != nu);
342		// if child was not already removed
343	94760	if (tinfo.find(added2[i]) != tinfo.end())
344		{
345	94760	if (tstrt == options::TriggerSelMode::MAX
346	94760	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
347		{
348		// discard all subterms
349		// do not remove if it has smaller weight
350		if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
351		{
352		Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
353		visited[added2[i]].clear();
354		tinfo.erase(added2[i]);
355		}
356		}
357		else
358		{
359	94760	if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
360		{
361	17032	if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
362		{
363		// discard if we added a subterm as a trigger with all
364		// variables that nu has
365	30960	Trace("auto-gen-trigger-debug2")
366	15480	<< "......subsumes parent " << tinfo[nu].d_weight << " "
367	15480	<< tinfo[added2[i]].d_weight << "." << std::endl;
368	15480	rm_nu = true;
369		}
370		}
371	94760	if (std::find(added.begin(), added.end(), added2[i]) == added.end())
372		{
373	87981	added.push_back(added2[i]);
374		}
375		}
376		}
377		}
378	91610	if (rm_nu
379	13007	&& (tstrt == options::TriggerSelMode::MIN
380	6681	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
381		{
382	6326	tinfo.erase(nu);
383		}
384		else
385		{
386	85284	if (std::find(added.begin(), added.end(), nu) == added.end())
387		{
388	85276	added.push_back(nu);
389		}
390		}
391	91610	visited[n].insert(visited[n].end(), added.begin(), added.end());
392		}
393
394	10659	void PatternTermSelector::collect(Node n,
395		std::vector<Node>& patTerms,
396		std::map<Node, TriggerTermInfo>& tinfo)
397		{
398	10659	collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
399	10659	}
400
401	21318	void PatternTermSelector::collectInternal(
402		Node n,
403		std::vector<Node>& patTerms,
404		std::map<Node, TriggerTermInfo>& tinfo,
405		options::TriggerSelMode tstrt,
406		bool filterInst)
407		{
408	42626	std::map<Node, std::vector<Node> > visited;
409	21318	if (filterInst)
410		{
411		// immediately do not consider any term t for which another term is an
412		// instance of t
413	21308	std::vector<Node> patTerms2;
414	21308	std::map<Node, TriggerTermInfo> tinfo2;
415	10659	collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
416	21308	std::vector<Node> temp;
417	10659	temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
418	10659	filterInstances(temp);
419	10659	if (Trace.isOn("trigger-filter-instance"))
420		{
421		if (temp.size() != patTerms2.size())
422		{
423		Trace("trigger-filter-instance")
424		<< "Filtered an instance: " << std::endl;
425		Trace("trigger-filter-instance") << "Old: ";
426		for (unsigned i = 0; i < patTerms2.size(); i++)
427		{
428		Trace("trigger-filter-instance") << patTerms2[i] << " ";
429		}
430		Trace("trigger-filter-instance") << std::endl << "New: ";
431		for (unsigned i = 0; i < temp.size(); i++)
432		{
433		Trace("trigger-filter-instance") << temp[i] << " ";
434		}
435		Trace("trigger-filter-instance") << std::endl;
436		}
437		}
438	10659	if (tstrt == options::TriggerSelMode::ALL)
439		{
440	14	for (const Node& t : temp)
441		{
442		// copy information
443	8	tinfo[t].d_fv.insert(
444	8	tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
445	4	tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
446	4	tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
447	4	patTerms.push_back(t);
448		}
449	10	return;
450		}
451		// do not consider terms that have instances
452	57639	for (const Node& t : patTerms2)
453		{
454	46990	if (std::find(temp.begin(), temp.end(), t) == temp.end())
455		{
456	2993	visited[t].clear();
457		}
458		}
459		}
460	42616	std::vector<Node> added;
461	21308	collectTermsInternal(
462		n, visited, tinfo, tstrt, added, true, true, false, true);
463	106110	for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
464		{
465	84802	patTerms.push_back(t.first);
466		}
467		}
468
469	159574	int PatternTermSelector::isInstanceOf(Node n1,
470		Node n2,
471		const std::vector<Node>& fv1,
472		const std::vector<Node>& fv2)
473		{
474	159574	Assert(n1 != n2);
475	159574	int status = 0;
476	319148	std::unordered_set<TNode> subs_vars;
477		std::unordered_set<
478		std::pair<TNode, TNode>,
479		PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>>
480	319148	visited;
481	319148	std::vector<std::pair<TNode, TNode> > visit;
482	319148	std::pair<TNode, TNode> cur;
483	319148	TNode cur1;
484	319148	TNode cur2;
485	159574	visit.push_back(std::pair<TNode, TNode>(n1, n2));
486	32061	do
487		{
488	191635	cur = visit.back();
489	191635	visit.pop_back();
490	191635	if (visited.find(cur) != visited.end())
491		{
492	4020	continue;
493		}
494	187615	visited.insert(cur);
495	187615	cur1 = cur.first;
496	187615	cur2 = cur.second;
497	187615	Assert(cur1 != cur2);
498		// recurse if they have the same operator
499	544400	if (cur1.hasOperator() && cur2.hasOperator()
500	166611	&& cur1.getNumChildren() == cur2.getNumChildren()
501	288448	&& cur1.getOperator() == cur2.getOperator()
502	401068	&& cur1.getOperator().getKind() != INST_CONSTANT)
503		{
504	25790	visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
505	77895	for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
506		{
507	52124	if (cur1[i] != cur2[i])
508		{
509	36979	visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
510		}
511	15145	else if (cur1[i].getKind() == INST_CONSTANT)
512		{
513	6577	if (subs_vars.find(cur1[i]) != subs_vars.end())
514		{
515	19	return 0;
516		}
517		// the variable must map to itself in the substitution
518	6558	subs_vars.insert(cur1[i]);
519		}
520		}
521	25771	continue;
522		}
523	161825	bool success = false;
524		// check if we are in a unifiable instance case
525		// must be only this case
526	476367	for (unsigned r = 0; r < 2; r++)
527		{
528	319805	if (status == 0 \|\| ((status == 1) == (r == 0)))
529		{
530	630429	TNode curi = r == 0 ? cur1 : cur2;
531	635692	if (curi.getKind() == INST_CONSTANT
532	317846	&& subs_vars.find(curi) == subs_vars.end())
533		{
534	48841	TNode curj = r == 0 ? cur2 : cur1;
535		// RHS must be a simple trigger
536	27052	if (TriggerTermInfo::getTriggerWeight(curj) == 0)
537		{
538		// must occur in the free variables in the other
539	6929	const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
540	20787	if (std::find(free_vars.begin(), free_vars.end(), curi)
541	20787	!= free_vars.end())
542		{
543	5263	status = r == 0 ? 1 : -1;
544	5263	subs_vars.insert(curi);
545	5263	success = true;
546	5263	break;
547		}
548		}
549		}
550		}
551		}
552	161825	if (!success)
553		{
554	156562	return 0;
555		}
556	35054	} while (!visit.empty());
557	2993	return status;
558		}
559
560	10659	void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
561		{
562	21318	std::map<unsigned, std::vector<Node> > fvs;
563	57653	for (size_t i = 0, size = nodes.size(); i < size; i++)
564		{
565	46994	quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
566		}
567	21318	std::vector<bool> active;
568	10659	active.resize(nodes.size(), true);
569	57653	for (size_t i = 0, size = nodes.size(); i < size; i++)
570		{
571	46994	std::vector<Node>& fvsi = fvs[i];
572	46994	if (!active[i])
573		{
574	1075	continue;
575		}
576	204212	for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
577		{
578	160211	if (!active[j])
579		{
580	637	continue;
581		}
582	159574	int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
583	159574	if (result == 1)
584		{
585	3836	Trace("filter-instances")
586	1918	<< nodes[j] << " is an instance of " << nodes[i] << std::endl;
587	1918	active[i] = false;
588	1918	break;
589		}
590	157656	else if (result == -1)
591		{
592	2150	Trace("filter-instances")
593	1075	<< nodes[i] << " is an instance of " << nodes[j] << std::endl;
594	1075	active[j] = false;
595		}
596		}
597		}
598	21318	std::vector<Node> temp;
599	57653	for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
600		{
601	46994	if (active[i])
602		{
603	44001	temp.push_back(nodes[i]);
604		}
605		}
606	10659	nodes.clear();
607	10659	nodes.insert(nodes.begin(), temp.begin(), temp.end());
608	10659	}
609
610	335	Node PatternTermSelector::getInversionVariable(Node n)
611		{
612	335	Kind nk = n.getKind();
613	335	if (nk == INST_CONSTANT)
614		{
615	88	return n;
616		}
617	247	else if (nk == PLUS \|\| nk == MULT)
618		{
619	212	Node ret;
620	294	for (const Node& nc : n)
621		{
622	206	if (quantifiers::TermUtil::hasInstConstAttr(nc))
623		{
624	106	if (ret.isNull())
625		{
626	106	ret = getInversionVariable(nc);
627	106	if (ret.isNull())
628		{
629	36	Trace("var-trigger-debug")
630	18	<< "No : multiple variables " << n << std::endl;
631	18	return Node::null();
632		}
633		}
634		else
635		{
636		return Node::null();
637		}
638		}
639	100	else if (nk == MULT)
640		{
641	50	if (!nc.isConst())
642		{
643		Trace("var-trigger-debug")
644		<< "No : non-linear coefficient " << n << std::endl;
645		return Node::null();
646		}
647		}
648		}
649	88	return ret;
650		}
651	282	Trace("var-trigger-debug")
652	141	<< "No : unsupported operator " << n << "." << std::endl;
653	141	return Node::null();
654		}
655
656	16	Node PatternTermSelector::getInversion(Node n, Node x)
657		{
658	16	Kind nk = n.getKind();
659	16	if (nk == INST_CONSTANT)
660		{
661	8	return x;
662		}
663	8	else if (nk == PLUS \|\| nk == MULT)
664		{
665	8	NodeManager* nm = NodeManager::currentNM();
666	8	int cindex = -1;
667	8	bool cindexSet = false;
668	24	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
669		{
670	32	Node nc = n[i];
671	16	if (!quantifiers::TermUtil::hasInstConstAttr(nc))
672		{
673	8	if (nk == PLUS)
674		{
675	4	x = nm->mkNode(MINUS, x, nc);
676		}
677	4	else if (nk == MULT)
678		{
679	4	Assert(nc.isConst());
680	4	if (x.getType().isInteger())
681		{
682	8	Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
683	4	if (!nc.getConst<Rational>().abs().isOne())
684		{
685	4	x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
686		}
687	4	if (nc.getConst<Rational>().sgn() < 0)
688		{
689		x = nm->mkNode(UMINUS, x);
690		}
691		}
692		else
693		{
694		Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
695		x = nm->mkNode(MULT, x, coeff);
696		}
697		}
698	8	x = Rewriter::rewrite(x);
699		}
700		else
701		{
702	8	Assert(!cindexSet);
703	8	cindex = i;
704	8	cindexSet = true;
705		}
706		}
707	8	if (cindexSet)
708		{
709	8	return getInversion(n[cindex], x);
710		}
711		}
712		return Node::null();
713		}
714
715	10	void PatternTermSelector::getTriggerVariables(Node n,
716		Node q,
717		std::vector<Node>& tvars)
718		{
719	20	PatternTermSelector pts(q, options::TriggerSelMode::ALL);
720	20	std::vector<Node> patTerms;
721	20	std::map<Node, TriggerTermInfo> tinfo;
722		// collect all patterns from n
723	10	pts.collect(n, patTerms, tinfo);
724		// collect all variables from all patterns in patTerms, add to tvars
725	14	for (const Node& pat : patTerms)
726		{
727	4	quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
728		}
729	10	}
730
731		} // namespace inst
732		} // namespace quantifiers
733		} // namespace theory
734	29502	} // namespace cvc5