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 : : * Rewrite database
11 : : */
12 : :
13 : : #include "rewriter/rewrite_db.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "rewriter/rewrite_db_term_process.h"
17 : : #include "rewriter/rewrites.h"
18 : :
19 : : using namespace cvc5::internal::kind;
20 : :
21 : : namespace cvc5::internal {
22 : : namespace rewriter {
23 : :
24 : 8921755 : uint32_t IsListTypeClassCallback::getTypeClass(TNode v)
25 : : {
26 [ + + ]: 8921755 : return expr::isListVar(v) ? 1 : 0;
27 : : }
28 : :
29 : 6943 : RewriteDb::RewriteDb(NodeManager* nm) : d_canonCb(), d_canon(&d_canonCb)
30 : : {
31 : 6943 : d_true = nm->mkConst(true);
32 : 6943 : d_false = nm->mkConst(false);
33 : 6943 : rewriter::addRules(nm, *this);
34 : :
35 [ - + ]: 6943 : if (TraceIsOn("rewrite-db"))
36 : : {
37 [ - - ]: 0 : Trace("rewrite-db") << "Rewrite database:" << std::endl;
38 [ - - ]: 0 : Trace("rewrite-db") << "START" << std::endl;
39 : 0 : Trace("rewrite-db") << d_mt.debugPrint();
40 [ - - ]: 0 : Trace("rewrite-db") << "END" << std::endl;
41 : : }
42 : 6943 : }
43 : :
44 : 3041034 : void RewriteDb::addRule(ProofRewriteRule id,
45 : : const std::vector<Node> fvs,
46 : : Node a,
47 : : Node b,
48 : : Node cond,
49 : : Node context,
50 : : Level _level)
51 : : {
52 : 3041034 : NodeManager* nm = a.getNodeManager();
53 : 3041034 : std::vector<Node> fvsf = fvs;
54 : 3041034 : std::vector<Node> condsn;
55 : 3041034 : Node eq = a.eqNode(b);
56 : : // we canonize left-to-right, hence we should traverse in the opposite
57 : : // order, since we index based on conclusion, we make a dummy node here
58 : 3041034 : std::vector<Node> tmpArgs;
59 : 3041034 : tmpArgs.push_back(eq);
60 : 3041034 : tmpArgs.push_back(cond);
61 [ + + ]: 3041034 : if (!context.isNull())
62 : : {
63 : 118031 : tmpArgs.push_back(context);
64 : : }
65 : 3041034 : Node tmp = nm->mkNode(Kind::SEXPR, tmpArgs);
66 : :
67 : : // must canonize
68 [ + - ]: 6082068 : Trace("rewrite-db") << "Add rule " << id << ": " << cond << " => " << a
69 : 3041034 : << " == " << b << std::endl;
70 [ - + ][ - + ]: 3041034 : Assert(a.getType().isComparableTo(b.getType()));
[ - - ]
71 : 3041034 : Node ctmp = d_canon.getCanonicalTerm(tmp, false, false);
72 [ + + ]: 3041034 : if (!context.isNull())
73 : : {
74 : 118031 : context = ctmp[2];
75 : : }
76 : :
77 : 3041034 : Node condC = ctmp[1];
78 : 3041034 : std::vector<Node> conds;
79 [ + + ]: 3041034 : if (condC.getKind() == Kind::AND)
80 : : {
81 [ + + ]: 2291190 : for (const Node& c : condC)
82 : : {
83 : : // should flatten in proof inference listing
84 [ - + ][ - + ]: 1666320 : Assert(c.getKind() != Kind::AND);
[ - - ]
85 : 1666320 : conds.push_back(c);
86 : 1666320 : }
87 : : }
88 [ + + ]: 2416164 : else if (!condC.isConst())
89 : : {
90 : 777616 : conds.push_back(condC);
91 : : }
92 [ - + ]: 1638548 : else if (!condC.getConst<bool>())
93 : : {
94 : : // skip those with false condition
95 : 0 : return;
96 : : }
97 : : // make as expected matching: top symbol of all conditions is equality
98 : : // this means (not p) becomes (= p false), p becomes (= p true)
99 [ + + ]: 5484970 : for (size_t i = 0, nconds = conds.size(); i < nconds; i++)
100 : : {
101 [ + + ]: 2443936 : if (conds[i].getKind() == Kind::NOT)
102 : : {
103 : 333264 : conds[i] = conds[i][0].eqNode(d_false);
104 : : }
105 [ + + ]: 2110672 : else if (conds[i].getKind() != Kind::EQUAL)
106 : : {
107 : 708186 : conds[i] = conds[i].eqNode(d_true);
108 : : }
109 : : }
110 : : // register side conditions?
111 : :
112 : 3041034 : Node eqC = ctmp[0];
113 [ - + ][ - + ]: 3041034 : Assert(eqC.getKind() == Kind::EQUAL);
[ - - ]
114 : :
115 : : // add to discrimination tree
116 [ + - ]: 3041034 : Trace("proof-db-debug") << "Add (canonical) rule " << eqC << std::endl;
117 : 3041034 : d_mt.addTerm(eqC[0]);
118 : :
119 : : // match to get canonical variables
120 : 3041034 : std::unordered_map<Node, Node> msubs;
121 [ - + ]: 3041034 : if (!expr::match(eq, eqC, msubs))
122 : : {
123 : 0 : DebugUnhandled();
124 : : }
125 : 3041034 : std::unordered_map<Node, Node>::iterator its;
126 : 3041034 : std::vector<Node> ofvs;
127 : 3041034 : std::vector<Node> cfvs;
128 [ + + ]: 11844758 : for (const Node& v : fvsf)
129 : : {
130 : 8803724 : its = msubs.find(v);
131 [ + - ]: 8803724 : if (its != msubs.end())
132 : : {
133 : 8803724 : ofvs.push_back(v);
134 : 8803724 : cfvs.push_back(its->second);
135 [ + + ]: 8803724 : if (expr::isListVar(v))
136 : : {
137 : : // mark the canonical variable as a list variable as well
138 : 1062279 : expr::markListVar(its->second);
139 : : }
140 : : }
141 : : else
142 : : {
143 : 0 : Unhandled() << "In DSL rule " << id << ", variable " << v
144 : 0 : << " is unused, dropping it" << std::endl;
145 : : }
146 : : // remember the free variables
147 : 8803724 : d_allFv.insert(v);
148 : : }
149 : :
150 : : // initialize rule
151 : 3041034 : d_rewDbRule[id].init(id, ofvs, cfvs, conds, eqC, context, _level);
152 : 3041034 : d_concToRules[eqC].push_back(id);
153 : 3041034 : d_headToRules[eqC[0]].push_back(id);
154 [ + - ][ + - ]: 3041034 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
155 : :
156 : 891077 : void RewriteDb::getMatches(const Node& eq, expr::NotifyMatch* ntm)
157 : : {
158 : 891077 : d_mt.getMatches(eq, ntm);
159 : 891077 : }
160 : :
161 : 1995643 : const RewriteProofRule& RewriteDb::getRule(ProofRewriteRule id) const
162 : : {
163 : : std::map<ProofRewriteRule, RewriteProofRule>::const_iterator it =
164 : 1995643 : d_rewDbRule.find(id);
165 [ - + ][ - + ]: 1995643 : Assert(it != d_rewDbRule.end());
[ - - ]
166 : 1995643 : return it->second;
167 : : }
168 : :
169 : 0 : const std::vector<ProofRewriteRule>& RewriteDb::getRuleIdsForConclusion(
170 : : const Node& eq) const
171 : : {
172 : : std::map<Node, std::vector<ProofRewriteRule> >::const_iterator it =
173 : 0 : d_concToRules.find(eq);
174 [ - - ]: 0 : if (it != d_concToRules.end())
175 : : {
176 : 0 : return it->second;
177 : : }
178 : 0 : return d_emptyVec;
179 : : }
180 : :
181 : 1046284 : const std::vector<ProofRewriteRule>& RewriteDb::getRuleIdsForHead(
182 : : const Node& eq) const
183 : : {
184 : : std::map<Node, std::vector<ProofRewriteRule> >::const_iterator it =
185 : 1046284 : d_headToRules.find(eq);
186 [ + - ]: 1046284 : if (it != d_headToRules.end())
187 : : {
188 : 1046284 : return it->second;
189 : : }
190 : 0 : return d_emptyVec;
191 : : }
192 : 0 : const std::unordered_set<Node>& RewriteDb::getAllFreeVariables() const
193 : : {
194 : 0 : return d_allFv;
195 : : }
196 : :
197 : 0 : const std::map<ProofRewriteRule, RewriteProofRule>& RewriteDb::getAllRules()
198 : : const
199 : : {
200 : 0 : return d_rewDbRule;
201 : : }
202 : :
203 : : } // namespace rewriter
204 : : } // namespace cvc5::internal
|
