summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171)Mathias Preiner
2021-09-10Refactor command-line help (#7157)Gereon Kremer
2021-09-09Use EnvObj-based options in preprocessing (#7165)Gereon Kremer
2021-09-09pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)Aina Niemetz
2021-09-09Remove `TheoryState::getEnv()` (#7163)Andres Noetzli
2021-09-09Add Solver::getOutput() (#7162)Gereon Kremer
2021-09-09Add difficulty manager (#7151)Andrew Reynolds
2021-09-09Add difficulty post-processor (#7150)Andrew Reynolds
2021-09-09Disable shared selectors for quantified logics without SyGuS (#7156)Andrew Reynolds
2021-09-09Remove `TheoryState::options()` (#7148)Andres Noetzli
2021-09-08Remove deprecated SyGuS method evaluateWithUnfolding (#7155)Andrew Reynolds
2021-09-08Add Lfsc print channel utilities (#7123)Andrew Reynolds
2021-09-08Improve pre-skolemization, move quantifiers preprocess to own file (#7153)Andrew Reynolds
2021-09-08Refactor options::set() (#7138)Gereon Kremer
2021-09-08Work on comments (#7139)Gereon Kremer
2021-09-08A couple of minor cleanups (#7141)Gereon Kremer
2021-09-08Refactor code generation for options.h/.cpp (#7126)Gereon Kremer
2021-09-08Towards standard usage of ExtendedRewriter (#7145)Andrew Reynolds
2021-09-08Add option for using bound inference for relevant assertions (#7152)Andrew Reynolds
2021-09-08Add LFSC side condition conversion utility for list variables (#7131)Andrew Reynolds
2021-09-08Add Datatype.java to the Java API (#6389)mudathirmahgoub
2021-09-08Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java...mudathirmahgoub
2021-09-08Use rewriteViaMethod instead of accessing builtin proof checker (#7146)Andrew Reynolds
2021-09-07Refactoring of proof manager initialization (#7073)Andrew Reynolds
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres 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-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-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-02Implement lazy proof checking modes (#7106)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback