GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/trigger_term_info.cpp Lines: 42 42 100.0 %
Date: 2021-03-22 Branches: 102 134 76.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file trigger_term_info.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Yoni Zohar
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of trigger term info class
13
 **/
14
15
#include "theory/quantifiers/ematching/trigger_term_info.h"
16
17
#include "theory/quantifiers/term_util.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace inst {
24
25
89436
void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq)
26
{
27
89436
  if (d_fv.empty())
28
  {
29
89034
    quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv);
30
  }
31
89436
  if (d_reqPol == 0)
32
  {
33
89300
    d_reqPol = reqPol;
34
89300
    d_reqPolEq = reqPolEq;
35
  }
36
  else
37
  {
38
    // determined a ground (dis)equality must hold or else q is a tautology?
39
  }
40
89436
  d_weight = getTriggerWeight(n);
41
89436
}
42
43
3244246
bool TriggerTermInfo::isAtomicTrigger(Node n)
44
{
45
3244246
  return isAtomicTriggerKind(n.getKind());
46
}
47
48
11426510
bool TriggerTermInfo::isAtomicTriggerKind(Kind k)
49
{
50
  // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
51
  // method is used both for trigger selection and for ground term registration,
52
  // where these two things require those kinds respectively.
53
3637718
  return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
54
2143466
         || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL
55
2092449
         || k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET
56
2013095
         || k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO
57
1992077
         || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY
58
13410455
         || k == STRING_LENGTH || k == SEQ_NTH;
59
}
60
61
352807
bool TriggerTermInfo::isRelationalTrigger(Node n)
62
{
63
352807
  return isRelationalTriggerKind(n.getKind());
64
}
65
66
352807
bool TriggerTermInfo::isRelationalTriggerKind(Kind k)
67
{
68
352807
  return k == EQUAL || k == GEQ;
69
}
70
71
23042
bool TriggerTermInfo::isSimpleTrigger(Node n)
72
{
73
46084
  Node t = n.getKind() == NOT ? n[0] : n;
74
23042
  if (t.getKind() == EQUAL)
75
  {
76
2993
    if (!quantifiers::TermUtil::hasInstConstAttr(t[1]))
77
    {
78
2975
      t = t[0];
79
    }
80
  }
81
23042
  if (!isAtomicTrigger(t))
82
  {
83
82
    return false;
84
  }
85
58618
  for (const Node& tc : t)
86
  {
87
86572
    if (tc.getKind() != INST_CONSTANT
88
86572
        && quantifiers::TermUtil::hasInstConstAttr(tc))
89
    {
90
7628
      return false;
91
    }
92
  }
93
15332
  if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
94
  {
95
12
    return false;
96
  }
97
15320
  return true;
98
}
99
100
164687
int32_t TriggerTermInfo::getTriggerWeight(Node n)
101
{
102
164687
  if (n.getKind() == APPLY_UF)
103
  {
104
132414
    return 0;
105
  }
106
32273
  if (isAtomicTrigger(n))
107
  {
108
9495
    return 1;
109
  }
110
22778
  return 2;
111
}
112
113
}  // namespace inst
114
}  // namespace theory
115
26676
}  // namespace CVC4