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 : 40900 : Assertions::Assertions(Env& env)
37 : : : EnvObj(env),
38 : 40900 : d_assertionList(userContext()),
39 : 40900 : d_assertionListDefs(userContext()),
40 : 81800 : d_globalDefineFunLemmasIndex(userContext(), 0)
41 : : {
42 : 40900 : }
43 : :
44 : 36268 : Assertions::~Assertions() {}
45 : :
46 : 40415 : 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 : 40415 : size_t numGlobalDefs = d_globalDefineFunLemmas.size();
52 [ + + ]: 40532 : for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++)
53 : : {
54 : 117 : addFormula(d_globalDefineFunLemmas[i], true, false);
55 : : }
56 : 40415 : d_globalDefineFunLemmasIndex = numGlobalDefs;
57 : 40415 : }
58 : :
59 : 31686 : void Assertions::setAssumptions(const std::vector<Node>& assumptions)
60 : : {
61 : 31686 : d_assumptions.clear();
62 : 31686 : d_assumptions = assumptions;
63 : :
64 [ + + ]: 35476 : for (const Node& n : d_assumptions)
65 : : {
66 : : // Ensure expr is type-checked at this point.
67 : 3790 : ensureBoolean(n);
68 : 3790 : addFormula(n, false, false);
69 : : }
70 : 31686 : }
71 : :
72 : 144429 : void Assertions::assertFormula(const Node& n)
73 : : {
74 : 144429 : ensureBoolean(n);
75 : 144429 : bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
76 : 144429 : addFormula(n, false, maybeHasFv);
77 : 144429 : }
78 : :
79 : 22 : std::vector<Node>& Assertions::getAssumptions() { return d_assumptions; }
80 : :
81 : 79296 : const context::CDList<Node>& Assertions::getAssertionList() const
82 : : {
83 : 79296 : return d_assertionList;
84 : : }
85 : :
86 : 3982 : const context::CDList<Node>& Assertions::getAssertionListDefinitions() const
87 : : {
88 : 3982 : return d_assertionListDefs;
89 : : }
90 : :
91 : 2325 : std::unordered_set<Node> Assertions::getCurrentAssertionListDefitions() const
92 : : {
93 : 2325 : std::unordered_set<Node> defSet;
94 [ + + ]: 3008 : for (const Node& a : d_assertionListDefs)
95 : : {
96 : 683 : defSet.insert(a);
97 : : }
98 : 2325 : return defSet;
99 : 0 : }
100 : :
101 : 156930 : void Assertions::addFormula(TNode n, bool isFunDef, bool maybeHasFv)
102 : : {
103 : : // add to assertion list
104 : 156930 : d_assertionList.push_back(n);
105 [ + + ][ + + ]: 156930 : if (n.isConst() && n.getConst<bool>())
[ + + ]
106 : : {
107 : : // true, nothing to do
108 : 629 : return;
109 : : }
110 [ + - ]: 312602 : Trace("smt") << "Assertions::addFormula(" << n << ", isFunDef = " << isFunDef
111 : 156301 : << std::endl;
112 : : // In non-incremental, we treat higher-order equality as define-fun
113 [ + + ][ + + ]: 156301 : if (!options().base.incrementalSolving || isFunDef)
[ + + ]
114 : : {
115 : : // if a non-recursive define-fun, just add as a top-level substitution
116 [ + + ][ + + ]: 140627 : if (n.getKind() == Kind::EQUAL && n[0].isVar())
[ + + ][ + + ]
[ - - ]
117 : : {
118 [ + - ]: 38052 : Trace("smt-define-fun")
119 : 19026 : << "Define fun: " << n[0] << " = " << n[1] << std::endl;
120 : 19026 : NodeManager* nm = nodeManager();
121 : 19026 : TrustSubstitutionMap& tsm = d_env.getTopLevelSubstitutions();
122 : 38052 : if (!isFunDef
123 [ + + ][ + + ]: 49038 : && (tsm.get().hasSubstitution(n[0])
[ + + ][ - - ]
124 [ + + ][ + + ]: 30012 : || n[1].getKind() != Kind::LAMBDA))
[ + + ][ - - ]
125 : : {
126 : 10649 : 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 : 8377 : 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 [ + + ]: 8377 : if (n[1].getKind() == Kind::LAMBDA)
136 : : {
137 : : // Rewrite the body of the lambda.
138 : 5358 : defRewBody = tsm.applyTrusted(n[1][1], d_env.getRewriter());
139 : : }
140 : 8377 : Node defRew = n[1];
141 : : // If we rewrote the body
142 [ + + ]: 8377 : if (!defRewBody.isNull())
143 : : {
144 : : // The rewritten form is the rewritten body with original variable list.
145 : 3293 : defRew = defRewBody.getNode();
146 : 3293 : defRew = nm->mkNode(Kind::LAMBDA, n[1][0], defRew);
147 : : }
148 [ + + ]: 8377 : if (expr::hasSubterm(defRew, n[0]))
149 : : {
150 : 16 : return;
151 : : }
152 : : // if we need to track proofs
153 [ + + ]: 8361 : if (d_env.isProofProducing())
154 : : {
155 : : // initialize the proof generator if not already done so
156 [ + + ]: 3248 : if (d_defFunRewPf == nullptr)
157 : : {
158 : 568 : 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 : 6496 : d_defFunRewPf->addStep(n, ProofRule::ASSUME, {}, {n});
163 : : // If changed, prove the rewrite
164 [ + + ]: 3248 : if (defRew != n[1])
165 : : {
166 : 1187 : Node eqBody = defRewBody.getProven();
167 : 1187 : d_defFunRewPf->addLazyStep(eqBody, defRewBody.getGenerator());
168 : 1187 : Node eqRew = n[1].eqNode(defRew);
169 [ - + ][ - + ]: 1187 : Assert(n[1].getKind() == Kind::LAMBDA);
[ - - ]
170 : : // congruence over the binder
171 : 1187 : std::vector<Node> cargs;
172 : 1187 : ProofRule cr = expr::getCongRule(n[1], cargs);
173 : 2374 : 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 : 1187 : Node eqFinal = n[0].eqNode(defRew);
182 [ + + ][ - - ]: 3561 : d_defFunRewPf->addStep(eqFinal, ProofRule::TRANS, {n, eqRew}, {});
183 : 1187 : }
184 : : }
185 [ + - ]: 8361 : Trace("smt-define-fun") << "...rewritten to " << defRew << std::endl;
186 : 8361 : d_assertionListDefs.push_back(n);
187 [ + + ]: 16722 : d_env.getTopLevelSubstitutions().addSubstitution(
188 : 8361 : n[0], defRew, d_defFunRewPf.get());
189 : 8361 : return;
190 : 8377 : }
191 : : }
192 : :
193 : : // Ensure that it does not contain free variables
194 [ + + ]: 137275 : 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 [ - + ]: 1761 : 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 : 8699 : void Assertions::addDefineFunDefinition(Node n, bool global)
222 : : {
223 [ + + ]: 8699 : 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 [ - + ][ - + ]: 105 : Assert(!language::isLangSygus(options().base.inputLanguage));
[ - - ]
228 : 105 : 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 : 8594 : bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
236 : 8594 : addFormula(n, true, maybeHasFv);
237 : : }
238 : 8699 : }
239 : :
240 : 148219 : void Assertions::ensureBoolean(const Node& n)
241 : : {
242 : 148219 : TypeNode type = n.getType(options().expr.typeChecking);
243 [ - + ]: 148219 : 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 : 148219 : }
252 : :
253 : : } // namespace smt
254 : : } // namespace cvc5::internal
|
