Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Gereon Kremer, Daniel Larraz, Andrew Reynolds
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 : : */
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 : 23697 : bool ExecutionContext::solveContinuous(parser::InputParser* parser,
47 : : bool stopAtSetLogic,
48 : : bool stopAtCheckSat)
49 : : {
50 : 23757 : Command cmd;
51 : 23697 : bool interrupted = false;
52 : 23697 : bool status = true;
53 [ + + ]: 688370 : while (status)
54 : : {
55 [ - + ]: 688279 : if (interrupted)
56 : : {
57 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
58 : 0 : d_executor->reset();
59 : 0 : break;
60 : : }
61 : 688279 : cmd = parser->nextCommand();
62 [ + + ]: 688221 : if (cmd.isNull())
63 : : {
64 : 20511 : break;
65 : : }
66 : 667710 : Cmd* cc = cmd.d_cmd.get();
67 [ + + ]: 667710 : if (stopAtCheckSat)
68 : : {
69 [ + - ][ + + ]: 4 : if (dynamic_cast<CheckSatCommand*>(cc) != nullptr)
70 : : {
71 : 1 : d_hasReadCheckSat = true;
72 : 1 : break;
73 : : }
74 : : }
75 : 667709 : status = d_executor->doCommand(&cmd);
76 [ - + ][ - - ]: 667707 : if (cc->interrupted() && status == 0)
[ - + ]
77 : : {
78 : 0 : interrupted = true;
79 : 0 : break;
80 : : }
81 [ + - ][ + + ]: 667707 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
82 : : {
83 : 3033 : break;
84 : : }
85 [ + + ]: 664674 : if (stopAtSetLogic)
86 : : {
87 [ + - ]: 1 : auto* slc = dynamic_cast<SetBenchmarkLogicCommand*>(cc);
88 [ + - ]: 1 : if (slc != nullptr)
89 : : {
90 : 1 : d_logic = slc->getLogic();
91 : 1 : break;
92 : : }
93 : : }
94 : : }
95 : 47274 : return status;
96 : : }
97 : :
98 : 0 : bool ExecutionContext::continueAfterSolving(parser::InputParser* parser)
99 : : {
100 : 0 : Command cmd;
101 : 0 : bool interrupted = false;
102 : 0 : bool status = true;
103 [ - - ]: 0 : while (status)
104 : : {
105 [ - - ]: 0 : if (interrupted)
106 : : {
107 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
108 : 0 : d_executor->reset();
109 : 0 : break;
110 : : }
111 : 0 : cmd = parser->nextCommand();
112 [ - - ]: 0 : if (cmd.isNull())
113 : : {
114 : 0 : break;
115 : : }
116 : 0 : Cmd* cc = cmd.d_cmd.get();
117 [ - - ][ - - ]: 0 : if (dynamic_cast<GetModelCommand*>(cc) != nullptr)
118 : : {
119 : : try
120 : : {
121 : 0 : std::string result = solver().getModel(d_sorts, d_terms);
122 : 0 : solver().getDriverOptions().out() << result;
123 : 0 : status = true;
124 : : }
125 : 0 : catch (std::exception& e)
126 : : {
127 : 0 : status = false;
128 : : }
129 : : }
130 [ - - ][ - - ]: 0 : else if (dynamic_cast<GetUnsatCoreCommand*>(cc) != nullptr)
131 : : {
132 : : try
133 : : {
134 : 0 : std::vector<cvc5::Term> core = solver().getUnsatCore();
135 : 0 : std::ostream& out = solver().getDriverOptions().out();
136 : 0 : out << "(" << std::endl;
137 [ - - ]: 0 : for (const cvc5::Term& t : core)
138 : : {
139 : 0 : auto it = d_named_terms.find(t);
140 [ - - ]: 0 : if (it != d_named_terms.end())
141 : : {
142 : 0 : out << it->second << std::endl;
143 : : }
144 : : }
145 : 0 : out << ")" << std::endl;
146 : 0 : status = true;
147 : : }
148 : 0 : catch (std::exception& e)
149 : : {
150 : 0 : status = false;
151 : : }
152 : : }
153 : : else
154 : : {
155 : 0 : status = d_executor->doCommand(&cmd);
156 : : }
157 : 0 : if (cc->interrupted() && status == 0)
158 : : {
159 : 0 : interrupted = true;
160 : 0 : break;
161 : : }
162 [ - - ][ - - ]: 0 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
163 : : {
164 : 0 : break;
165 : : }
166 : : }
167 : 0 : return status;
168 : : }
169 : :
170 : 0 : bool ExecutionContext::runCheckSatCommand()
171 : : {
172 : 0 : std::shared_ptr<Cmd> cmd(new CheckSatCommand());
173 : 0 : Command command(cmd);
174 : 0 : return d_executor->doCommand(&command);
175 : : }
176 : :
177 : 0 : void ExecutionContext::storeDeclarationsAndNamedTerms()
178 : : {
179 : 0 : SymbolManager* sm = d_executor->getSymbolManager();
180 : 0 : d_sorts = sm->getDeclaredSorts();
181 : 0 : d_terms = sm->getDeclaredTerms();
182 : 0 : d_named_terms = sm->getNamedTerms();
183 : 0 : }
184 : :
185 : 0 : bool ExecutionContext::runResetCommand()
186 : : {
187 : 0 : std::shared_ptr<Cmd> cmd(new ResetCommand());
188 : 0 : Command command(cmd);
189 : 0 : return d_executor->doCommand(&command);
190 : : }
191 : :
192 : 0 : std::vector<Command> ExecutionContext::parseCommands(
193 : : parser::InputParser* parser)
194 : : {
195 : 0 : std::vector<Command> res;
196 : : while (true)
197 : : {
198 : 0 : Command cmd = parser->nextCommand();
199 [ - - ]: 0 : if (cmd.isNull())
200 : : {
201 : 0 : break;
202 : : }
203 : 0 : res.emplace_back(cmd);
204 [ - - ][ - - ]: 0 : if (dynamic_cast<QuitCommand*>(cmd.d_cmd.get()) != nullptr)
205 : : {
206 : 0 : break;
207 : : }
208 : 0 : }
209 : 0 : return res;
210 : : }
211 : :
212 : 0 : bool ExecutionContext::solveCommands(std::vector<Command>& cmds)
213 : : {
214 : 0 : bool interrupted = false;
215 : 0 : bool status = true;
216 [ - - ]: 0 : for (Command& cmd : cmds)
217 : : {
218 [ - - ]: 0 : if (interrupted)
219 : : {
220 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
221 : 0 : d_executor->reset();
222 : 0 : break;
223 : : }
224 : :
225 : 0 : status = d_executor->doCommand(&cmd);
226 : 0 : Cmd* cc = cmd.d_cmd.get();
227 : 0 : if (cc->interrupted() && status == 0)
228 : : {
229 : 0 : interrupted = true;
230 : 0 : break;
231 : : }
232 : :
233 [ - - ][ - - ]: 0 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
234 : : {
235 : 0 : break;
236 : : }
237 : : }
238 : 0 : return status;
239 : : }
240 : :
241 : : #if HAVE_SYS_WAIT_H
242 : :
243 : : namespace {
244 : :
245 : : /**
246 : : * Provides a convenient wrapper for POSIX pipes in the context of forking.
247 : : * The implemented mechanism is using a pipe to buffer the (standard or error)
248 : : * output of a child process and optionally copy it to the respective output of
249 : : * the parent process. This wrapper closely follows
250 : : * http://www.microhowto.info/howto/capture_the_output_of_a_child_process_in_c.html
251 : : */
252 : : class Pipe
253 : : {
254 : : public:
255 : : /** Open a new pipe */
256 : 2 : void open()
257 : : {
258 [ - + ]: 2 : if (pipe(d_pipe) == -1)
259 : : {
260 : 0 : throw internal::Exception("Unable to open pipe for child process");
261 : : }
262 : 2 : }
263 : : /**
264 : : * Redirects the given file descriptor fd into this pipe using dup2 and closes
265 : : * both ends of the pipe. This method should be called within the child
266 : : * process after forking to redirect standard out or error out into the pipe.
267 : : */
268 : 0 : void dup(int fd)
269 : : {
270 : : // dup2 may get interrupted by a signal. If this happens the error is EINTR
271 : : // and we can simply try again.
272 [ - - ][ - - ]: 0 : while ((dup2(d_pipe[1], fd) == -1) && (errno == EINTR))
[ - - ]
273 : : {
274 : : }
275 : 0 : close(d_pipe[0]);
276 : 0 : close(d_pipe[1]);
277 : 0 : }
278 : : /**
279 : : * Close the input of this pipe. This method should be called within the
280 : : * parent process after forking.
281 : : */
282 : 2 : void closeIn() { close(d_pipe[1]); }
283 : : /**
284 : : * Copy the content of the pipe into the given output stream. This method
285 : : * should be called within the parent process after the child process has
286 : : * terminated.
287 : : */
288 : 3 : void flushTo(std::ostream& os)
289 : : {
290 : : char buf[4096];
291 : : while (true)
292 : : {
293 : 3 : ssize_t cnt = read(d_pipe[0], buf, sizeof(buf));
294 [ - + ]: 3 : if (cnt == -1)
295 : : {
296 [ - - ]: 0 : if (errno == EINTR)
297 : : {
298 : 0 : continue;
299 : : }
300 : : else
301 : : {
302 : 0 : throw internal::Exception("Unable to read from pipe");
303 : : }
304 : : }
305 [ + + ]: 3 : else if (cnt == 0)
306 : : {
307 : 2 : break;
308 : : }
309 : 1 : os.write(buf, cnt);
310 : 1 : }
311 : 2 : }
312 : :
313 : : private:
314 : : int d_pipe[2];
315 : : };
316 : :
317 : 1 : void printPortfolioConfig(Solver& solver, PortfolioConfig& config)
318 : : {
319 : 1 : bool dry_run = solver.getOption("portfolio-dry-run") == "true";
320 : 1 : if (dry_run || solver.isOutputOn("portfolio"))
321 : : {
322 [ - + ]: 1 : std::ostream& out = (dry_run) ? solver.getDriverOptions().out()
323 : 1 : : solver.getOutput("portfolio");
324 : 1 : out << "(portfolio \"" << config.toOptionString() << "\"";
325 : 1 : out << " :timeout " << config.d_timeout;
326 : 1 : out << ")" << std::endl;
327 : : }
328 : 1 : }
329 : :
330 : : /**
331 : : * Manages running portfolio configurations until one has solved the input
332 : : * problem. Depending on --portfolio-jobs runs multiple jobs in parallel.
333 : : */
334 : : class PortfolioProcessPool
335 : : {
336 : : enum class JobState
337 : : {
338 : : PENDING,
339 : : RUNNING,
340 : : DONE
341 : : };
342 : : /**
343 : : * A job, consisting of the configuration, the pids of the worker and timeout
344 : : * process, the stderr and stdout pipes and the job state.
345 : : * Initially, a job is created but not started and all properties except for
346 : : * the configuration have their default value. Then starting a job, the state
347 : : * ich changed to RUNNING and the pids and pipes have their proper values. If
348 : : * no timeout is enforced, the timeout pid remains unchanged. After the job
349 : : * has finished, checkResults() eventually analyzes the jobs result and
350 : : * changes the state to DONE.
351 : : */
352 : : struct Job
353 : : {
354 : 25 : Job(PortfolioConfig config)
355 : 25 : : d_config(config),
356 : : d_worker(-1),
357 : : d_timeout(-1),
358 : : d_errPipe(),
359 : : d_outPipe(),
360 [ + + ][ + + ]: 75 : d_state(JobState::PENDING)
361 : : {
362 : 25 : }
363 : : PortfolioConfig d_config;
364 : : pid_t d_worker;
365 : : pid_t d_timeout;
366 : : Pipe d_errPipe;
367 : : Pipe d_outPipe;
368 : : JobState d_state;
369 : : };
370 : :
371 : : public:
372 : 1 : PortfolioProcessPool(ExecutionContext& ctx, parser::InputParser* parser, uint64_t timeout)
373 : 1 : : d_ctx(ctx),
374 : : d_parser(parser),
375 : 2 : d_maxJobs(ctx.solver().getOptionInfo("portfolio-jobs").uintValue()),
376 : 2 : d_timeout(timeout)
377 : : {
378 : 1 : }
379 : :
380 : 1 : bool run(PortfolioStrategy& strategy)
381 : : {
382 [ + + ]: 26 : for (const auto& s : strategy.d_strategies)
383 : : {
384 : 25 : d_jobs.emplace_back(Job{s});
385 : : }
386 : :
387 : : // While there are jobs to be run or jobs still running
388 [ - + ][ - - ]: 1 : while (d_nextJob < d_jobs.size() || d_running > 0)
[ + - ]
389 : : {
390 : : // Check if any job was successful
391 [ - + ]: 1 : if (checkResults())
392 : : {
393 : 0 : return true;
394 : : }
395 : :
396 : : // While we can start jobs right now
397 [ + - ][ + + ]: 2 : while (d_nextJob < d_jobs.size() && d_running < d_maxJobs)
[ + + ]
398 : : {
399 : 1 : startNextJob();
400 : : }
401 : :
402 [ + - ]: 1 : if (d_running > 0)
403 : : {
404 : 1 : int wstatus = 0;
405 : 1 : pid_t child = wait(&wstatus);
406 [ + - ]: 1 : if (checkResults(child, wstatus))
407 : : {
408 : 1 : return true;
409 : : }
410 : : }
411 : : }
412 [ - - ]: 0 : if (checkResults()) return true;
413 : :
414 : 0 : return false;
415 : : }
416 : :
417 : : private:
418 : 1 : void startNextJob()
419 : : {
420 [ - + ][ - + ]: 1 : Assert(d_nextJob < d_jobs.size());
[ - - ]
421 : 1 : Job& job = d_jobs[d_nextJob];
422 [ + - ]: 1 : Trace("portfolio") << "Starting " << job.d_config << std::endl;
423 : 1 : printPortfolioConfig(d_ctx.solver(), job.d_config);
424 : :
425 : : // Set up pipes to capture output of worker
426 : 1 : job.d_errPipe.open();
427 : 1 : job.d_outPipe.open();
428 : : // Start the worker process
429 : 1 : job.d_worker = fork();
430 [ - + ]: 1 : if (job.d_worker == -1)
431 : : {
432 : 0 : throw internal::Exception("Unable to fork");
433 : : }
434 [ - + ]: 1 : if (job.d_worker == 0)
435 : : {
436 : 0 : job.d_errPipe.dup(STDERR_FILENO);
437 : 0 : job.d_outPipe.dup(STDOUT_FILENO);
438 : :
439 : 0 : std::vector<cvc5::Term> assertions = d_ctx.solver().getAssertions();
440 : 0 : std::string logic = d_ctx.solver().getLogic();
441 : :
442 : : std::string produceUnsatCoresValue =
443 : 0 : d_ctx.solver().getOption("produce-unsat-cores");
444 : : std::string produceModelsValue =
445 : 0 : d_ctx.solver().getOption("produce-models");
446 : 0 : d_ctx.storeDeclarationsAndNamedTerms();
447 : :
448 : 0 : d_ctx.runResetCommand();
449 : :
450 : 0 : d_ctx.solver().setOption("produce-unsat-cores", produceUnsatCoresValue);
451 : 0 : d_ctx.solver().setOption("produce-models", produceModelsValue);
452 : 0 : job.d_config.applyOptions(d_ctx.solver());
453 : 0 : d_ctx.solver().setLogic(logic);
454 : :
455 [ - - ]: 0 : for (Term& t : assertions)
456 : : {
457 : 0 : d_ctx.solver().assertFormula(t);
458 : : }
459 : : // 0 = solved, 1 = not solved
460 : 0 : SolveStatus rc = SolveStatus::STATUS_UNSOLVED;
461 [ - - ]: 0 : if (d_ctx.runCheckSatCommand())
462 : : // if (d_ctx.solveCommands(d_commands))
463 : : {
464 : 0 : Result res = d_ctx.d_executor->getResult();
465 : 0 : d_ctx.continueAfterSolving(d_parser);
466 : 0 : if (res.isSat() || res.isUnsat())
467 : : {
468 : 0 : rc = SolveStatus::STATUS_SOLVED;
469 : : }
470 : : }
471 : 0 : _exit(rc);
472 : : }
473 : 1 : job.d_errPipe.closeIn();
474 : 1 : job.d_outPipe.closeIn();
475 : :
476 : : // Start the timeout process
477 [ + - ][ + - ]: 1 : if (d_timeout > 0 && job.d_config.d_timeout > 0)
478 : : {
479 : 1 : job.d_timeout = fork();
480 [ - + ]: 1 : if (job.d_timeout == 0)
481 : : {
482 : : auto duration = std::chrono::duration<double, std::milli>(
483 : 0 : job.d_config.d_timeout * d_timeout);
484 : 0 : std::this_thread::sleep_for(duration);
485 : 0 : kill(job.d_worker, SIGKILL);
486 : 0 : _exit(0);
487 : : }
488 : : }
489 : :
490 : 1 : ++d_nextJob;
491 : 1 : ++d_running;
492 : 1 : job.d_state = JobState::RUNNING;
493 : 1 : }
494 : :
495 : : /**
496 : : * Check whether some process terminated and solved the input. If so,
497 : : * forward the child process output to the main out and return true.
498 : : * Otherwise return false.
499 : : * If child and status are given, only the job with this particular worker is
500 : : * considered and status is assumed to be the wstatus reported by waitpid.
501 : : */
502 : 2 : bool checkResults(pid_t child = -1, int status = 0)
503 : : {
504 : : // check d_jobs for items where worker has terminated and timeout != -1
505 [ + + ]: 27 : for (auto& job : d_jobs)
506 : : {
507 : : // has not been started yet
508 [ + + ]: 26 : if (job.d_state == JobState::PENDING) continue;
509 : : // has already been analyzed
510 [ - + ]: 1 : if (job.d_state == JobState::DONE) continue;
511 : : // was given an explicit child, but this is not it.
512 [ + - ][ - + ]: 1 : if (child != -1 && job.d_worker != child) continue;
513 : :
514 : 1 : int wstatus = 0;
515 : 1 : pid_t res = 0;
516 [ - + ]: 1 : if (child == -1)
517 : : {
518 : 0 : res = waitpid(job.d_worker, &wstatus, WNOHANG);
519 : : // has not terminated yet
520 [ - - ]: 0 : if (res == 0) continue;
521 [ - - ]: 0 : if (res == -1) continue;
522 : : }
523 : : else
524 : : {
525 : 1 : res = child;
526 : 1 : wstatus = status;
527 : : }
528 : : // mark as analyzed
529 [ + - ]: 1 : Trace("portfolio") << "Finished " << job.d_config << std::endl;
530 : : // terminate the corresponding timeout process if it is still running
531 [ + - ]: 1 : if (job.d_timeout > 0)
532 : : {
533 : 1 : kill(job.d_timeout, SIGKILL);
534 : : }
535 : 1 : job.d_state = JobState::DONE;
536 : 1 : --d_running;
537 : : // check if exited normally
538 [ - + ]: 1 : if (WIFSIGNALED(wstatus))
539 : : {
540 : 0 : continue;
541 : : }
542 [ + - ]: 1 : if (WIFEXITED(wstatus))
543 : : {
544 [ + - ]: 1 : if (WEXITSTATUS(wstatus) == SolveStatus::STATUS_SOLVED)
545 : : {
546 [ + - ]: 1 : Trace("portfolio") << "Successful!" << std::endl;
547 [ + - ]: 1 : if (d_ctx.solver().isOutputOn("portfolio"))
548 : : {
549 : 1 : std::ostream& out = d_ctx.solver().getOutput("portfolio");
550 : 1 : out << "(portfolio-success \"" << job.d_config.toOptionString()
551 : 1 : << "\")" << std::endl;
552 : : }
553 : 1 : job.d_errPipe.flushTo(std::cerr);
554 : 1 : job.d_outPipe.flushTo(std::cout);
555 : 1 : return true;
556 : : }
557 : : }
558 : : }
559 : 1 : return false;
560 : : }
561 : :
562 : : ExecutionContext& d_ctx;
563 : : parser::InputParser* d_parser;
564 : : /** All jobs. */
565 : : std::vector<Job> d_jobs;
566 : : /** The id of the next job to be started within d_jobs */
567 : : size_t d_nextJob = 0;
568 : : /** The number of currently running jobs */
569 : : size_t d_running = 0;
570 : : const uint64_t d_maxJobs;
571 : : const uint64_t d_timeout;
572 : : };
573 : :
574 : : } // namespace
575 : :
576 : : #endif
577 : :
578 : 23696 : bool PortfolioDriver::solve(std::unique_ptr<CommandExecutor>& executor)
579 : : {
580 : 47392 : ExecutionContext ctx{executor.get()};
581 : 23696 : Solver& solver = ctx.solver();
582 : 23696 : bool use_portfolio = solver.getOption("use-portfolio") == "true";
583 [ + + ]: 23696 : if (!use_portfolio)
584 : : {
585 : 23695 : return ctx.solveContinuous(d_parser, false);
586 : : }
587 : : #if HAVE_SYS_WAIT_H
588 : 1 : ctx.solveContinuous(d_parser, true);
589 : :
590 [ - + ]: 1 : if (!ctx.d_logic)
591 : : {
592 : 0 : return ctx.solveContinuous(d_parser, false);
593 : : }
594 : :
595 : 1 : bool dry_run = solver.getOption("portfolio-dry-run") == "true";
596 : :
597 : 1 : bool incremental_solving = solver.getOption("incremental") == "true";
598 : 2 : PortfolioStrategy strategy = getStrategy(incremental_solving, *ctx.d_logic);
599 [ - + ][ - + ]: 1 : Assert(!strategy.d_strategies.empty()) << "The portfolio strategy should never be empty.";
[ - - ]
600 [ - + ]: 1 : if (strategy.d_strategies.size() == 1)
601 : : {
602 : 0 : PortfolioConfig& config = strategy.d_strategies.front();
603 : 0 : printPortfolioConfig(ctx.solver(), config);
604 [ - - ]: 0 : if (dry_run) return true;
605 : 0 : config.applyOptions(solver);
606 : 0 : return ctx.solveContinuous(d_parser, false);
607 : : }
608 : :
609 : 1 : uint64_t total_timeout = ctx.solver().getOptionInfo("tlimit").uintValue();
610 [ + - ]: 1 : if (total_timeout == 0)
611 : : {
612 : 1 : total_timeout = 1'200'000; // miliseconds
613 : : }
614 : :
615 [ - + ]: 1 : if (dry_run)
616 : : {
617 [ - - ]: 0 : for (PortfolioConfig& config : strategy.d_strategies)
618 : : {
619 : 0 : printPortfolioConfig(ctx.solver(), config);
620 : : }
621 : 0 : return true;
622 : : }
623 : :
624 : 1 : bool uninterrupted = ctx.solveContinuous(d_parser, false, true);
625 [ + - ][ + - ]: 1 : if (uninterrupted && ctx.d_hasReadCheckSat)
626 : : {
627 : 1 : PortfolioProcessPool pool(ctx, d_parser, total_timeout); // ctx.parseCommands(d_parser));
628 : 1 : bool solved = pool.run(strategy);
629 [ - + ]: 1 : if (!solved)
630 : : {
631 : 0 : std::cout << "unknown" << std::endl;
632 : : }
633 : 1 : return solved;
634 : : }
635 : 0 : return uninterrupted;
636 : : #else
637 : : Warning() << "Can't run portfolio without <sys/wait.h>.";
638 : : return ctx.solveContinuous(d_parser, false);
639 : : #endif
640 : : }
641 : :
642 : 2 : std::string PortfolioConfig::toOptionString() const
643 : : {
644 : 4 : std::stringstream ss;
645 : 2 : bool firstTime = true;
646 [ + + ]: 6 : for (const std::pair<std::string, std::string>& o : d_options)
647 : : {
648 [ + + ]: 4 : if (firstTime)
649 : : {
650 : 2 : firstTime = false;
651 : : }
652 : : else
653 : : {
654 : 2 : ss << " ";
655 : : }
656 : 4 : ss << "--";
657 [ + + ]: 4 : if (o.second == "true")
658 : : {
659 : 2 : ss << o.first;
660 : : }
661 [ - + ]: 2 : else if (o.second == "false")
662 : : {
663 : 0 : ss << "no-" << o.first;
664 : : }
665 : : else
666 : : {
667 : 2 : ss << o.first << "=" << o.second;
668 : : }
669 : : }
670 : 4 : return ss.str();
671 : : }
672 : :
673 : 0 : std::ostream& operator<<(std::ostream& os, const PortfolioConfig& config)
674 : : {
675 [ - - ]: 0 : for (const auto& o : config.d_options)
676 : : {
677 : 0 : os << o.first << "=" << o.second << " ";
678 : : }
679 : 0 : os << "timeout=" << config.d_timeout;
680 : 0 : return os;
681 : : }
682 : :
683 : : /**
684 : : * Check if the first string (the logic) is one of the remaining strings.
685 : : * Used to have a reasonably concise syntax to check the current logic against a
686 : : * lengthy list.
687 : : */
688 : : template <typename... T>
689 : 5 : bool isOneOf(const std::string& logic, T&&... list)
690 : : {
691 [ + - ][ + - ]: 5 : return ((logic == list) || ...);
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ - + ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
692 : : }
693 : :
694 : 1 : PortfolioStrategy PortfolioDriver::getStrategy(bool incremental_solving,
695 : : const std::string& logic)
696 : : {
697 [ - + ]: 1 : if (incremental_solving)
698 : : {
699 : 0 : return getIncrementalStrategy(logic);
700 : : }
701 : : else
702 : : {
703 : 1 : return getNonIncrementalStrategy(logic);
704 : : }
705 : : }
706 : :
707 : 0 : PortfolioStrategy PortfolioDriver::getIncrementalStrategy(
708 : : const std::string& logic)
709 : : {
710 : 0 : PortfolioStrategy s;
711 [ - - ]: 0 : if (isOneOf(logic, "QF_AUFLIA"))
712 : : {
713 : 0 : s.add().unset("arrays-eager-index").set("arrays-eager-lemmas");
714 : : }
715 [ - - ]: 0 : else if (isOneOf(logic, "QF_BV"))
716 : : {
717 : 0 : s.add().set("bitblast", "eager");
718 : : }
719 : : else
720 : : {
721 : 0 : s.add();
722 : : }
723 : 0 : return s;
724 : : }
725 : :
726 : 1 : PortfolioStrategy PortfolioDriver::getNonIncrementalStrategy(
727 : : const std::string& logic)
728 : : {
729 : 1 : PortfolioStrategy s;
730 [ - + ]: 1 : if (isOneOf(logic, "QF_LRA"))
731 : : {
732 : 0 : s.add(0.166666667)
733 : 0 : .set("miplib-trick")
734 : 0 : .set("miplib-trick-subs", "4")
735 : 0 : .set("use-approx")
736 : 0 : .set("lemmas-on-replay-failure")
737 : 0 : .set("replay-early-close-depth", "4")
738 : 0 : .set("replay-lemma-reject-cut", "128")
739 : 0 : .set("replay-reject-cut", "512")
740 : 0 : .set("unconstrained-simp")
741 : 0 : .set("use-soi");
742 : 0 : s.add(0.583333333)
743 : 0 : .unset("restrict-pivots")
744 : 0 : .set("use-soi")
745 : 0 : .set("new-prop")
746 : 0 : .set("unconstrained-simp");
747 : 0 : s.add();
748 : : }
749 [ - + ]: 1 : else if (isOneOf(logic, "QF_LIA"))
750 : : {
751 : : // same as QF_LRA but add --pb-rewrites
752 : 0 : s.add(0.95)
753 : 0 : .set("miplib-trick")
754 : 0 : .set("miplib-trick-subs", "4")
755 : 0 : .set("use-approx")
756 : 0 : .set("lemmas-on-replay-failure")
757 : 0 : .set("replay-early-close-depth", "4")
758 : 0 : .set("replay-lemma-reject-cut", "128")
759 : 0 : .set("replay-reject-cut", "512")
760 : 0 : .set("unconstrained-simp")
761 : 0 : .set("use-soi")
762 : 0 : .set("pb-rewrites")
763 : 0 : .set("ite-simp")
764 : 0 : .set("simp-ite-compress");
765 : 0 : s.add();
766 : : }
767 [ - + ]: 1 : else if (isOneOf(logic, "QF_NIA"))
768 : : {
769 : 0 : s.add(0.35)
770 : 0 : .set("nl-ext-tplanes")
771 : 0 : .set("decision", "justification");
772 : 0 : s.add(0.05)
773 : 0 : .set("nl-ext-tplanes")
774 : 0 : .set("decision", "internal");
775 : 0 : s.add(0.05)
776 : 0 : .unset("nl-ext-tplanes")
777 : 0 : .set("decision", "internal");
778 : 0 : s.add(0.05)
779 : 0 : .unset("arith-brab")
780 : 0 : .set("nl-ext-tplanes")
781 : 0 : .set("decision", "internal");
782 : : // totals to more than 100%, but smaller bit-widths usually fail quickly
783 : 0 : s.add(0.25)
784 : 0 : .set("solve-int-as-bv", "2")
785 : 0 : .set("bitblast", "eager");
786 : 0 : s.add(0.25)
787 : 0 : .set("solve-int-as-bv", "4")
788 : 0 : .set("bitblast", "eager");
789 : 0 : s.add(0.25)
790 : 0 : .set("solve-int-as-bv", "8")
791 : 0 : .set("bitblast", "eager");
792 : 0 : s.add(0.25)
793 : 0 : .set("solve-int-as-bv", "16")
794 : 0 : .set("bitblast", "eager");
795 : 0 : s.add(0.5)
796 : 0 : .set("solve-int-as-bv", "32")
797 : 0 : .set("bitblast", "eager");
798 : 0 : s.add().set("nl-ext-tplanes").set("decision", "internal");
799 : : }
800 [ - + ]: 1 : else if (isOneOf(logic, "QF_NRA"))
801 : : {
802 : 0 : s.add(0.5).set("decision", "justification");
803 : 0 : s.add(0.25)
804 : 0 : .set("decision", "internal")
805 : 0 : .unset("nl-cov")
806 : 0 : .set("nl-ext", "full")
807 : 0 : .set("nl-ext-tplanes");
808 : 0 : s.add().set("decision", "internal").set("nl-ext", "none");
809 : : }
810 [ + - ]: 1 : else if (isOneOf(logic,
811 : : "ALIA",
812 : : "AUFLIA",
813 : : "AUFLIRA",
814 : : "AUFNIRA",
815 : : "UF",
816 : : "UFBVLIA",
817 : : "UFBVFP",
818 : : "UFIDL",
819 : : "UFLIA",
820 : : "UFLRA",
821 : : "UFNIA",
822 : : "UFDT",
823 : : "UFDTLIA",
824 : : "UFDTLIRA",
825 : : "AUFDTLIA",
826 : : "AUFDTLIRA",
827 : : "AUFBV",
828 : : "AUFBVDTLIA",
829 : : "AUFBVFP",
830 : : "AUFNIA",
831 : : "UFFPDTLIRA",
832 : : "UFFPDTNIRA"))
833 : : {
834 : : // initial runs
835 : 1 : s.add(0.025).set("simplification", "none").set("enum-inst");
836 : 1 : s.add(0.025).unset("e-matching").set("enum-inst");
837 : 1 : s.add(0.025)
838 : 2 : .unset("e-matching")
839 : 2 : .set("enum-inst")
840 : 1 : .set("enum-inst-sum");
841 : : // trigger selections
842 : 1 : s.add(0.025).set("relevant-triggers").set("enum-inst");
843 : 1 : s.add(0.025).set("trigger-sel", "max").set("enum-inst");
844 : 1 : s.add(0.025)
845 : 2 : .set("multi-trigger-when-single")
846 : 1 : .set("enum-inst");
847 : 1 : s.add(0.025)
848 : 2 : .set("multi-trigger-when-single")
849 : 2 : .set("multi-trigger-priority")
850 : 1 : .set("enum-inst");
851 : 1 : s.add(0.025).set("multi-trigger-cache").set("enum-inst");
852 : 1 : s.add(0.025).unset("multi-trigger-linear").set("enum-inst");
853 : : // other
854 : 1 : s.add(0.025).set("pre-skolem-quant", "on").set("enum-inst");
855 : 1 : s.add(0.025).set("inst-when", "full").set("enum-inst");
856 : 1 : s.add(0.025)
857 : 2 : .unset("e-matching")
858 : 2 : .unset("cbqi")
859 : 1 : .set("enum-inst");
860 : 1 : s.add(0.025).set("enum-inst").set("quant-ind");
861 : 1 : s.add(0.025)
862 : 2 : .set("decision", "internal")
863 : 2 : .set("simplification", "none")
864 : 2 : .unset("inst-no-entail")
865 : 2 : .unset("cbqi")
866 : 1 : .set("enum-inst");
867 : 1 : s.add(0.025)
868 : 2 : .set("decision", "internal")
869 : 2 : .set("enum-inst")
870 : 1 : .set("enum-inst-sum");
871 : 1 : s.add(0.025).set("term-db-mode", "relevant").set("enum-inst");
872 : 1 : s.add(0.025).set("enum-inst-interleave").set("enum-inst");
873 : 1 : s.add(0.025).set("preregister-mode", "lazy").set("enum-inst");
874 : : // finite model find
875 : 1 : s.add(0.025).set("finite-model-find").set("fmf-mbqi", "none");
876 : 1 : s.add(0.025)
877 : 2 : .set("finite-model-find")
878 : 1 : .set("decision", "internal");
879 : 1 : s.add(0.025)
880 : 2 : .set("finite-model-find")
881 : 2 : .set("macros-quant")
882 : 1 : .set("macros-quant-mode", "all");
883 : 1 : s.add(0.05).set("finite-model-find").set("e-matching");
884 : 1 : s.add(0.05).set("mbqi");
885 : : // long runs
886 : 1 : s.add(0.15)
887 : 2 : .set("finite-model-find")
888 : 1 : .set("decision", "internal");
889 : 1 : s.add().set("enum-inst");
890 : : }
891 [ - - ]: 0 : else if (isOneOf(logic, "UFBV"))
892 : : {
893 : : // most problems in UFBV are essentially BV
894 : 0 : s.add(0.125).set("sygus-inst");
895 : 0 : s.add(0.125).set("mbqi").unset("cegqi").unset("sygus-inst");
896 : 0 : s.add(0.25)
897 : 0 : .set("enum-inst")
898 : 0 : .set("cegqi-nested-qe")
899 : 0 : .set("decision", "internal");
900 : 0 : s.add(0.25)
901 : 0 : .set("mbqi-enum")
902 : 0 : .unset("cegqi")
903 : 0 : .unset("sygus-inst");
904 : 0 : s.add(0.025)
905 : 0 : .set("enum-inst")
906 : 0 : .unset("cegqi-innermost")
907 : 0 : .set("global-negate");
908 : : ;
909 : 0 : s.add().set("finite-model-find");
910 : : }
911 [ - - ]: 0 : else if (isOneOf(logic, "ABV", "BV"))
912 : : {
913 : 0 : s.add(0.066666667).set("sygus-inst");
914 : 0 : s.add(0.066666667).set("mbqi").unset("cegqi").unset("sygus-inst");
915 : 0 : s.add(0.25)
916 : 0 : .set("mbqi-enum")
917 : 0 : .unset("cegqi")
918 : 0 : .unset("sygus-inst");
919 : 0 : s.add(0.25)
920 : 0 : .set("enum-inst")
921 : 0 : .set("cegqi-nested-qe")
922 : 0 : .set("decision", "internal");
923 : 0 : s.add(0.025).set("enum-inst").unset("cegqi-bv");
924 : 0 : s.add(0.025)
925 : 0 : .set("enum-inst")
926 : 0 : .set("cegqi-bv-ineq", "eq-slack");
927 : 0 : s.add(0.066666667).set("enum-inst").unset("cegqi-innermost").set("global-negate");
928 : 0 : s.add().set("enum-inst");
929 : : }
930 [ - - ]: 0 : else if (isOneOf(logic, "ABVFP", "ABVFPLRA", "BVFP", "FP", "NIA", "NRA", "BVFPLRA"))
931 : : {
932 : 0 : s.add(0.25)
933 : 0 : .set("mbqi-enum")
934 : 0 : .unset("cegqi")
935 : 0 : .unset("sygus-inst");
936 : 0 : s.add(0.25).set("enum-inst").set("nl-ext-tplanes");
937 : 0 : s.add(0.05).set("mbqi").unset("cegqi").unset("sygus-inst");
938 : 0 : s.add().set("sygus-inst");
939 : : }
940 [ - - ]: 0 : else if (isOneOf(logic, "LIA", "LRA"))
941 : : {
942 : 0 : s.add(0.025).set("enum-inst");
943 : 0 : s.add(0.25).set("enum-inst").set("cegqi-nested-qe");
944 : 0 : s.add(0.025).set("mbqi").unset("cegqi").unset("sygus-inst");
945 : 0 : s.add(0.025)
946 : 0 : .set("mbqi-enum")
947 : 0 : .unset("cegqi")
948 : 0 : .unset("sygus-inst");
949 : 0 : s.add()
950 : 0 : .set("enum-inst")
951 : 0 : .set("cegqi-nested-qe")
952 : 0 : .set("decision", "internal");
953 : : }
954 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFBV"))
955 : : {
956 : 0 : s.add(0.5);
957 : 0 : s.add().set("decision", "stoponly");
958 : : }
959 [ - - ]: 0 : else if (isOneOf(logic, "QF_ABV"))
960 : : {
961 : 0 : s.add(0.41666667)
962 : 0 : .set("ite-simp")
963 : 0 : .set("simp-with-care")
964 : 0 : .set("repeat-simp");
965 : 0 : s.add();
966 : : }
967 [ - - ]: 0 : else if (isOneOf(logic, "QF_BV"))
968 : : {
969 : 0 : s.add().set("bitblast", "eager").set("bv-assert-input");
970 : : }
971 [ - - ]: 0 : else if (isOneOf(logic, "QF_UFBV"))
972 : : {
973 : 0 : s.add(0.75).set("bitblast", "eager").set("bv-assert-input");
974 : 0 : s.add();
975 : : }
976 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFLIA"))
977 : : {
978 : 0 : s.add()
979 : 0 : .unset("arrays-eager-index")
980 : 0 : .set("arrays-eager-lemmas")
981 : 0 : .set("decision", "justification");
982 : : }
983 [ - - ]: 0 : else if (isOneOf(logic, "QF_AX"))
984 : : {
985 : 0 : s.add()
986 : 0 : .unset("arrays-eager-index")
987 : 0 : .set("arrays-eager-lemmas")
988 : 0 : .set("decision", "internal");
989 : : }
990 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFNIA"))
991 : : {
992 : 0 : s.add()
993 : 0 : .set("decision", "justification")
994 : 0 : .unset("arrays-eager-index")
995 : 0 : .set("arrays-eager-lemmas");
996 : : }
997 [ - - ]: 0 : else if (isOneOf(logic, "QF_ALIA"))
998 : : {
999 : 0 : s.add(0.116666667).set("decision", "justification");
1000 : 0 : s.add()
1001 : 0 : .set("decision", "stoponly")
1002 : 0 : .unset("arrays-eager-index")
1003 : 0 : .set("arrays-eager-lemmas");
1004 : : }
1005 [ - - ]: 0 : else if (isOneOf(logic, "QF_S", "QF_SLIA"))
1006 : : {
1007 : 0 : s.add(0.25)
1008 : 0 : .set("strings-exp")
1009 : 0 : .set("strings-fmf")
1010 : 0 : .unset("jh-rlv-order");
1011 : 0 : s.add().set("strings-exp").unset("jh-rlv-order");
1012 : : }
1013 : : else
1014 : : {
1015 : 0 : s.add();
1016 : : }
1017 : 1 : return s;
1018 : : }
1019 : :
1020 : : } // namespace cvc5::main
|
