summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2022-01-03IDL solver starter projectAndres Noetzli
2021-12-22Add support for incremental + interpolants (#7853)Andrew Reynolds
2021-12-21Support get-abduct-next (#7850)Andrew Reynolds
2021-12-20Allow SyGuS subsolver to be reused in incremental mode (#7785)Andrew Reynolds
2021-12-17Refactoring initialization of proofs (#7834)Andrew Reynolds
2021-12-16Fix get-model when sort constructors are present (#7828)Andrew Reynolds
2021-12-16Minor fix for print benchmark. (#7821)Andrew Reynolds
2021-12-15Add trace to see inferences in final proof (#7813)Andrew Reynolds
2021-12-14Connecting the core array solver in strings (#7800)Andrew Reynolds
2021-12-13Initial cut at distinguishing uses of CONST_RATIONAL (#7682)Andrew Reynolds
2021-12-13Improve nonlinear solver (#7787)Gereon Kremer
2021-12-10[proofs] Add option to prune inputs from final proof (#7789)Haniel Barbosa
2021-12-09Remove a few static access to options in proof code (#7780)Andrew Reynolds
2021-12-09Do not make SyGuS subsolver in unsat state after solving (#7759)Andrew Reynolds
2021-12-08Static options acceses again (#7771)Gereon Kremer
2021-12-07Remove more static accesses to options (#7764)Gereon Kremer
2021-12-07Add proof annotation option (#7750)Andrew Reynolds
2021-12-07Allow sygus in incremental mode (#7756)Andrew Reynolds
2021-12-07Make data structures in relevance manager SAT-context dependent (#7733)Andrew Reynolds
2021-12-07Towards support for incremental sygus (#7736)Andrew Reynolds
2021-12-07Eliminate more static calls to Rewriter::rewrite (#7740)Andrew Reynolds
2021-12-01Improvements for get-difficulty (#7720)Andrew Reynolds
2021-11-24Minor fixes (#7691)Andres Noetzli
2021-11-22Refactor IO stream manipulators (#7555)Gereon Kremer
2021-11-17Fix binding of quoted symbols in `define-fun` (#7655)Andres Noetzli
2021-11-16[proofs] Make sure --proof-check=... is no-op when not checking proofs (#7638)Haniel Barbosa
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-11Generalize front-end checks to check for shadowed variables (#7634)Andrew Reynolds
2021-11-11Add lazy approach for handling lambdas in the HO extension (#7625)Andrew Reynolds
2021-11-09Remove command-verbosity option (#7581)Gereon Kremer
2021-11-06Print `unsupported` for unrecognized flags. (#7384)Abdalrhman Mohamed
2021-11-06Remove `Notice()` in favor of new `verbose()` (#7588)Gereon Kremer
2021-11-05Eliminate a level of nesting of traversals in theory preprocessing (#7345)Andrew Reynolds
2021-11-05Remove `Chat()` in favor of new `verbose()` (#7586)Gereon Kremer
2021-11-05Remove many static calls to rewrite (#7580)Andrew Reynolds
2021-11-05Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)Gereon Kremer
2021-11-04Replace the old dump infrastructure (#7572)Andrew Reynolds
2021-11-04Start refactoring of `-o` and `-v` (#7449)Gereon Kremer
2021-11-04Enable CDCAC solver for selected quantified logics (#7571)Gereon Kremer
2021-11-04Minor cleanup in SolverEngine::setInfo() (#7566)Gereon Kremer
2021-11-03api: Rename some separation logic functions for consistency. (#7564)Aina Niemetz
2021-11-03Refactor skolem construction (#7561)Andrew Reynolds
2021-11-02Add printing methods for some commands. (#7557)Abdalrhman Mohamed
2021-11-02Fix setDefaults() for proofs with bitblast-internal. (#7552)Mathias Preiner
2021-11-02Make quant elimination robust to presence of other quantified formulas (#7551)Andrew Reynolds
2021-11-01bv: Remove layered solver. (#7455)Mathias Preiner
2021-11-01Replace more static options accesses (#7531)Gereon Kremer
2021-10-28Add a `define-fun` command for each `:named` term. (#7308)Abdalrhman Mohamed
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
2021-10-26[proofs] Fix singleton check in MACRO_RES post-processing (#7498)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback