| 67 | } |
| 68 | |
| 69 | void SMTSolverCommand::setZ3(std::optional<unsigned int> timeoutInMilliseconds, bool _preprocessing, bool _computeInvariants) |
| 70 | { |
| 71 | constexpr int Z3ResourceLimit = 2000000; |
| 72 | m_arguments.clear(); |
| 73 | m_solverCmd = "z3"; |
| 74 | m_arguments.emplace_back("-in"); // Read from standard input |
| 75 | m_arguments.emplace_back("-smt2"); // Expect input in SMT-LIB2 format |
| 76 | if (_computeInvariants) |
| 77 | m_arguments.emplace_back("-model"); // Output model automatically after check-sat |
| 78 | if (timeoutInMilliseconds) |
| 79 | m_arguments.emplace_back("-t:" + std::to_string(timeoutInMilliseconds.value())); |
| 80 | else |
| 81 | m_arguments.emplace_back("rlimit=" + std::to_string(Z3ResourceLimit)); |
| 82 | |
| 83 | // These options have been empirically established to be helpful |
| 84 | m_arguments.emplace_back("rewriter.pull_cheap_ite=true"); |
| 85 | m_arguments.emplace_back("fp.spacer.q3.use_qgen=true"); |
| 86 | m_arguments.emplace_back("fp.spacer.mbqi=false"); |
| 87 | m_arguments.emplace_back("fp.spacer.ground_pobs=false"); |
| 88 | |
| 89 | // Spacer optimization should be |
| 90 | // - enabled for better solving (default) |
| 91 | // - disable for counterexample generation |
| 92 | std::string preprocessingArg = _preprocessing ? "true" : "false"; |
| 93 | m_arguments.emplace_back("fp.xform.slice=" + preprocessingArg); |
| 94 | m_arguments.emplace_back("fp.xform.inline_linear=" + preprocessingArg); |
| 95 | m_arguments.emplace_back("fp.xform.inline_eager=" + preprocessingArg); |
| 96 | } |
| 97 | |
| 98 | ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query) const |
| 99 | { |
no test coverage detected