summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2014-06-21Sets kinds documentationMorgan Deters
2014-06-21fixed build failurelianah
2014-06-20Implement RecordProperties::mkGroundTerm(). Resolves bug #546.Morgan Deters
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19Fix GLPK builds: correct access specifier on cut classes.Morgan Deters
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-19Fix for pre-C++11 is_sorted().Morgan Deters
2014-06-19Final preparations for arithmetic for building with libc++.Morgan Deters
2014-06-19This commit adds a priority queue implementation. This is to avoid compilati...Tim King
2014-06-19Fix rewriter typo.Morgan Deters
2014-06-19Clean up glpk detection a little, fix a detection bug.Morgan Deters
2014-06-19Fix compile errors with some versions of GCC.Morgan Deters
2014-06-19dos2unix-convert some sources.Morgan Deters
2014-06-19Minor fixes, spelling etc.Morgan Deters
2014-06-19More proof support for CASC : include skolemizationajreynol
2014-06-15core solver fixlianah
2014-06-15fixed bv bug due to applying equisatisfiable transformations in ppRewritelianah
2014-06-15fixed fuzzer assertion failures for bvlianah
2014-06-14added rewriting to bv-pow2 passlianah
2014-06-14Evil bitvector preprocessing pass for simplifying powers of two.lianah
2014-06-14bv static learning and rewrites for power of 2 termslianah
2014-06-14more bv rewriteslianah
2014-06-14fix to inequality rewritelianah
2014-06-14added bv inequality rewritelianah
2014-06-14added bv inequality lemmasLiana Hadarean
2014-06-14Fix for fmf with large finite cardinalities.ajreynol
2014-06-12Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2014-06-12fixing bv inequality solver explanation buglianah
2014-06-12added bvcomp case to bv to bool liftinglianah
2014-06-11added optionException for trying to use abc in an non-abc buildlianah
2014-06-11switched bv equality orderlianah
2014-06-11Merge pull request #31 from kbansal/setsKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-06-11sets: comment out an assertion too strongKshitij Bansal
2014-06-11user/sat context issue in setsKshitij Bansal
2014-06-11fix in sets rewriterKshitij Bansal
2014-06-11fixing bv ackermanization cache buglianah
2014-06-10Merging Tim's pseudoboolean work from his fmcad14 branch.Tim King
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-06-06Merge pull request #28 from kbansal/setsKshitij Bansal
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-06-06sets: fix equality propagationKshitij Bansal
2014-06-03Support E-matching/QCF for Set operators.ajreynol
2014-05-30Bug fix for string-opt2 (copied from Tianyi's branch).Morgan Deters
2014-05-30Improve --dt-stc-ind for multi-variable datatype properties.ajreynol
2014-05-30Fixes for --inst-max-levelajreynol
2014-05-28Minor changes to script. Disable cbqi sat.ajreynol
2014-05-27Improved type-checking for tuple and record selects.Morgan Deters
2014-05-26Fix bug 567Kshitij Bansal
2014-05-26Fixing Tim's subtype/solving bug for arraysClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback