summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-09-23Use `|` to print quoted strings in `set-info` command. (#7240)Abdalrhman Mohamed
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
2021-09-22Make cegqi subsolvers EnvObj (#7205)Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-22Towards standard usage of evaluator (#7189)Andrew Reynolds
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
2021-09-22arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)Aina Niemetz
2021-09-22arrays: Move type enumerator implementation to .cpp. (#7216)Aina Niemetz
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
2021-09-22Minimal fixing version for tuple update parsing (#7228)Andrew Reynolds
2021-09-21[Proofs] Alethe: Translate ASSUME rule (#7213)Lachnitt
2021-09-21[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)Lachnitt
2021-09-20Fix handling of conversions between FP and reals (#7149)Andres Noetzli
2021-09-20Start python API Solver documentation (#7064)Alex Ozdemir
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
2021-09-20Add the LFSC proof post-processor (#7134)Andrew Reynolds
2021-09-20TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)Aina Niemetz
2021-09-20Add anchors to cmdline options (#7210)Gereon Kremer
2021-09-18Fix printer for datatype udpater (#7208)Andrew Reynolds
2021-09-18Refactor tag suggestion mechanism (#7199)Gereon Kremer
2021-09-17Use a single `NodeManager` per thread (#7204)Andres Noetzli
2021-09-17[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)Lachnitt
2021-09-17[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)Lachnitt
2021-09-17Replace write access to options by a local variable (#7207)Gereon Kremer
2021-09-17Minor cleanup related to EnvObj (#7206)Gereon Kremer
2021-09-16Fix relevant domain for parametric operators (#7198)Andrew Reynolds
2021-09-15[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)Lachnitt
2021-09-15Minor changes to E-matching utilities (#7062)Andrew Reynolds
2021-09-15remove options that are no longer used (#7197)Gereon Kremer
2021-09-15[proof] Added printer for proof rule names (#7185)Lachnitt
2021-09-15[proof] Alethe proof rules (#7180)Lachnitt
2021-09-15Eliminate global access to options:: from quantifiers rewriter (#7192)Andrew Reynolds
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
2021-09-14Final cleanup (#7193)Gereon Kremer
2021-09-14Make `-o raw-benchmark` work with `--parse-only` (#7195)Andres Noetzli
2021-09-14Support sygus version 2.1 command assume (#7081)Andrew Reynolds
2021-09-14Utilities in preparation for print benchmark utility (#7190)Andrew Reynolds
2021-09-14Add proof manager method to translate difficulty map (#7159)Andrew Reynolds
2021-09-14Refactor code generation for option modules (#7182)Gereon Kremer
2021-09-14Turn sphinx generation into a function (#7181)Gereon Kremer
2021-09-14bv: Unify bit-blasting code for udiv and urem. (#7188)Mathias Preiner
2021-09-14proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)Mathias Preiner
2021-09-14Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)Andrew Reynolds
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-09-13Connect difficulty manager to TheoryEngine (#7161)Andrew Reynolds
2021-09-13Add Solver::isOutputOn() (#7187)Gereon Kremer
2021-09-13FP: Rename FpConverter to FpWordBlaster. (#7170)Aina Niemetz
2021-09-13Refactor generation code for getInfo() (#7176)Gereon Kremer
2021-09-13Add main options to cmake (#7178)Gereon Kremer
2021-09-13Reorder code (#7175)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback