summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2014-06-18Options script fix.Morgan Deters
2014-06-18Fix for mac readline.Morgan Deters
2014-06-18Better error for invalid concrete syntax of sorts with too many parens, like ...Morgan Deters
2014-06-18Fix GLPK builds: correct access specifier on cut classes.Morgan Deters
2014-06-17Java bindings fixes.Morgan Deters
2014-06-17disable unate lemmas when using incremental modeKshitij Bansal
2014-06-17Fix for pre-C++11 is_sorted().Morgan Deters
2014-06-17More minor code cleanup.Morgan Deters
2014-06-17New translator features: expand define-funs and combine assertions.Morgan Deters
2014-06-17Merge pull request #33 from mdeters/arith-proposalTim King
2014-06-17Code cleanup.Morgan Deters
2014-06-17Another fix for the CASC stuff.Morgan Deters
2014-06-17Final preparations for arithmetic for building with libc++.Morgan Deters
2014-06-17Fix for new CASC features, fixes Java builds.Morgan Deters
2014-06-17Some reversions of recent commits re: portfolio failure.Morgan Deters
2014-06-17This commit adds a priority queue implementation. This is to avoid compilati...Tim King
2014-06-17For casc : print models of functions rewritten by sort inference.ajreynol
2014-06-17Fix rewriter typo.Morgan Deters
2014-06-16Clean up glpk detection a little, fix a detection bug.Morgan Deters
2014-06-16More application-track fixes for use with trace executor.Morgan Deters
2014-06-16Some fixes for tear-down-incremental and "success" output.Morgan Deters
2014-06-16Disallow context-dependent copy/assignment.Morgan Deters
2014-06-16Fix compile errors with some versions of GCC.Morgan Deters
2014-06-16Clean up some compiler warnings on 32-bit.Morgan Deters
2014-06-16get-glpk-cut-log script, and configure code.Morgan Deters
2014-06-16dos2unix-convert some sources.Morgan Deters
2014-06-16Minor fixes, spelling etc.Morgan Deters
2014-06-16More proof support for CASC : include skolemizationajreynol
2014-06-15core solver fixlianah
2014-06-15Careful there aren't too many "success" messages with --tear-down-incremental...Morgan Deters
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-13fixed BVMinisat bug due to not clearing seen properlylianah
2014-06-13Fix handling of ALIA.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-11Flush output stream after result printed in portfolio.Morgan Deters
2014-06-11Fix for competition mode + parallel.Morgan Deters
2014-06-11switched bv equality orderlianah
2014-06-11Fix an omission in bv sources.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback