summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2021-08-31bv-to-int-module: implementations and stubs for translating operators (#7086)yoni206
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
2021-08-30Add API function to obtain information about a single option (#6980)Gereon Kremer
2021-08-30Add kind BAG_MAP and its type rule to bags (#6503)mudathirmahgoub
2021-08-30Further refactoring of set defaults for incompatibility methods (#7072)Andrew Reynolds
2021-08-30Refactor filename handling (#7088)Gereon Kremer
2021-08-30Fix proof equality engine for "no-explain" premises (#7079)Andrew Reynolds
2021-08-30python docs for Datatype-related classes (#7058)yoni206
2021-08-30Fix quantifiers dynamic split module for parametric datatypes (#7085)Andrew Reynolds
2021-08-27Add Driver options (#7078)Gereon Kremer
2021-08-27Handle languages as strings in driver (#7074)Gereon Kremer
2021-08-27Expand definitions in sygus operators at the SMT level (#7077)Andrew Reynolds
2021-08-27Add n-ary match trie utility (#6909)Andrew Reynolds
2021-08-27Add missing methods to Solver API for models (#7052)Andrew Reynolds
2021-08-27Add `isNull` to cpp api tests, python api, and python api tests (#7059)yoni206
2021-08-26Fix a subtle issues with squashing the docs-ci history (#7075)Gereon Kremer
2021-08-26Eliminate currentSmtEngine for subsolver calls (#7068)Andrew Reynolds
2021-08-26Dump models for isNotEntailed results (#7071)Andrew Reynolds
2021-08-26Make datatype selector expansion to its own accessible method (#7069)Andrew Reynolds
2021-08-26Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)Gereon Kremer
2021-08-26int2bv: Fix conversion of signed bit-vector values. (#7061)Mathias Preiner
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-08-25Add missing include (#7067)Gereon Kremer
2021-08-25Eliminate calls to currentSmtEngine (#7060)Andrew Reynolds
2021-08-24Split higher-order term database (#7045)Andrew Reynolds
2021-08-24Refactor enumerator management in synth conjecture (#6942)Andrew Reynolds
2021-08-24bv-to-int: more implementations (#7051)yoni206
2021-08-24Top-level structure for set defaults (#7047)Andrew Reynolds
2021-08-24Uniform treatment of trusted theory inferences in proofs (#7044)Andrew Reynolds
2021-08-24Miscellaneous changes from proof-new (#7042)Andrew Reynolds
2021-08-23Fix non-deterministism in quantified datatypes expansion rewrite (#7036)Andrew Reynolds
2021-08-23Purify substitutions in strings proof reconstruction (#7035)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback