projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Statistics on instantiations per quantified formula. (#4719)
[cvc5.git] / src / theory / bv /
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-07 Andrew ReynoldsTransfer ownership of internal Options from NodeManager... tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-16 Aina NiemetzBV: Fix querying equality status in lazy bit-blaster... tree | commitdiff
2020-06-15 Aina NiemetzBV: Add missing type check for BITVECTOR_REPEAT_OP... tree | commitdiff
2020-06-15 Aina NiemetzBV: Add missing type check for INT_TO_BITVECTOR. (... tree | commitdiff
2020-05-22 Aina NiemetzAdd support for SAT solver Kissat. (#4514) tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-19 Andres NoetzliMake SolveEq and PlusCombineLikeTerms idempotent (... tree | commitdiff
2020-04-10 Andrew ReynoldsTowards proper use of resource managers (#4233) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-26 Andrew ReynoldsFix regression (#3827) tree | commitdiff
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... tree | commitdiff
2020-01-10 Mathias PreinerFix enum names in AIG bitblaster. (#3599) tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-11 Andres NoetzliAdd support for UBSan instrumentation (#3382) tree | commitdiff
2019-10-08 Piotr Trojanekpass parameters by reference where it affects performance tree | commitdiff
2019-09-29 Andres NoetzliIntroduce template classes for simple type rules (... tree | commitdiff
2019-07-29 yoni206Refactoring of bit-vector elimination rules (#3105) tree | commitdiff
2019-05-18 Andres NoetzliFix BV ITE rewrite (#3004) tree | commitdiff
2019-05-15 Andres NoetzliFix model of Boolean vars with eager bit-blaster (... tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-01 Andres NoetzliFix RewriteITEBv to ensure rewrite to fixpoint (#2878) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-24 Aina NiemetzBV: Fix typerules for rotate operators. (#2895) tree | commitdiff
2019-01-19 Andres NoetzliFix missing-override warning (#2811) tree | commitdiff
2019-01-18 Andres Noetzli Fix ABC build (#2808) tree | commitdiff
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786) tree | commitdiff
2018-12-20 Aina NiemetzClean up BV kinds and type rules. (#2766) tree | commitdiff
2018-12-20 Aina NiemetzAdd missing type rules for parameterized operator kinds... tree | commitdiff
2018-12-13 Aina NiemetzFix compiler warnings. (#2748) tree | commitdiff
2018-12-10 makaimannBoolToBV modes (off, ite, all) (#2530) tree | commitdiff
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733) tree | commitdiff
2018-12-03 Alex OzdemirBit vector proof superclass (#2599) tree | commitdiff
2018-10-20 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp with special... tree | commitdiff
2018-10-20 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X... tree | commitdiff
2018-10-17 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: Generalized ConcatPullUp... tree | commitdiff
2018-10-16 Aina NiemetzBV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A... tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-11 Andrew ReynoldsSupport model cores via option --produce-model-cores... tree | commitdiff
2018-08-27 Mathias PreinerUse std:unique_ptr instead of raw pointers in theory... tree | commitdiff
2018-08-21 Tim KingAdd constexpr annotations to help coverity understand... tree | commitdiff
2018-08-16 Andres NoetzliMove node algorithms to separate file (#2311) tree | commitdiff
2018-08-08 Andres NoetzliRequire Swig 3 (#2283) tree | commitdiff
2018-08-07 Aina NiemetzAdd rewrite for nested BITVECTOR_ITE that can be merged... tree | commitdiff
2018-08-04 Aina Niemetz Add rewrite for nested BITVECTOR_ITE with cond_outer... tree | commitdiff
2018-08-04 Aina NiemetzAdd rewrite for BITVECTOR_ITE with const children.... tree | commitdiff
2018-08-03 Aina NiemetzAdd rewrite for BITVECTOR_ITE with term_then == term_el... tree | commitdiff
2018-08-03 Aina Niemetz Add timer for BV inequality solver. (#2265) tree | commitdiff
2018-08-02 Aina NiemetzAdd rewrites for BITVECTOR_ITE and BITVECTOR_COMP with... tree | commitdiff
2018-08-01 Andrew ReynoldsFix issues with bv2nat (#2219) tree | commitdiff
2018-08-01 Mathias PreinerRemove hasAssertions() method from eager BV solver... tree | commitdiff
2018-07-30 Mathias PreinerAdd support for incremental eager bit-blasting. (#1838) tree | commitdiff
2018-07-06 Andrew ReynoldsSplit ext theory to own file and document (#1809) tree | commitdiff
2018-06-25 Aina NiemetzUpdated copyright headers. tree | commitdiff
2018-06-21 Andres NoetzliFix warnings and enable -Wnon-virtual-dtor warning... tree | commitdiff
2018-06-07 Aina NiemetzRemove invalid assertion (#1993). (#2057) tree | commitdiff
2018-06-02 Mathias PreinerFix BV-abstraction check to consider SKOLEM. (#2042) tree | commitdiff
2018-05-31 Mathias PreinerFix bv-abstraction check for AND with non bit-vector... tree | commitdiff
2018-05-30 Mathias PreinerNormalize negated bit-vector terms over equalities... tree | commitdiff
2018-05-23 Andrew ReynoldsAdd notions of evaluated kinds in TheoryModel (#1947) tree | commitdiff
2018-05-10 Aina NiemetzRefactored BVAckermann preprocessing pass. (#1889) tree | commitdiff
2018-05-04 Mathias PreinerRefactor bv-intro-pow2 preprocessing pass. (#1851) tree | commitdiff
2018-04-25 yoni206Refactor bv-to-bool and bool-to-bv preprocessing passes... tree | commitdiff
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv... tree | commitdiff
2018-04-14 Andres NoetzliFix use-after-free in eager bitblaster (#1772) tree | commitdiff
2018-04-11 Aina NiemetzRefactored BVGauss preprocessing pass. (#1766) tree | commitdiff
2018-04-05 Mathias PreinerAdd more general SignExtendUltConst rewriting. (#1385) tree | commitdiff
2018-04-02 Mathias PreinerReorganize bitblaster code. (#1695) tree | commitdiff
2018-03-20 Mathias PreinerAdd support for CaDiCaL as eager BV SAT solver. (#1675) tree | commitdiff
2018-03-09 Aina NiemetzSome minor cleanup in bv::utils. (#1663) tree | commitdiff
2018-03-07 Mathias PreinerMake statistics output consistent. (#1647) tree | commitdiff
2018-03-05 Mathias PreinerEnable -Wsuggest-override by default. (#1643) tree | commitdiff
2018-02-24 Andres NoetzliAdd unit tests for BitVector, minor BV rewrite fix... tree | commitdiff
2018-02-20 Aina NiemetzImprove documentation of bv::utils::isCoreTerm (#1617) tree | commitdiff
2018-02-20 Aina NiemetzMoved and simplified bv::utils::intersect. (#1614) tree | commitdiff
2018-02-20 Aina NiemetzUnrecursified and merged bv::utils::is(Core|Equality... tree | commitdiff
2018-02-17 Aina Niemetzbv::utils::mk(And|Or) Do not return true if size of... tree | commitdiff
2018-02-16 Aina NiemetzRemoved bv::utils::mkConjunction (redundant). (#1610) tree | commitdiff
2018-02-15 Andrew ReynoldsFix corner case for rewrite of mult by pow 2 (#1601) tree | commitdiff
2018-02-14 Andres NoetzliRemove unused cd_set_collection.h (#1606) tree | commitdiff
2018-02-13 Aina NiemetzMoved (unrecursified) bv::utils::collectVars. (#1602) tree | commitdiff
2018-02-11 Aina NiemetzMove (unrecursified) bv::utils::numNodes to lazy_bitbla... tree | commitdiff
2018-02-10 Aina NiemetzMove BitVector specific funs from bv::utils to util... tree | commitdiff
2018-02-10 Aina NiemetzRemove mkNode from bv::utils (#1587) tree | commitdiff
2018-02-09 Tim KingRemoving an always true comparison (unsigned) >= 0u... tree | commitdiff
2018-02-08 Aina NiemetzClean up bv utils (part one). (#1580) tree | commitdiff
next