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/command_status.h"
31 : : #include "parser/commands.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 : 24107 : bool ExecutionContext::solveContinuous(parser::InputParser* parser,
44 : : bool stopAtSetLogic,
45 : : bool stopAtCheckSat)
46 : : {
47 : 24107 : Command cmd;
48 : 24107 : bool status = true;
49 [ + + ]: 690019 : while (status)
50 : : {
51 : 689936 : cmd = parser->nextCommand();
52 [ + + ]: 689874 : if (cmd.isNull())
53 : : {
54 : 20923 : break;
55 : : }
56 : 668951 : Cmd* cc = cmd.d_cmd.get();
57 [ + + ]: 668951 : if (stopAtCheckSat)
58 : : {
59 [ + - ][ + + ]: 4 : if (dynamic_cast<CheckSatCommand*>(cc) != nullptr)
60 : : {
61 : 1 : d_hasReadCheckSat = true;
62 : 1 : break;
63 : : }
64 : : }
65 : 668950 : status = d_executor->doCommand(&cmd);
66 [ + + ][ - + ]: 668948 : if (!status && cc->interrupted())
[ - + ]
67 : : {
68 : 0 : solver().getDriverOptions().out() << CommandInterrupted();
69 : 0 : d_executor->reset();
70 : 0 : break;
71 : : }
72 [ + - ][ + + ]: 668948 : if (dynamic_cast<QuitCommand*>(cc) != nullptr)
73 : : {
74 : 3035 : break;
75 : : }
76 [ + + ]: 665913 : 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 : 24043 : return status;
87 : 24107 : }
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,
351 : : parser::InputParser* parser,
352 : : uint64_t timeout)
353 : 1 : : d_ctx(ctx),
354 : 1 : d_parser(parser),
355 : 1 : d_maxJobs(ctx.solver().getOptionInfo("portfolio-jobs").uintValue()),
356 : 1 : d_timeout(timeout)
357 : : {
358 : 1 : }
359 : :
360 : 1 : bool run(PortfolioStrategy& strategy)
361 : : {
362 [ + + ]: 26 : for (const auto& s : strategy.d_strategies)
363 : : {
364 : 25 : d_jobs.emplace_back(Job{s});
365 : : }
366 : :
367 : : // While there are jobs to be run or jobs still running
368 [ - + ][ - - ]: 1 : while (d_nextJob < d_jobs.size() || d_running > 0)
[ + - ]
369 : : {
370 : : // Check if any job was successful
371 [ - + ]: 1 : if (checkResults())
372 : : {
373 : 0 : return true;
374 : : }
375 : :
376 : : // While we can start jobs right now
377 [ + - ][ + + ]: 2 : while (d_nextJob < d_jobs.size() && d_running < d_maxJobs)
[ + + ]
378 : : {
379 : 1 : startNextJob();
380 : : }
381 : :
382 [ + - ]: 1 : if (d_running > 0)
383 : : {
384 : 1 : int wstatus = 0;
385 : 1 : pid_t child = wait(&wstatus);
386 [ + - ]: 1 : if (checkResults(child, wstatus))
387 : : {
388 : 1 : return true;
389 : : }
390 : : }
391 : : }
392 [ - - ]: 0 : if (checkResults()) return true;
393 : :
394 : 0 : return false;
395 : : }
396 : :
397 : : private:
398 : 1 : void startNextJob()
399 : : {
400 [ - + ][ - + ]: 1 : Assert(d_nextJob < d_jobs.size());
[ - - ]
401 : 1 : Job& job = d_jobs[d_nextJob];
402 [ + - ]: 1 : Trace("portfolio") << "Starting " << job.d_config << std::endl;
403 : 1 : printPortfolioConfig(d_ctx.solver(), job.d_config);
404 : :
405 : : // Set up pipes to capture output of worker
406 : 1 : job.d_errPipe.open();
407 : 1 : job.d_outPipe.open();
408 : : // Start the worker process
409 : 1 : job.d_worker = fork();
410 [ - + ]: 1 : if (job.d_worker == -1)
411 : : {
412 : 0 : throw internal::Exception("Unable to fork");
413 : : }
414 [ - + ]: 1 : if (job.d_worker == 0)
415 : : {
416 : 0 : job.d_errPipe.dup(STDERR_FILENO);
417 : 0 : job.d_outPipe.dup(STDOUT_FILENO);
418 : :
419 : 0 : std::vector<cvc5::Term> assertions = d_ctx.solver().getAssertions();
420 : 0 : std::string logic = d_ctx.solver().getLogic();
421 : :
422 : : std::string produceUnsatCoresValue =
423 : 0 : d_ctx.solver().getOption("produce-unsat-cores");
424 : : std::string produceModelsValue =
425 : 0 : d_ctx.solver().getOption("produce-models");
426 : 0 : d_ctx.storeDeclarationsAndNamedTerms();
427 : :
428 : 0 : d_ctx.runResetCommand();
429 : :
430 : 0 : d_ctx.solver().setOption("produce-unsat-cores", produceUnsatCoresValue);
431 : 0 : d_ctx.solver().setOption("produce-models", produceModelsValue);
432 : 0 : job.d_config.applyOptions(d_ctx.solver());
433 : 0 : d_ctx.solver().setLogic(logic);
434 : :
435 [ - - ]: 0 : for (Term& t : assertions)
436 : : {
437 : 0 : d_ctx.solver().assertFormula(t);
438 : : }
439 : : // 0 = solved, 1 = not solved
440 : 0 : SolveStatus rc = SolveStatus::STATUS_UNSOLVED;
441 [ - - ]: 0 : if (d_ctx.runCheckSatCommand())
442 : : // if (d_ctx.solveCommands(d_commands))
443 : : {
444 : 0 : Result res = d_ctx.d_executor->getResult();
445 : 0 : d_ctx.continueAfterSolving(d_parser);
446 : 0 : if (res.isSat() || res.isUnsat())
447 : : {
448 : 0 : rc = SolveStatus::STATUS_SOLVED;
449 : : }
450 : 0 : }
451 : 0 : _exit(rc);
452 : 0 : }
453 : 1 : job.d_errPipe.closeIn();
454 : 1 : job.d_outPipe.closeIn();
455 : :
456 : : // Start the timeout process
457 [ + - ][ + - ]: 1 : if (d_timeout > 0 && job.d_config.d_timeout > 0)
458 : : {
459 : 1 : job.d_timeout = fork();
460 [ - + ]: 1 : if (job.d_timeout == 0)
461 : : {
462 : : auto duration = std::chrono::duration<double, std::milli>(
463 : 0 : job.d_config.d_timeout * d_timeout);
464 : 0 : std::this_thread::sleep_for(duration);
465 : 0 : kill(job.d_worker, SIGKILL);
466 : 0 : _exit(0);
467 : : }
468 : : }
469 : :
470 : 1 : ++d_nextJob;
471 : 1 : ++d_running;
472 : 1 : job.d_state = JobState::RUNNING;
473 : 1 : }
474 : :
475 : : /**
476 : : * Check whether some process terminated and solved the input. If so,
477 : : * forward the child process output to the main out and return true.
478 : : * Otherwise return false.
479 : : * If child and status are given, only the job with this particular worker is
480 : : * considered and status is assumed to be the wstatus reported by waitpid.
481 : : */
482 : 2 : bool checkResults(pid_t child = -1, int status = 0)
483 : : {
484 : : // check d_jobs for items where worker has terminated and timeout != -1
485 [ + + ]: 27 : for (auto& job : d_jobs)
486 : : {
487 : : // has not been started yet
488 [ + + ]: 26 : if (job.d_state == JobState::PENDING) continue;
489 : : // has already been analyzed
490 [ - + ]: 1 : if (job.d_state == JobState::DONE) continue;
491 : : // was given an explicit child, but this is not it.
492 [ + - ][ - + ]: 1 : if (child != -1 && job.d_worker != child) continue;
493 : :
494 : 1 : int wstatus = 0;
495 [ - + ]: 1 : if (child == -1)
496 : : {
497 : 0 : pid_t res = waitpid(job.d_worker, &wstatus, WNOHANG);
498 : : // has not terminated yet
499 [ - - ]: 0 : if (res == 0) continue;
500 [ - - ]: 0 : if (res == -1) continue;
501 : : }
502 : : else
503 : : {
504 : 1 : wstatus = status;
505 : : }
506 : : // mark as analyzed
507 [ + - ]: 1 : Trace("portfolio") << "Finished " << job.d_config << std::endl;
508 : : // terminate the corresponding timeout process if it is still running
509 [ + - ]: 1 : if (job.d_timeout > 0)
510 : : {
511 : 1 : kill(job.d_timeout, SIGKILL);
512 : : }
513 : 1 : job.d_state = JobState::DONE;
514 : 1 : --d_running;
515 : : // check if exited normally
516 [ - + ]: 1 : if (WIFSIGNALED(wstatus))
517 : : {
518 : 0 : continue;
519 : : }
520 [ + - ]: 1 : if (WIFEXITED(wstatus))
521 : : {
522 [ + - ]: 1 : if (WEXITSTATUS(wstatus) == SolveStatus::STATUS_SOLVED)
523 : : {
524 [ + - ]: 1 : Trace("portfolio") << "Successful!" << std::endl;
525 [ + - ]: 1 : if (d_ctx.solver().isOutputOn("portfolio"))
526 : : {
527 : 1 : std::ostream& out = d_ctx.solver().getOutput("portfolio");
528 : 1 : out << "(portfolio-success \"" << job.d_config.toOptionString()
529 : 1 : << "\")" << std::endl;
530 : : }
531 : 1 : job.d_errPipe.flushTo(std::cerr);
532 : 1 : job.d_outPipe.flushTo(std::cout);
533 : 1 : return true;
534 : : }
535 : : }
536 : : }
537 : 1 : return false;
538 : : }
539 : :
540 : : ExecutionContext& d_ctx;
541 : : parser::InputParser* d_parser;
542 : : /** All jobs. */
543 : : std::vector<Job> d_jobs;
544 : : /** The id of the next job to be started within d_jobs */
545 : : size_t d_nextJob = 0;
546 : : /** The number of currently running jobs */
547 : : size_t d_running = 0;
548 : : const uint64_t d_maxJobs;
549 : : const uint64_t d_timeout;
550 : : };
551 : :
552 : : } // namespace
553 : :
554 : : #endif
555 : :
556 : 24106 : bool PortfolioDriver::solve(std::unique_ptr<CommandExecutor>& executor)
557 : : {
558 : 24106 : ExecutionContext ctx{executor.get()};
559 : 24106 : Solver& solver = ctx.solver();
560 : 24106 : bool use_portfolio = solver.getOption("use-portfolio") == "true";
561 [ + + ]: 24106 : if (!use_portfolio)
562 : : {
563 : 24105 : return ctx.solveContinuous(d_parser, false);
564 : : }
565 : : #if HAVE_SYS_WAIT_H
566 : 1 : ctx.solveContinuous(d_parser, true);
567 : :
568 [ - + ]: 1 : if (!ctx.d_logic)
569 : : {
570 : 0 : return ctx.solveContinuous(d_parser, false);
571 : : }
572 : :
573 : 1 : bool dry_run = solver.getOption("portfolio-dry-run") == "true";
574 : :
575 : 1 : bool incremental_solving = solver.getOption("incremental") == "true";
576 : 1 : PortfolioStrategy strategy = getStrategy(incremental_solving, *ctx.d_logic);
577 [ - + ][ - + ]: 1 : Assert(!strategy.d_strategies.empty())
[ - - ]
578 : 0 : << "The portfolio strategy should never be empty.";
579 [ - + ]: 1 : if (strategy.d_strategies.size() == 1)
580 : : {
581 : 0 : PortfolioConfig& config = strategy.d_strategies.front();
582 : 0 : printPortfolioConfig(ctx.solver(), config);
583 [ - - ]: 0 : if (dry_run) return true;
584 : 0 : config.applyOptions(solver);
585 : 0 : return ctx.solveContinuous(d_parser, false);
586 : : }
587 : :
588 : 1 : uint64_t total_timeout = ctx.solver().getOptionInfo("tlimit").uintValue();
589 [ + - ]: 1 : if (total_timeout == 0)
590 : : {
591 : 1 : total_timeout = 1'200'000; // miliseconds
592 : : }
593 : :
594 [ - + ]: 1 : if (dry_run)
595 : : {
596 [ - - ]: 0 : for (PortfolioConfig& config : strategy.d_strategies)
597 : : {
598 : 0 : printPortfolioConfig(ctx.solver(), config);
599 : : }
600 : 0 : return true;
601 : : }
602 : :
603 : 1 : bool uninterrupted = ctx.solveContinuous(d_parser, false, true);
604 [ + - ][ + - ]: 1 : if (uninterrupted && ctx.d_hasReadCheckSat)
605 : : {
606 : : PortfolioProcessPool pool(
607 : 1 : ctx, d_parser, total_timeout); // ctx.parseCommands(d_parser));
608 : 1 : bool solved = pool.run(strategy);
609 [ - + ]: 1 : if (!solved)
610 : : {
611 : 0 : std::cout << "unknown" << std::endl;
612 : : }
613 : 1 : return solved;
614 : 1 : }
615 : 0 : return uninterrupted;
616 : : #else
617 : : Warning() << "Can't run portfolio without <sys/wait.h>.";
618 : : return ctx.solveContinuous(d_parser, false);
619 : : #endif
620 : 24106 : }
621 : :
622 : 2 : std::string PortfolioConfig::toOptionString() const
623 : : {
624 : 2 : std::stringstream ss;
625 : 2 : bool firstTime = true;
626 [ + + ]: 6 : for (const std::pair<std::string, std::string>& o : d_options)
627 : : {
628 [ + + ]: 4 : if (firstTime)
629 : : {
630 : 2 : firstTime = false;
631 : : }
632 : : else
633 : : {
634 : 2 : ss << " ";
635 : : }
636 : 4 : ss << "--";
637 [ + + ]: 4 : if (o.second == "true")
638 : : {
639 : 2 : ss << o.first;
640 : : }
641 [ - + ]: 2 : else if (o.second == "false")
642 : : {
643 : 0 : ss << "no-" << o.first;
644 : : }
645 : : else
646 : : {
647 : 2 : ss << o.first << "=" << o.second;
648 : : }
649 : : }
650 : 4 : return ss.str();
651 : 2 : }
652 : :
653 : 0 : std::ostream& operator<<(std::ostream& os, const PortfolioConfig& config)
654 : : {
655 [ - - ]: 0 : for (const auto& o : config.d_options)
656 : : {
657 : 0 : os << o.first << "=" << o.second << " ";
658 : : }
659 : 0 : os << "timeout=" << config.d_timeout;
660 : 0 : return os;
661 : : }
662 : :
663 : : /**
664 : : * Check if the first string (the logic) is one of the remaining strings.
665 : : * Used to have a reasonably concise syntax to check the current logic against a
666 : : * lengthy list.
667 : : */
668 : : template <typename... T>
669 : 5 : bool isOneOf(const std::string& logic, T&&... list)
670 : : {
671 [ + - ][ + - ]: 5 : return ((logic == list) || ...);
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ - + ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
672 : : }
673 : :
674 : 1 : PortfolioStrategy PortfolioDriver::getStrategy(bool incremental_solving,
675 : : const std::string& logic)
676 : : {
677 [ - + ]: 1 : if (incremental_solving)
678 : : {
679 : 0 : return getIncrementalStrategy(logic);
680 : : }
681 : : else
682 : : {
683 : 1 : return getNonIncrementalStrategy(logic);
684 : : }
685 : : }
686 : :
687 : 0 : PortfolioStrategy PortfolioDriver::getIncrementalStrategy(
688 : : const std::string& logic)
689 : : {
690 : 0 : PortfolioStrategy s;
691 [ - - ]: 0 : if (isOneOf(logic, "QF_AUFLIA"))
692 : : {
693 : 0 : s.add().unset("arrays-eager-index").set("arrays-eager-lemmas");
694 : : }
695 [ - - ]: 0 : else if (isOneOf(logic, "QF_BV"))
696 : : {
697 : 0 : s.add().set("bitblast", "eager");
698 : : }
699 : : else
700 : : {
701 : 0 : s.add();
702 : : }
703 : 0 : return s;
704 : 0 : }
705 : :
706 : 1 : PortfolioStrategy PortfolioDriver::getNonIncrementalStrategy(
707 : : const std::string& logic)
708 : : {
709 : 1 : PortfolioStrategy s;
710 [ - + ]: 1 : if (isOneOf(logic, "QF_LRA"))
711 : : {
712 : 0 : s.add(0.166666667)
713 : 0 : .set("miplib-trick")
714 : 0 : .set("miplib-trick-subs", "4")
715 : 0 : .set("use-approx")
716 : 0 : .set("lemmas-on-replay-failure")
717 : 0 : .set("replay-early-close-depth", "4")
718 : 0 : .set("replay-lemma-reject-cut", "128")
719 : 0 : .set("replay-reject-cut", "512")
720 : 0 : .set("unconstrained-simp")
721 : 0 : .set("use-soi");
722 : 0 : s.add(0.583333333)
723 : 0 : .unset("restrict-pivots")
724 : 0 : .set("use-soi")
725 : 0 : .set("new-prop")
726 : 0 : .set("unconstrained-simp");
727 : 0 : s.add();
728 : : }
729 [ - + ]: 1 : else if (isOneOf(logic, "QF_LIA"))
730 : : {
731 : : // same as QF_LRA but add --pb-rewrites
732 : 0 : s.add(0.95)
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 : .set("pb-rewrites")
743 : 0 : .set("ite-simp")
744 : 0 : .set("simp-ite-compress");
745 : 0 : s.add();
746 : : }
747 [ - + ]: 1 : else if (isOneOf(logic, "QF_NIA"))
748 : : {
749 : 0 : s.add(0.35).set("nl-ext-tplanes").set("decision", "justification");
750 : 0 : s.add(0.05).set("nl-ext-tplanes").set("decision", "internal");
751 : 0 : s.add(0.05).unset("nl-ext-tplanes").set("decision", "internal");
752 : 0 : s.add(0.05)
753 : 0 : .unset("arith-brab")
754 : 0 : .set("nl-ext-tplanes")
755 : 0 : .set("decision", "internal");
756 : : // totals to more than 100%, but smaller bit-widths usually fail quickly
757 : 0 : s.add(0.25).set("solve-int-as-bv", "2").set("bitblast", "eager");
758 : 0 : s.add(0.25).set("solve-int-as-bv", "4").set("bitblast", "eager");
759 : 0 : s.add(0.25).set("solve-int-as-bv", "8").set("bitblast", "eager");
760 : 0 : s.add(0.25).set("solve-int-as-bv", "16").set("bitblast", "eager");
761 : 0 : s.add(0.5).set("solve-int-as-bv", "32").set("bitblast", "eager");
762 : 0 : s.add().set("nl-ext-tplanes").set("decision", "internal");
763 : : }
764 [ - + ]: 1 : else if (isOneOf(logic, "QF_NRA"))
765 : : {
766 : 0 : s.add(0.5).set("decision", "justification");
767 : 0 : s.add(0.25)
768 : 0 : .set("decision", "internal")
769 : 0 : .unset("nl-cov")
770 : 0 : .set("nl-ext", "full")
771 : 0 : .set("nl-ext-tplanes");
772 : 0 : s.add().set("decision", "internal").set("nl-ext", "none");
773 : : }
774 [ + - ]: 1 : else if (isOneOf(logic,
775 : : "ALIA",
776 : : "AUFLIA",
777 : : "AUFLIRA",
778 : : "AUFNIRA",
779 : : "UF",
780 : : "UFBVLIA",
781 : : "UFBVFP",
782 : : "UFIDL",
783 : : "UFLIA",
784 : : "UFLRA",
785 : : "UFNIA",
786 : : "UFDT",
787 : : "UFDTLIA",
788 : : "UFDTLIRA",
789 : : "AUFDTLIA",
790 : : "AUFDTLIRA",
791 : : "AUFBV",
792 : : "AUFBVDTLIA",
793 : : "AUFBVFP",
794 : : "AUFNIA",
795 : : "UFFPDTLIRA",
796 : : "UFFPDTNIRA"))
797 : : {
798 : : // initial runs
799 : 1 : s.add(0.025).set("simplification", "none").set("enum-inst");
800 : 1 : s.add(0.025).unset("e-matching").set("enum-inst");
801 : 1 : s.add(0.025).unset("e-matching").set("enum-inst").set("enum-inst-sum");
802 : : // trigger selections
803 : 1 : s.add(0.025).set("relevant-triggers").set("enum-inst");
804 : 1 : s.add(0.025).set("trigger-sel", "max").set("enum-inst");
805 : 1 : s.add(0.025).set("multi-trigger-when-single").set("enum-inst");
806 : 1 : s.add(0.025)
807 : 2 : .set("multi-trigger-when-single")
808 : 2 : .set("multi-trigger-priority")
809 : 1 : .set("enum-inst");
810 : 1 : s.add(0.025).set("multi-trigger-cache").set("enum-inst");
811 : 1 : s.add(0.025).unset("multi-trigger-linear").set("enum-inst");
812 : : // other
813 : 1 : s.add(0.025).set("pre-skolem-quant", "on").set("enum-inst");
814 : 1 : s.add(0.025).set("inst-when", "full").set("enum-inst");
815 : 1 : s.add(0.025).unset("e-matching").unset("cbqi").set("enum-inst");
816 : 1 : s.add(0.025).set("enum-inst").set("quant-ind");
817 : 1 : s.add(0.025)
818 : 2 : .set("decision", "internal")
819 : 2 : .set("simplification", "none")
820 : 2 : .unset("inst-no-entail")
821 : 2 : .unset("cbqi")
822 : 1 : .set("enum-inst");
823 : 1 : s.add(0.025)
824 : 2 : .set("decision", "internal")
825 : 2 : .set("enum-inst")
826 : 1 : .set("enum-inst-sum");
827 : 1 : s.add(0.025).set("term-db-mode", "relevant").set("enum-inst");
828 : 1 : s.add(0.025).set("enum-inst-interleave").set("enum-inst");
829 : 1 : s.add(0.025).set("preregister-mode", "lazy").set("enum-inst");
830 : : // finite model find
831 : 1 : s.add(0.025).set("finite-model-find").set("fmf-mbqi", "none");
832 : 1 : s.add(0.025).set("finite-model-find").set("decision", "internal");
833 : 1 : s.add(0.025)
834 : 2 : .set("finite-model-find")
835 : 2 : .set("macros-quant")
836 : 1 : .set("macros-quant-mode", "all");
837 : 1 : s.add(0.05).set("finite-model-find").set("e-matching");
838 : 1 : s.add(0.05).set("mbqi");
839 : : // long runs
840 : 1 : s.add(0.15).set("finite-model-find").set("decision", "internal");
841 : 1 : s.add().set("enum-inst");
842 : : }
843 [ - - ]: 0 : else if (isOneOf(logic, "UFBV"))
844 : : {
845 : : // most problems in UFBV are essentially BV
846 : 0 : s.add(0.125).set("sygus-inst");
847 : 0 : s.add(0.125).set("mbqi").unset("cegqi").unset("sygus-inst");
848 : 0 : s.add(0.25)
849 : 0 : .set("enum-inst")
850 : 0 : .set("cegqi-nested-qe")
851 : 0 : .set("decision", "internal");
852 : 0 : s.add(0.25).set("mbqi-enum").unset("cegqi").unset("sygus-inst");
853 : 0 : s.add(0.025).set("enum-inst").unset("cegqi-innermost").set("global-negate");
854 : : ;
855 : 0 : s.add().set("finite-model-find");
856 : : }
857 [ - - ]: 0 : else if (isOneOf(logic, "ABV", "BV"))
858 : : {
859 : 0 : s.add(0.066666667).set("sygus-inst");
860 : 0 : s.add(0.066666667).set("mbqi").unset("cegqi").unset("sygus-inst");
861 : 0 : s.add(0.25).set("mbqi-enum").unset("cegqi").unset("sygus-inst");
862 : 0 : s.add(0.25)
863 : 0 : .set("enum-inst")
864 : 0 : .set("cegqi-nested-qe")
865 : 0 : .set("decision", "internal");
866 : 0 : s.add(0.025).set("enum-inst").unset("cegqi-bv");
867 : 0 : s.add(0.025).set("enum-inst").set("cegqi-bv-ineq", "eq-slack");
868 : 0 : s.add(0.066666667)
869 : 0 : .set("enum-inst")
870 : 0 : .unset("cegqi-innermost")
871 : 0 : .set("global-negate");
872 : 0 : s.add().set("enum-inst");
873 : : }
874 [ - - ]: 0 : else if (isOneOf(logic,
875 : : "ABVFP",
876 : : "ABVFPLRA",
877 : : "BVFP",
878 : : "FP",
879 : : "NIA",
880 : : "NRA",
881 : : "BVFPLRA"))
882 : : {
883 : 0 : s.add(0.25).set("mbqi-enum").unset("cegqi").unset("sygus-inst");
884 : 0 : s.add(0.25).set("enum-inst").set("nl-ext-tplanes");
885 : 0 : s.add(0.05).set("mbqi").unset("cegqi").unset("sygus-inst");
886 : 0 : s.add().set("sygus-inst");
887 : : }
888 [ - - ]: 0 : else if (isOneOf(logic, "LIA", "LRA"))
889 : : {
890 : 0 : s.add(0.025).set("enum-inst");
891 : 0 : s.add(0.25).set("enum-inst").set("cegqi-nested-qe");
892 : 0 : s.add(0.025).set("mbqi").unset("cegqi").unset("sygus-inst");
893 : 0 : s.add(0.025).set("mbqi-enum").unset("cegqi").unset("sygus-inst");
894 : 0 : s.add().set("enum-inst").set("cegqi-nested-qe").set("decision", "internal");
895 : : }
896 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFBV"))
897 : : {
898 : 0 : s.add(0.5);
899 : 0 : s.add().set("decision", "stoponly");
900 : : }
901 [ - - ]: 0 : else if (isOneOf(logic, "QF_ABV"))
902 : : {
903 : 0 : s.add(0.41666667).set("ite-simp").set("simp-with-care").set("repeat-simp");
904 : 0 : s.add();
905 : : }
906 [ - - ]: 0 : else if (isOneOf(logic, "QF_BV"))
907 : : {
908 : 0 : s.add().set("bitblast", "eager").set("bv-assert-input");
909 : : }
910 [ - - ]: 0 : else if (isOneOf(logic, "QF_UFBV"))
911 : : {
912 : 0 : s.add(0.75).set("bitblast", "eager").set("bv-assert-input");
913 : 0 : s.add();
914 : : }
915 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFLIA"))
916 : : {
917 : 0 : s.add()
918 : 0 : .unset("arrays-eager-index")
919 : 0 : .set("arrays-eager-lemmas")
920 : 0 : .set("decision", "justification");
921 : : }
922 [ - - ]: 0 : else if (isOneOf(logic, "QF_AX"))
923 : : {
924 : 0 : s.add()
925 : 0 : .unset("arrays-eager-index")
926 : 0 : .set("arrays-eager-lemmas")
927 : 0 : .set("decision", "internal");
928 : : }
929 [ - - ]: 0 : else if (isOneOf(logic, "QF_AUFNIA"))
930 : : {
931 : 0 : s.add()
932 : 0 : .set("decision", "justification")
933 : 0 : .unset("arrays-eager-index")
934 : 0 : .set("arrays-eager-lemmas");
935 : : }
936 [ - - ]: 0 : else if (isOneOf(logic, "QF_ALIA"))
937 : : {
938 : 0 : s.add(0.116666667).set("decision", "justification");
939 : 0 : s.add()
940 : 0 : .set("decision", "stoponly")
941 : 0 : .unset("arrays-eager-index")
942 : 0 : .set("arrays-eager-lemmas");
943 : : }
944 [ - - ]: 0 : else if (isOneOf(logic, "QF_S", "QF_SLIA"))
945 : : {
946 : 0 : s.add(0.25).set("strings-exp").set("strings-fmf").unset("jh-rlv-order");
947 : 0 : s.add().set("strings-exp").unset("jh-rlv-order");
948 : : }
949 : : else
950 : : {
951 : 0 : s.add();
952 : : }
953 : 1 : return s;
954 : 0 : }
955 : :
956 : : } // namespace cvc5::main
|
