summaryrefslogtreecommitdiff
path: root/src/Makefile.am
AgeCommit message (Expand)Author
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
2015-11-03Adding a test to ensure the <build>/src/theory directory is available to the ...Tim King
2015-10-27Adding the new mkdirs script to EXTRA_DIST. This should fix the failing night...Tim King
2015-10-26This commit removes using absolute paths in the generation of the .subdirs fi...Tim King
2015-10-22Enable counterexample-guided quantifier instantiation by default for quantifi...ajreynol
2015-09-09Working towards a fair enumerator for codatatypes.ajreynol
2015-08-12Improvements to --macros-quant. Enable --clause-split by default. Bug fix for...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-29Module to infer alpha equivalence of quantified formulas. Minor clean up of ...ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other refactor...ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback