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 |
13209 |
QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms) |
34 |
13209 |
: EnvObj(env), d_smtSolver(sms) |
35 |
|
{ |
36 |
13209 |
} |
37 |
|
|
38 |
21124 |
QuantElimSolver::~QuantElimSolver() {} |
39 |
|
|
40 |
30 |
Node QuantElimSolver::getQuantifierElimination(Assertions& as, |
41 |
|
Node q, |
42 |
|
bool doFull, |
43 |
|
bool isInternalSubsolver) |
44 |
|
{ |
45 |
30 |
Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; |
46 |
30 |
if (q.getKind() != EXISTS && q.getKind() != FORALL) |
47 |
|
{ |
48 |
|
throw ModalException( |
49 |
|
"Expecting a quantified formula as argument to get-qe."); |
50 |
|
} |
51 |
30 |
NodeManager* nm = NodeManager::currentNM(); |
52 |
|
// ensure the body is rewritten |
53 |
30 |
q = nm->mkNode(q.getKind(), q[0], rewrite(q[1])); |
54 |
|
// do nested quantifier elimination if necessary |
55 |
30 |
q = quantifiers::NestedQe::doNestedQe(d_env, q, true); |
56 |
60 |
Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " |
57 |
30 |
<< q << std::endl; |
58 |
|
// tag the quantified formula with the quant-elim attribute |
59 |
60 |
TypeNode t = nm->booleanType(); |
60 |
30 |
TheoryEngine* te = d_smtSolver.getTheoryEngine(); |
61 |
30 |
Assert(te != nullptr); |
62 |
|
Node keyword = |
63 |
60 |
nm->mkConst(String(doFull ? "quant-elim" : "quant-elim-partial")); |
64 |
60 |
Node n_attr = nm->mkNode(INST_ATTRIBUTE, keyword); |
65 |
30 |
n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); |
66 |
60 |
std::vector<Node> children; |
67 |
30 |
children.push_back(q[0]); |
68 |
30 |
children.push_back(q.getKind() == EXISTS ? q[1] : q[1].negate()); |
69 |
30 |
children.push_back(n_attr); |
70 |
60 |
Node ne = nm->mkNode(EXISTS, children); |
71 |
60 |
Trace("smt-qe-debug") << "Query for quantifier elimination : " << ne |
72 |
30 |
<< std::endl; |
73 |
30 |
Assert(ne.getNumChildren() == 3); |
74 |
|
// We consider this to be an entailment check, which also avoids incorrect |
75 |
|
// status reporting (see SmtEngineState::d_expectedStatus). |
76 |
60 |
Result r = d_smtSolver.checkSatisfiability(as, std::vector<Node>{ne}, 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 |
21 |
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 |
42 |
std::vector<Node> inst_qs; |
94 |
21 |
qe->getInstantiatedQuantifiedFormulas(inst_qs); |
95 |
21 |
Assert(inst_qs.size() <= 1); |
96 |
42 |
Node ret; |
97 |
21 |
if (inst_qs.size() == 1) |
98 |
|
{ |
99 |
32 |
Node topq = inst_qs[0]; |
100 |
16 |
Assert(topq.getKind() == FORALL); |
101 |
32 |
Trace("smt-qe") << "Get qe based on preprocessed quantified formula " |
102 |
16 |
<< topq << std::endl; |
103 |
32 |
std::vector<Node> insts; |
104 |
16 |
qe->getInstantiations(topq, insts); |
105 |
|
// note we do not convert to witness form here, since we could be |
106 |
|
// an internal subsolver (SmtEngine::isInternalSubsolver). |
107 |
16 |
ret = nm->mkAnd(insts); |
108 |
16 |
Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl; |
109 |
16 |
if (q.getKind() == EXISTS) |
110 |
|
{ |
111 |
13 |
ret = rewrite(ret.negate()); |
112 |
|
} |
113 |
|
} |
114 |
|
else |
115 |
|
{ |
116 |
5 |
ret = nm->mkConst(q.getKind() != EXISTS); |
117 |
|
} |
118 |
|
// do extended rewrite to minimize the size of the formula aggressively |
119 |
21 |
ret = extendedRewrite(ret); |
120 |
|
// if we are not an internal subsolver, convert to witness form, since |
121 |
|
// internally generated skolems should not escape |
122 |
21 |
if (!isInternalSubsolver) |
123 |
|
{ |
124 |
12 |
ret = SkolemManager::getOriginalForm(ret); |
125 |
|
} |
126 |
21 |
return ret; |
127 |
|
} |
128 |
|
// otherwise, just true/false |
129 |
9 |
return nm->mkConst(q.getKind() == EXISTS); |
130 |
|
} |
131 |
|
|
132 |
|
} // namespace smt |
133 |
29577 |
} // namespace cvc5 |