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 : : * Implementation of utilities for initializing subsolvers (copies of
11 : : * SolverEngine) during solving.
12 : : */
13 : :
14 : : #include "theory/smt_engine_subsolver.h"
15 : :
16 : : #include "proof/unsat_core.h"
17 : : #include "smt/env.h"
18 : :
19 : : namespace cvc5::internal {
20 : : namespace theory {
21 : :
22 : 3751 : SubsolverSetupInfo::SubsolverSetupInfo(const Options& opts,
23 : : const LogicInfo& logicInfo,
24 : : TypeNode sepLocType,
25 : 3751 : TypeNode sepDataType)
26 : 3751 : : d_opts(opts),
27 : 3751 : d_logicInfo(logicInfo),
28 : 3751 : d_sepLocType(sepLocType),
29 : 3751 : d_sepDataType(sepDataType)
30 : : {
31 : 3751 : }
32 : :
33 : 7568 : SubsolverSetupInfo::SubsolverSetupInfo(const Env& env)
34 : 7568 : : d_opts(env.getOptions()),
35 : 7568 : d_logicInfo(env.getLogicInfo()),
36 : 7568 : d_sepLocType(env.getSepLocType()),
37 : 7568 : d_sepDataType(env.getSepDataType())
38 : : {
39 : 7568 : }
40 : :
41 : 3203 : SubsolverSetupInfo::SubsolverSetupInfo(const Env& env, const Options& opts)
42 : 3203 : : d_opts(opts),
43 : 3203 : d_logicInfo(env.getLogicInfo()),
44 : 3203 : d_sepLocType(env.getSepLocType()),
45 : 3203 : d_sepDataType(env.getSepDataType())
46 : : {
47 : 3203 : }
48 : :
49 : : // optimization: try to rewrite to constant
50 : 8471 : Result quickCheck(Node& query)
51 : : {
52 [ + + ]: 8471 : if (query.isConst())
53 : : {
54 [ + + ]: 4941 : if (!query.getConst<bool>())
55 : : {
56 : 4770 : return Result(Result::UNSAT);
57 : : }
58 : : else
59 : : {
60 : 171 : return Result(Result::SAT);
61 : : }
62 : : }
63 : 3530 : return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
64 : : }
65 : :
66 : 14415 : void initializeSubsolver(NodeManager* nm,
67 : : std::unique_ptr<SolverEngine>& smte,
68 : : const SubsolverSetupInfo& info,
69 : : bool needsTimeout,
70 : : unsigned long timeout)
71 : : {
72 : 14415 : smte.reset(new SolverEngine(nm, &info.d_opts));
73 : 14415 : smte->setIsInternalSubsolver();
74 : 14415 : smte->setLogic(info.d_logicInfo);
75 : : // set the options
76 [ + + ]: 14415 : if (needsTimeout)
77 : : {
78 : 1345 : smte->setTimeLimit(timeout);
79 : : }
80 : : // set up separation logic heap if necessary
81 [ + + ][ + - ]: 14415 : if (!info.d_sepLocType.isNull() && !info.d_sepDataType.isNull())
[ + + ]
82 : : {
83 : 51 : smte->declareSepHeap(info.d_sepLocType, info.d_sepDataType);
84 : : }
85 : 14415 : }
86 : 7108 : void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
87 : : const Env& env,
88 : : bool needsTimeout,
89 : : unsigned long timeout)
90 : : {
91 : 7108 : SubsolverSetupInfo ssi(env);
92 : 7108 : initializeSubsolver(env.getNodeManager(), smte, ssi, needsTimeout, timeout);
93 : 7108 : }
94 : :
95 : 0 : Result checkWithSubsolver(std::unique_ptr<SolverEngine>& smte,
96 : : Node query,
97 : : const SubsolverSetupInfo& info,
98 : : bool needsTimeout,
99 : : unsigned long timeout)
100 : : {
101 : 0 : Assert(query.getType().isBoolean());
102 : 0 : Result r = quickCheck(query);
103 [ - - ]: 0 : if (!r.isUnknown())
104 : : {
105 : 0 : return r;
106 : : }
107 : 0 : initializeSubsolver(
108 : : query.getNodeManager(), smte, info, needsTimeout, timeout);
109 : 0 : smte->assertFormula(query);
110 : 0 : return smte->checkSat();
111 : 0 : }
112 : :
113 : 5034 : Result checkWithSubsolver(Node query,
114 : : const SubsolverSetupInfo& info,
115 : : bool needsTimeout,
116 : : unsigned long timeout)
117 : : {
118 : 5034 : std::vector<Node> vars;
119 : 5034 : std::vector<Node> modelVals;
120 : : return checkWithSubsolver(
121 : 10068 : query, vars, modelVals, info, needsTimeout, timeout);
122 : 5034 : }
123 : :
124 : 8471 : Result checkWithSubsolver(Node query,
125 : : const std::vector<Node>& vars,
126 : : std::vector<Node>& modelVals,
127 : : const SubsolverSetupInfo& info,
128 : : bool needsTimeout,
129 : : unsigned long timeout)
130 : : {
131 [ - + ][ - + ]: 8471 : Assert(query.getType().isBoolean());
[ - - ]
132 [ - + ][ - + ]: 8471 : Assert(modelVals.empty());
[ - - ]
133 : : // ensure clear
134 : 8471 : modelVals.clear();
135 : 8471 : Result r = quickCheck(query);
136 [ + + ]: 8471 : if (!r.isUnknown())
137 : : {
138 [ + + ]: 4941 : if (r.getStatus() == Result::SAT)
139 : : {
140 : : // default model
141 [ + + ]: 215 : for (const Node& v : vars)
142 : : {
143 : 44 : modelVals.push_back(NodeManager::mkGroundTerm(v.getType()));
144 : : }
145 : : }
146 : 4941 : return r;
147 : : }
148 : 3530 : std::unique_ptr<SolverEngine> smte;
149 : 3530 : initializeSubsolver(
150 : : query.getNodeManager(), smte, info, needsTimeout, timeout);
151 : 3530 : smte->assertFormula(query);
152 : 3530 : r = smte->checkSat();
153 [ + + ][ + + ]: 3530 : if (r.getStatus() == Result::SAT || r.getStatus() == Result::UNKNOWN)
[ + + ]
154 : : {
155 [ + + ]: 13832 : for (const Node& v : vars)
156 : : {
157 : 11509 : Node val = smte->getValue(v);
158 : 11509 : modelVals.push_back(val);
159 : 11509 : }
160 : : }
161 : 3530 : return r;
162 : 3530 : }
163 : :
164 : 2162 : void assertToSubsolver(SolverEngine& subsolver,
165 : : const std::vector<Node>& core,
166 : : const std::unordered_set<Node>& defs,
167 : : const std::unordered_set<Node>& removed)
168 : : {
169 [ + + ]: 10270 : for (const Node& f : core)
170 : : {
171 : : // check if it is excluded
172 [ + + ]: 8108 : if (removed.find(f) != removed.end())
173 : : {
174 : 7 : continue;
175 : : }
176 : : // check if it is an ordinary function definition
177 [ + + ]: 8101 : if (defs.find(f) != defs.end())
178 : : {
179 [ + - ][ + - ]: 628 : if (f.getKind() == Kind::EQUAL && f[0].isVar())
[ + - ][ + - ]
[ - - ]
180 : : {
181 : 628 : subsolver.defineFunction(f[0], f[1]);
182 : 628 : continue;
183 : : }
184 : : }
185 : 7473 : subsolver.assertFormula(f);
186 : : }
187 : 2162 : }
188 : :
189 : 763 : void getModelFromSubsolver(SolverEngine& smt,
190 : : const std::vector<Node>& vars,
191 : : std::vector<Node>& vals)
192 : : {
193 [ + + ]: 2421 : for (const Node& v : vars)
194 : : {
195 : 1658 : Node mv = smt.getValue(v);
196 : 1658 : vals.push_back(mv);
197 : 1658 : }
198 : 763 : }
199 : :
200 : 1730 : bool getUnsatCoreFromSubsolver(SolverEngine& smt,
201 : : const std::unordered_set<Node>& queryAsserts,
202 : : std::vector<Node>& uasserts)
203 : : {
204 : 1730 : UnsatCore uc = smt.getUnsatCore();
205 : 1730 : bool hasQuery = false;
206 [ + + ]: 5448 : for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
207 : : {
208 : 3718 : Node uassert = *i;
209 [ + + ]: 3718 : if (queryAsserts.find(uassert) != queryAsserts.end())
210 : : {
211 : 1686 : hasQuery = true;
212 : 1686 : continue;
213 : : }
214 : 2032 : uasserts.push_back(uassert);
215 [ + + ]: 3718 : }
216 : 1730 : return hasQuery;
217 : 1730 : }
218 : :
219 : 204 : void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts)
220 : : {
221 : 204 : std::unordered_set<Node> queryAsserts;
222 : 204 : getUnsatCoreFromSubsolver(smt, queryAsserts, uasserts);
223 : 204 : }
224 : :
225 : : } // namespace theory
226 : : } // namespace cvc5::internal
|
