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