Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Gereon Kremer, Andrew Reynolds, 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 : : */
14 : : #include "main/portfolio_driver.h"
15 : :
16 : : #if HAVE_SYS_WAIT_H
17 : : #include <signal.h>
18 : : #include <sys/wait.h>
19 : : #include <unistd.h>
20 : : #endif
21 : :
22 : : #include <cvc5/cvc5.h>
23 : :
24 : : #include <chrono>
25 : : #include <cstdlib>
26 : : #include <optional>
27 : : #include <thread>
28 : :
29 : : #include "base/check.h"
30 : : #include "base/exception.h"
31 : : #include "base/output.h"
32 : : #include "main/command_executor.h"
33 : : #include "parser/commands.h"
34 : : #include "parser/command_status.h"
35 : :
36 : : using namespace cvc5::parser;
37 : :
38 : : namespace cvc5::main {
39 : :
40 : : enum SolveStatus : int
41 : : {
42 : : STATUS_SOLVED = 0,
43 : : STATUS_UNSOLVED = 1,
44 : : };
45 : :
46 : 22738 : bool ExecutionContext::solveContinuous(parser::InputParser* parser,
47 : : bool stopAtSetLogic)
48 : : {
49 : 22786 : Command cmd;
50 : 22738 : bool interrupted = false;
51 : 22738 : bool status = true;
52 [ + + ]: 712102 : while (status)
53 : : {
54 [ - + ]: 712030 : if (interrupted)
55 : : {
56 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
57 : 0 : d_executor->reset();
58 : 0 : break;
59 : : }
60 : 712030 : cmd = parser->nextCommand();
61 [ + + ]: 711984 : if (cmd.isNull())
62 : : {
63 : 19420 : break;
64 : : }
65 : 692564 : status = d_executor->doCommand(&cmd);
66 : 692562 : Cmd* cc = cmd.d_cmd.get();
67 [ - + ][ - - ]: 692562 : if (cc->interrupted() && status == 0)
[ - + ]
68 : : {
69 : 0 : interrupted = true;
70 : 0 : break;
71 : : }
72 [ + - ][ + + ]: 692562 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
73 : : {
74 : 3197 : break;
75 : : }
76 [ + + ]: 689365 : if (stopAtSetLogic)
77 : : {
78 [ + - ]: 1 : auto* slc = dynamic_cast<SetBenchmarkLogicCommand*>(cc);
79 [ + - ]: 1 : if (slc != nullptr)
80 : : {
81 : 1 : d_logic = slc->getLogic();
82 : 1 : break;
83 : : }
84 : : }
85 : : }
86 : 45380 : return status;
87 : : }
88 : :
89 : 0 : std::vector<Command> ExecutionContext::parseCommands(
90 : : parser::InputParser* parser)
91 : : {
92 : 0 : std::vector<Command> res;
93 : : while (true)
94 : : {
95 : 0 : Command cmd = parser->nextCommand();
96 [ - - ]: 0 : if (cmd.isNull())
97 : : {
98 : 0 : break;
99 : : }
100 : 0 : res.emplace_back(cmd);
101 [ - - ][ - - ]: 0 : if (dynamic_cast<QuitCommand*>(cmd.d_cmd.get()) != nullptr)
102 : : {
103 : 0 : break;
104 : : }
105 : 0 : }
106 : 0 : return res;
107 : : }
108 : :
109 : 0 : bool ExecutionContext::solveCommands(std::vector<Command>& cmds)
110 : : {
111 : 0 : bool interrupted = false;
112 : 0 : bool status = true;
113 [ - - ]: 0 : for (Command& cmd : cmds)
114 : : {
115 [ - - ]: 0 : if (interrupted)
116 : : {
117 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
118 : 0 : d_executor->reset();
119 : 0 : break;
120 : : }
121 : :
122 : 0 : status = d_executor->doCommand(&cmd);
123 : 0 : Cmd* cc = cmd.d_cmd.get();
124 : 0 : if (cc->interrupted() && status == 0)
125 : : {
126 : 0 : interrupted = true;
127 : 0 : break;
128 : : }
129 : :
130 [ - - ][ - - ]: 0 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
131 : : {
132 : 0 : break;
133 : : }
134 : : }
135 : 0 : return status;
136 : : }
137 : :
138 : : #if HAVE_SYS_WAIT_H
139 : :
140 : : namespace {
141 : :
142 : : /**
143 : : * Provides a convenient wrapper for POSIX pipes in the context of forking.
144 : : * The implemented mechanism is using a pipe to buffer the (standard or error)
145 : : * output of a child process and optionally copy it to the respective output of
146 : : * the parent process. This wrapper closely follows
147 : : * http://www.microhowto.info/howto/capture_the_output_of_a_child_process_in_c.html
148 : : */
149 : : class Pipe
150 : : {
151 : : public:
152 : : /** Open a new pipe */
153 : 2 : void open()
154 : : {
155 [ - + ]: 2 : if (pipe(d_pipe) == -1)
156 : : {
157 : 0 : throw internal::Exception("Unable to open pipe for child process");
158 : : }
159 : 2 : }
160 : : /**
161 : : * Redirects the given file descriptor fd into this pipe using dup2 and closes
162 : : * both ends of the pipe. This method should be called within the child
163 : : * process after forking to redirect standard out or error out into the pipe.
164 : : */
165 : 0 : void dup(int fd)
166 : : {
167 : : // dup2 may get interrupted by a signal. If this happens the error is EINTR
168 : : // and we can simply try again.
169 [ - - ][ - - ]: 0 : while ((dup2(d_pipe[1], fd) == -1) && (errno == EINTR))
[ - - ]
170 : : {
171 : : }
172 : 0 : close(d_pipe[0]);
173 : 0 : close(d_pipe[1]);
174 : 0 : }
175 : : /**
176 : : * Close the input of this pipe. This method should be called within the
177 : : * parent process after forking.
178 : : */
179 : 2 : void closeIn() { close(d_pipe[1]); }
180 : : /**
181 : : * Copy the content of the pipe into the given output stream. This method
182 : : * should be called within the parent process after the child process has
183 : : * terminated.
184 : : */
185 : 3 : void flushTo(std::ostream& os)
186 : : {
187 : : char buf[4096];
188 : : while (true)
189 : : {
190 : 3 : ssize_t cnt = read(d_pipe[0], buf, sizeof(buf));
191 [ - + ]: 3 : if (cnt == -1)
192 : : {
193 [ - - ]: 0 : if (errno == EINTR)
194 : : {
195 : 0 : continue;
196 : : }
197 : : else
198 : : {
199 : 0 : throw internal::Exception("Unable to read from pipe");
200 : : }
201 : : }
202 [ + + ]: 3 : else if (cnt == 0)
203 : : {
204 : 2 : break;
205 : : }
206 : 1 : os.write(buf, cnt);
207 : 1 : }
208 : 2 : }
209 : :
210 : : private:
211 : : int d_pipe[2];
212 : : };
213 : :
214 : : /**
215 : : * Manages running portfolio configurations until one has solved the input
216 : : * problem. Depending on --portfolio-jobs runs multiple jobs in parallel.
217 : : */
218 : : class PortfolioProcessPool
219 : : {
220 : : enum class JobState
221 : : {
222 : : PENDING,
223 : : RUNNING,
224 : : DONE
225 : : };
226 : : /**
227 : : * A job, consisting of the configuration, the pids of the worker and timeout
228 : : * process, the stderr and stdout pipes and the job state.
229 : : * Initially, a job is created but not started and all properties except for
230 : : * the configuration have their default value. Then starting a job, the state
231 : : * ich changed to RUNNING and the pids and pipes have their proper values. If
232 : : * no timeout is enforced, the timeout pid remains unchanged. After the job
233 : : * has finished, checkResults() eventually analyzes the jobs result and
234 : : * changes the state to DONE.
235 : : */
236 : : struct Job
237 : : {
238 : : PortfolioConfig d_config;
239 : : pid_t d_worker = -1;
240 : : pid_t d_timeout = -1;
241 : : Pipe d_errPipe;
242 : : Pipe d_outPipe;
243 : : JobState d_state = JobState::PENDING;
244 : : };
245 : :
246 : : public:
247 : 1 : PortfolioProcessPool(ExecutionContext& ctx, parser::InputParser* parser)
248 : 1 : : d_ctx(ctx),
249 : : d_parser(parser),
250 : 2 : d_maxJobs(ctx.solver().getOptionInfo("portfolio-jobs").uintValue()),
251 : 3 : d_timeout(ctx.solver().getOptionInfo("tlimit").uintValue())
252 : : {
253 : 1 : }
254 : :
255 : 1 : bool run(PortfolioStrategy& strategy)
256 : : {
257 [ + + ]: 24 : for (const auto& s : strategy.d_strategies)
258 : : {
259 [ + + ][ + + ]: 69 : d_jobs.emplace_back(Job{s});
260 : : }
261 : :
262 : : // While there are jobs to be run or jobs still running
263 [ - + ][ - - ]: 1 : while (d_nextJob < d_jobs.size() || d_running > 0)
[ + - ]
264 : : {
265 : : // Check if any job was successful
266 [ - + ]: 1 : if (checkResults())
267 : : {
268 : 0 : return true;
269 : : }
270 : :
271 : : // While we can start jobs right now
272 [ + - ][ + + ]: 2 : while (d_nextJob < d_jobs.size() && d_running < d_maxJobs)
[ + + ]
273 : : {
274 : 1 : startNextJob();
275 : : }
276 : :
277 [ + - ]: 1 : if (d_running > 0)
278 : : {
279 : 1 : int wstatus = 0;
280 : 1 : pid_t child = wait(&wstatus);
281 [ + - ]: 1 : if (checkResults(child, wstatus))
282 : : {
283 : 1 : return true;
284 : : }
285 : : }
286 : : }
287 [ - - ]: 0 : if (checkResults()) return true;
288 : :
289 : 0 : return false;
290 : : }
291 : :
292 : : private:
293 : 1 : void startNextJob()
294 : : {
295 [ - + ][ - + ]: 1 : Assert(d_nextJob < d_jobs.size());
[ - - ]
296 : 1 : Job& job = d_jobs[d_nextJob];
297 [ + - ]: 1 : Trace("portfolio") << "Starting " << job.d_config << std::endl;
298 [ + - ]: 1 : if (d_ctx.solver().isOutputOn("portfolio"))
299 : : {
300 : 1 : std::ostream& out = d_ctx.solver().getOutput("portfolio");
301 : 1 : out << "(portfolio \"" << job.d_config.toOptionString() << "\"";
302 : 1 : out << " :timeout " << job.d_config.d_timeout;
303 : 1 : out << ")" << std::endl;
304 : : }
305 : :
306 : : // Set up pipes to capture output of worker
307 : 1 : job.d_errPipe.open();
308 : 1 : job.d_outPipe.open();
309 : : // Start the worker process
310 : 1 : job.d_worker = fork();
311 [ - + ]: 1 : if (job.d_worker == -1)
312 : : {
313 : 0 : throw internal::Exception("Unable to fork");
314 : : }
315 [ - + ]: 1 : if (job.d_worker == 0)
316 : : {
317 : 0 : job.d_errPipe.dup(STDERR_FILENO);
318 : 0 : job.d_outPipe.dup(STDOUT_FILENO);
319 : 0 : job.d_config.applyOptions(d_ctx.solver());
320 : : // 0 = solved, 1 = not solved
321 : 0 : SolveStatus rc = SolveStatus::STATUS_UNSOLVED;
322 [ - - ]: 0 : if (d_ctx.solveContinuous(d_parser, false))
323 : : // if (d_ctx.solveCommands(d_commands))
324 : : {
325 : 0 : Result res = d_ctx.d_executor->getResult();
326 : 0 : if (res.isSat() || res.isUnsat())
327 : : {
328 : 0 : rc = SolveStatus::STATUS_SOLVED;
329 : : }
330 : : }
331 : 0 : _exit(rc);
332 : : }
333 : 1 : job.d_errPipe.closeIn();
334 : 1 : job.d_outPipe.closeIn();
335 : :
336 : : // Start the timeout process
337 [ - + ][ - - ]: 1 : if (d_timeout > 0 && job.d_config.d_timeout > 0)
338 : : {
339 : 0 : job.d_timeout = fork();
340 [ - - ]: 0 : if (job.d_timeout == 0)
341 : : {
342 : : auto duration = std::chrono::duration<double, std::milli>(
343 : 0 : job.d_config.d_timeout * d_timeout);
344 : 0 : std::this_thread::sleep_for(duration);
345 : 0 : kill(job.d_worker, SIGKILL);
346 : 0 : _exit(0);
347 : : }
348 : : }
349 : :
350 : 1 : ++d_nextJob;
351 : 1 : ++d_running;
352 : 1 : job.d_state = JobState::RUNNING;
353 : 1 : }
354 : :
355 : : /**
356 : : * Check whether some process terminated and solved the input. If so,
357 : : * forward the child process output to the main out and return true.
358 : : * Otherwise return false.
359 : : * If child and status are given, only the job with this particular worker is
360 : : * considered and status is assumed to be the wstatus reported by waitpid.
361 : : */
362 : 2 : bool checkResults(pid_t child = -1, int status = 0)
363 : : {
364 : : // check d_jobs for items where worker has terminated and timeout != -1
365 [ + + ]: 25 : for (auto& job : d_jobs)
366 : : {
367 : : // has not been started yet
368 [ + + ]: 24 : if (job.d_state == JobState::PENDING) continue;
369 : : // has already been analyzed
370 [ - + ]: 1 : if (job.d_state == JobState::DONE) continue;
371 : : // was given an explicit child, but this is not it.
372 [ + - ][ - + ]: 1 : if (child != -1 && job.d_worker != child) continue;
373 : :
374 : 1 : int wstatus = 0;
375 : 1 : pid_t res = 0;
376 [ - + ]: 1 : if (child == -1)
377 : : {
378 : 0 : res = waitpid(job.d_worker, &wstatus, WNOHANG);
379 : : // has not terminated yet
380 [ - - ]: 0 : if (res == 0) continue;
381 [ - - ]: 0 : if (res == -1) continue;
382 : : }
383 : : else
384 : : {
385 : 1 : res = child;
386 : 1 : wstatus = status;
387 : : }
388 : : // mark as analyzed
389 [ + - ]: 1 : Trace("portfolio") << "Finished " << job.d_config << std::endl;
390 : 1 : job.d_state = JobState::DONE;
391 : 1 : --d_running;
392 : : // check if exited normally
393 [ - + ]: 1 : if (WIFSIGNALED(wstatus))
394 : : {
395 : 0 : continue;
396 : : }
397 [ + - ]: 1 : if (WIFEXITED(wstatus))
398 : : {
399 [ + - ]: 1 : if (WEXITSTATUS(wstatus) == SolveStatus::STATUS_SOLVED)
400 : : {
401 [ + - ]: 1 : Trace("portfolio") << "Successful!" << std::endl;
402 [ + - ]: 1 : if (d_ctx.solver().isOutputOn("portfolio"))
403 : : {
404 : 1 : std::ostream& out = d_ctx.solver().getOutput("portfolio");
405 : 1 : out << "(portfolio-success \"" << job.d_config.toOptionString()
406 : 1 : << "\")" << std::endl;
407 : : }
408 : 1 : job.d_errPipe.flushTo(std::cerr);
409 : 1 : job.d_outPipe.flushTo(std::cout);
410 : 1 : return true;
411 : : }
412 : : }
413 : : }
414 : 1 : return false;
415 : : }
416 : :
417 : : ExecutionContext& d_ctx;
418 : : parser::InputParser* d_parser;
419 : : /** All jobs. */
420 : : std::vector<Job> d_jobs;
421 : : /** The id of the next job to be started within d_jobs */
422 : : size_t d_nextJob = 0;
423 : : /** The number of currently running jobs */
424 : : size_t d_running = 0;
425 : : const uint64_t d_maxJobs;
426 : : const uint64_t d_timeout;
427 : : };
428 : :
429 : : } // namespace
430 : :
431 : : #endif
432 : :
433 : 22738 : bool PortfolioDriver::solve(std::unique_ptr<CommandExecutor>& executor)
434 : : {
435 : 45476 : ExecutionContext ctx{executor.get()};
436 : 22738 : Solver& solver = ctx.solver();
437 : 22738 : bool use_portfolio = solver.getOption("use-portfolio") == "true";
438 [ + + ]: 22738 : if (!use_portfolio)
439 : : {
440 : 22737 : return ctx.solveContinuous(d_parser, false);
441 : : }
442 : : #if HAVE_SYS_WAIT_H
443 : 1 : ctx.solveContinuous(d_parser, true);
444 : :
445 [ - + ]: 1 : if (!ctx.d_logic)
446 : : {
447 : 0 : return ctx.solveContinuous(d_parser, false);
448 : : }
449 : :
450 : 2 : PortfolioStrategy strategy = getStrategy(*ctx.d_logic);
451 [ - + ][ - + ]: 1 : Assert(!strategy.d_strategies.empty()) << "The portfolio strategy should never be empty.";
[ - - ]
452 [ - + ]: 1 : if (strategy.d_strategies.size() == 1)
453 : : {
454 : 0 : strategy.d_strategies.front().applyOptions(solver);
455 : 0 : return ctx.solveContinuous(d_parser, false);
456 : : }
457 : :
458 : 1 : uint64_t total_timeout = ctx.solver().getOptionInfo("tlimit").uintValue();
459 [ + - ]: 1 : if (total_timeout == 0)
460 : : {
461 : 1 : total_timeout = 1200;
462 : : }
463 : :
464 : 2 : PortfolioProcessPool pool(ctx, d_parser); // ctx.parseCommands(d_parser));
465 : :
466 : 1 : return pool.run(strategy);
467 : : #else
468 : : Warning() << "Can't run portfolio without <sys/wait.h>.";
469 : : return ctx.solveContinuous(d_parser, false);
470 : : #endif
471 : : }
472 : :
473 : 2 : std::string PortfolioConfig::toOptionString() const
474 : : {
475 : 4 : std::stringstream ss;
476 : 2 : bool firstTime = true;
477 [ + + ]: 6 : for (const std::pair<std::string, std::string>& o : d_options)
478 : : {
479 [ + + ]: 4 : if (firstTime)
480 : : {
481 : 2 : firstTime = false;
482 : : }
483 : : else
484 : : {
485 : 2 : ss << " ";
486 : : }
487 : 4 : ss << "--";
488 [ + + ]: 4 : if (o.second == "true")
489 : : {
490 : 2 : ss << o.first;
491 : : }
492 [ - + ]: 2 : else if (o.second == "false")
493 : : {
494 : 0 : ss << "no-" << o.first;
495 : : }
496 : : else
497 : : {
498 : 2 : ss << o.first << "=" << o.second;
499 : : }
500 : : }
501 : 4 : return ss.str();
502 : : }
503 : :
504 : 0 : std::ostream& operator<<(std::ostream& os, const PortfolioConfig& config)
505 : : {
506 [ - - ]: 0 : for (const auto& o : config.d_options)
507 : : {
508 : 0 : os << o.first << "=" << o.second << " ";
509 : : }
510 : 0 : os << "timeout=" << config.d_timeout;
511 : 0 : return os;
512 : : }
513 : :
514 : : /**
515 : : * Check if the first string (the logic) is one of the remaining strings.
516 : : * Used to have a reasonably concise syntax to check the current logic against a
517 : : * lengthy list.
518 : : */
519 : : template <typename... T>
520 : 5 : bool isOneOf(const std::string& logic, T&&... list)
521 : : {
522 [ + - ][ + - ]: 5 : return ((logic == list) || ...);
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ - + ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ]
523 : : }
524 : :
525 : 1 : PortfolioStrategy PortfolioDriver::getStrategy(const std::string& logic)
526 : : {
527 : 1 : PortfolioStrategy s;
528 [ - + ]: 1 : if (isOneOf(logic, "QF_LRA"))
529 : : {
530 : 0 : s.add(0.2)
531 : 0 : .set("miplib-trick")
532 : 0 : .set("miplib-trick-subs", "4")
533 : 0 : .set("use-approx")
534 : 0 : .set("lemmas-on-replay-failure")
535 : 0 : .set("replay-early-close-depth", "4")
536 : 0 : .set("replay-lemma-reject-cut", "128")
537 : 0 : .set("replay-reject-cut", "512")
538 : 0 : .set("unconstrained-simp")
539 : 0 : .set("use-soi");
540 : 0 : s.add()
541 : 0 : .unset("restrict-pivots")
542 : 0 : .set("use-soi")
543 : 0 : .set("new-prop")
544 : 0 : .set("unconstrained-simp");
545 : : }
546 [ - + ]: 1 : else if (isOneOf(logic, "QF_LIA"))
547 : : {
548 : : // same as QF_LRA but add --pb-rewrites
549 : 0 : s.add()
550 : 0 : .set("miplib-trick")
551 : 0 : .set("miplib-trick-subs", "4")
552 : 0 : .set("use-approx")
553 : 0 : .set("lemmas-on-replay-failure")
554 : 0 : .set("replay-early-close-depth", "4")
555 : 0 : .set("replay-lemma-reject-cut", "128")
556 : 0 : .set("replay-reject-cut", "512")
557 : 0 : .set("unconstrained-simp")
558 : 0 : .set("use-soi")
559 : 0 : .set("pb-rewrites")
560 : 0 : .set("ite-simp")
561 : 0 : .set("simp-ite-compress");
562 : : }
563 [ - + ]: 1 : else if (isOneOf(logic, "QF_NIA"))
564 : : {
565 : 0 : s.add(0.35).set("nl-ext-tplanes").set("decision", "justification");
566 : 0 : s.add(0.05).set("nl-ext-tplanes").set("decision", "internal");
567 : 0 : s.add(0.05).set("nl-ext-tplanes").set("decision", "justification-old");
568 : 0 : s.add(0.05).unset("nl-ext-tplanes").set("decision", "internal");
569 : 0 : s.add(0.05)
570 : 0 : .unset("arith-brab")
571 : 0 : .set("nl-ext-tplanes")
572 : 0 : .set("decision", "internal");
573 : : // totals to more than 100%, but smaller bit-widths usually fail quickly
574 : 0 : s.add(0.25).set("solve-int-as-bv", "2").set("bitblast", "eager");
575 : 0 : s.add(0.25).set("solve-int-as-bv", "4").set("bitblast", "eager");
576 : 0 : s.add(0.25).set("solve-int-as-bv", "8").set("bitblast", "eager");
577 : 0 : s.add(0.25).set("solve-int-as-bv", "16").set("bitblast", "eager");
578 : 0 : s.add(0.5).set("solve-int-as-bv", "32").set("bitblast", "eager");
579 : 0 : s.add().set("nl-ext-tplanes").set("decision", "internal");
580 : : }
581 [ - + ]: 1 : else if (isOneOf(logic, "QF_NRA"))
582 : : {
583 : 0 : s.add(0.5).set("decision", "justification");
584 : 0 : s.add(0.25)
585 : 0 : .set("decision", "internal")
586 : 0 : .unset("nl-cov")
587 : 0 : .set("nl-ext", "full")
588 : 0 : .set("nl-ext-tplanes");
589 : 0 : s.add().set("decision", "internal").set("nl-ext", "none");
590 : : }
591 [ + - ]: 1 : else if (isOneOf(logic,
592 : : "ALIA",
593 : : "AUFLIA",
594 : : "AUFLIRA",
595 : : "AUFNIRA",
596 : : "UF",
597 : : "UFBVLIA",
598 : : "UFIDL",
599 : : "UFLIA",
600 : : "UFLRA",
601 : : "UFNIA",
602 : : "UFDT",
603 : : "UFDTLIA",
604 : : "AUFDTLIA",
605 : : "AUFBV",
606 : : "AUFBVDTLIA",
607 : : "AUFBVFP",
608 : : "AUFNIA",
609 : : "UFFPDTLIRA",
610 : : "UFFPDTNIRA"))
611 : : {
612 : : // initial runs
613 : 1 : s.add(0.025).set("simplification", "none").set("enum-inst");
614 : 1 : s.add(0.025).unset("e-matching").set("enum-inst");
615 : 1 : s.add(0.025).unset("e-matching").set("enum-inst").set("enum-inst-sum");
616 : : // trigger selections
617 : 1 : s.add(0.025).set("relevant-triggers").set("enum-inst");
618 : 1 : s.add(0.025).set("trigger-sel", "max").set("enum-inst");
619 : 1 : s.add(0.025).set("multi-trigger-when-single").set("enum-inst");
620 : 1 : s.add(0.025)
621 : 2 : .set("multi-trigger-when-single")
622 : 2 : .set("multi-trigger-priority")
623 : 1 : .set("enum-inst");
624 : 1 : s.add(0.025).set("multi-trigger-cache").set("enum-inst");
625 : 1 : s.add(0.025).unset("multi-trigger-linear").set("enum-inst");
626 : : // other
627 : 1 : s.add(0.025).set("pre-skolem-quant", "on").set("enum-inst");
628 : 1 : s.add(0.025).set("inst-when", "full").set("enum-inst");
629 : 1 : s.add(0.025).unset("e-matching").unset("cbqi").set("enum-inst");
630 : 1 : s.add(0.025).set("enum-inst").set("quant-ind");
631 : 1 : s.add(0.025)
632 : 2 : .set("decision", "internal")
633 : 2 : .set("simplification", "none")
634 : 2 : .unset("inst-no-entail")
635 : 2 : .unset("cbqi")
636 : 1 : .set("enum-inst");
637 : 1 : s.add(0.025)
638 : 2 : .set("decision", "internal")
639 : 2 : .set("enum-inst")
640 : 1 : .set("enum-inst-sum");
641 : 1 : s.add(0.025).set("term-db-mode", "relevant").set("enum-inst");
642 : 1 : s.add(0.025).set("enum-inst-interleave").set("enum-inst");
643 : : // finite model find
644 : 1 : s.add(0.025).set("finite-model-find").set("fmf-mbqi", "none");
645 : 1 : s.add(0.025).set("finite-model-find").set("decision", "internal");
646 : 1 : s.add(0.025)
647 : 2 : .set("finite-model-find")
648 : 2 : .set("macros-quant")
649 : 1 : .set("macros-quant-mode", "all");
650 : 1 : s.add(0.05).set("finite-model-find").set("e-matching");
651 : : // long runs
652 : 1 : s.add(0.2).set("finite-model-find").set("decision", "internal");
653 : 1 : s.add().set("enum-inst");
654 : : }
655 [ - - ]: 0 : else if (isOneOf(logic, "UFBV"))
656 : : {
657 : : // most problems in UFBV are essentially BV
658 : 0 : s.add(0.25).set("sygus-inst");
659 : 0 : s.add(0.25)
660 : 0 : .set("enum-inst")
661 : 0 : .set("cegqi-nested-qe")
662 : 0 : .set("decision", "internal");
663 : 0 : s.add(0.025).set("enum-inst").unset("cegqi-innermost").set("global-negate");
664 : : ;
665 : 0 : s.add().set("finite-model-find");
666 : : }
667 [ - - ]: 0 : else if (isOneOf(logic, "ABV", "BV"))
668 : : {
669 : 0 : s.add(0.1).set("enum-inst");
670 : 0 : s.add(0.1).set("sygus-inst");
671 : 0 : s.add(0.25)
672 : 0 : .set("enum-inst")
673 : 0 : .set("cegqi-nested-qe")
674 : 0 : .set("decision", "internal");
675 : 0 : s.add(0.025).set("enum-inst").unset("cegqi-bv");
676 : 0 : s.add(0.025).set("enum-inst").set("cegqi-bv-ineq", "eq-slack");
677 : 0 : s.add().set("enum-inst").unset("cegqi-innermost").set("global-negate");
678 : : }
679 [ - - ]: 0 : else if (isOneOf(logic, "ABVFP", "ABVFPLRA", "BVFP", "FP", "NIA", "NRA"))
680 : : {
681 : 0 : s.add(0.25).set("enum-inst").set("nl-ext-tplanes").set("fp-exp");
682 : 0 : s.add().set("sygus-inst").set("fp-exp");
683 : : }
684 [ - - ]: 0 : else if (isOneOf(logic, "LIA", "LRA"))
685 : : {
686 : 0 : s.add(0.025).set("enum-inst");
687 : 0 : s.add(0.25).set("enum-inst").set("cegqi-nested-qe");
688 : 0 : s.add().set("enum-inst").set("cegqi-nested-qe").set("decision", "internal");
689 : : }
690 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFBV"))
691 : : {
692 : 0 : s.add(0.5);
693 : 0 : s.add().set("decision", "justification-stoponly");
694 : : }
695 [ - - ]: 0 : else if (isOneOf(logic, "QF_ABV"))
696 : : {
697 : 0 : s.add(0.05)
698 : 0 : .set("ite-simp")
699 : 0 : .set("simp-with-care")
700 : 0 : .set("repeat-simp")
701 : 0 : .set("arrays-weak-equiv");
702 : 0 : s.add(0.5).set("arrays-weak-equiv");
703 : 0 : s.add()
704 : 0 : .set("ite-simp")
705 : 0 : .set("simp-with-care")
706 : 0 : .set("repeat-simp")
707 : 0 : .set("arrays-weak-equiv");
708 : : }
709 [ - - ]: 0 : else if (isOneOf(logic, "QF_BV", "QF_UFBV"))
710 : : {
711 : 0 : s.add().set("bitblast", "eager").set("bv-assert-input");
712 : : }
713 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFLIA"))
714 : : {
715 : 0 : s.add()
716 : 0 : .unset("arrays-eager-index")
717 : 0 : .set("arrays-eager-lemmas")
718 : 0 : .set("decision", "justification");
719 : : }
720 [ - - ]: 0 : else if (isOneOf(logic, "QF_AX"))
721 : : {
722 : 0 : s.add()
723 : 0 : .unset("arrays-eager-index")
724 : 0 : .set("arrays-eager-lemmas")
725 : 0 : .set("decision", "internal");
726 : : }
727 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFNIA"))
728 : : {
729 : 0 : s.add()
730 : 0 : .set("decision", "justification")
731 : 0 : .unset("arrays-eager-index")
732 : 0 : .set("arrays-eager-lemmas");
733 : : }
734 [ - - ]: 0 : else if (isOneOf(logic, "QF_ALIA"))
735 : : {
736 : 0 : s.add(0.15).set("decision", "justification").set("arrays-weak-equiv");
737 : 0 : s.add()
738 : 0 : .set("decision", "justification-stoponly")
739 : 0 : .unset("arrays-eager-index")
740 : 0 : .set("arrays-eager-lemmas");
741 : : }
742 [ - - ]: 0 : else if (isOneOf(logic, "QF_S", "QF_SLIA"))
743 : : {
744 : 0 : s.add(0.25).set("strings-exp").set("strings-fmf").unset("jh-rlv-order");
745 : 0 : s.add().set("strings-exp").unset("jh-rlv-order");
746 : : }
747 [ - - ]: 0 : else if (isOneOf(logic,
748 : : "QF_ABVFP",
749 : : "QF_ABVFPLRA",
750 : : "QF_BVFP",
751 : : "QF_BVFPLRA",
752 : : "QF_FP",
753 : : "QF_FPLRA"))
754 : : {
755 : 0 : s.add().set("fp-exp");
756 : : }
757 : : else
758 : : {
759 : 0 : s.add();
760 : : }
761 : 1 : return s;
762 : : }
763 : :
764 : : } // namespace cvc5::main
|
