Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Andres Noetzli
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 storing assertions for an SMT engine.
14 : : */
15 : :
16 : : #include "smt/assertions.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "base/modal_exception.h"
21 : : #include "expr/node_algorithm.h"
22 : : #include "options/base_options.h"
23 : : #include "options/expr_options.h"
24 : : #include "options/language.h"
25 : : #include "options/smt_options.h"
26 : : #include "proof/lazy_proof.h"
27 : : #include "proof/proof_node_algorithm.h"
28 : : #include "smt/env.h"
29 : : #include "theory/trust_substitutions.h"
30 : : #include "util/result.h"
31 : :
32 : : using namespace cvc5::internal::theory;
33 : : using namespace cvc5::internal::kind;
34 : :
35 : : namespace cvc5::internal {
36 : : namespace smt {
37 : :
38 : 72393 : Assertions::Assertions(Env& env)
39 : : : EnvObj(env),
40 : 144786 : d_assertionList(userContext()),
41 : 144786 : d_assertionListDefs(userContext()),
42 : 72393 : d_globalDefineFunLemmasIndex(userContext(), 0)
43 : : {
44 : 72393 : }
45 : :
46 : 67747 : Assertions::~Assertions()
47 : : {
48 : 67747 : }
49 : :
50 : 70219 : void Assertions::refresh()
51 : : {
52 : : // Global definitions are asserted now to ensure they always exist. This is
53 : : // done at the beginning of preprocessing, to ensure that definitions take
54 : : // priority over, e.g. solving during preprocessing. See issue #7479.
55 : 70219 : size_t numGlobalDefs = d_globalDefineFunLemmas.size();
56 [ + + ]: 72660 : for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
57 : : {
58 : 2441 : addFormula(d_globalDefineFunLemmas[i], true, false);
59 : : }
60 : 70219 : d_globalDefineFunLemmasIndex = numGlobalDefs;
61 : 70219 : }
62 : :
63 : 51414 : void Assertions::setAssumptions(const std::vector<Node>& assumptions)
64 : : {
65 : 51414 : d_assumptions.clear();
66 : 51414 : d_assumptions = assumptions;
67 : :
68 [ + + ]: 59228 : for (const Node& n : d_assumptions)
69 : : {
70 : : // Ensure expr is type-checked at this point.
71 : 7814 : ensureBoolean(n);
72 : 7814 : addFormula(n, false, false);
73 : : }
74 : 51414 : }
75 : :
76 : 200505 : void Assertions::assertFormula(const Node& n)
77 : : {
78 : 200505 : ensureBoolean(n);
79 : 200505 : bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
80 : 200505 : addFormula(n, false, maybeHasFv);
81 : 200505 : }
82 : :
83 : 225 : std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
84 : :
85 : 106050 : const context::CDList<Node>& Assertions::getAssertionList() const
86 : : {
87 : 106050 : return d_assertionList;
88 : : }
89 : :
90 : 6379 : const context::CDList<Node>& Assertions::getAssertionListDefinitions() const
91 : : {
92 : 6379 : return d_assertionListDefs;
93 : : }
94 : :
95 : 2058 : std::unordered_set<Node> Assertions::getCurrentAssertionListDefitions() const
96 : : {
97 : 2058 : std::unordered_set<Node> defSet;
98 [ + + ]: 2667 : for (const Node& a : d_assertionListDefs)
99 : : {
100 : 609 : defSet.insert(a);
101 : : }
102 : 2058 : return defSet;
103 : : }
104 : :
105 : 228738 : void Assertions::addFormula(TNode n,
106 : : bool isFunDef,
107 : : bool maybeHasFv)
108 : : {
109 : : // add to assertion list
110 : 228738 : d_assertionList.push_back(n);
111 [ + + ]: 228738 : if (isFunDef)
112 : : {
113 : 20419 : d_assertionListDefs.push_back(n);
114 : : }
115 [ + + ][ + + ]: 228738 : if (n.isConst() && n.getConst<bool>())
[ + + ]
116 : : {
117 : : // true, nothing to do
118 : 4810 : return;
119 : : }
120 [ + - ]: 447856 : Trace("smt") << "Assertions::addFormula(" << n
121 : 223928 : << ", isFunDef = " << isFunDef << std::endl;
122 [ + + ]: 223928 : if (isFunDef)
123 : : {
124 : : // if a non-recursive define-fun, just add as a top-level substitution
125 [ + + ][ + - ]: 20419 : if (n.getKind() == Kind::EQUAL && n[0].isVar())
[ + + ][ + + ]
[ - - ]
126 : : {
127 [ + - ]: 26400 : Trace("smt-define-fun")
128 : 13200 : << "Define fun: " << n[0] << " = " << n[1] << std::endl;
129 : 13200 : NodeManager* nm = nodeManager();
130 : 13200 : TrustSubstitutionMap& tsm = d_env.getTopLevelSubstitutions();
131 : : // If it is a lambda, we rewrite the body, otherwise we rewrite itself.
132 : : // For lambdas, we prefer rewriting only the body since we don't want
133 : : // higher-order rewrites (e.g. value normalization) to apply by default.
134 : 26400 : TrustNode defRewBody;
135 : : // For efficiency, we only do this if it is a lambda.
136 : : // Note this is important since some benchmarks treat define-fun as a
137 : : // global let. We should not eagerly rewrite in these cases.
138 [ + + ]: 13200 : if (n[1].getKind() == Kind::LAMBDA)
139 : : {
140 : : // Rewrite the body of the lambda.
141 : 7202 : defRewBody = tsm.applyTrusted(n[1][1], d_env.getRewriter());
142 : : }
143 : 13200 : Node defRew = n[1];
144 : : // If we rewrote the body
145 [ + + ]: 13200 : if (!defRewBody.isNull())
146 : : {
147 : : // The rewritten form is the rewritten body with original variable list.
148 : 3209 : defRew = defRewBody.getNode();
149 : 3209 : defRew = nm->mkNode(Kind::LAMBDA, n[1][0], defRew);
150 : : }
151 : : // if we need to track proofs
152 [ + + ]: 13200 : if (d_env.isProofProducing())
153 : : {
154 : : // initialize the proof generator if not already done so
155 [ + + ]: 3869 : if (d_defFunRewPf == nullptr)
156 : : {
157 : 606 : d_defFunRewPf = std::make_shared<LazyCDProof>(d_env);
158 : : }
159 : : // A define-fun is an assumption in the overall proof, thus
160 : : // we justify the substitution with ASSUME here.
161 : 7738 : d_defFunRewPf->addStep(n, ProofRule::ASSUME, {}, {n});
162 : : // If changed, prove the rewrite
163 [ + + ]: 3869 : if (defRew != n[1])
164 : : {
165 : 2570 : Node eqBody = defRewBody.getProven();
166 : 1285 : d_defFunRewPf->addLazyStep(eqBody, defRewBody.getGenerator());
167 : 2570 : Node eqRew = n[1].eqNode(defRew);
168 [ - + ][ - + ]: 1285 : Assert (n[1].getKind() == Kind::LAMBDA);
[ - - ]
169 : : // congruence over the binder
170 : 2570 : std::vector<Node> cargs;
171 : 1285 : ProofRule cr = expr::getCongRule(n[1], cargs);
172 : 2570 : d_defFunRewPf->addStep(eqRew, cr, {eqBody}, cargs);
173 : : // Proof is:
174 : : // ------ from tsm
175 : : // t = t'
176 : : // ------------------ ASSUME -------------------------- CONG
177 : : // n = lambda x. t lambda x. t = lambda x. t'
178 : : // ------------------------------------------------------ TRANS
179 : : // n = lambda x. t'
180 : 1285 : Node eqFinal = n[0].eqNode(defRew);
181 [ + + ][ - - ]: 3855 : d_defFunRewPf->addStep(eqFinal, ProofRule::TRANS, {n, eqRew}, {});
182 : : }
183 : : }
184 [ + - ]: 13200 : Trace("smt-define-fun") << "...rewritten to " << defRew << std::endl;
185 [ + + ]: 26400 : d_env.getTopLevelSubstitutions().addSubstitution(
186 : 13200 : n[0], defRew, d_defFunRewPf.get());
187 : 13200 : return;
188 : : }
189 : : }
190 : :
191 : : // Ensure that it does not contain free variables
192 [ + + ]: 210728 : if (maybeHasFv)
193 : : {
194 : : // Note that API users and the smt2 parser may generate assertions with
195 : : // shadowed variables, which are resolved during rewriting. Hence we do not
196 : : // check for this here.
197 [ - + ]: 2262 : if (expr::hasFreeVar(n))
198 : : {
199 : 0 : std::stringstream se;
200 [ - - ]: 0 : if (isFunDef)
201 : : {
202 : 0 : se << "Cannot process function definition with free variable.";
203 : : }
204 : : else
205 : : {
206 : 0 : se << "Cannot process assertion with free variable.";
207 [ - - ]: 0 : if (language::isLangSygus(options().base.inputLanguage))
208 : : {
209 : : // Common misuse of SyGuS is to use top-level assert instead of
210 : : // constraint when defining the synthesis conjecture.
211 : 0 : se << " Perhaps you meant `constraint` instead of `assert`?";
212 : : }
213 : : }
214 : 0 : throw ModalException(se.str().c_str());
215 : : }
216 : : }
217 : : }
218 : :
219 : 19697 : void Assertions::addDefineFunDefinition(Node n, bool global)
220 : : {
221 [ + + ]: 19697 : if (global)
222 : : {
223 : : // Global definitions are asserted at check-sat-time because we have to
224 : : // make sure that they are always present
225 [ - + ][ - + ]: 1719 : Assert(!language::isLangSygus(options().base.inputLanguage));
[ - - ]
226 : 1719 : d_globalDefineFunLemmas.emplace_back(n);
227 : : }
228 : : else
229 : : {
230 : : // We don't permit functions-to-synthesize within recursive function
231 : : // definitions currently. Thus, we should check for free variables if the
232 : : // input language is SyGuS.
233 : 17978 : bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
234 : 17978 : addFormula(n, true, maybeHasFv);
235 : : }
236 : 19697 : }
237 : :
238 : 208319 : void Assertions::ensureBoolean(const Node& n)
239 : : {
240 : 416638 : TypeNode type = n.getType(options().expr.typeChecking);
241 [ - + ]: 208319 : if (!type.isBoolean())
242 : : {
243 : 0 : std::stringstream ss;
244 : : ss << "Expected Boolean type\n"
245 : 0 : << "The assertion : " << n << "\n"
246 : 0 : << "Its type : " << type;
247 : 0 : throw TypeCheckingExceptionPrivate(n, ss.str());
248 : : }
249 : 208319 : }
250 : :
251 : : } // namespace smt
252 : : } // namespace cvc5::internal
|
