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