GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/nested_qe.cpp Lines: 70 78 89.7 %
Date: 2021-03-23 Branches: 146 328 44.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file nested_qe.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Methods for counterexample-guided quantifier instantiation
13
 ** based on nested quantifier elimination.
14
 **/
15
16
#include "theory/quantifiers/cegqi/nested_qe.h"
17
18
#include "expr/node_algorithm.h"
19
#include "expr/subs.h"
20
#include "theory/smt_engine_subsolver.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
26
30
NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {}
27
28
58
bool NestedQe::process(Node q, std::vector<Node>& lems)
29
{
30
58
  NodeNodeMap::iterator it = d_qnqe.find(q);
31
58
  if (it != d_qnqe.end())
32
  {
33
    // already processed
34
22
    return (*it).second != q;
35
  }
36
36
  Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl;
37
72
  Node qqe = doNestedQe(q, true);
38
36
  d_qnqe[q] = qqe;
39
36
  if (qqe == q)
40
  {
41
22
    Trace("cegqi-nested-qe") << "...did not apply nested QE" << std::endl;
42
22
    return false;
43
  }
44
14
  Trace("cegqi-nested-qe") << "...applied nested QE" << std::endl;
45
14
  Trace("cegqi-nested-qe") << "Result is " << qqe << std::endl;
46
47
  // add as lemma
48
14
  lems.push_back(q.eqNode(qqe));
49
14
  return true;
50
}
51
52
bool NestedQe::hasProcessed(Node q) const
53
{
54
  return d_qnqe.find(q) != d_qnqe.end();
55
}
56
57
125
bool NestedQe::getNestedQuantification(
58
    Node q, std::unordered_set<Node, NodeHashFunction>& nqs)
59
{
60
125
  expr::getKindSubterms(q[1], kind::FORALL, true, nqs);
61
125
  return !nqs.empty();
62
}
63
64
40
bool NestedQe::hasNestedQuantification(Node q)
65
{
66
80
  std::unordered_set<Node, NodeHashFunction> nqs;
67
80
  return getNestedQuantification(q, nqs);
68
}
69
70
85
Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
71
{
72
85
  NodeManager* nm = NodeManager::currentNM();
73
170
  Node qOrig = q;
74
85
  bool inputExists = false;
75
85
  if (q.getKind() == kind::EXISTS)
76
  {
77
23
    q = nm->mkNode(kind::FORALL, q[0], q[1].negate());
78
23
    inputExists = true;
79
  }
80
85
  Assert(q.getKind() == kind::FORALL);
81
170
  std::unordered_set<Node, NodeHashFunction> nqs;
82
85
  if (!getNestedQuantification(q, nqs))
83
  {
84
132
    Trace("cegqi-nested-qe-debug")
85
66
        << "...no nested quantification" << std::endl;
86
66
    if (keepTopLevel)
87
    {
88
51
      return qOrig;
89
    }
90
    // just do ordinary quantifier elimination
91
30
    Node qqe = doQe(q);
92
15
    Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl;
93
15
    return qqe;
94
  }
95
38
  Trace("cegqi-nested-qe-debug")
96
19
      << "..." << nqs.size() << " nested quantifiers" << std::endl;
97
  // otherwise, skolemize the arguments of this and apply
98
38
  std::vector<Node> vars(q[0].begin(), q[0].end());
99
38
  Subs sk;
100
19
  sk.add(vars);
101
  // do nested quantifier elimination on each nested quantifier, skolemizing the
102
  // free variables
103
38
  Subs snqe;
104
38
  for (const Node& nq : nqs)
105
  {
106
38
    Node nqk = sk.apply(nq);
107
38
    Node nqqe = doNestedQe(nqk);
108
19
    if (nqqe == nqk)
109
    {
110
      // failed
111
      Trace("cegqi-nested-qe-debug")
112
          << "...failed to apply to nested" << std::endl;
113
      return q;
114
    }
115
19
    snqe.add(nqk, nqqe);
116
  }
117
  // get the result of nested quantifier elimination
118
38
  Node qeBody = sk.apply(q[1]);
119
19
  qeBody = snqe.apply(qeBody);
120
  // undo the skolemization
121
19
  qeBody = sk.rapply(qeBody, true);
122
  // reconstruct the body
123
38
  std::vector<Node> qargs;
124
19
  qargs.push_back(q[0]);
125
19
  qargs.push_back(inputExists ? qeBody.negate() : qeBody);
126
19
  if (q.getNumChildren() == 3)
127
  {
128
    qargs.push_back(q[2]);
129
  }
130
19
  return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs);
131
}
132
133
15
Node NestedQe::doQe(Node q)
134
{
135
15
  Assert(q.getKind() == kind::FORALL);
136
15
  Trace("cegqi-nested-qe") << "  Apply qe to " << q << std::endl;
137
15
  NodeManager* nm = NodeManager::currentNM();
138
15
  q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
139
30
  std::unique_ptr<SmtEngine> smt_qe;
140
15
  initializeSubsolver(smt_qe);
141
30
  Node qqe = smt_qe->getQuantifierElimination(q, true, false);
142
15
  if (expr::hasBoundVar(qqe))
143
  {
144
    Trace("cegqi-nested-qe") << "  ...failed QE" << std::endl;
145
    //...failed to apply
146
    return q;
147
  }
148
30
  Node res = qqe.negate();
149
15
  Trace("cegqi-nested-qe") << "  ...success, result = " << res << std::endl;
150
15
  return res;
151
}
152
153
}  // namespace quantifiers
154
}  // namespace theory
155
26685
}  // namespace CVC4