summaryrefslogtreecommitdiff
path: root/src/CMakeLists.txt
AgeCommit message (Expand)Author
2021-10-20Reimplement support for relational triggers (#7063)Andrew Reynolds
2021-10-20Add basic regular expression type enumerator (#7416)Andrew Reynolds
2021-10-14Split entailment check from term database (#7342)Andrew Reynolds
2021-10-14Fix GLPK linking (#7357)Gereon Kremer
2021-10-12Rename SmtEngineState to SolverEngineState. (#7344)Aina Niemetz
2021-10-12Fix glpk, add antlr.so (#7341)Gereon Kremer
2021-10-11Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)Aina Niemetz
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-11Revert #7257 (#7337)Gereon Kremer
2021-10-11Restore compatibility with cmake 3.9 (#7329)Gereon Kremer
2021-10-07Add new versioning scheme (#7253)Gereon Kremer
2021-10-07Fix/Improve static and shared builds with CLN or Poly (#7306)Gereon Kremer
2021-10-01Add the LFSC printer (#7158)Andrew Reynolds
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-30Refactor our static builds (#7251)Gereon Kremer
2021-09-29Add the strings array solver (#7232)Andrew Reynolds
2021-09-29remove stuff (#7258)Gereon Kremer
2021-09-28Remove linking against RT (#7257)Gereon Kremer
2021-09-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-22arrays: Move type enumerator implementation to .cpp. (#7216)Aina Niemetz
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
2021-09-20Add the LFSC proof post-processor (#7134)Andrew Reynolds
2021-09-14proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)Mathias Preiner
2021-09-13FP: Rename FpConverter to FpWordBlaster. (#7170)Aina Niemetz
2021-09-13Add main options to cmake (#7178)Gereon Kremer
2021-09-09Add difficulty manager (#7151)Andrew Reynolds
2021-09-09Add difficulty post-processor (#7150)Andrew Reynolds
2021-09-08Add Lfsc print channel utilities (#7123)Andrew Reynolds
2021-09-08Improve pre-skolemization, move quantifiers preprocess to own file (#7153)Andrew Reynolds
2021-09-08Add LFSC side condition conversion utility for list variables (#7131)Andrew Reynolds
2021-09-02Add LFSC node converter (#6944)Andrew Reynolds
2021-09-02Add class EnvObj. (#7113)Aina Niemetz
2021-08-30Fix proof equality engine for "no-explain" premises (#7079)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-22Simplify model printing modes (#7049)Andrew Reynolds
2021-08-19Split proof final callback to its own file (#6984)Andrew Reynolds
2021-08-17Initial refactoring of set defaults (#7021)Andrew Reynolds
2021-08-09Support older CMake versions (#7003)Andres Noetzli
2021-08-06Merge options cmake into general cmake file (#6989)Gereon Kremer
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-07-27Add basic LFSC utilities (#6879)Andrew Reynolds
2021-07-27Move enum value generator to own file (#6941)Andrew Reynolds
2021-07-27Add proof letify utility (#6881)Andrew Reynolds
2021-07-27Add sygus enumerator callback (#6923)Andrew Reynolds
2021-07-22Add the central equality engine manager (#6893)Andrew Reynolds
2021-07-15Connect the equality solver to theory arith (#6894)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback