summaryrefslogtreecommitdiff
path: root/src/CMakeLists.txt
AgeCommit message (Expand)Author
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
2021-04-07New C++ Api: Rename and move checks.h. (#6306)Aina Niemetz
2021-04-07Add term pools utility (#6243)Andrew Reynolds
2021-04-05New C++ Api: Rename and move headers. (#6292)Aina Niemetz
2021-04-05Optimizer for BitVectors (#6213)Yancheng Ou
2021-04-01Refactor CLN dependency & Cleanup (#6251)Gereon Kremer
2021-03-31Refactor GMP and Poly dependencies (#6245)Gereon Kremer
2021-03-31Refactor dependencies for external SAT solvers (#6215)Gereon Kremer
2021-03-31Refactor SymFPU dependency (#6218)Gereon Kremer
2021-03-31Bags: Move implementation of type rules from header to .cpp file. (#6247)Aina Niemetz
2021-03-31FP: Move implementation of type rules from header to .cpp file. (#6241)Aina Niemetz
2021-03-29Modular bv2int part 1 (#6212)yoni206
2021-03-25Refactor construction of triggers (#6209)Andrew Reynolds
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
2021-03-22Add skolem definition manager (#6187)Andrew Reynolds
2021-03-17Move utilities for inferred bounds on quantifers to own class (#6159)Andrew Reynolds
2021-03-16cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)Mathias Preiner
2021-03-15Split inst match generator class to own file (#6125)Andrew Reynolds
2021-03-14[proof-new] Adding a dot printer for proof nodes (#6144)Diego Della Rocca de Camargos
2021-03-12New C++ Api: Move checks to separate file. (#6138)Aina Niemetz
2021-03-12cmake: Remove install rules for old API headers. (#6120)Mathias Preiner
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-11Improvements and refactoring for enumeratative strategy (#6030)MikolasJanota
2021-03-11(proof-new) Clean up uses of witness with skolem lemmas (#6109)Andrew Reynolds
2021-03-10Add Env class (#6093)Andrew Reynolds
2021-03-09Remove logic request (#6089)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)Andrew Reynolds
2021-03-05Initial implementation of an optimization solver with unit tests. (#5849)mcjuneho
2021-03-04Add initial bit-blaster for proof logging. (#6053)Aina Niemetz
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-02-27google test: theory: Migrate theory_white. (#6006)Aina Niemetz
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-22Add the LazyTreeProofGenerator. (#5948)Gereon Kremer
2021-02-19Cleanup of inferences in arithmetic theory (#5927)Gereon Kremer
2021-02-17Move first order model for full model check to own file (#5918)Andrew Reynolds
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
2021-02-13Moving methods from quantifiers engine to quantifiers state (#5881)Andrew Reynolds
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
2021-02-03Add BV solver bitblast. (#5851)Mathias Preiner
2021-01-27Split pattern term selector from trigger (#5811)Andrew Reynolds
2021-01-26Introduce quantifiers inference manager (#5821)Andrew Reynolds
2021-01-26Remove deprecated quantifiers modules (#5820)Andrew Reynolds
2021-01-25Split inst match generator into multiple files (#5805)Andrew Reynolds
2021-01-25Split E-matching strategies to own files (#5807)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback