summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-09-20Optionally enable interprocedural optimization (#7209)Andres Noetzli
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
2021-09-13Refactor options parsing (#7143)Gereon Kremer
2021-09-11Use StatisticsRegistry from Env (#7166)Gereon Kremer
2021-09-11checkModel: Extend documentation. (#7177)Aina Niemetz
2021-09-11bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)Mathias Preiner
2021-09-11Add casc 28 scripts (#7070)Andrew Reynolds
2021-09-10FP: Enable caching in the theory inference manager. (#7168)Aina Niemetz
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)Mathias Preiner
2021-09-10FP: Use EnvObj::rewrite() and options() in theory_fp. (#7169)Aina Niemetz
2021-09-10FP: Do not send trivial lemmas. (#7167)Aina Niemetz
2021-09-10Add Op.java to the java API (#6387)mudathirmahgoub
2021-09-10Use C++17 attributes (#7154)Andres Noetzli
2021-09-10More refactoring of set defaults (#7160)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback