summaryrefslogtreecommitdiff
path: root/src/CMakeLists.txt
AgeCommit message (Expand)Author
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-12-06New algorithm for interpolation and abduction based on unsat cores (#3255)Andrew Reynolds
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-05Separate model object in non-linear extension (#3426)Andrew Reynolds
2019-10-31Rename datatypes sygus solver (#3417)Andrew Reynolds
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
2019-10-17 Move datatype utility functions to own file (#3397)Andrew Reynolds
2019-10-16Solver state for theory of strings (#3181)Andrew Reynolds
2019-10-10Make order of theories explicit in the source code. (#3379)Aina Niemetz
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-09-25Use separate CMake project for CVC4 examples. (#3196)Mathias Preiner
2019-09-16Sygus type info class (#3187)Andrew Reynolds
2019-09-16Move virtual term substitution utilities to own file and document (#3278)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
2019-09-11Refactoring finite bounds in Quantifiers Engine (#3261)Andrew Reynolds
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-08-23Document transition inference utility (#3207)Andrew Reynolds
2019-08-14cmake: Export CVC4 library interface. (#3179)Mathias Preiner
2019-08-02 Move basic sygus enumerator to its own file (#3149)Andrew Reynolds
2019-08-01Move some generic utilities out of quantifiers (#3139)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-25Split infer info data structure in strings (#3107)Andrew Reynolds
2019-07-08Towards refactoring relations (#3078)Andrew Reynolds
2019-07-05Refactor strings to use an inference manager object (#3076)Andrew Reynolds
2019-07-02Optimize DRAT optimization: clause matching (#3074)Alex Ozdemir
2019-07-01 Split higher-order UF solver (#2890)Andrew Reynolds
2019-07-01Add higher-order elimination preprocessing pass (#2865)Andrew Reynolds
2019-06-05DRAT-Optimization (#2971)Alex Ozdemir
2019-04-23Refactor normal forms in strings (#2897)Andrew Reynolds
2019-04-15Check for rt library in configuration -- support for glibc<2.17 (#2854)makaimann
2019-03-24 Split regular expression solver (#2891)Andrew Reynolds
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-13Add statistics for proof gen./checking time, size (#2850)Andres Noetzli
2019-03-12Fix public headers for make install. (#2856)Mathias Preiner
2019-02-28ErProof class with LFSC output (#2812)Alex Ozdemir
2019-01-18Extract DIMACS Printing (#2800)Alex Ozdemir
2019-01-14ClausalBitvectorProof (#2786)Alex Ozdemir
2019-01-06[DRAT] DRAT data structure (#2767)Alex Ozdemir
2019-01-04[LRAT] A C++ data structure for LRAT. (#2737)Alex Ozdemir
2018-12-17 Configured for linking against drat2er (#2754)Alex Ozdemir
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-12-03Bit vector proof superclass (#2599)Alex Ozdemir
2018-10-31Add optimized sygus enumeration (#2677)Andrew Reynolds
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-17Sygus query generator (#2465)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback