summaryrefslogtreecommitdiff
path: root/src/Makefile.am
AgeCommit message (Expand)Author
2018-03-01Create infrastructure for sygus modules (#1632)Andrew Reynolds
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-13Remove unused cd_set_collection.h (#1606)Andres Noetzli
2018-02-09Class to reduce printing of redundant candidate rewrites (#1588)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-08Document and clean datatypes rewriter (#1437)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
2017-11-18Ho instantiation (#1204)Andrew Reynolds
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
2017-11-13Implement enumerator for functions. (#1243)Andrew Reynolds
2017-11-01(Move-only) Split quant util (#1306)Andrew Reynolds
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
2017-10-28(Move only) Move enumerative instantiation strategy to its own file and docum...Andrew Reynolds
2017-10-28Sygus process conjecture (#1286)Andrew Reynolds
2017-10-27Modify LDFLAGS to support shared libraries for Win (#1280)Andres Noetzli
2017-10-24Removing deprecated file. (#1270)Andrew Reynolds
2017-10-09Add skeleton of the FP theory solver (#1130)Martin
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-03Move sygus grammar utilities to separate file. (#1184)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Move BvInverter class into separate file. (#1173)Mathias Preiner
2017-09-19Add FP type enumerator and cardinality computer (#1104)Martin
2017-08-30Use thread_local instead of compiler extensions (#210)Andres Noetzli
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
2017-08-14Build and test suite fixes for Windows (#186)Mark Laws
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Remove unused stacking_vector class (#185)Andres Noetzli
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-03-27Moving the CareGraph into its own file.Tim King
2017-03-27Moving the theory::Assertion struct into its own file.Tim King
2017-03-26Alphabetizing libcvc4_la_SOURCES.Tim King
2017-03-17better support for proof production when encountering bool terms: handle the ...guykatzz
2017-03-02Minor cleanup and reorganization related to last commit.ajreynol
2016-10-26Fix typo in Makefile that makes distcheck failAndres Notzli
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-20Refactor, separate theory-specific counterexample-guided instantiation.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback