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