projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Properly set up equality engine for BV bitblast solver. (#5905)
[cvc5.git]
/
src
/
theory
/
bv
/
theory_bv.cpp
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-11-05
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-17
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-16
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-11
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-10
Kshitij Bansal
Merge remote-tracking branch 'origin/1.4.x'
blob
|
commitdiff
|
raw
2014-10-09
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-10-02
Morgan Deters
Merge branch '1.4.x'.
blob
|
commitdiff
|
raw
2014-09-30
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-09-27
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-09-26
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-09-17
Kshitij Bansal
Merge branch '1.4.x' while ignoring commit 8d5eb49.
blob
|
commitdiff
|
raw
2014-09-17
Kshitij Bansal
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
2014-09-03
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
blob
|
commitdiff
|
raw
2014-09-03
Kshitij Bansal
check() optimization
blob
|
commitdiff
|
raw
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-19
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-19
lianah
Making getEqualityStatus more powerful for bit-vector...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-10
Kshitij Bansal
Merge remote-tracking branch 'origin/master' into segfa...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Update copyrights.
blob
|
commitdiff
|
raw
|
diff to current
2014-06-26
Morgan Deters
Merge tag 'smtcomp2014-resubmission'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-22
Morgan Deters
Merge tag 'smtcomp2014-application'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
lianah
fixed merge conflict
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
lianah
added model generation to eager bit-blasting and turned...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-16
lianah
fixed bv bug due to applying equisatisfiable transforma...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-15
lianah
Evil bitvector preprocessing pass for simplifying power...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-15
lianah
bv static learning and rewrites for power of 2 terms
blob
|
commitdiff
|
raw
|
diff to current
2014-06-14
lianah
more bv rewrites
blob
|
commitdiff
|
raw
|
diff to current
2014-06-14
lianah
fixed merge
blob
|
commitdiff
|
raw
|
diff to current
2014-06-14
lianah
added bv inequality rewrite
blob
|
commitdiff
|
raw
|
diff to current
2014-06-11
Kshitij Bansal
Merge pull request #31 from kbansal/sets
blob
|
commitdiff
|
raw
|
diff to current
2014-06-11
lianah
fixing bv ackermanization cache bug
blob
|
commitdiff
|
raw
|
diff to current
2014-06-10
lianah
Merging CAV14 paper bit-vector work.
blob
|
commitdiff
|
raw
|
diff to current
2014-04-06
Tim King
Merge pull request #21 from pcc/ite-fix
blob
|
commitdiff
|
raw
|
diff to current
2014-04-01
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-26
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-21
Kshitij Bansal
Merge pull request #22 from kbansal/sets-model
blob
|
commitdiff
|
raw
|
diff to current
2014-03-19
Martin Brain
Refactor the theory specific parts of definition expans...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-19
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-27
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-22
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-01-22
Morgan Deters
Delay QuantifiersEngine and UF strong solver initializa...
blob
|
commitdiff
|
raw
|
diff to current
2013-12-05
Morgan Deters
Update copyrights, add missing file-level documentation...
blob
|
commitdiff
|
raw
|
diff to current
2013-12-03
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-11-27
Morgan Deters
General pre-release cleanup commit
blob
|
commitdiff
|
raw
|
diff to current
2013-11-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-11-04
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-10-07
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-09-30
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-08-26
Kshitij Bansal
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-07-22
Andrew Reynolds
Bug fix for --fmf-fmc for non-uninterpreted sort quanti...
blob
|
commitdiff
|
raw
|
diff to current
2013-07-16
Liana Hadarean
fixed seg fault when bv equality is turned off
blob
|
commitdiff
|
raw
|
diff to current
2013-06-25
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-19
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-06-04
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-29
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-21
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-21
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-20
Morgan Deters
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-14
lianah
added some extra options to the bit-vector theory
blob
|
commitdiff
|
raw
|
diff to current
2013-05-03
lianah
changed the shifting bit-blasting to potentially be...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-03
Tim King
Merging branch 'soiquickexplain'.
blob
|
commitdiff
|
raw
|
diff to current
2013-05-03
Tim King
Merge branch 'fcexplanations'
blob
|
commitdiff
|
raw
|
diff to current
2013-05-02
lianah
merged master
blob
|
commitdiff
|
raw
|
diff to current
2013-05-02
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-05-01
lianah
removed tracing code causing slowdown; cleaned up some...
blob
|
commitdiff
|
raw
|
diff to current
2013-05-01
lianah
added back BitwiseEq rule
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
fixed merge conflicts
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
merged cvc4 master
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
added several rewrite rules (BitwiseSlicing, Ule/SleEli...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
added bvule, bvsle operator elimination rulesl; added...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
added some bv rewrite rules
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
finished implementing bv to bool lifting and added...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-30
lianah
added several rewrite rules (BitwiseSlicing, Ule/SleEli...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-29
Kshitij Bansal
Merge pull request #9 from kbansal/master
blob
|
commitdiff
|
raw
|
diff to current
2013-04-26
Kshitij Bansal
Merge experimental decisionweight branch
blob
|
commitdiff
|
raw
|
diff to current
2013-04-25
lianah
added bvule, bvsle operator elimination rulesl; added...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-21
lianah
added some bv rewrite rules
blob
|
commitdiff
|
raw
|
diff to current
2013-04-18
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-04-12
lianah
finished implementing bv to bool lifting and added...
blob
|
commitdiff
|
raw
|
diff to current
2013-04-03
Dejan Jovanović
* changing the bitblast-eager to bitblast on pre-register
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
Regenerated copyrights: canonicalized names, no emails
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
update copyrights
blob
|
commitdiff
|
raw
|
diff to current
2013-03-29
Dejan Jovanović
Merge branch 'master' of github.com:CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2013-03-27
lianah
reverted the core solver to do static slicing, added...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-27
lianah
Merge branch 'master' into bv-core
blob
|
commitdiff
|
raw
|
diff to current
2013-03-27
lianah
fixed model generation bug; commented out attempt...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-27
lianah
added model generation for bv subtheories and bv-inequa...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-26
Dejan Jovanović
getModelValue implementation in bitvectors
blob
|
commitdiff
|
raw
|
diff to current
2013-03-26
lianah
fixed inequality bugs due to improper explanation
blob
|
commitdiff
|
raw
|
diff to current
next