summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-09-07Merge branch 'master' into theoryElimContexttheoryElimContextAndres Noetzli
2021-09-07sygus: Eliminate calls to Rewriter::rewrite. (#7142)Aina Niemetz
2021-09-07Refactoring and fixes of set defaults for quantifiers (#7120)Andrew Reynolds
2021-09-05Use `EnvObj` methods instead of `Theory` methodsAndres Noetzli
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-09-03Avoiding duplicate search in maps (#7055)MikolasJanota
2021-09-03sygus: Make more classes derive from EnvObj. (#7140)Aina Niemetz
2021-09-03Refactor option sanitizations (#7129)Gereon Kremer
2021-09-03Standardize Rewriter::rewriteViaMethod call (#7119)Andrew Reynolds
2021-09-03Check that alternate is only set for bool (#7125)Gereon Kremer
2021-09-03Refactor options::get() and options::getNames() (#7135)Gereon Kremer
2021-09-03Make quantifier module classes derive from EnvObj (#7132)Andrew Reynolds
2021-09-03sygus: Make CeSingleInv derive from EnvObj. (#7136)Aina Niemetz
2021-09-03Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)Andrew Reynolds
2021-09-03theory: Have more classes in theory with reference to Env derive from EnvObj....Aina Niemetz
2021-09-03theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)Aina Niemetz
2021-09-03Remove "experimental" options (#7124)Gereon Kremer
2021-09-02pp: Have PreprocessingPassContext derive from EnvObj. (#7127)Aina Niemetz
2021-09-02Add LFSC node converter (#6944)Andrew Reynolds
2021-09-02Refactor options handlers (#7080)Gereon Kremer
2021-09-02[Unit Tests] Fix shell test for Editline (#7117)Andres Noetzli
2021-09-02Disable sygus-inst for regression close to time limit. (#7122)Aina Niemetz
2021-09-02EnvObj: Restrict access. (#7121)Aina Niemetz
2021-09-02Add API check whether option in getOptionInfo() exists (#7093)Gereon Kremer
2021-09-02Driver & Options cleanup (#7109)Gereon Kremer
2021-09-02Remove more instances of ufHo (#7087)Andrew Reynolds
2021-09-02Remove options::getAll() (#7111)Gereon Kremer
2021-09-02[CI] Add step for running unit/API tests (#7116)Andres Noetzli
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-02Remove PreprocessingPassContext::getSmt(). (#7118)Aina Niemetz
2021-09-02Remove unused `Backtracker` (#7115)Andres Noetzli
2021-09-02[Unit Tests] Fix bags rewrite test (#7114)Andres Noetzli
2021-09-02pp: Derive PreprocessingPass from EnvObj. (#7112)Aina Niemetz
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-09-02rewriter: Make rewriteEqualityExt non-static. (#7110)Aina Niemetz
2021-09-02Add class EnvObj. (#7113)Aina Niemetz
2021-09-02Update CI to macOS 11 (#7104)Andres Noetzli
2021-09-01Clean up and document PP context. (#7102)Aina Niemetz
2021-09-01Clean up TheoryEngine header according to code style guidelines. (#7107)Aina Niemetz
2021-09-01[proof] [sat] Fix lost reference to reason when processing redundant literals...Haniel Barbosa
2021-09-01Print response to get-model using the API (#7084)Andrew Reynolds
2021-09-01rewriter: Make registerTheoryRewriter non-static. (#7101)Aina Niemetz
2021-09-01Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)mudathirmahgoub
2021-09-01Fix issues with cyclic proofs due to double SYMM applications (#7083)Andrew Reynolds
2021-09-01Make driver::totalTime a TimerStat (#7089)Gereon Kremer
2021-09-01No longer use direct access to options in driver (#7094)Gereon Kremer
2021-09-01rewriter: Make clearCaches non-static. (#7100)Aina Niemetz
2021-09-01Lazy proof reconstruction for strings theory solver (#7096)Andrew Reynolds
2021-08-31bv: Remove dump=bv-rewrites. (#7099)Aina Niemetz
2021-08-31Make sure modes are sorted in ModeInfo (#7097)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback