Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Hans-Joerg Schurr
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 module for managing witness form conversion in proofs.
14 : : */
15 : :
16 : : #include "smt/witness_form.h"
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "smt/env.h"
20 : : #include "theory/rewriter.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace smt {
24 : :
25 : 0 : std::ostream& operator<<(std::ostream& out, WitnessReq wr)
26 : : {
27 [ - - ][ - - ]: 0 : switch (wr)
[ - ]
28 : : {
29 : 0 : case WitnessReq::WITNESS_AND_REWRITE: out << "WITNESS_AND_REWRITE"; break;
30 : 0 : case WitnessReq::WITNESS: out << "WITNESS"; break;
31 : 0 : case WitnessReq::REWRITE: out << "REWRITE"; break;
32 : 0 : case WitnessReq::NONE: out << "NONE"; break;
33 : : }
34 : 0 : return out;
35 : : }
36 : :
37 : 20440 : WitnessFormGenerator::WitnessFormGenerator(Env& env)
38 : : : EnvObj(env),
39 : 20440 : d_rewriter(env.getRewriter()),
40 : : d_tcpg(env,
41 : : nullptr,
42 : : TConvPolicy::FIXPOINT,
43 : : TConvCachePolicy::NEVER,
44 : : "WfGenerator::TConvProofGenerator",
45 : : nullptr,
46 : : true),
47 : : d_wintroPf(env, nullptr, nullptr, "WfGenerator::LazyCDProof"),
48 : 40880 : d_pskPf(env, nullptr, "WfGenerator::PurifySkolemProof")
49 : : {
50 : 20440 : d_true = nodeManager()->mkConst(true);
51 : 20440 : }
52 : :
53 : 31019 : std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq)
54 : : {
55 [ - + ]: 31019 : if (eq.getKind() != Kind::EQUAL)
56 : : {
57 : : // expecting an equality
58 : 0 : return nullptr;
59 : : }
60 : 62038 : Node lhs = eq[0];
61 : 62038 : Node rhs = convertToWitnessForm(eq[0]);
62 [ - + ]: 31019 : if (rhs != eq[1])
63 : : {
64 : : // expecting witness form
65 : 0 : return nullptr;
66 : : }
67 : 62038 : std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq);
68 [ - + ][ - + ]: 31019 : Assert(pn != nullptr);
[ - - ]
69 : 31019 : return pn;
70 : : }
71 : :
72 : 0 : std::string WitnessFormGenerator::identify() const
73 : : {
74 : 0 : return "WitnessFormGenerator";
75 : : }
76 : :
77 : 31019 : Node WitnessFormGenerator::convertToWitnessForm(Node t)
78 : : {
79 : 31019 : Node tw = SkolemManager::getOriginalForm(t);
80 [ - + ]: 31019 : if (t == tw)
81 : : {
82 : : // trivial case
83 : 0 : return tw;
84 : : }
85 : 31019 : std::unordered_set<Node>::iterator it;
86 : 62038 : std::vector<TNode> visit;
87 : 62038 : TNode cur;
88 : 62038 : TNode curw;
89 : 31019 : visit.push_back(t);
90 : 293186 : do
91 : : {
92 : 324205 : cur = visit.back();
93 : 324205 : visit.pop_back();
94 : 324205 : it = d_visited.find(cur);
95 [ + + ]: 324205 : if (it == d_visited.end())
96 : : {
97 : 147613 : d_visited.insert(cur);
98 : 147613 : curw = SkolemManager::getOriginalForm(cur);
99 : : // if its original form is different
100 [ + + ]: 147613 : if (cur != curw)
101 : : {
102 [ + + ]: 106835 : if (cur.isVar())
103 : : {
104 : 18815 : curw = SkolemManager::getUnpurifiedForm(cur);
105 : 37630 : Node eq = cur.eqNode(curw);
106 : : // equality between a variable and its unpurified form
107 : 18815 : d_eqs.insert(eq);
108 : : // ------- SKOLEM_INTRO
109 : : // k = t
110 : 37630 : d_wintroPf.addStep(eq, ProofRule::SKOLEM_INTRO, {}, {cur});
111 : 18815 : d_tcpg.addRewriteStep(
112 : : cur, curw, &d_wintroPf, true, TrustId::NONE, true);
113 : : // recursively transform
114 : 18815 : visit.push_back(curw);
115 : : }
116 : : else
117 : : {
118 : : // A term whose original form is different from itself, recurse.
119 : : // It should be the case that cur has children, since the original
120 : : // form of constants are themselves.
121 [ - + ][ - + ]: 88020 : Assert(cur.getNumChildren() > 0);
[ - - ]
122 [ + - ]: 88020 : if (cur.hasOperator())
123 : : {
124 : 88020 : visit.push_back(cur.getOperator());
125 : : }
126 : 88020 : visit.insert(visit.end(), cur.begin(), cur.end());
127 : : }
128 : : }
129 : : }
130 [ + + ]: 324205 : } while (!visit.empty());
131 : 31019 : return tw;
132 : : }
133 : :
134 : 252569 : WitnessReq WitnessFormGenerator::requiresWitnessFormTransform(
135 : : Node t, Node s, MethodId idr) const
136 : : {
137 : 505138 : Node tr = d_env.rewriteViaMethod(t, idr);
138 : 505138 : Node sr = d_env.rewriteViaMethod(s, idr);
139 [ + + ]: 252569 : if (tr == sr)
140 : : {
141 : : // rewriting via the method is enough
142 : 229195 : return WitnessReq::NONE;
143 : : }
144 [ + + ]: 23374 : if (rewrite(tr) == rewrite(sr))
145 : : {
146 : : // calling ordinary rewrite after (extended) rewriting is enough
147 : 62 : return WitnessReq::REWRITE;
148 : : }
149 : 46624 : Node trw = SkolemManager::getOriginalForm(tr);
150 : 46624 : Node srw = SkolemManager::getOriginalForm(sr);
151 [ + + ]: 23312 : if (trw == srw)
152 : : {
153 : : // witness is enough
154 : 4305 : return WitnessReq::WITNESS;
155 : : }
156 : 19007 : return WitnessReq::WITNESS_AND_REWRITE;
157 : : }
158 : :
159 : 52293 : WitnessReq WitnessFormGenerator::requiresWitnessFormIntro(Node t,
160 : : MethodId idr) const
161 : : {
162 : 52293 : return requiresWitnessFormTransform(t, d_true, idr);
163 : : }
164 : :
165 : 0 : const std::unordered_set<Node>& WitnessFormGenerator::getWitnessFormEqs() const
166 : : {
167 : 0 : return d_eqs;
168 : : }
169 : :
170 : : } // namespace smt
171 : : } // namespace cvc5::internal
|
