1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
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/skolem_manager.h" |
20 |
|
#include "expr/subs.h" |
21 |
|
#include "smt/smt_solver.h" |
22 |
|
#include "theory/quantifiers/cegqi/nested_qe.h" |
23 |
|
#include "theory/quantifiers_engine.h" |
24 |
|
#include "theory/theory_engine.h" |
25 |
|
#include "util/string.h" |
26 |
|
|
27 |
|
using namespace cvc5::theory; |
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace smt { |
32 |
|
|
33 |
18633 |
QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms) |
34 |
18633 |
: EnvObj(env), d_smtSolver(sms) |
35 |
|
{ |
36 |
18633 |
} |
37 |
|
|
38 |
31768 |
QuantElimSolver::~QuantElimSolver() {} |
39 |
|
|
40 |
32 |
Node QuantElimSolver::getQuantifierElimination(Assertions& as, |
41 |
|
Node q, |
42 |
|
bool doFull, |
43 |
|
bool isInternalSubsolver) |
44 |
|
{ |
45 |
32 |
Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; |
46 |
32 |
if (q.getKind() != EXISTS && q.getKind() != FORALL) |
47 |
|
{ |
48 |
|
throw ModalException( |
49 |
|
"Expecting a quantified formula as argument to get-qe."); |
50 |
|
} |
51 |
32 |
NodeManager* nm = NodeManager::currentNM(); |
52 |
|
// ensure the body is rewritten |
53 |
32 |
q = nm->mkNode(q.getKind(), q[0], rewrite(q[1])); |
54 |
|
// do nested quantifier elimination if necessary |
55 |
32 |
q = quantifiers::NestedQe::doNestedQe(d_env, q, true); |
56 |
64 |
Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " |
57 |
32 |
<< q << std::endl; |
58 |
|
// tag the quantified formula with the quant-elim attribute |
59 |
64 |
TypeNode t = nm->booleanType(); |
60 |
32 |
TheoryEngine* te = d_smtSolver.getTheoryEngine(); |
61 |
32 |
Assert(te != nullptr); |
62 |
|
Node keyword = |
63 |
64 |
nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial")); |
64 |
64 |
Node n_attr = nm->mkNode(INST_ATTRIBUTE, keyword); |
65 |
32 |
n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); |
66 |
64 |
std::vector<Node> children; |
67 |
32 |
children.push_back(q[0]); |
68 |
32 |
children.push_back(q.getKind() == EXISTS ? q[1] : q[1].negate()); |
69 |
32 |
children.push_back(n_attr); |
70 |
64 |
Node ne = nm->mkNode(EXISTS, children); |
71 |
64 |
Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne |
72 |
32 |
<< std::endl; |
73 |
32 |
Assert(ne.getNumChildren() == 3); |
74 |
|
// We consider this to be an entailment check, which also avoids incorrect |
75 |
|
// status reporting (see SolverEngineState::d_expectedStatus). |
76 |
64 |
Result r = d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne}, true); |
77 |
32 |
Trace("smt-qe") << "Query returned " << r << std::endl; |
78 |
32 |
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) |
79 |
|
{ |
80 |
23 |
if (r.asSatisfiabilityResult().isSat() != Result::SAT && doFull) |
81 |
|
{ |
82 |
|
verbose(1) |
83 |
|
<< "While performing quantifier elimination, unexpected result : " |
84 |
|
<< r << " for query." << std::endl; |
85 |
|
// failed, return original |
86 |
|
return q; |
87 |
|
} |
88 |
23 |
QuantifiersEngine* qe = te->getQuantifiersEngine(); |
89 |
|
// must use original quantified formula to compute QE, which ensures that |
90 |
|
// e.g. term formula removal is not run on the body. Notice that we assume |
91 |
|
// that the (single) quantified formula is preprocessed, rewritten |
92 |
|
// version of the input quantified formula q. |
93 |
46 |
std::vector<Node> inst_qs; |
94 |
23 |
qe->getInstantiatedQuantifiedFormulas(inst_qs); |
95 |
46 |
Node topq; |
96 |
|
// Find the quantified formula corresponding to the quantifier elimination |
97 |
24 |
for (const Node& qinst : inst_qs) |
98 |
|
{ |
99 |
|
// Should have the same attribute mark as above |
100 |
19 |
if (qinst.getNumChildren() == 3 && qinst[2] == n_attr) |
101 |
|
{ |
102 |
18 |
topq = qinst; |
103 |
18 |
break; |
104 |
|
} |
105 |
|
} |
106 |
46 |
Node ret; |
107 |
23 |
if (!topq.isNull()) |
108 |
|
{ |
109 |
18 |
Assert(topq.getKind() == FORALL); |
110 |
36 |
Trace("smt-qe") << "Get qe based on preprocessed quantified formula " |
111 |
18 |
<< topq << std::endl; |
112 |
36 |
std::vector<Node> insts; |
113 |
18 |
qe->getInstantiations(topq, insts); |
114 |
|
// note we do not convert to witness form here, since we could be |
115 |
|
// an internal subsolver (SolverEngine::isInternalSubsolver). |
116 |
18 |
ret = nm->mkAnd(insts); |
117 |
18 |
Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; |
118 |
18 |
if (q.getKind() == EXISTS) |
119 |
|
{ |
120 |
15 |
ret = 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 |
23 |
ret = extendedRewrite(ret); |
129 |
|
// if we are not an internal subsolver, convert to witness form, since |
130 |
|
// internally generated skolems should not escape |
131 |
23 |
if (!isInternalSubsolver) |
132 |
|
{ |
133 |
13 |
ret = SkolemManager::getOriginalForm(ret); |
134 |
|
} |
135 |
23 |
return ret; |
136 |
|
} |
137 |
|
// otherwise, just true/false |
138 |
9 |
return nm->mkConst(q.getKind() == EXISTS); |
139 |
|
} |
140 |
|
|
141 |
|
} // namespace smt |
142 |
31137 |
} // namespace cvc5 |