projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
bv: Refactor getEqualityStatus and use for both bitblasting solvers. (#6933)
[cvc5.git] / src / theory / bv / bv_solver_bitblast.cpp
2021-07-27 Mathias Preinerbv: Refactor getEqualityStatus and use for both bitblas... blob | commitdiff | raw
2021-07-15 Mathias Preinerbv: Rename BBSimple to NodeBitblaster. (#6891) blob | commitdiff | raw | diff to current
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) blob | commitdiff | raw | diff to current
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... blob | commitdiff | raw | diff to current
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) blob | commitdiff | raw | diff to current
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) blob | commitdiff | raw | diff to current
2021-06-04 Mathias Preinerbv: Enable bitblast solver by default. (#6660) blob | commitdiff | raw | diff to current
2021-05-19 Mathias Preinerbv: Add support for --bitblast=eager. (#6516) blob | commitdiff | raw | diff to current
2021-05-14 Mathias Preinerbv: Assert input facts on user-level 0. (#6515) blob | commitdiff | raw | diff to current
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... blob | commitdiff | raw | diff to current
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909) blob | commitdiff | raw | diff to current
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... blob | commitdiff | raw | diff to current
2021-02-13 Mathias PreinerProperly set up equality engine for BV bitblast solver... blob | commitdiff | raw | diff to current
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... blob | commitdiff | raw | diff to current
2021-02-03 Mathias PreinerAdd BV solver bitblast. (#5851) blob | commitdiff | raw | diff to current