projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167) commit | commitdiff | tree
2021-09-10 mudathirmahgoubAdd Op.java to the java API (#6387) commit | commitdiff | tree
2021-09-10 Andres NoetzliUse C++17 attributes (#7154) commit | commitdiff | tree
2021-09-10 Andrew ReynoldsMore refactoring of set defaults (#7160) commit | commitdiff | tree
2021-09-10 Mathias Preinerbv: Use EnvObj::rewrite() and EnvObj::options() in... commit | commitdiff | tree
2021-09-10 Gereon KremerRefactor command-line help (#7157) commit | commitdiff | tree
2021-09-10 Gereon KremerUse EnvObj-based options in preprocessing (#7165) commit | commitdiff | tree
2021-09-09 Aina Niemetzpp passes: Use EnvObj::rewrite() instead of Rewriter... commit | commitdiff | tree
2021-09-09 Andres NoetzliRemove `TheoryState::getEnv()` (#7163) commit | commitdiff | tree
2021-09-09 Gereon KremerAdd Solver::getOutput() (#7162) commit | commitdiff | tree
2021-09-09 Andrew ReynoldsAdd difficulty manager (#7151) commit | commitdiff | tree
2021-09-09 Andrew ReynoldsAdd difficulty post-processor (#7150) commit | commitdiff | tree
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without... commit | commitdiff | tree
2021-09-09 Andres NoetzliRemove `TheoryState::options()` (#7148) commit | commitdiff | tree
2021-09-09 Andrew ReynoldsRemove deprecated SyGuS method evaluateWithUnfolding... commit | commitdiff | tree
2021-09-08 Andrew ReynoldsAdd Lfsc print channel utilities (#7123) commit | commitdiff | tree
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... commit | commitdiff | tree
2021-09-08 Gereon KremerRefactor options::set() (#7138) commit | commitdiff | tree
2021-09-08 Gereon KremerWork on comments (#7139) commit | commitdiff | tree
2021-09-08 Gereon KremerA couple of minor cleanups (#7141) commit | commitdiff | tree
2021-09-08 Gereon KremerRefactor code generation for options.h/.cpp (#7126) commit | commitdiff | tree
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145) commit | commitdiff | tree
2021-09-08 Andrew ReynoldsAdd option for using bound inference for relevant asser... commit | commitdiff | tree
2021-09-08 Andrew ReynoldsAdd LFSC side condition conversion utility for list... commit | commitdiff | tree
2021-09-08 mudathirmahgoubAdd Datatype.java to the Java API (#6389) commit | commitdiff | tree
2021-09-08 mudathirmahgoubAdd DatatypeConstructor.java, DatatypeConstructorDecl... commit | commitdiff | tree
2021-09-08 Andrew ReynoldsUse rewriteViaMethod instead of accessing builtin proof... commit | commitdiff | tree
2021-09-07 Andrew ReynoldsRefactoring of proof manager initialization (#7073) commit | commitdiff | tree
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... commit | commitdiff | tree
2021-09-07 Aina Niemetzsygus: Eliminate calls to Rewriter::rewrite. (#7142) commit | commitdiff | tree
2021-09-07 Andrew ReynoldsRefactoring and fixes of set defaults for quantifiers... commit | commitdiff | tree
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... commit | commitdiff | tree
2021-09-03 MikolasJanotaAvoiding duplicate search in maps (#7055) commit | commitdiff | tree
2021-09-03 Aina Niemetzsygus: Make more classes derive from EnvObj. (#7140) commit | commitdiff | tree
2021-09-03 Gereon KremerRefactor option sanitizations (#7129) commit | commitdiff | tree
2021-09-03 Andrew ReynoldsStandardize Rewriter::rewriteViaMethod call (#7119) commit | commitdiff | tree
2021-09-03 Gereon KremerCheck that alternate is only set for bool (#7125) commit | commitdiff | tree
2021-09-03 Gereon KremerRefactor options::get() and options::getNames() (#7135) commit | commitdiff | tree
2021-09-03 Andrew ReynoldsMake quantifier module classes derive from EnvObj ... commit | commitdiff | tree
2021-09-03 Aina Niemetzsygus: Make CeSingleInv derive from EnvObj. (#7136) commit | commitdiff | tree
2021-09-03 Andrew ReynoldsEliminate backwards ref to SmtEngine from abduction... commit | commitdiff | tree
2021-09-03 Aina Niemetztheory: Have more classes in theory with reference... commit | commitdiff | tree
2021-09-03 Aina Niemetztheory: Have Theory and TheoryArith* derive from EnvObj... commit | commitdiff | tree
2021-09-03 Gereon KremerRemove "experimental" options (#7124) commit | commitdiff | tree
2021-09-03 Aina Niemetzpp: Have PreprocessingPassContext derive from EnvObj... commit | commitdiff | tree
2021-09-02 Andrew ReynoldsAdd LFSC node converter (#6944) commit | commitdiff | tree
2021-09-02 Gereon KremerRefactor options handlers (#7080) commit | commitdiff | tree
2021-09-02 Andres Noetzli[Unit Tests] Fix shell test for Editline (#7117) commit | commitdiff | tree
2021-09-02 Aina NiemetzDisable sygus-inst for regression close to time limit... commit | commitdiff | tree
2021-09-02 Aina NiemetzEnvObj: Restrict access. (#7121) commit | commitdiff | tree
2021-09-02 Gereon KremerAdd API check whether option in getOptionInfo() exists... commit | commitdiff | tree
2021-09-02 Gereon KremerDriver & Options cleanup (#7109) commit | commitdiff | tree
2021-09-02 Andrew ReynoldsRemove more instances of ufHo (#7087) commit | commitdiff | tree
2021-09-02 Gereon KremerRemove options::getAll() (#7111) commit | commitdiff | tree
2021-09-02 Andres Noetzli[CI] Add step for running unit/API tests (#7116) commit | commitdiff | tree
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) commit | commitdiff | tree
2021-09-02 Aina NiemetzRemove PreprocessingPassContext::getSmt(). (#7118) commit | commitdiff | tree
2021-09-02 Andres NoetzliRemove unused `Backtracker` (#7115) commit | commitdiff | tree
2021-09-02 Andres Noetzli[Unit Tests] Fix bags rewrite test (#7114) commit | commitdiff | tree
2021-09-02 Aina Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112) commit | commitdiff | tree
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098) commit | commitdiff | tree
2021-09-02 Aina Niemetzrewriter: Make rewriteEqualityExt non-static. (#7110) commit | commitdiff | tree
2021-09-02 Aina NiemetzAdd class EnvObj. (#7113) commit | commitdiff | tree
2021-09-02 Andres NoetzliUpdate CI to macOS 11 (#7104) commit | commitdiff | tree
2021-09-01 Aina NiemetzClean up and document PP context. (#7102) commit | commitdiff | tree
2021-09-01 Aina NiemetzClean up TheoryEngine header according to code style... commit | commitdiff | tree
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process... commit | commitdiff | tree
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) commit | commitdiff | tree
2021-09-01 Aina Niemetzrewriter: Make registerTheoryRewriter non-static. ... commit | commitdiff | tree
2021-09-01 mudathirmahgoubFixed TestTheoryWhiteBagsRewriter.map failure (#7103) commit | commitdiff | tree
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic... commit | commitdiff | tree
2021-09-01 Gereon KremerMake driver::totalTime a TimerStat (#7089) commit | commitdiff | tree
2021-09-01 Gereon KremerNo longer use direct access to options in driver (... commit | commitdiff | tree
2021-09-01 Aina Niemetzrewriter: Make clearCaches non-static. (#7100) commit | commitdiff | tree
2021-09-01 Andrew ReynoldsLazy proof reconstruction for strings theory solver... commit | commitdiff | tree
2021-08-31 Aina Niemetzbv: Remove dump=bv-rewrites. (#7099) commit | commitdiff | tree
2021-08-31 Gereon KremerMake sure modes are sorted in ModeInfo (#7097) commit | commitdiff | tree
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla... commit | commitdiff | tree
2021-08-31 Andrew ReynoldsFix normal forms context-dependent simplification for... commit | commitdiff | tree
2021-08-31 Andrew ReynoldsMake regular expression sort not closed enumerable... commit | commitdiff | tree
2021-08-30 Gereon KremerAdd API function to obtain information about a single... commit | commitdiff | tree
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503) commit | commitdiff | tree
2021-08-30 Andrew ReynoldsFurther refactoring of set defaults for incompatibility... commit | commitdiff | tree
2021-08-30 Gereon KremerRefactor filename handling (#7088) commit | commitdiff | tree
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... commit | commitdiff | tree
2021-08-30 yoni206python docs for Datatype-related classes (#7058) commit | commitdiff | tree
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... commit | commitdiff | tree
2021-08-27 Gereon KremerAdd Driver options (#7078) commit | commitdiff | tree
2021-08-27 Gereon KremerHandle languages as strings in driver (#7074) commit | commitdiff | tree
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level... commit | commitdiff | tree
2021-08-27 Andrew ReynoldsAdd n-ary match trie utility (#6909) commit | commitdiff | tree
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) commit | commitdiff | tree
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python... commit | commitdiff | tree
2021-08-26 Gereon KremerFix a subtle issues with squashing the docs-ci history... commit | commitdiff | tree
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) commit | commitdiff | tree
2021-08-26 Andrew ReynoldsDump models for isNotEntailed results (#7071) commit | commitdiff | tree
2021-08-26 Andrew ReynoldsMake datatype selector expansion to its own accessible... commit | commitdiff | tree
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the... commit | commitdiff | tree
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... commit | commitdiff | tree
2021-08-26 Gereon KremerConsolidate language types (#7065) commit | commitdiff | tree
next