summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-10-05tmpproof-new-dslAndres Noetzli
2021-09-02Formatajreynol
2021-09-02Fixes from mergeajreynol
2021-09-02Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
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-02Add missing Boolean rules to LFSC printerajreynol
2021-09-02Remove unused `Backtracker` (#7115)Andres Noetzli
2021-09-02Disable proofs for failing regressionajreynol
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-01Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-09-01Clean up TheoryEngine header according to code style guidelines. (#7107)Aina Niemetz
2021-09-01Formatajreynol
2021-09-01Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
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-01Fix lost reference to reason when processing redundant literalsHaniel Barbosa
2021-09-01rewriter: Make registerTheoryRewriter non-static. (#7101)Aina Niemetz
2021-09-01Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)mudathirmahgoub
2021-09-01Fix namespaceajreynol
2021-09-01Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
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-31Formatajreynol
2021-08-31Avoid use of extended rewriter in strings proof reconstruction, no use of REW...ajreynol
2021-08-31Formatajreynol
2021-08-31Justify extended rewrites via normal + extended equality rewritesajreynol
2021-08-31Use more robust conversion for arithmetic trichotomyajreynol
2021-08-31Support arith trichotomy in LFSCajreynol
2021-08-31Formatajreynol
2021-08-31Extended rewriter to show core steps in strings reconstructionajreynol
2021-08-31Formatajreynol
2021-08-31Use extended equality rewriter for showing proofs of prefix conflictsajreynol
2021-08-31Make sure modes are sorted in ModeInfo (#7097)Gereon Kremer
2021-08-31Add support concat unify in LFSCajreynol
2021-08-31bv-to-int-module: implementations and stubs for translating operators (#7086)yoni206
2021-08-31Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-08-31Fix normal forms context-dependent simplification for strings (#7090)Andrew Reynolds
2021-08-31Make regular expression sort not closed enumerable (#7092)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback