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