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