projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
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 Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-16
Aina Niemetz
BV: Fix querying equality status in lazy bit-blaster...
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for BITVECTOR_REPEAT_OP...
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for INT_TO_BITVECTOR. (...
tree
|
commitdiff
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
tree
|
commitdiff
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
tree
|
commitdiff
2020-04-10
Andrew Reynolds
Towards proper use of resource managers (#4233)
tree
|
commitdiff
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andres Noetzli
Fix -Wshadow warnings in common headers (#3826)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Fix regression (#3827)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Fix node arity issue in reduction of int2bv (#3777)
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
tree
|
commitdiff
2020-01-10
Mathias Preiner
Fix enum names in AIG bitblaster. (#3599)
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-11
Andres Noetzli
Add support for UBSan instrumentation (#3382)
tree
|
commitdiff
2019-10-08
Piotr Trojanek
pass parameters by reference where it affects performance
tree
|
commitdiff
2019-09-29
Andres Noetzli
Introduce template classes for simple type rules (...
tree
|
commitdiff
2019-07-29
yoni206
Refactoring of bit-vector elimination rules (#3105)
tree
|
commitdiff
2019-05-18
Andres Noetzli
Fix BV ITE rewrite (#3004)
tree
|
commitdiff
2019-05-15
Andres Noetzli
Fix model of Boolean vars with eager bit-blaster (...
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-01
Andres Noetzli
Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-24
Aina Niemetz
BV: Fix typerules for rotate operators. (#2895)
tree
|
commitdiff
2019-01-19
Andres Noetzli
Fix missing-override warning (#2811)
tree
|
commitdiff
2019-01-18
Andres Noetzli
Fix ABC build (#2808)
tree
|
commitdiff
2019-01-14
Alex Ozdemir
ClausalBitvectorProof (#2786)
tree
|
commitdiff
2018-12-20
Aina Niemetz
Clean up BV kinds and type rules. (#2766)
tree
|
commitdiff
2018-12-20
Aina Niemetz
Add missing type rules for parameterized operator kinds...
tree
|
commitdiff
2018-12-13
Aina Niemetz
Fix compiler warnings. (#2748)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
tree
|
commitdiff
2018-12-03
Alex Ozdemir
Bit vector proof superclass (#2599)
tree
|
commitdiff
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp with special...
tree
|
commitdiff
2018-10-20
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X...
tree
|
commitdiff
2018-10-17
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O...
tree
|
commitdiff
2018-10-16
Aina Niemetz
BV rewrites (mined): Rule 35: Generalized ConcatPullUp...
tree
|
commitdiff
2018-10-16
Aina Niemetz
BV rewrites (mined): Rule 35: Generalized ConcatPullUp...
tree
|
commitdiff
2018-10-16
Aina Niemetz
BV rewrites (mined): Rule 35: Generalized ConcatPullUp...
tree
|
commitdiff
2018-10-16
Aina Niemetz
BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A...
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Remove unused CMakeLists.txt
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
tree
|
commitdiff
2018-08-27
Mathias Preiner
Use std:unique_ptr instead of raw pointers in theory...
tree
|
commitdiff
2018-08-21
Tim King
Add constexpr annotations to help coverity understand...
tree
|
commitdiff
2018-08-16
Andres Noetzli
Move node algorithms to separate file (#2311)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
tree
|
commitdiff
2018-08-07
Aina Niemetz
Add 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 Niemetz
Add rewrite for BITVECTOR_ITE with const children....
tree
|
commitdiff
2018-08-03
Aina Niemetz
Add 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 Niemetz
Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...
tree
|
commitdiff
2018-08-01
Andrew Reynolds
Fix issues with bv2nat (#2219)
tree
|
commitdiff
2018-08-01
Mathias Preiner
Remove hasAssertions() method from eager BV solver...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-06
Andrew Reynolds
Split ext theory to own file and document (#1809)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-21
Andres Noetzli
Fix warnings and enable -Wnon-virtual-dtor warning...
tree
|
commitdiff
2018-06-07
Aina Niemetz
Remove invalid assertion (#1993). (#2057)
tree
|
commitdiff
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
tree
|
commitdiff
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
tree
|
commitdiff
2018-05-30
Mathias Preiner
Normalize negated bit-vector terms over equalities...
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Add notions of evaluated kinds in TheoryModel (#1947)
tree
|
commitdiff
2018-05-10
Aina Niemetz
Refactored BVAckermann preprocessing pass. (#1889)
tree
|
commitdiff
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
tree
|
commitdiff
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
tree
|
commitdiff
2018-04-20
yoni206
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
tree
|
commitdiff
2018-04-14
Andres Noetzli
Fix use-after-free in eager bitblaster (#1772)
tree
|
commitdiff
2018-04-11
Aina Niemetz
Refactored BVGauss preprocessing pass. (#1766)
tree
|
commitdiff
2018-04-05
Mathias Preiner
Add more general SignExtendUltConst rewriting. (#1385)
tree
|
commitdiff
2018-04-02
Mathias Preiner
Reorganize bitblaster code. (#1695)
tree
|
commitdiff
2018-03-20
Mathias Preiner
Add support for CaDiCaL as eager BV SAT solver. (#1675)
tree
|
commitdiff
2018-03-09
Aina Niemetz
Some minor cleanup in bv::utils. (#1663)
tree
|
commitdiff
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
tree
|
commitdiff
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
tree
|
commitdiff
2018-02-24
Andres Noetzli
Add unit tests for BitVector, minor BV rewrite fix...
tree
|
commitdiff
2018-02-20
Aina Niemetz
Improve documentation of bv::utils::isCoreTerm (#1617)
tree
|
commitdiff
2018-02-20
Aina Niemetz
Moved and simplified bv::utils::intersect. (#1614)
tree
|
commitdiff
2018-02-20
Aina Niemetz
Unrecursified and merged bv::utils::is(Core|Equality...
tree
|
commitdiff
2018-02-17
Aina Niemetz
bv::utils::mk(And|Or) Do not return true if size of...
tree
|
commitdiff
2018-02-16
Aina Niemetz
Removed bv::utils::mkConjunction (redundant). (#1610)
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Fix corner case for rewrite of mult by pow 2 (#1601)
tree
|
commitdiff
2018-02-14
Andres Noetzli
Remove unused cd_set_collection.h (#1606)
tree
|
commitdiff
2018-02-13
Aina Niemetz
Moved (unrecursified) bv::utils::collectVars. (#1602)
tree
|
commitdiff
2018-02-11
Aina Niemetz
Move (unrecursified) bv::utils::numNodes to lazy_bitbla...
tree
|
commitdiff
2018-02-10
Aina Niemetz
Move BitVector specific funs from bv::utils to util...
tree
|
commitdiff
2018-02-10
Aina Niemetz
Remove mkNode from bv::utils (#1587)
tree
|
commitdiff
2018-02-09
Tim King
Removing an always true comparison (unsigned) >= 0u...
tree
|
commitdiff
2018-02-08
Aina Niemetz
Clean up bv utils (part one). (#1580)
tree
|
commitdiff
next