summaryrefslogtreecommitdiff
path: root/src/Makefile.am
AgeCommit message (Expand)Author
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
2016-06-23Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.Clark Barrett
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-04-20update from the masterPaulMeng
2016-04-19Refactored codePaulMeng
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ...ajreynol
2016-03-28Implement equality inference module for arithmetic terms. Optimization for e...ajreynol
2016-03-24Refactored the equality engine in order to remove theory-specific logic from ...Guy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback