Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * The solver for quantifier elimination queries.
14 : : */
15 : :
16 : : #include "smt/quant_elim_solver.h"
17 : :
18 : : #include "base/modal_exception.h"
19 : : #include "expr/node_algorithm.h"
20 : : #include "expr/skolem_manager.h"
21 : : #include "expr/subs.h"
22 : : #include "expr/subtype_elim_node_converter.h"
23 : : #include "smt/smt_driver.h"
24 : : #include "smt/smt_solver.h"
25 : : #include "theory/quantifiers/cegqi/nested_qe.h"
26 : : #include "theory/quantifiers_engine.h"
27 : : #include "theory/theory_engine.h"
28 : : #include "util/string.h"
29 : :
30 : : using namespace cvc5::internal::theory;
31 : : using namespace cvc5::internal::kind;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace smt {
35 : :
36 : 74702 : QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms, ContextManager* ctx)
37 : 74702 : : EnvObj(env), d_smtSolver(sms), d_ctx(ctx)
38 : : {
39 : 74702 : }
40 : :
41 : 139508 : QuantElimSolver::~QuantElimSolver() {}
42 : :
43 : 415 : Node QuantElimSolver::getQuantifierElimination(Node q,
44 : : bool doFull,
45 : : bool isInternalSubsolver)
46 : : {
47 [ + - ]: 415 : Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
48 [ + + ][ + + ]: 415 : if (q.getKind() != Kind::EXISTS && q.getKind() != Kind::FORALL)
[ + + ]
49 : : {
50 : : throw ModalException(
51 : 4 : "Expecting a quantified formula as argument to get-qe.");
52 : : }
53 : 411 : NodeManager* nm = nodeManager();
54 : : // ensure the body is rewritten
55 : 411 : q = nm->mkNode(q.getKind(), q[0], rewrite(q[1]));
56 : : // do nested quantifier elimination if necessary
57 : 411 : q = quantifiers::NestedQe::doNestedQe(d_env, q, true);
58 [ + - ]: 822 : Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
59 : 411 : << q << std::endl;
60 : : Node keyword =
61 [ + + ]: 822 : nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial"));
62 : 822 : Node n_attr = nm->mkNode(Kind::INST_ATTRIBUTE, keyword);
63 : : // Polarity is the Boolean constant we return if the subquery is "sat".
64 : 411 : bool polarity = (q.getKind() != Kind::EXISTS);
65 : 822 : Node ne;
66 : : // Special case: if we have no free symbols, just use a quantifier-free
67 : : // query. This ensures we don't depend on quantifier instantiation in
68 : : // these cases, which is especially important if the theory does not admit
69 : : // QE, e.g. strings.
70 : 822 : std::unordered_set<Node> syms;
71 : 411 : expr::getSymbols(q, syms);
72 : 411 : bool closed = false;
73 [ + + ]: 411 : if (syms.empty())
74 : : {
75 : : // Partial elimination is irrelevant since we have a closed formula, so we
76 : : // assume we are doing full elimination.
77 : 368 : doFull = true;
78 : 368 : closed = true;
79 : 736 : Subs sq;
80 : 368 : SkolemManager* sm = nm->getSkolemManager();
81 [ + + ]: 756 : for (const Node& v : q[0])
82 : : {
83 : : Node k = sm->mkInternalSkolemFunction(
84 : 1552 : InternalSkolemId::QE_CLOSED_INPUT, v.getType(), {v});
85 : 388 : sq.add(v, k);
86 : : }
87 : 368 : ne = sq.apply(q[1]);
88 : : // We are skolemizing, so we flip the polarity
89 : 368 : polarity = !polarity;
90 [ + + ]: 368 : if (q.getKind() == Kind::EXISTS)
91 : : {
92 : 5 : ne = ne.negate();
93 : : }
94 : : }
95 : : else
96 : : {
97 : : // tag the quantified formula with the quant-elim attribute
98 : 86 : TypeNode t = nm->booleanType();
99 : 43 : n_attr = nm->mkNode(Kind::INST_PATTERN_LIST, n_attr);
100 : 43 : std::vector<Node> children;
101 : 43 : children.push_back(q[0]);
102 [ + + ][ + + ]: 43 : children.push_back(q.getKind() == Kind::EXISTS ? q[1] : q[1].negate());
[ - - ]
103 : 43 : children.push_back(n_attr);
104 : 43 : ne = nm->mkNode(Kind::EXISTS, children);
105 [ - + ][ - + ]: 43 : Assert(ne.getNumChildren() == 3);
[ - - ]
106 : : }
107 [ + - ]: 822 : Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne
108 : 411 : << std::endl;
109 : : // use a single call driver
110 : 822 : SmtDriverSingleCall sdsc(d_env, d_smtSolver, d_ctx);
111 : 1644 : Result r = sdsc.checkSat(std::vector<Node>{ne.notNode()});
112 [ + - ]: 411 : Trace("smt-qe") << "Query returned " << r << std::endl;
113 [ + + ]: 411 : if (r.getStatus() != Result::UNSAT)
114 : : {
115 [ + + ][ - + ]: 36 : if (r.getStatus() != Result::SAT && doFull)
[ - + ]
116 : : {
117 : 0 : verbose(1)
118 : 0 : << "While performing quantifier elimination, unexpected result : "
119 : 0 : << r << " for query." << std::endl;
120 : : // failed, return original
121 : 0 : return q;
122 : : }
123 : : // must use original quantified formula to compute QE, which ensures that
124 : : // e.g. term formula removal is not run on the body. Notice that we assume
125 : : // that the (single) quantified formula is preprocessed, rewritten
126 : : // version of the input quantified formula q.
127 : 72 : std::vector<Node> inst_qs;
128 : 72 : Node topq;
129 : 72 : Node ret;
130 [ + + ]: 36 : if (!closed)
131 : : {
132 : 32 : TheoryEngine* te = d_smtSolver.getTheoryEngine();
133 [ - + ][ - + ]: 32 : Assert(te != nullptr);
[ - - ]
134 : 32 : QuantifiersEngine* qe = te->getQuantifiersEngine();
135 : 32 : qe->getInstantiatedQuantifiedFormulas(inst_qs);
136 : : // Find the quantified formula corresponding to the quantifier elimination
137 [ + - ]: 33 : for (const Node& qinst : inst_qs)
138 : : {
139 : : // Should have the same attribute mark as above
140 [ + + ][ + - ]: 33 : if (qinst.getNumChildren() == 3 && qinst[2] == n_attr)
[ + + ][ + + ]
[ - - ]
141 : : {
142 : 32 : topq = qinst;
143 : 32 : break;
144 : : }
145 : : }
146 [ + - ]: 32 : if (!topq.isNull())
147 : : {
148 [ - + ][ - + ]: 32 : Assert(topq.getKind() == Kind::FORALL);
[ - - ]
149 [ + - ]: 64 : Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
150 : 32 : << topq << std::endl;
151 : 64 : std::vector<Node> insts;
152 : 32 : qe->getInstantiations(topq, insts);
153 : : // note we do not convert to witness form here, since we could be
154 : : // an internal subsolver (SolverEngine::isInternalSubsolver).
155 : 32 : ret = nm->mkAnd(insts);
156 [ + - ]: 32 : Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
157 [ + + ]: 32 : if (q.getKind() == Kind::EXISTS)
158 : : {
159 : 27 : ret = rewrite(ret.negate());
160 : : }
161 : : // do extended rewrite to minimize the size of the formula aggressively
162 : 32 : ret = extendedRewrite(ret);
163 : : // if we are not an internal subsolver, convert to witness form, since
164 : : // internally generated skolems should not escape
165 [ + + ]: 32 : if (!isInternalSubsolver)
166 : : {
167 : 12 : ret = SkolemManager::getOriginalForm(ret);
168 : : }
169 : : // make so that the returned formula does not involve arithmetic
170 : : // subtyping
171 : 32 : SubtypeElimNodeConverter senc(nodeManager());
172 : 32 : ret = senc.convert(ret);
173 : : }
174 : : }
175 : : // If we are closed, or the quantified formula was not instantiated in the
176 : : // subsolver, then we are a constant.
177 [ + + ]: 36 : if (ret.isNull())
178 : : {
179 : 4 : ret = nm->mkConst(polarity);
180 : : }
181 : 36 : return ret;
182 : : }
183 : : // otherwise, just true/false
184 : 750 : return nm->mkConst(!polarity);
185 : : }
186 : :
187 : : } // namespace smt
188 : : } // namespace cvc5::internal
|
