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