summaryrefslogtreecommitdiff
path: root/src/Makefile.am
AgeCommit message (Expand)Author
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
2016-03-23squash-merge from proof branchGuy
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2016-02-24Unifying the definitions of ClauseId to a single source of truth.Tim King
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of re...ajreynol
2016-02-09- extend cvc4 frontend parser to accept relational operators (product,PaulMeng
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-02-01Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build p...Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Removing dead code. StackingMap only appeared in unit tests.Tim King
2016-01-05Add SmtGlobals ClassTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-01More work on --cegqi-si-partial, incomplete.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback