Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The module for managing witness form conversion in proofs.
11 : : */
12 : :
13 : : #include "smt/witness_form.h"
14 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "smt/env.h"
17 : : #include "theory/rewriter.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace smt {
21 : :
22 : 0 : std::ostream& operator<<(std::ostream& out, WitnessReq wr)
23 : : {
24 [ - - ][ - - ]: 0 : switch (wr)
[ - ]
25 : : {
26 : 0 : case WitnessReq::WITNESS_AND_REWRITE: out << "WITNESS_AND_REWRITE"; break;
27 : 0 : case WitnessReq::WITNESS: out << "WITNESS"; break;
28 : 0 : case WitnessReq::REWRITE: out << "REWRITE"; break;
29 : 0 : case WitnessReq::NONE: out << "NONE"; break;
30 : : }
31 : 0 : return out;
32 : : }
33 : :
34 : 19796 : WitnessFormGenerator::WitnessFormGenerator(Env& env)
35 : : : EnvObj(env),
36 : 19796 : d_rewriter(env.getRewriter()),
37 : 19796 : d_tcpg(env,
38 : : nullptr,
39 : : TConvPolicy::FIXPOINT,
40 : : TConvCachePolicy::NEVER,
41 : : "WfGenerator::TConvProofGenerator",
42 : : nullptr,
43 : : true),
44 : 19796 : d_wintroPf(env, nullptr, nullptr, "WfGenerator::LazyCDProof"),
45 : 59388 : d_pskPf(env, nullptr, "WfGenerator::PurifySkolemProof")
46 : : {
47 : 19796 : d_true = nodeManager()->mkConst(true);
48 : 19796 : }
49 : :
50 : 25267 : std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq)
51 : : {
52 [ - + ]: 25267 : if (eq.getKind() != Kind::EQUAL)
53 : : {
54 : : // expecting an equality
55 : 0 : return nullptr;
56 : : }
57 : 25267 : Node lhs = eq[0];
58 : 25267 : Node rhs = convertToWitnessForm(eq[0]);
59 [ - + ]: 25267 : if (rhs != eq[1])
60 : : {
61 : : // expecting witness form
62 : 0 : return nullptr;
63 : : }
64 : 25267 : std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq);
65 [ - + ][ - + ]: 25267 : Assert(pn != nullptr);
[ - - ]
66 : 25267 : return pn;
67 : 25267 : }
68 : :
69 : 0 : std::string WitnessFormGenerator::identify() const
70 : : {
71 : 0 : return "WitnessFormGenerator";
72 : : }
73 : :
74 : 25267 : Node WitnessFormGenerator::convertToWitnessForm(Node t)
75 : : {
76 : 25267 : Node tw = SkolemManager::getOriginalForm(t);
77 [ - + ]: 25267 : if (t == tw)
78 : : {
79 : : // trivial case
80 : 0 : return tw;
81 : : }
82 : 25267 : std::unordered_set<Node>::iterator it;
83 : 25267 : std::vector<TNode> visit;
84 : 25267 : TNode cur;
85 : 25267 : TNode curw;
86 : 25267 : visit.push_back(t);
87 : : do
88 : : {
89 : 268149 : cur = visit.back();
90 : 268149 : visit.pop_back();
91 : 268149 : it = d_visited.find(cur);
92 [ + + ]: 268149 : if (it == d_visited.end())
93 : : {
94 : 122931 : d_visited.insert(cur);
95 : 122931 : curw = SkolemManager::getOriginalForm(cur);
96 : : // if its original form is different
97 [ + + ]: 122931 : if (cur != curw)
98 : : {
99 [ + + ]: 88421 : if (cur.isVar())
100 : : {
101 : 14920 : curw = SkolemManager::getUnpurifiedForm(cur);
102 : 14920 : Node eq = cur.eqNode(curw);
103 : : // equality between a variable and its unpurified form
104 : 14920 : d_eqs.insert(eq);
105 : : // ------- SKOLEM_INTRO
106 : : // k = t
107 : 29840 : d_wintroPf.addStep(eq, ProofRule::SKOLEM_INTRO, {}, {cur});
108 : 14920 : d_tcpg.addRewriteStep(
109 : : cur, curw, &d_wintroPf, true, TrustId::NONE, true);
110 : : // recursively transform
111 : 14920 : visit.push_back(curw);
112 : 14920 : }
113 : : else
114 : : {
115 : : // A term whose original form is different from itself, recurse.
116 : : // It should be the case that cur has children, since the original
117 : : // form of constants are themselves.
118 [ - + ][ - + ]: 73501 : Assert(cur.getNumChildren() > 0);
[ - - ]
119 [ + - ]: 73501 : if (cur.hasOperator())
120 : : {
121 : 73501 : visit.push_back(cur.getOperator());
122 : : }
123 : 73501 : visit.insert(visit.end(), cur.begin(), cur.end());
124 : : }
125 : : }
126 : : }
127 [ + + ]: 268149 : } while (!visit.empty());
128 : 25267 : return tw;
129 : 25267 : }
130 : :
131 : 230501 : WitnessReq WitnessFormGenerator::requiresWitnessFormTransform(
132 : : Node t, Node s, MethodId idr) const
133 : : {
134 : 230501 : Node tr = d_env.rewriteViaMethod(t, idr);
135 : 230501 : Node sr = d_env.rewriteViaMethod(s, idr);
136 [ + + ]: 230501 : if (tr == sr)
137 : : {
138 : : // rewriting via the method is enough
139 : 211121 : return WitnessReq::NONE;
140 : : }
141 [ + + ]: 19380 : if (rewrite(tr) == rewrite(sr))
142 : : {
143 : : // calling ordinary rewrite after (extended) rewriting is enough
144 : 55 : return WitnessReq::REWRITE;
145 : : }
146 : 19325 : Node trw = SkolemManager::getOriginalForm(tr);
147 : 19325 : Node srw = SkolemManager::getOriginalForm(sr);
148 [ + + ]: 19325 : if (trw == srw)
149 : : {
150 : : // witness is enough
151 : 3303 : return WitnessReq::WITNESS;
152 : : }
153 : 16022 : return WitnessReq::WITNESS_AND_REWRITE;
154 : 230501 : }
155 : :
156 : 43532 : WitnessReq WitnessFormGenerator::requiresWitnessFormIntro(Node t,
157 : : MethodId idr) const
158 : : {
159 : 43532 : return requiresWitnessFormTransform(t, d_true, idr);
160 : : }
161 : :
162 : 0 : const std::unordered_set<Node>& WitnessFormGenerator::getWitnessFormEqs() const
163 : : {
164 : 0 : return d_eqs;
165 : : }
166 : :
167 : : } // namespace smt
168 : : } // namespace cvc5::internal
|
