Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, 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 : : * Utility for constructing and maintaining abstract values.
14 : : */
15 : :
16 : : #include "smt/check_models.h"
17 : :
18 : : #include "base/modal_exception.h"
19 : : #include "expr/non_closed_node_converter.h"
20 : : #include "options/quantifiers_options.h"
21 : : #include "options/smt_options.h"
22 : : #include "smt/env.h"
23 : : #include "smt/expand_definitions.h"
24 : : #include "smt/preprocessor.h"
25 : : #include "smt/set_defaults.h"
26 : : #include "smt/smt_solver.h"
27 : : #include "theory/rewriter.h"
28 : : #include "theory/smt_engine_subsolver.h"
29 : : #include "theory/theory_model.h"
30 : : #include "theory/trust_substitutions.h"
31 : :
32 : : using namespace cvc5::internal::theory;
33 : :
34 : : namespace cvc5::internal {
35 : : namespace smt {
36 : :
37 : 0 : void getTheoriesOf(Env& env, const Node& n, std::vector<TheoryId>& theories)
38 : : {
39 : 0 : std::unordered_set<TNode> visited;
40 : 0 : std::vector<TNode> visit;
41 : 0 : TNode cur;
42 : 0 : visit.push_back(n);
43 : 0 : do
44 : : {
45 : 0 : cur = visit.back();
46 : 0 : visit.pop_back();
47 [ - - ]: 0 : if (visited.find(cur) == visited.end())
48 : : {
49 : 0 : visited.insert(cur);
50 : : // get the theories of the term and its type
51 : 0 : TheoryId tid = env.theoryOf(cur);
52 [ - - ]: 0 : if (std::find(theories.begin(), theories.end(), tid) == theories.end())
53 : : {
54 : 0 : theories.push_back(tid);
55 : : }
56 : 0 : TheoryId ttid = env.theoryOf(cur.getType());
57 [ - - ]: 0 : if (ttid!=tid)
58 : : {
59 [ - - ]: 0 : if (std::find(theories.begin(), theories.end(), ttid) == theories.end())
60 : : {
61 : 0 : theories.push_back(ttid);
62 : : }
63 : : }
64 : 0 : visit.insert(visit.end(), cur.begin(), cur.end());
65 : : }
66 [ - - ]: 0 : } while (!visit.empty());
67 : 0 : }
68 : :
69 : 2411 : CheckModels::CheckModels(Env& e) : EnvObj(e) {}
70 : :
71 : 3077 : void CheckModels::checkModel(TheoryModel* m,
72 : : const context::CDList<Node>& al,
73 : : bool hardFailure)
74 : : {
75 : : // Throughout, we use verbose(1) to give diagnostic output.
76 : : //
77 : : // If this function is running, the user gave --check-model (or equivalent),
78 : : // and if verbose(1) is on, the user gave --verbose (or equivalent).
79 : :
80 : 3077 : Node sepHeap, sepNeq;
81 [ - + ]: 3077 : if (m->getHeapModel(sepHeap, sepNeq))
82 : : {
83 : : throw RecoverableModalException(
84 : 0 : "Cannot run check-model on a model with a separation logic heap.");
85 : : }
86 [ + + ]: 3077 : if (options().quantifiers.fmfFunWellDefined)
87 : : {
88 : 4 : warning() << "Running check-model is not guaranteed to pass when fmf-fun "
89 : 4 : "is enabled."
90 : 4 : << std::endl;
91 : : // only throw warning
92 : 4 : hardFailure = false;
93 : : }
94 : : // expand definitions module and substitutions
95 : 3077 : std::unordered_map<Node, Node> ecache;
96 : 3077 : ExpandDefs expDef(d_env);
97 : :
98 : 3077 : theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
99 [ + - ]: 3077 : Trace("check-model") << "checkModel: Check assertions..." << std::endl;
100 : 3077 : std::unordered_map<Node, Node> cache;
101 : : // the list of assertions that did not rewrite to true
102 : 3077 : std::vector<Node> noCheckList;
103 : : // Now go through all our user assertions checking if they're satisfied.
104 [ + + ]: 27338 : for (const Node& assertion : al)
105 : : {
106 : 48522 : verbose(1) << "SolverEngine::checkModel(): checking assertion " << assertion
107 : 24261 : << std::endl;
108 : :
109 : : // Apply any define-funs from the problem. We do not expand theory symbols
110 : : // like integer division here. Hence, the code below is not able to properly
111 : : // evaluate e.g. divide-by-zero. This is intentional since the evaluation
112 : : // is not trustworthy, since the UF introduced by expanding definitions may
113 : : // not be properly constrained.
114 : 24261 : Node n = sm.apply(assertion);
115 : 48522 : verbose(1) << "SolverEngine::checkModel(): -- substitutes to " << n
116 : 24261 : << std::endl;
117 : :
118 : : // Expand definitions, which is required for being accurate for operators
119 : : // that expand involving skolems during preprocessing. Not doing this will
120 : : // increase the spurious warnings raised by this class.
121 : 24261 : n = expDef.expandDefinitions(n, cache);
122 : 24261 : bool checkAgain = false;
123 : 24261 : bool processed = false;
124 : 24261 : Node nval;
125 [ + - ]: 15 : do
126 : : {
127 : 24276 : checkAgain = false;
128 : 48552 : verbose(1) << "SolverEngine::checkModel(): -- expands to " << n
129 : 24276 : << std::endl;
130 : :
131 : 24276 : n = rewrite(n);
132 : 48552 : verbose(1) << "SolverEngine::checkModel(): -- rewrites to " << n
133 : 24276 : << std::endl;
134 : :
135 : 24276 : nval = m->getValue(n);
136 : 48552 : verbose(1) << "SolverEngine::checkModel(): -- get value : " << n
137 : 24276 : << std::endl;
138 : :
139 [ + + ][ + - ]: 24276 : if (nval.isConst() && nval.getConst<bool>())
[ + + ]
140 : : {
141 : : // assertion is true, everything is fine
142 : 24178 : processed = true;
143 : 24178 : break;
144 : : }
145 : :
146 : : // Otherwise, we did not succeed in showing the current assertion to be
147 : : // true. This may either indicate that our model is wrong, or that we
148 : : // cannot check it. The latter may be the case for several reasons. One
149 : : // example is the occurrence of partial operators. Another example are
150 : : // quantified formulas, which are not checkable, although we assign them
151 : : // to true/false based on the satisfying assignment. However, quantified
152 : : // formulas can be modified during preprocess, so they may not correspond
153 : : // to those in the satisfying assignment. Hence we throw warnings for
154 : : // assertions that do not simplify to either true or false. Other theories
155 : : // such as non-linear arithmetic (in particular, transcendental functions)
156 : : // also have the property of not being able to be checked precisely here.
157 : : // Note that warnings like these can be avoided for quantified formulas
158 : : // by making preprocessing passes explicitly record how they
159 : : // rewrite quantified formulas (see cvc4-wishues#43).
160 [ + - ]: 98 : if (!nval.isConst())
161 : : {
162 : 98 : n = expDef.expandDefinitions(nval, cache);
163 [ + + ]: 98 : if (n != nval)
164 : : {
165 : : // It could be that we can expand again after simplifying. This is
166 : : // the case e.g. if a quantified formula with division is simplified
167 : : // to a quantifier-free formula.
168 : 15 : checkAgain = true;
169 : : }
170 : : else
171 : : {
172 : : // Note that we must be a "closed" term, i.e. one that can be
173 : : // given in an assertion.
174 : 83 : if (options().smt.checkModelSubsolver
175 [ + - ][ + + ]: 83 : && NonClosedNodeConverter::isClosed(d_env, nval))
[ + + ]
176 : : {
177 [ + - ]: 66 : Trace("check-model-subsolver") << "Query is " << nval << std::endl;
178 : : // satisfiability call
179 : 66 : Options subOptions;
180 : 66 : subOptions.copyValues(options());
181 : 66 : smt::SetDefaults::disableChecking(subOptions);
182 : : // initialize the subsolver
183 : 66 : SubsolverSetupInfo ssi(d_env, subOptions);
184 : 0 : std::unique_ptr<SolverEngine> checkModelChecker;
185 : 66 : initializeSubsolver(nodeManager(), checkModelChecker, ssi);
186 : 66 : checkModelChecker->assertFormula(nval);
187 : 66 : Result r = checkModelChecker->checkSat();
188 [ + - ]: 66 : Trace("check-model-subsolver") << "..result is " << r << std::endl;
189 [ + + ]: 66 : if (r == Result::SAT)
190 : : {
191 : 63 : processed = true;
192 : 63 : break;
193 : : }
194 : : }
195 : : // Not constant, print a less severe warning message here.
196 : 20 : warning() << "Warning : SolverEngine::checkModel(): cannot check "
197 : : "simplified "
198 : 20 : "assertion : "
199 : 20 : << nval << std::endl;
200 : 20 : noCheckList.push_back(nval);
201 : 20 : processed = true;
202 : 20 : break;
203 : : }
204 : : }
205 : : } while (checkAgain);
206 : : // If processed in the loop above, we go to the next term
207 [ + - ]: 24261 : if (processed)
208 : : {
209 : 24261 : continue;
210 : : }
211 : : // Assertions that simplify to false result in an InternalError or
212 : : // Warning being thrown below (when hardFailure is false).
213 : 0 : verbose(1) << "SolverEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
214 : 0 : << std::endl;
215 : 0 : std::stringstream ss;
216 : : ss << "SolverEngine::checkModel(): "
217 : 0 : << "ERRORS SATISFYING ASSERTIONS WITH MODEL";
218 : 0 : std::stringstream ssdet;
219 : 0 : ssdet << ":" << std::endl
220 : 0 : << "assertion: " << assertion << std::endl
221 : 0 : << "simplifies to: " << nval << std::endl
222 : 0 : << "expected `true'." << std::endl
223 : 0 : << "Run with `--check-models -v' for additional diagnostics.";
224 [ - - ]: 0 : if (hardFailure)
225 : : {
226 : : // compute the theories involved, e.g. for the sake of issue tracking.
227 : : // to ensure minimality, if this is a topmost AND, miniscope
228 : 0 : Node nmin = n;
229 [ - - ]: 0 : while (nmin.getKind() == Kind::AND)
230 : : {
231 [ - - ]: 0 : for (const Node& nc : nmin)
232 : : {
233 [ - - ]: 0 : if (m->getValue(nc) == nval)
234 : : {
235 : 0 : nmin = nc;
236 : 0 : break;
237 : : }
238 : : }
239 : : }
240 : : // collect the theories of the assertion
241 : 0 : std::vector<TheoryId> theories;
242 : 0 : getTheoriesOf(d_env, nmin, theories);
243 : 0 : std::sort(theories.begin(), theories.end());
244 : 0 : ss << " {";
245 [ - - ]: 0 : for (TheoryId tid : theories)
246 : : {
247 [ - - ]: 0 : if (tid != THEORY_BOOL)
248 : : {
249 : 0 : ss << " " << tid;
250 : : }
251 : : }
252 : 0 : ss << " }";
253 : : // internal error if hardFailure is true
254 : 0 : InternalError() << ss.str() << ssdet.str();
255 : : }
256 : : else
257 : : {
258 : 0 : warning() << ss.str() << ssdet.str() << std::endl;
259 : : }
260 : : }
261 [ + + ]: 3077 : if (noCheckList.empty())
262 : : {
263 : 3060 : verbose(1) << "SolverEngine::checkModel(): all assertions checked out OK !"
264 : 3060 : << std::endl;
265 : 3060 : return;
266 : : }
267 : : // if the noCheckList is non-empty, we could expand definitions on this list
268 : : // and check satisfiability
269 : :
270 [ + - ]: 17 : Trace("check-model") << "checkModel: Finish" << std::endl;
271 : : }
272 : :
273 : : } // namespace smt
274 : : } // namespace cvc5::internal
|
