Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/ematching/pattern_term_selector.cpp	Lines:	334	359	93.0 %
Date:	2021-11-07	Branches:	761	1524	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;
  }
  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(EQUAL, 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	11120	PatternTermSelector::PatternTermSelector(Node q,
33		options::TriggerSelMode tstrt,
34		const std::vector<Node>& exc,
35	11120	bool filterInst)
36	11120	: d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
37		{
38	11120	}
39
40	11120	PatternTermSelector::~PatternTermSelector() {}
41
42	2194091	bool PatternTermSelector::isUsable(Node n, Node q)
43		{
44	2194091	if (quantifiers::TermUtil::getInstConstAttr(n) != q)
45		{
46	282226	return true;
47		}
48	1911865	if (TriggerTermInfo::isAtomicTrigger(n))
49		{
50	2567474	for (const Node& nc : n)
51		{
52	1721558	if (!isUsable(nc, q))
53		{
54	8704	return false;
55		}
56		}
57	845916	return true;
58		}
59	1057245	else if (n.getKind() == INST_CONSTANT)
60		{
61	1025912	return true;
62		}
63	31333	if (options::purifyTriggers())
64		{
65	204	Node x = getInversionVariable(n);
66	142	if (!x.isNull())
67		{
68	80	return true;
69		}
70		}
71	31253	return false;
72		}
73
74	40805	Node PatternTermSelector::getIsUsableEq(Node q, Node n)
75		{
76	40805	Assert(TriggerTermInfo::isRelationalTrigger(n));
77	106839	for (size_t i = 0; i < 2; i++)
78		{
79	78135	if (isUsableEqTerms(q, n[i], n[1 - i]))
80		{
81	20727	if (i == 1 && n.getKind() == EQUAL
82	20699	&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
83		{
84	8354	return NodeManager::currentNM()->mkNode(EQUAL, n[1], n[0]);
85		}
86		else
87		{
88	3747	return n;
89		}
90		}
91		}
92	28704	return Node::null();
93		}
94
95	78135	bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
96		{
97	78135	if (n1.getKind() == INST_CONSTANT)
98		{
99	15067	if (options::relationalTriggers())
100		{
101	3107	Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
102	2497	if (q1 != q)
103		{
104		// x is a variable from another quantified formula, fail
105		return false;
106		}
107	3107	Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
108	2497	if (q2.isNull())
109		{
110		// x = c
111	1492	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	63068	else if (isUsableAtomicTrigger(n1, q))
123		{
124	68958	if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
125	33232	&& quantifiers::TermUtil::getInstConstAttr(n2) == q
126	65878	&& !expr::hasSubterm(n1, n2))
127		{
128		// f(x) = y
129	244	return true;
130		}
131	32402	else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
132		{
133		// f(x) = c
134	9970	return true;
135		}
136		}
137	66034	return false;
138		}
139
140	289574	Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
141		{
142	289574	bool pol = true;
143	289574	Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
144	289574	if (n.getKind() == NOT)
145		{
146		pol = !pol;
147		n = n[0];
148		}
149	289574	NodeManager* nm = NodeManager::currentNM();
150	289574	if (n.getKind() == INST_CONSTANT)
151		{
152	12	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
153		}
154	289562	else if (TriggerTermInfo::isRelationalTrigger(n))
155		{
156	73966	Node rtr = getIsUsableEq(q, n);
157	36983	if (rtr.isNull() && n[0].getType().isReal())
158		{
159		// try to solve relation
160	20788	std::map<Node, Node> m;
161	10394	if (ArithMSum::getMonomialSumLit(n, m))
162		{
163	24638	for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
164		{
165	18078	bool trySolve = false;
166	18078	if (!it->first.isNull())
167		{
168	15644	if (it->first.getKind() == INST_CONSTANT)
169		{
170	9066	trySolve = options::relationalTriggers();
171		}
172	6578	else if (isUsableTrigger(it->first, q))
173		{
174	3810	trySolve = true;
175		}
176		}
177	18078	if (trySolve)
178		{
179	7668	Trace("trigger-debug")
180	3834	<< "Try to solve for " << it->first << std::endl;
181	7668	Node veq;
182	3834	if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
183		{
184	3822	rtr = getIsUsableEq(q, veq);
185		}
186		// either all solves will succeed or all solves will fail
187	3834	break;
188		}
189		}
190		}
191		}
192	36983	if (!rtr.isNull())
193		{
194	12101	Trace("relational-trigger") << "Relational trigger : " << std::endl;
195	24202	Trace("relational-trigger")
196	12101	<< " " << rtr << " (from " << n << ")" << std::endl;
197	12101	Trace("relational-trigger") << " in quantifier " << q << std::endl;
198	24202	Node rtr2 = pol ? rtr : rtr.negate();
199	12101	Trace("relational-trigger") << " return : " << rtr2 << std::endl;
200	12101	return rtr2;
201		}
202	24882	return Node::null();
203		}
204	505158	Trace("trigger-debug") << n << " usable : "
205	505158	<< (quantifiers::TermUtil::getInstConstAttr(n) == q)
206	505158	<< " " << TriggerTermInfo::isAtomicTrigger(n) << " "
207	252579	<< isUsable(n, q) << std::endl;
208	252579	if (isUsableAtomicTrigger(n, q))
209		{
210	183876	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
211		}
212	68703	return Node::null();
213		}
214
215	315647	bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
216		{
217	946941	return quantifiers::TermUtil::getInstConstAttr(n) == q
218	1262588	&& TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
219		}
220
221	100595	bool PatternTermSelector::isUsableTrigger(Node n, Node q)
222		{
223	201190	Node nu = getIsUsableTrigger(n, q);
224	201190	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	464739	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	464739	std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
242	464739	if (itv != visited.end())
243		{
244		// already visited
245	202519	for (const Node& t : itv->second)
246		{
247	19407	if (std::find(added.begin(), added.end(), t) == added.end())
248		{
249	17746	added.push_back(t);
250		}
251		}
252	553834	return;
253		}
254	281627	visited[n].clear();
255	563254	Trace("auto-gen-trigger-debug2")
256	281627	<< "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
257	281627	<< " " << hasEPol << std::endl;
258	281627	Kind nk = n.getKind();
259	281627	if (nk == FORALL \|\| nk == INST_CONSTANT)
260		{
261		// do not traverse beneath quantified formulas
262	63776	return;
263		}
264	311868	Node nu;
265	217851	bool nu_single = false;
266	217851	if (knowIsUsable)
267		{
268	8386	nu = n;
269		}
270	209465	else if (nk != NOT
271	579079	&& std::find(d_excluded.begin(), d_excluded.end(), n)
272	579079	== d_excluded.end())
273		{
274	184807	nu = getIsUsableTrigger(n, d_quant);
275	184807	if (!nu.isNull() && nu != n)
276		{
277	8386	collectTermsInternal(
278		nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
279		// copy to n
280	8386	visited[n].insert(visited[n].end(), added.begin(), added.end());
281	8386	return;
282		}
283		}
284	209465	if (!nu.isNull())
285		{
286	94017	Assert(nu == n);
287	94017	Assert(nu.getKind() != NOT);
288	188034	Trace("auto-gen-trigger-debug2")
289	94017	<< "...found usable trigger : " << nu << std::endl;
290	188034	Node reqEq;
291	94017	if (nu.getKind() == EQUAL)
292		{
293	29592	if (TriggerTermInfo::isAtomicTrigger(nu[0])
294	29592	&& !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
295		{
296	8826	if (hasPol)
297		{
298	5960	reqEq = nu[1];
299		}
300	8826	nu = nu[0];
301		}
302		}
303	94017	Assert(reqEq.isNull() \|\| !quantifiers::TermUtil::hasInstConstAttr(reqEq));
304	94017	Assert(isUsableTrigger(nu, d_quant));
305	188034	Trace("auto-gen-trigger-debug2")
306	94017	<< "...add usable trigger : " << nu << std::endl;
307	94017	tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
308	94017	nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
309		}
310	303482	Node nrec = nu.isNull() ? n : nu;
311	303482	std::vector<Node> added2;
312	643590	for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
313		{
314		bool newHasPol, newPol;
315		bool newHasEPol, newEPol;
316	434125	QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
317	434125	QuantPhaseReq::getEntailPolarity(
318		nrec, i, hasEPol, epol, newHasEPol, newEPol);
319	434125	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	209465	if (nu.isNull())
332		{
333	115448	return;
334		}
335	94017	bool rm_nu = false;
336	189914	for (size_t i = 0, asize = added2.size(); i < asize; i++)
337		{
338	191794	Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
339	95897	<< " : " << added2[i] << std::endl;
340	95897	Assert(added2[i] != nu);
341		// if child was not already removed
342	95897	if (tinfo.find(added2[i]) != tinfo.end())
343		{
344	95897	if (tstrt == options::TriggerSelMode::MAX
345	95897	\|\| (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	95897	if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
359		{
360	17410	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	31732	Trace("auto-gen-trigger-debug2")
365	15866	<< "......subsumes parent " << tinfo[nu].d_weight << " "
366	15866	<< tinfo[added2[i]].d_weight << "." << std::endl;
367	15866	rm_nu = true;
368		}
369		}
370	95897	if (std::find(added.begin(), added.end(), added2[i]) == added.end())
371		{
372	89071	added.push_back(added2[i]);
373		}
374		}
375		}
376		}
377	94017	if (rm_nu
378	13360	&& (tstrt == options::TriggerSelMode::MIN
379	6866	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
380		{
381	6494	tinfo.erase(nu);
382		}
383		else
384		{
385	87523	if (std::find(added.begin(), added.end(), nu) == added.end())
386		{
387	87507	added.push_back(nu);
388		}
389		}
390	94017	visited[n].insert(visited[n].end(), added.begin(), added.end());
391		}
392
393	11120	void PatternTermSelector::collect(Node n,
394		std::vector<Node>& patTerms,
395		std::map<Node, TriggerTermInfo>& tinfo)
396		{
397	11120	collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
398	11120	}
399
400	22240	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	44468	std::map<Node, std::vector<Node> > visited;
408	22240	if (filterInst)
409		{
410		// immediately do not consider any term t for which another term is an
411		// instance of t
412	22228	std::vector<Node> patTerms2;
413	22228	std::map<Node, TriggerTermInfo> tinfo2;
414	11120	collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
415	22228	std::vector<Node> temp;
416	11120	temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
417	11120	filterInstances(temp);
418	11120	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	11120	if (tstrt == options::TriggerSelMode::ALL)
438		{
439	18	for (const Node& t : temp)
440		{
441		// copy information
442	12	tinfo[t].d_fv.insert(
443	12	tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
444	6	tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
445	6	tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
446	6	patTerms.push_back(t);
447		}
448	12	return;
449		}
450		// do not consider terms that have instances
451	59339	for (const Node& t : patTerms2)
452		{
453	48231	if (std::find(temp.begin(), temp.end(), t) == temp.end())
454		{
455	3082	visited[t].clear();
456		}
457		}
458		}
459	44456	std::vector<Node> added;
460	22228	collectTermsInternal(
461		n, visited, tinfo, tstrt, added, true, true, false, true);
462	109257	for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
463		{
464	87029	patTerms.push_back(t.first);
465		}
466		}
467
468	161131	int PatternTermSelector::isInstanceOf(Node n1,
469		Node n2,
470		const std::vector<Node>& fv1,
471		const std::vector<Node>& fv2)
472		{
473	161131	Assert(n1 != n2);
474	161131	int status = 0;
475	322262	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	322262	visited;
480	322262	std::vector<std::pair<TNode, TNode> > visit;
481	322262	std::pair<TNode, TNode> cur;
482	322262	TNode cur1;
483	322262	TNode cur2;
484	161131	visit.push_back(std::pair<TNode, TNode>(n1, n2));
485	32409	do
486		{
487	193540	cur = visit.back();
488	193540	visit.pop_back();
489	193540	if (visited.find(cur) != visited.end())
490		{
491	4109	continue;
492		}
493	189431	visited.insert(cur);
494	189431	cur1 = cur.first;
495	189431	cur2 = cur.second;
496	189431	Assert(cur1 != cur2);
497		// recurse if they have the same operator
498	549663	if (cur1.hasOperator() && cur2.hasOperator()
499	168190	&& cur1.getNumChildren() == cur2.getNumChildren()
500	291188	&& cur1.getOperator() == cur2.getOperator()
501	404943	&& cur1.getOperator().getKind() != INST_CONSTANT)
502		{
503	26033	visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
504	78573	for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
505		{
506	52559	if (cur1[i] != cur2[i])
507		{
508	37247	visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
509		}
510	15312	else if (cur1[i].getKind() == INST_CONSTANT)
511		{
512	6706	if (subs_vars.find(cur1[i]) != subs_vars.end())
513		{
514	19	return 0;
515		}
516		// the variable must map to itself in the substitution
517	6687	subs_vars.insert(cur1[i]);
518		}
519		}
520	26014	continue;
521		}
522	163398	bool success = false;
523		// check if we are in a unifiable instance case
524		// must be only this case
525	480914	for (unsigned r = 0; r < 2; r++)
526		{
527	322884	if (status == 0 \|\| ((status == 1) == (r == 0)))
528		{
529	636450	TNode curi = r == 0 ? cur1 : cur2;
530	641818	if (curi.getKind() == INST_CONSTANT
531	320909	&& subs_vars.find(curi) == subs_vars.end())
532		{
533	49066	TNode curj = r == 0 ? cur2 : cur1;
534		// RHS must be a simple trigger
535	27217	if (TriggerTermInfo::getTriggerWeight(curj) == 0)
536		{
537		// must occur in the free variables in the other
538	7034	const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
539	21102	if (std::find(free_vars.begin(), free_vars.end(), curi)
540	21102	!= free_vars.end())
541		{
542	5368	status = r == 0 ? 1 : -1;
543	5368	subs_vars.insert(curi);
544	5368	success = true;
545	5368	break;
546		}
547		}
548		}
549		}
550		}
551	163398	if (!success)
552		{
553	158030	return 0;
554		}
555	35491	} while (!visit.empty());
556	3082	return status;
557		}
558
559	11120	void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
560		{
561	22240	std::map<unsigned, std::vector<Node> > fvs;
562	59357	for (size_t i = 0, size = nodes.size(); i < size; i++)
563		{
564	48237	quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
565		}
566	22240	std::vector<bool> active;
567	11120	active.resize(nodes.size(), true);
568	59357	for (size_t i = 0, size = nodes.size(); i < size; i++)
569		{
570	48237	std::vector<Node>& fvsi = fvs[i];
571	48237	if (!active[i])
572		{
573	1113	continue;
574		}
575	206923	for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
576		{
577	161768	if (!active[j])
578		{
579	637	continue;
580		}
581	161131	int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
582	161131	if (result == 1)
583		{
584	3938	Trace("filter-instances")
585	1969	<< nodes[j] << " is an instance of " << nodes[i] << std::endl;
586	1969	active[i] = false;
587	1969	break;
588		}
589	159162	else if (result == -1)
590		{
591	2226	Trace("filter-instances")
592	1113	<< nodes[i] << " is an instance of " << nodes[j] << std::endl;
593	1113	active[j] = false;
594		}
595		}
596		}
597	22240	std::vector<Node> temp;
598	59357	for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
599		{
600	48237	if (active[i])
601		{
602	45155	temp.push_back(nodes[i]);
603		}
604		}
605	11120	nodes.clear();
606	11120	nodes.insert(nodes.begin(), temp.begin(), temp.end());
607	11120	}
608
609	405	Node PatternTermSelector::getInversionVariable(Node n)
610		{
611	405	Kind nk = n.getKind();
612	405	if (nk == INST_CONSTANT)
613		{
614	88	return n;
615		}
616	317	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	422	Trace("var-trigger-debug")
651	211	<< "No : unsupported operator " << n << "." << std::endl;
652	211	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	12	void PatternTermSelector::getTriggerVariables(Node n,
715		Node q,
716		std::vector<Node>& tvars)
717		{
718	24	PatternTermSelector pts(q, options::TriggerSelMode::ALL);
719	24	std::vector<Node> patTerms;
720	24	std::map<Node, TriggerTermInfo> tinfo;
721		// collect all patterns from n
722	12	pts.collect(n, patTerms, tinfo);
723		// collect all variables from all patterns in patTerms, add to tvars
724	18	for (const Node& pat : patTerms)
725		{
726	6	quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
727		}
728	12	}
729
730		} // namespace inst
731		} // namespace quantifiers
732		} // namespace theory
733	31137	} // namespace cvc5