GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/quant_elim_solver.cpp Lines: 61 66 92.4 %
Date: 2021-03-22 Branches: 148 342 43.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_elim_solver.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 The solver for quantifier elimination queries
13
 **/
14
15
#include "smt/quant_elim_solver.h"
16
17
#include "expr/skolem_manager.h"
18
#include "expr/subs.h"
19
#include "smt/smt_solver.h"
20
#include "theory/quantifiers/cegqi/nested_qe.h"
21
#include "theory/quantifiers/extended_rewrite.h"
22
#include "theory/quantifiers_engine.h"
23
#include "theory/rewriter.h"
24
#include "theory/theory_engine.h"
25
26
using namespace CVC4::theory;
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace smt {
31
32
9619
QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {}
33
34
9598
QuantElimSolver::~QuantElimSolver() {}
35
36
30
Node QuantElimSolver::getQuantifierElimination(Assertions& as,
37
                                               Node q,
38
                                               bool doFull,
39
                                               bool isInternalSubsolver)
40
{
41
30
  Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
42
30
  if (q.getKind() != EXISTS && q.getKind() != FORALL)
43
  {
44
    throw ModalException(
45
        "Expecting a quantified formula as argument to get-qe.");
46
  }
47
30
  NodeManager* nm = NodeManager::currentNM();
48
  // ensure the body is rewritten
49
30
  q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
50
  // do nested quantifier elimination if necessary
51
30
  q = quantifiers::NestedQe::doNestedQe(q, true);
52
60
  Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
53
30
                  << q << std::endl;
54
  // tag the quantified formula with the quant-elim attribute
55
60
  TypeNode t = nm->booleanType();
56
60
  Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
57
60
  std::vector<Node> node_values;
58
30
  TheoryEngine* te = d_smtSolver.getTheoryEngine();
59
30
  Assert(te != nullptr);
60
30
  te->setUserAttribute(
61
      doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
62
30
  QuantifiersEngine* qe = te->getQuantifiersEngine();
63
30
  n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
64
30
  n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
65
60
  std::vector<Node> children;
66
30
  children.push_back(q[0]);
67
30
  children.push_back(q.getKind() == EXISTS ? q[1] : q[1].negate());
68
30
  children.push_back(n_attr);
69
60
  Node ne = nm->mkNode(EXISTS, children);
70
60
  Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne
71
30
                        << std::endl;
72
30
  Assert(ne.getNumChildren() == 3);
73
  // We consider this to be an entailment check, which also avoids incorrect
74
  // status reporting (see SmtEngineState::d_expectedStatus).
75
  Result r =
76
60
      d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne}, false, true);
77
30
  Trace("smt-qe") << "Query returned " << r << std::endl;
78
30
  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
79
  {
80
21
    if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull)
81
    {
82
      Notice()
83
          << "While performing quantifier elimination, unexpected result : "
84
          << r << " for query.";
85
      // failed, return original
86
      return q;
87
    }
88
    // must use original quantified formula to compute QE, which ensures that
89
    // e.g. term formula removal is not run on the body. Notice that we assume
90
    // that the (single) quantified formula is preprocessed, rewritten
91
    // version of the input quantified formula q.
92
42
    std::vector<Node> inst_qs;
93
21
    qe->getInstantiatedQuantifiedFormulas(inst_qs);
94
21
    Assert(inst_qs.size() <= 1);
95
42
    Node ret;
96
21
    if (inst_qs.size() == 1)
97
    {
98
32
      Node topq = inst_qs[0];
99
16
      Assert(topq.getKind() == FORALL);
100
32
      Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
101
16
                      << topq << std::endl;
102
32
      std::vector<std::vector<Node>> insts;
103
16
      qe->getInstantiationTermVectors(topq, insts);
104
32
      std::vector<Node> vars(ne[0].begin(), ne[0].end());
105
32
      std::vector<Node> conjs;
106
      // apply the instantiation on the original body
107
36
      for (const std::vector<Node>& inst : insts)
108
      {
109
        // note we do not convert to witness form here, since we could be
110
        // an internal subsolver
111
40
        Subs s;
112
20
        s.add(vars, inst);
113
40
        Node c = s.apply(ne[1].negate());
114
20
        conjs.push_back(c);
115
      }
116
16
      ret = nm->mkAnd(conjs);
117
16
      Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
118
16
      if (q.getKind() == EXISTS)
119
      {
120
13
        ret = Rewriter::rewrite(ret.negate());
121
      }
122
    }
123
    else
124
    {
125
5
      ret = nm->mkConst(q.getKind() != EXISTS);
126
    }
127
    // do extended rewrite to minimize the size of the formula aggressively
128
42
    theory::quantifiers::ExtendedRewriter extr(true);
129
21
    ret = extr.extendedRewrite(ret);
130
    // if we are not an internal subsolver, convert to witness form, since
131
    // internally generated skolems should not escape
132
21
    if (!isInternalSubsolver)
133
    {
134
11
      ret = SkolemManager::getOriginalForm(ret);
135
    }
136
21
    return ret;
137
  }
138
  // otherwise, just true/false
139
9
  return nm->mkConst(q.getKind() == EXISTS);
140
}
141
142
}  // namespace smt
143
26676
}  // namespace CVC4