summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-12-02Remove void as possible option type (#7731)Gereon Kremer
2021-12-02Fixes for sygus-rr-synth-input (#7716)Andrew Reynolds
2021-12-02[proofs] Fix a trace in SAT proof manager (#7732)Haniel Barbosa
2021-12-02add bag.fold operator (#7718)mudathirmahgoub
2021-12-02Add unit tests for api::Solver::setOption() (#7708)Gereon Kremer
2021-12-01api: Add missing bit-width 0 check to mkBVFromStrHelper. (#7727)Mathias Preiner
2021-12-01[proofs] Add method to CDProof to obtain number of proof nodes (#7725)Haniel Barbosa
2021-12-01[proofs] Alethe: Add finalize function to insert missing OR steps (#7724)Lachnitt
2021-12-01Improvements for get-difficulty (#7720)Andrew Reynolds
2021-12-01Enable Java examples (#7702)mudathirmahgoub
2021-12-01Alethe: Add function that adds final steps to proof (#7710)Lachnitt
2021-12-01Remove spurious assertion in parser (#7713)Andrew Reynolds
2021-12-01Define sort undeclared (#7714)Andrew Reynolds
2021-11-30Add rewrite for is_int pi (#7711)Andrew Reynolds
2021-11-30Generalize eager length bound conflicts for regular expression memberships (#...Andrew Reynolds
2021-11-30Proper check for first-class types in datatype subfields (#7712)Andrew Reynolds
2021-11-30Alethe: Further Printer Implementation (#7675)Lachnitt
2021-11-30[proofs] Alethe: Implementation of Printer (#7674)Lachnitt
2021-11-30Remove now unused dumping infrastructure (#7703)Gereon Kremer
2021-11-30[proofs] Alethe: Printer Specification (#7673)Lachnitt
2021-11-29Fix minor issues (#7704)Gereon Kremer
2021-11-25api: Refactor mkTerm for kinds with arity = 0. (#7699)Aina Niemetz
2021-11-24cmake: Add option --[no]-static-binary. (#7695)Mathias Preiner
2021-11-24Remove dependency of `TypeNode` on `Node` (#7690)Andres Noetzli
2021-11-24Fix potential for cycles in trust substitutions (#7687)Andrew Reynolds
2021-11-24Minor fixes (#7691)Andres Noetzli
2021-11-24api: Fix creation of nary term kinds via Op. (#7688)Aina Niemetz
2021-11-23Make difficulty manager only consider lemmas at full effort (#7685)Andrew Reynolds
2021-11-23Enable model-based reduction technique for strings (#7680)Andrew Reynolds
2021-11-23Push output language inside the printing code (#7683)Gereon Kremer
2021-11-23Add rewrite rule for bag.card operator using bag.map and lambda (#7643)mudathirmahgoub
2021-11-23Python API documentation: terms (#7659)yoni206
2021-11-23Make `node_value.h` not depend on `node_manager.h` (#7676)Andres Noetzli
2021-11-22Refactor IO stream manipulators (#7555)Gereon Kremer
2021-11-22Add rewrite for repeated re.allchar (#7681)Andrew Reynolds
2021-11-22[prop] Remove unused #define in theory proxy (#7670)Haniel Barbosa
2021-11-22Improve error for check theory assertions with model (#7679)Andrew Reynolds
2021-11-21Fix const RE test for internal regexp rv kind (#7678)Andrew Reynolds
2021-11-20bv2int module: translation of more cases (#7653)yoni206
2021-11-19[API] Avoid copying values (#7666)Andres Noetzli
2021-11-19Clean up relationship of metakind and node_manager (#7649)Andres Noetzli
2021-11-19Remove n-ary builder (#7671)Andrew Reynolds
2021-11-19Allow negative denominator for CLN Rationals constructed from string. (#7667)Mathias Preiner
2021-11-18api: Fix categorization of DT kinds in kind maps. (#7668)Aina Niemetz
2021-11-18Refactor CAD option for linear model seed (#7657)Gereon Kremer
2021-11-18[proofs] Fix trace in SatProofManager (#7664)Haniel Barbosa
2021-11-18[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)Lachnitt
2021-11-18api: Fix kind documentation for BAG_MAKE. (#7663)Aina Niemetz
2021-11-17Improve naming in term canonization when handling HO variables (#7660)Haniel Barbosa
2021-11-17[sat] Fix indentation in "reason" (#7662)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback