Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Implementation of utilities for initializing subsolvers (copies of
14 : : * SolverEngine) during solving.
15 : : */
16 : :
17 : : #include "theory/smt_engine_subsolver.h"
18 : :
19 : : #include "proof/unsat_core.h"
20 : : #include "smt/env.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : :
25 : 3606 : SubsolverSetupInfo::SubsolverSetupInfo(const Options& opts,
26 : : const LogicInfo& logicInfo,
27 : : TypeNode sepLocType,
28 : 3606 : TypeNode sepDataType)
29 : : : d_opts(opts),
30 : : d_logicInfo(logicInfo),
31 : : d_sepLocType(sepLocType),
32 : 3606 : d_sepDataType(sepDataType)
33 : : {
34 : 3606 : }
35 : :
36 : 8732 : SubsolverSetupInfo::SubsolverSetupInfo(const Env& env)
37 : 8732 : : d_opts(env.getOptions()),
38 : 17464 : d_logicInfo(env.getLogicInfo()),
39 : : d_sepLocType(env.getSepLocType()),
40 : 8732 : d_sepDataType(env.getSepDataType())
41 : : {
42 : 8732 : }
43 : :
44 : 3482 : SubsolverSetupInfo::SubsolverSetupInfo(const Env& env, const Options& opts)
45 : : : d_opts(opts),
46 : 6964 : d_logicInfo(env.getLogicInfo()),
47 : : d_sepLocType(env.getSepLocType()),
48 : 3482 : d_sepDataType(env.getSepDataType())
49 : : {
50 : 3482 : }
51 : :
52 : : // optimization: try to rewrite to constant
53 : 8986 : Result quickCheck(Node& query)
54 : : {
55 [ + + ]: 8986 : if (query.isConst())
56 : : {
57 [ + + ]: 5617 : if (!query.getConst<bool>())
58 : : {
59 : 5424 : return Result(Result::UNSAT);
60 : : }
61 : : else
62 : : {
63 : 193 : return Result(Result::SAT);
64 : : }
65 : : }
66 : 3369 : return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
67 : : }
68 : :
69 : 15719 : void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
70 : : const SubsolverSetupInfo& info,
71 : : bool needsTimeout,
72 : : unsigned long timeout)
73 : : {
74 : 15719 : smte.reset(new SolverEngine(&info.d_opts));
75 : 15719 : smte->setIsInternalSubsolver();
76 : 15719 : smte->setLogic(info.d_logicInfo);
77 : : // set the options
78 [ + + ]: 15719 : if (needsTimeout)
79 : : {
80 : 1175 : smte->setTimeLimit(timeout);
81 : : }
82 : : // set up separation logic heap if necessary
83 [ + + ][ + - ]: 15719 : if (!info.d_sepLocType.isNull() && !info.d_sepDataType.isNull())
[ + + ]
84 : : {
85 : 51 : smte->declareSepHeap(info.d_sepLocType, info.d_sepDataType);
86 : : }
87 : 15719 : }
88 : 7832 : void initializeSubsolver(std::unique_ptr<SolverEngine>& smte,
89 : : const Env& env,
90 : : bool needsTimeout,
91 : : unsigned long timeout)
92 : : {
93 : 15664 : SubsolverSetupInfo ssi(env);
94 : 7832 : initializeSubsolver(smte, ssi, needsTimeout, timeout);
95 : 7832 : }
96 : :
97 : 0 : Result checkWithSubsolver(std::unique_ptr<SolverEngine>& smte,
98 : : Node query,
99 : : const SubsolverSetupInfo& info,
100 : : bool needsTimeout,
101 : : unsigned long timeout)
102 : : {
103 : 0 : Assert(query.getType().isBoolean());
104 : 0 : Result r = quickCheck(query);
105 [ - - ]: 0 : if (!r.isUnknown())
106 : : {
107 : 0 : return r;
108 : : }
109 : 0 : initializeSubsolver(smte, info, needsTimeout, timeout);
110 : 0 : smte->assertFormula(query);
111 : 0 : return smte->checkSat();
112 : : }
113 : :
114 : 5692 : Result checkWithSubsolver(Node query,
115 : : const SubsolverSetupInfo& info,
116 : : bool needsTimeout,
117 : : unsigned long timeout)
118 : : {
119 : 11384 : std::vector<Node> vars;
120 : 5692 : std::vector<Node> modelVals;
121 : : return checkWithSubsolver(
122 : 11384 : query, vars, modelVals, info, needsTimeout, timeout);
123 : : }
124 : :
125 : 8986 : Result checkWithSubsolver(Node query,
126 : : const std::vector<Node>& vars,
127 : : std::vector<Node>& modelVals,
128 : : const SubsolverSetupInfo& info,
129 : : bool needsTimeout,
130 : : unsigned long timeout)
131 : : {
132 [ - + ][ - + ]: 8986 : Assert(query.getType().isBoolean());
[ - - ]
133 [ - + ][ - + ]: 8986 : Assert(modelVals.empty());
[ - - ]
134 : : // ensure clear
135 : 8986 : modelVals.clear();
136 : 8986 : Result r = quickCheck(query);
137 [ + + ]: 8986 : if (!r.isUnknown())
138 : : {
139 [ + + ]: 5617 : if (r.getStatus() == Result::SAT)
140 : : {
141 : : // default model
142 [ + + ]: 237 : for (const Node& v : vars)
143 : : {
144 : 44 : modelVals.push_back(NodeManager::mkGroundTerm(v.getType()));
145 : : }
146 : : }
147 : 5617 : return r;
148 : : }
149 : 3369 : std::unique_ptr<SolverEngine> smte;
150 : 3369 : initializeSubsolver(smte, info, needsTimeout, timeout);
151 : 3369 : smte->assertFormula(query);
152 : 3369 : r = smte->checkSat();
153 [ + + ][ + + ]: 3369 : if (r.getStatus() == Result::SAT || r.getStatus() == Result::UNKNOWN)
[ + + ]
154 : : {
155 [ + + ]: 14036 : for (const Node& v : vars)
156 : : {
157 : 23596 : Node val = smte->getValue(v);
158 : 11798 : modelVals.push_back(val);
159 : : }
160 : : }
161 : 3369 : return r;
162 : : }
163 : :
164 : 1945 : 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 [ + + ]: 9720 : for (const Node& f : core)
170 : : {
171 : : // check if it is excluded
172 [ + + ]: 7775 : if (removed.find(f) != removed.end())
173 : : {
174 : 7 : continue;
175 : : }
176 : : // check if it is an ordinary function definition
177 [ + + ]: 7768 : if (defs.find(f) != defs.end())
178 : : {
179 [ + + ][ + - ]: 594 : if (f.getKind() == Kind::EQUAL && f[0].isVar())
[ + + ][ + + ]
[ - - ]
180 : : {
181 : 568 : subsolver.defineFunction(f[0], f[1]);
182 : 568 : continue;
183 : : }
184 : : }
185 : 7200 : subsolver.assertFormula(f);
186 : : }
187 : 1945 : }
188 : :
189 : 971 : void getModelFromSubsolver(SolverEngine& smt,
190 : : const std::vector<Node>& vars,
191 : : std::vector<Node>& vals)
192 : : {
193 [ + + ]: 3311 : for (const Node& v : vars)
194 : : {
195 : 4680 : Node mv = smt.getValue(v);
196 : 2340 : vals.push_back(mv);
197 : : }
198 : 971 : }
199 : :
200 : 2386 : bool getUnsatCoreFromSubsolver(SolverEngine& smt,
201 : : const std::unordered_set<Node>& queryAsserts,
202 : : std::vector<Node>& uasserts)
203 : : {
204 : 2386 : UnsatCore uc = smt.getUnsatCore();
205 : 2386 : bool hasQuery = false;
206 [ + + ]: 8530 : for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
207 : : {
208 : 6144 : Node uassert = *i;
209 [ + + ]: 6144 : if (queryAsserts.find(uassert) != queryAsserts.end())
210 : : {
211 : 2168 : hasQuery = true;
212 : 2168 : continue;
213 : : }
214 : 3976 : uasserts.push_back(uassert);
215 : : }
216 : 4772 : return hasQuery;
217 : : }
218 : :
219 : 206 : void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts)
220 : : {
221 : 412 : std::unordered_set<Node> queryAsserts;
222 : 206 : getUnsatCoreFromSubsolver(smt, queryAsserts, uasserts);
223 : 206 : }
224 : :
225 : : } // namespace theory
226 : : } // namespace cvc5::internal
|
