summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast_strategies.cpp
AgeCommit message (Collapse)Author
2014-06-10Merging CAV14 paper bit-vector work.lianah
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-05-03changed the shifting bit-blasting to potentially be more efficientlianah
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-02-14Removing BVDebug and replacing with Debug.Tim King
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
* added printing for total bit-vector division kinds for debugging purposes
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-10-23fixed TheoryBV collectModel info to check for shared terms; this seems to ↵Liana Hadarean
fix bug424
2012-10-19BV theory model fixLiana Hadarean
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-03implemented collectModelInfo for TheoryBVLiana Hadarean
2012-08-29* Numerous documentation fixes (fix doxygen warnings, add missing ↵Morgan Deters
documentation, etc.). * Remove sat_module.cpp, which was no longer used (was previously refactored?)
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
See below for details. * Fix the "assert" name-collision bug (resolves bug #364). Our identifiers should never be named "assert", as that's a preprocessor definition in <assert.h>, which is often #included indirectly (so simply having a policy of not including <assert.h> isn't good enough---one of our dependences might include it). It was once the case that we didn't have anything named "assert", but "assert()" has now crept back in. Instead, name things "assertFoo()" or similar. Thanks to Tim for the report. To fix this, I've changed some of Dejan's circuit-propagator code from "assert()" to "assertTrue()". Ditto for Andy's explanation manager. Guys, if you prefer a different name in your code, please change it. * Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365). Inner lets now shadow outer lets (previously, they incorrectly gave an error). Additionally, while looking at this, I found that a sequential let was implemented rather than a parallel let. This is now fixed. Thanks to Liana for the report. * Remove ANTLR parser generation warnings in CVC parser (resolves bug #314). * There were a lot of Debug lines in bitvectors that had embedded toString() calls. This wasted a LOT of time in debug builds for BV benchmarks (like in "make regress"). Added if(Debug.isOn(...)) guards; much faster now. * Support for building public-facing interface documentation only (as opposed to all internals documentation). Now "make doc" does the public-facing and "make doc-internals" does documentation of everything. (Along with changes to the nightly build script---which will now build and publish both types of Doxygen documentation---this resolves bug #359). * Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the report (a long long time ago--sorry). * The default output language for all streams is now based on the current set of Options (if there is one). This has been a constant annoyance, especially when stringstreams are used to construct output. However, it doesn't work for calls from outside the library, so it's mainly an annoyance-fixer for CVC4 library code itself. * Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that are used only in assertions-enabled builds (and thus give warnings in production builds). This was briefly discussed at the meeting this week.
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ↵Morgan Deters
\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-05-28Added some BV rewrites, fixed bugs in array theory, made ite simp work with BVClark Barrett
2012-05-15renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectivelyLiana Hadarean
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
* modified BVMinisat to work incrementally * added more bv regressions
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
* added simplification rewrites
2012-03-02CDMap -> CDHashMapDejan Jovanović
CDSet -> CDHashSet
2012-02-29This should fix the debian build fails:Liana Hadarean
* removed bvpicosat directory as it is currently not used Cleared some of the flurry of warnings my previous merge caused in src/prop/
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
* separated SatSolverInput interface class into two classes: - TheoryProxy for the sat solver to communicate with the theories - SatSolverInterface abstract class to communicate with the sat solver * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces Replaced TheoryBV with bitblasting implementation: * all operators bitblasted * only operator elimination rewrite rules so far
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback