GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_qe_preproc.cpp Lines: 81 82 98.8 %
Date: 2021-03-22 Branches: 178 376 47.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_qe_preproc.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 Sygus quantifier elimination preprocessor
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_qe_preproc.h"
16
17
#include "expr/node_algorithm.h"
18
#include "theory/quantifiers/single_inv_partition.h"
19
#include "theory/rewriter.h"
20
#include "theory/smt_engine_subsolver.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
2190
SygusQePreproc::SygusQePreproc(QuantifiersEngine* qe) {}
29
30
10
Node SygusQePreproc::preprocess(Node q)
31
{
32
20
  Node body = q[1];
33
10
  if (body.getKind() == NOT && body[0].getKind() == FORALL)
34
  {
35
8
    body = body[0][1];
36
  }
37
10
  NodeManager* nm = NodeManager::currentNM();
38
20
  Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
39
10
                     << std::endl;
40
20
  quantifiers::SingleInvocationPartition sip;
41
20
  std::vector<Node> funcs0;
42
10
  funcs0.insert(funcs0.end(), q[0].begin(), q[0].end());
43
10
  sip.init(funcs0, body);
44
10
  Trace("cegqi-qep") << "...finished, got:" << std::endl;
45
10
  sip.debugPrint("cegqi-qep");
46
47
10
  if (sip.isPurelySingleInvocation() || !sip.isNonGroundSingleInvocation())
48
  {
49
6
    return Node::null();
50
  }
51
  // create new smt engine to do quantifier elimination
52
8
  std::unique_ptr<SmtEngine> smt_qe;
53
4
  initializeSubsolver(smt_qe);
54
8
  Trace("cegqi-qep") << "Property is non-ground single invocation, run "
55
4
                        "QE to obtain single invocation."
56
4
                     << std::endl;
57
  // partition variables
58
8
  std::vector<Node> all_vars;
59
4
  sip.getAllVariables(all_vars);
60
8
  std::vector<Node> si_vars;
61
4
  sip.getSingleInvocationVariables(si_vars);
62
8
  std::vector<Node> qe_vars;
63
8
  std::vector<Node> nqe_vars;
64
140
  for (unsigned i = 0, size = all_vars.size(); i < size; i++)
65
  {
66
272
    Node v = all_vars[i];
67
136
    if (std::find(funcs0.begin(), funcs0.end(), v) != funcs0.end())
68
    {
69
126
      Trace("cegqi-qep") << "- fun var: " << v << std::endl;
70
    }
71
10
    else if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
72
    {
73
4
      qe_vars.push_back(v);
74
4
      Trace("cegqi-qep") << "- qe var: " << v << std::endl;
75
    }
76
    else
77
    {
78
6
      nqe_vars.push_back(v);
79
6
      Trace("cegqi-qep") << "- non qe var: " << v << std::endl;
80
    }
81
  }
82
8
  std::vector<Node> orig;
83
8
  std::vector<Node> subs;
84
  // skolemize non-qe variables
85
10
  for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
86
  {
87
    Node k = nm->mkSkolem(
88
12
        "k", nqe_vars[i].getType(), "qe for non-ground single invocation");
89
6
    orig.push_back(nqe_vars[i]);
90
6
    subs.push_back(k);
91
12
    Trace("cegqi-qep") << "  subs : " << nqe_vars[i] << " -> " << k
92
6
                       << std::endl;
93
  }
94
8
  std::vector<Node> funcs1;
95
4
  sip.getFunctions(funcs1);
96
130
  for (unsigned i = 0, size = funcs1.size(); i < size; i++)
97
  {
98
252
    Node f = funcs1[i];
99
252
    Node fi = sip.getFunctionInvocationFor(f);
100
252
    Node fv = sip.getFirstOrderVariableForFunction(f);
101
126
    Assert(!fi.isNull());
102
126
    orig.push_back(fi);
103
    Node k = nm->mkSkolem(
104
252
        "k", fv.getType(), "qe for function in non-ground single invocation");
105
126
    subs.push_back(k);
106
126
    Trace("cegqi-qep") << "  subs : " << fi << " -> " << k << std::endl;
107
  }
108
8
  Node conj_se_ngsi = sip.getFullSpecification();
109
4
  Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi << std::endl;
110
  Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
111
8
      orig.begin(), orig.end(), subs.begin(), subs.end());
112
4
  Assert(!qe_vars.empty());
113
12
  conj_se_ngsi_subs = nm->mkNode(
114
16
      EXISTS, nm->mkNode(BOUND_VAR_LIST, qe_vars), conj_se_ngsi_subs.negate());
115
116
8
  Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs
117
4
                     << std::endl;
118
8
  Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false);
119
4
  Trace("cegqi-qep") << "Result : " << qeRes << std::endl;
120
121
  // create single invocation conjecture, if QE was successful
122
4
  if (!expr::hasBoundVar(qeRes))
123
  {
124
4
    qeRes =
125
8
        qeRes.substitute(subs.begin(), subs.end(), orig.begin(), orig.end());
126
4
    if (!nqe_vars.empty())
127
    {
128
2
      qeRes = nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qeRes);
129
    }
130
4
    Assert(q.getNumChildren() == 3);
131
4
    qeRes = nm->mkNode(FORALL, q[0], qeRes, q[2]);
132
8
    Trace("cegqi-qep") << "Converted conjecture after QE : " << qeRes
133
4
                       << std::endl;
134
4
    qeRes = Rewriter::rewrite(qeRes);
135
8
    Node nq = qeRes;
136
    // must assert it is equivalent to the original
137
8
    Node lem = q.eqNode(nq);
138
8
    Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
139
4
                         << std::endl;
140
4
    return lem;
141
  }
142
  return Node::null();
143
}
144
145
}  // namespace quantifiers
146
}  // namespace theory
147
26676
}  // namespace CVC4