| 580 | |
| 581 | |
| 582 | void solver_init() { |
| 583 | tactic.emplace({ |
| 584 | "simplify", |
| 585 | "propagate-values", |
| 586 | "simplify", |
| 587 | "elim-uncnstr", |
| 588 | "qe-light", |
| 589 | "simplify", |
| 590 | "elim-uncnstr", |
| 591 | "reduce-args", |
| 592 | "qe-light", |
| 593 | "simplify", |
| 594 | "smt" |
| 595 | }); |
| 596 | #if 0 |
| 597 | tactic->appendIf("is-qfbv", |
| 598 | AndTactic({ |
| 599 | "bit-blast", "simplify", "solve-eqs", "aig", "sat"}), |
| 600 | NamedTactic("smt")); |
| 601 | #endif |
| 602 | } |
| 603 | |
| 604 | void solver_destroy() { |
| 605 | tactic.reset(); |
no test coverage detected