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-09-29	Branches:	760	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	4298	PatternTermSelector::PatternTermSelector(Node q,
33		options::TriggerSelMode tstrt,
34		const std::vector<Node>& exc,
35	4298	bool filterInst)
36	4298	: d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
37		{
38	4298	}
39
40	4298	PatternTermSelector::~PatternTermSelector() {}
41
42	810497	bool PatternTermSelector::isUsable(Node n, Node q)
43		{
44	810497	if (quantifiers::TermUtil::getInstConstAttr(n) != q)
45		{
46	122108	return true;
47		}
48	688389	if (TriggerTermInfo::isAtomicTrigger(n))
49		{
50	949764	for (const Node& nc : n)
51		{
52	631408	if (!isUsable(nc, q))
53		{
54	3926	return false;
55		}
56		}
57	318356	return true;
58		}
59	366107	else if (n.getKind() == INST_CONSTANT)
60		{
61	352016	return true;
62		}
63	14091	if (options::purifyTriggers())
64		{
65	52	Node x = getInversionVariable(n);
66	36	if (!x.isNull())
67		{
68	20	return true;
69		}
70		}
71	14071	return false;
72		}
73
74	14427	Node PatternTermSelector::getIsUsableEq(Node q, Node n)
75		{
76	14427	Assert(TriggerTermInfo::isRelationalTrigger(n));
77	38127	for (size_t i = 0; i < 2; i++)
78		{
79	27567	if (isUsableEqTerms(q, n[i], n[1 - i]))
80		{
81	6447	if (i == 1 && n.getKind() == EQUAL
82	6439	&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
83		{
84	2492	return NodeManager::currentNM()->mkNode(EQUAL, n[1], n[0]);
85		}
86		else
87		{
88	1375	return n;
89		}
90		}
91		}
92	10560	return Node::null();
93		}
94
95	27567	bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
96		{
97	27567	if (n1.getKind() == INST_CONSTANT)
98		{
99	5347	if (options::relationalTriggers())
100		{
101	1013	Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
102	811	if (q1 != q)
103		{
104		// x is a variable from another quantified formula, fail
105		return false;
106		}
107	1013	Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
108	811	if (q2.isNull())
109		{
110		// x = c
111	484	return true;
112		}
113	327	if (n2.getKind() == INST_CONSTANT && q2 == q)
114		{
115		// x = y
116	125	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	22220	else if (isUsableAtomicTrigger(n1, q))
123		{
124	23664	if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
125	11422	&& quantifiers::TermUtil::getInstConstAttr(n2) == q
126	22650	&& !expr::hasSubterm(n1, n2))
127		{
128		// f(x) = y
129	80	return true;
130		}
131	11148	else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
132		{
133		// f(x) = c
134	3178	return true;
135		}
136		}
137	23700	return false;
138		}
139
140	110248	Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
141		{
142	110248	bool pol = true;
143	110248	Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
144	110248	if (n.getKind() == NOT)
145		{
146		pol = !pol;
147		n = n[0];
148		}
149	110248	NodeManager* nm = NodeManager::currentNM();
150	110248	if (n.getKind() == INST_CONSTANT)
151		{
152	3	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
153		}
154	110245	else if (TriggerTermInfo::isRelationalTrigger(n))
155		{
156	26338	Node rtr = getIsUsableEq(q, n);
157	13169	if (rtr.isNull() && n[0].getType().isReal())
158		{
159		// try to solve relation
160	6352	std::map<Node, Node> m;
161	3176	if (ArithMSum::getMonomialSumLit(n, m))
162		{
163	7394	for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
164		{
165	5480	bool trySolve = false;
166	5480	if (!it->first.isNull())
167		{
168	4750	if (it->first.getKind() == INST_CONSTANT)
169		{
170	2696	trySolve = options::relationalTriggers();
171		}
172	2054	else if (isUsableTrigger(it->first, q))
173		{
174	1254	trySolve = true;
175		}
176		}
177	5480	if (trySolve)
178		{
179	2524	Trace("trigger-debug")
180	1262	<< "Try to solve for " << it->first << std::endl;
181	2524	Node veq;
182	1262	if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
183		{
184	1258	rtr = getIsUsableEq(q, veq);
185		}
186		// either all solves will succeed or all solves will fail
187	1262	break;
188		}
189		}
190		}
191		}
192	13169	if (!rtr.isNull())
193		{
194	3867	Trace("relational-trigger") << "Relational trigger : " << std::endl;
195	7734	Trace("relational-trigger")
196	3867	<< " " << rtr << " (from " << n << ")" << std::endl;
197	3867	Trace("relational-trigger") << " in quantifier " << q << std::endl;
198	7734	Node rtr2 = pol ? rtr : rtr.negate();
199	3867	Trace("relational-trigger") << " return : " << rtr2 << std::endl;
200	3867	return rtr2;
201		}
202	9302	return Node::null();
203		}
204	194152	Trace("trigger-debug") << n << " usable : "
205	194152	<< (quantifiers::TermUtil::getInstConstAttr(n) == q)
206	194152	<< " " << TriggerTermInfo::isAtomicTrigger(n) << " "
207	97076	<< isUsable(n, q) << std::endl;
208	97076	if (isUsableAtomicTrigger(n, q))
209		{
210	68913	return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
211		}
212	28163	return Node::null();
213		}
214
215	119296	bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
216		{
217	357888	return quantifiers::TermUtil::getInstConstAttr(n) == q
218	477184	&& TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
219		}
220
221	37170	bool PatternTermSelector::isUsableTrigger(Node n, Node q)
222		{
223	74340	Node nu = getIsUsableTrigger(n, q);
224	74340	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	214734	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	214734	std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
242	214734	if (itv != visited.end())
243		{
244		// already visited
245	113991	for (const Node& t : itv->second)
246		{
247	6444	if (std::find(added.begin(), added.end(), t) == added.end())
248		{
249	5871	added.push_back(t);
250		}
251		}
252	287165	return;
253		}
254	107187	visited[n].clear();
255	214374	Trace("auto-gen-trigger-debug2")
256	107187	<< "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
257	107187	<< " " << hasEPol << std::endl;
258	107187	Kind nk = n.getKind();
259	107187	if (nk == FORALL \|\| nk == INST_CONSTANT)
260		{
261		// do not traverse beneath quantified formulas
262	23673	return;
263		}
264	118630	Node nu;
265	83514	bool nu_single = false;
266	83514	if (knowIsUsable)
267		{
268	2500	nu = n;
269		}
270	81014	else if (nk != NOT
271	224562	&& std::find(d_excluded.begin(), d_excluded.end(), n)
272	224562	== d_excluded.end())
273		{
274	71774	nu = getIsUsableTrigger(n, d_quant);
275	71774	if (!nu.isNull() && nu != n)
276		{
277	2500	collectTermsInternal(
278		nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
279		// copy to n
280	2500	visited[n].insert(visited[n].end(), added.begin(), added.end());
281	2500	return;
282		}
283		}
284	81014	if (!nu.isNull())
285		{
286	35116	Assert(nu == n);
287	35116	Assert(nu.getKind() != NOT);
288	70232	Trace("auto-gen-trigger-debug2")
289	35116	<< "...found usable trigger : " << nu << std::endl;
290	70232	Node reqEq;
291	35116	if (nu.getKind() == EQUAL)
292		{
293	9444	if (TriggerTermInfo::isAtomicTrigger(nu[0])
294	9444	&& !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
295		{
296	2810	if (hasPol)
297		{
298	1862	reqEq = nu[1];
299		}
300	2810	nu = nu[0];
301		}
302		}
303	35116	Assert(reqEq.isNull() \|\| !quantifiers::TermUtil::hasInstConstAttr(reqEq));
304	35116	Assert(isUsableTrigger(nu, d_quant));
305	70232	Trace("auto-gen-trigger-debug2")
306	35116	<< "...add usable trigger : " << nu << std::endl;
307	35116	tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
308	35116	nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
309		}
310	116130	Node nrec = nu.isNull() ? n : nu;
311	116130	std::vector<Node> added2;
312	284660	for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
313		{
314		bool newHasPol, newPol;
315		bool newHasEPol, newEPol;
316	203646	QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
317	203646	QuantPhaseReq::getEntailPolarity(
318		nrec, i, hasEPol, epol, newHasEPol, newEPol);
319	203646	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	81014	if (nu.isNull())
332		{
333	45898	return;
334		}
335	35116	bool rm_nu = false;
336	71531	for (size_t i = 0, asize = added2.size(); i < asize; i++)
337		{
338	72830	Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
339	36415	<< " : " << added2[i] << std::endl;
340	36415	Assert(added2[i] != nu);
341		// if child was not already removed
342	36415	if (tinfo.find(added2[i]) != tinfo.end())
343		{
344	36415	if (tstrt == options::TriggerSelMode::MAX
345	36415	\|\| (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	36415	if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
359		{
360	6480	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	11996	Trace("auto-gen-trigger-debug2")
365	5998	<< "......subsumes parent " << tinfo[nu].d_weight << " "
366	5998	<< tinfo[added2[i]].d_weight << "." << std::endl;
367	5998	rm_nu = true;
368		}
369		}
370	36415	if (std::find(added.begin(), added.end(), added2[i]) == added.end())
371		{
372	34039	added.push_back(added2[i]);
373		}
374		}
375		}
376		}
377	35116	if (rm_nu
378	5070	&& (tstrt == options::TriggerSelMode::MIN
379	2616	\|\| (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
380		{
381	2454	tinfo.erase(nu);
382		}
383		else
384		{
385	32662	if (std::find(added.begin(), added.end(), nu) == added.end())
386		{
387	32662	added.push_back(nu);
388		}
389		}
390	35116	visited[n].insert(visited[n].end(), added.begin(), added.end());
391		}
392
393	4298	void PatternTermSelector::collect(Node n,
394		std::vector<Node>& patTerms,
395		std::map<Node, TriggerTermInfo>& tinfo)
396		{
397	4298	collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
398	4298	}
399
400	8596	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	17184	std::map<Node, std::vector<Node> > visited;
408	8596	if (filterInst)
409		{
410		// immediately do not consider any term t for which another term is an
411		// instance of t
412	8588	std::vector<Node> patTerms2;
413	8588	std::map<Node, TriggerTermInfo> tinfo2;
414	4298	collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
415	8588	std::vector<Node> temp;
416	4298	temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
417	4298	filterInstances(temp);
418	4298	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	4298	if (tstrt == options::TriggerSelMode::ALL)
438		{
439	12	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	8	return;
449		}
450		// do not consider terms that have instances
451	22404	for (const Node& t : patTerms2)
452		{
453	18114	if (std::find(temp.begin(), temp.end(), t) == temp.end())
454		{
455	1339	visited[t].clear();
456		}
457		}
458		}
459	17176	std::vector<Node> added;
460	8588	collectTermsInternal(
461		n, visited, tinfo, tstrt, added, true, true, false, true);
462	41072	for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
463		{
464	32484	patTerms.push_back(t.first);
465		}
466		}
467
468	59988	int PatternTermSelector::isInstanceOf(Node n1,
469		Node n2,
470		const std::vector<Node>& fv1,
471		const std::vector<Node>& fv2)
472		{
473	59988	Assert(n1 != n2);
474	59988	int status = 0;
475	119976	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	119976	visited;
480	119976	std::vector<std::pair<TNode, TNode> > visit;
481	119976	std::pair<TNode, TNode> cur;
482	119976	TNode cur1;
483	119976	TNode cur2;
484	59988	visit.push_back(std::pair<TNode, TNode>(n1, n2));
485	12823	do
486		{
487	72811	cur = visit.back();
488	72811	visit.pop_back();
489	72811	if (visited.find(cur) != visited.end())
490		{
491	1767	continue;
492		}
493	71044	visited.insert(cur);
494	71044	cur1 = cur.first;
495	71044	cur2 = cur.second;
496	71044	Assert(cur1 != cur2);
497		// recurse if they have the same operator
498	206019	if (cur1.hasOperator() && cur2.hasOperator()
499	62805	&& cur1.getNumChildren() == cur2.getNumChildren()
500	112824	&& cur1.getOperator() == cur2.getOperator()
501	152196	&& cur1.getOperator().getKind() != INST_CONSTANT)
502		{
503	10096	visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
504	30420	for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
505		{
506	20333	if (cur1[i] != cur2[i])
507		{
508	14344	visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
509		}
510	5989	else if (cur1[i].getKind() == INST_CONSTANT)
511		{
512	2577	if (subs_vars.find(cur1[i]) != subs_vars.end())
513		{
514	9	return 0;
515		}
516		// the variable must map to itself in the substitution
517	2568	subs_vars.insert(cur1[i]);
518		}
519		}
520	10087	continue;
521		}
522	60948	bool success = false;
523		// check if we are in a unifiable instance case
524		// must be only this case
525	178868	for (unsigned r = 0; r < 2; r++)
526		{
527	120228	if (status == 0 \|\| ((status == 1) == (r == 0)))
528		{
529	236492	TNode curi = r == 0 ? cur1 : cur2;
530	238800	if (curi.getKind() == INST_CONSTANT
531	119400	&& subs_vars.find(curi) == subs_vars.end())
532		{
533	18246	TNode curj = r == 0 ? cur2 : cur1;
534		// RHS must be a simple trigger
535	10277	if (TriggerTermInfo::getTriggerWeight(curj) == 0)
536		{
537		// must occur in the free variables in the other
538	2917	const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
539	8751	if (std::find(free_vars.begin(), free_vars.end(), curi)
540	8751	!= free_vars.end())
541		{
542	2308	status = r == 0 ? 1 : -1;
543	2308	subs_vars.insert(curi);
544	2308	success = true;
545	2308	break;
546		}
547		}
548		}
549		}
550		}
551	60948	if (!success)
552		{
553	58640	return 0;
554		}
555	14162	} while (!visit.empty());
556	1339	return status;
557		}
558
559	4298	void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
560		{
561	8596	std::map<unsigned, std::vector<Node> > fvs;
562	22416	for (size_t i = 0, size = nodes.size(); i < size; i++)
563		{
564	18118	quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
565		}
566	8596	std::vector<bool> active;
567	4298	active.resize(nodes.size(), true);
568	22416	for (size_t i = 0, size = nodes.size(); i < size; i++)
569		{
570	18118	std::vector<Node>& fvsi = fvs[i];
571	18118	if (!active[i])
572		{
573	483	continue;
574		}
575	77091	for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
576		{
577	60312	if (!active[j])
578		{
579	324	continue;
580		}
581	59988	int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
582	59988	if (result == 1)
583		{
584	1712	Trace("filter-instances")
585	856	<< nodes[j] << " is an instance of " << nodes[i] << std::endl;
586	856	active[i] = false;
587	856	break;
588		}
589	59132	else if (result == -1)
590		{
591	966	Trace("filter-instances")
592	483	<< nodes[i] << " is an instance of " << nodes[j] << std::endl;
593	483	active[j] = false;
594		}
595		}
596		}
597	8596	std::vector<Node> temp;
598	22416	for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
599		{
600	18118	if (active[i])
601		{
602	16779	temp.push_back(nodes[i]);
603		}
604		}
605	4298	nodes.clear();
606	4298	nodes.insert(nodes.begin(), temp.begin(), temp.end());
607	4298	}
608
609	86	Node PatternTermSelector::getInversionVariable(Node n)
610		{
611	86	Kind nk = n.getKind();
612	86	if (nk == INST_CONSTANT)
613		{
614	22	return n;
615		}
616	64	else if (nk == PLUS \|\| nk == MULT)
617		{
618	56	Node ret;
619	76	for (const Node& nc : n)
620		{
621	54	if (quantifiers::TermUtil::hasInstConstAttr(nc))
622		{
623	28	if (ret.isNull())
624		{
625	28	ret = getInversionVariable(nc);
626	28	if (ret.isNull())
627		{
628	12	Trace("var-trigger-debug")
629	6	<< "No : multiple variables " << n << std::endl;
630	6	return Node::null();
631		}
632		}
633		else
634		{
635		return Node::null();
636		}
637		}
638	26	else if (nk == MULT)
639		{
640	13	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	22	return ret;
649		}
650	72	Trace("var-trigger-debug")
651	36	<< "No : unsupported operator " << n << "." << std::endl;
652	36	return Node::null();
653		}
654
655	4	Node PatternTermSelector::getInversion(Node n, Node x)
656		{
657	4	Kind nk = n.getKind();
658	4	if (nk == INST_CONSTANT)
659		{
660	2	return x;
661		}
662	2	else if (nk == PLUS \|\| nk == MULT)
663		{
664	2	NodeManager* nm = NodeManager::currentNM();
665	2	int cindex = -1;
666	2	bool cindexSet = false;
667	6	for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
668		{
669	8	Node nc = n[i];
670	4	if (!quantifiers::TermUtil::hasInstConstAttr(nc))
671		{
672	2	if (nk == PLUS)
673		{
674	1	x = nm->mkNode(MINUS, x, nc);
675		}
676	1	else if (nk == MULT)
677		{
678	1	Assert(nc.isConst());
679	1	if (x.getType().isInteger())
680		{
681	2	Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
682	1	if (!nc.getConst<Rational>().abs().isOne())
683		{
684	1	x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
685		}
686	1	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	2	x = Rewriter::rewrite(x);
698		}
699		else
700		{
701	2	Assert(!cindexSet);
702	2	cindex = i;
703	2	cindexSet = true;
704		}
705		}
706	2	if (cindexSet)
707		{
708	2	return getInversion(n[cindex], x);
709		}
710		}
711		return Node::null();
712		}
713
714	8	void PatternTermSelector::getTriggerVariables(Node n,
715		Node q,
716		std::vector<Node>& tvars)
717		{
718	16	PatternTermSelector pts(q, options::TriggerSelMode::ALL);
719	16	std::vector<Node> patTerms;
720	16	std::map<Node, TriggerTermInfo> tinfo;
721		// collect all patterns from n
722	8	pts.collect(n, patTerms, tinfo);
723		// collect all variables from all patterns in patTerms, add to tvars
724	12	for (const Node& pat : patTerms)
725		{
726	4	quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
727		}
728	8	}
729
730		} // namespace inst
731		} // namespace quantifiers
732		} // namespace theory
733	22746	} // namespace cvc5