projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Merge branch 'master' of github.com:tiliang/CVC4
2014-11-22
lianah
added number of resource units used as a stat
commit
|
commitdiff
|
tree
2014-11-18
Liana Hadarean
clear model cache in BVQuickCheck clearSolver() (fixes...
commit
|
commitdiff
|
tree
2014-11-18
lianah
All Minisat solve calls now return lbool (fixes bug...
commit
|
commitdiff
|
tree
2014-11-17
lianah
added command line option for extractArith bv rewrite
commit
|
commitdiff
|
tree
2014-11-17
Liana Hadarean
Resource-limiting work.
commit
|
commitdiff
|
tree
2014-10-23
lianah
Fixed inefficiency in bit-vector rewrite rule.
commit
|
commitdiff
|
tree
2014-10-14
lianah
fix for memory leak in BVQuickCheck
commit
|
commitdiff
|
tree
2014-08-28
lianah
fixing bug580 caused by bad bv inequality explanation
commit
|
commitdiff
|
tree
2014-08-28
lianah
fixing bug580 caused by bad bv inequality explanation
commit
|
commitdiff
|
tree
2014-08-19
lianah
Making getEqualityStatus more powerful for bit-vector...
commit
|
commitdiff
|
tree
2014-08-05
lianah
fixed bug575 for bv models
commit
|
commitdiff
|
tree
2014-08-05
lianah
fixed bug575 for bv models
commit
|
commitdiff
|
tree
2014-06-22
lianah
Merge pull request #39 from mdeters/bv-warnings
commit
|
commitdiff
|
tree
2014-06-22
lianah
Merge pull request #35 from mdeters/bv-kinds
commit
|
commitdiff
|
tree
2014-06-21
lianah
fixed build failure
commit
|
commitdiff
|
tree
2014-06-19
lianah
fixed merge conflict
commit
|
commitdiff
|
tree
2014-06-19
lianah
added model generation to eager bit-blasting and turned...
commit
|
commitdiff
|
tree
2014-06-19
lianah
update to abc install instructions
commit
|
commitdiff
|
tree
2014-06-16
lianah
core solver fix
commit
|
commitdiff
|
tree
2014-06-16
lianah
fixed bv bug due to applying equisatisfiable transformations...
commit
|
commitdiff
|
tree
2014-06-15
lianah
fixed fuzzer assertion failures for bv
commit
|
commitdiff
|
tree
2014-06-15
lianah
added rewriting to bv-pow2 pass
commit
|
commitdiff
|
tree
2014-06-15
lianah
Evil bitvector preprocessing pass for simplifying powers...
commit
|
commitdiff
|
tree
2014-06-15
lianah
bv static learning and rewrites for power of 2 terms
commit
|
commitdiff
|
tree
2014-06-14
lianah
more bv rewrites
commit
|
commitdiff
|
tree
2014-06-14
lianah
fix to inequality rewrite
commit
|
commitdiff
|
tree
2014-06-14
lianah
fixed merge
commit
|
commitdiff
|
tree
2014-06-14
lianah
added bv inequality rewrite
commit
|
commitdiff
|
tree
2014-06-14
Liana Hadarean
added bv inequality lemmas
commit
|
commitdiff
|
tree
2014-06-14
Liana Hadarean
added bv inequality lemmas
commit
|
commitdiff
|
tree
2014-06-13
lianah
fixed BVMinisat bug due to not clearing seen properly
commit
|
commitdiff
|
tree
2014-06-12
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2014-06-12
lianah
fixing bv inequality solver explanation bug
commit
|
commitdiff
|
tree
2014-06-12
lianah
added bvcomp case to bv to bool lifting
commit
|
commitdiff
|
tree
2014-06-12
lianah
added optionException for trying to use abc in an non...
commit
|
commitdiff
|
tree
2014-06-11
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2014-06-11
lianah
switched bv equality order
commit
|
commitdiff
|
tree
2014-06-11
lianah
fixed unit tests failures
commit
|
commitdiff
|
tree
2014-06-11
lianah
fixing bv ackermanization cache bug
commit
|
commitdiff
|
tree
2014-06-10
lianah
reverting portfolio hack
commit
|
commitdiff
|
tree
2014-06-10
lianah
Merging CAV14 paper bit-vector work.
commit
|
commitdiff
|
tree
2013-12-03
lianah
fixed rewriter bug where postRewrite was not caching...
commit
|
commitdiff
|
tree
2013-11-06
lianah
fixed proof regression script and added a new uf test...
commit
|
commitdiff
|
tree
2013-11-04
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2013-10-09
lianah
fixed options::proof() segfault
commit
|
commitdiff
|
tree
2013-10-09
lianah
cleaned up proof code
commit
|
commitdiff
|
tree
2013-10-09
lianah
fixed uf proof bug: now storing deleted theory lemmas
commit
|
commitdiff
|
tree
2013-10-08
lianah
added currying for uf proofs; still needs debugging
commit
|
commitdiff
|
tree
2013-10-08
lianah
fixed uf proof with holes bugs
commit
|
commitdiff
|
tree
2013-10-08
Liana Hadarean
fixed some bugs
commit
|
commitdiff
|
tree
2013-10-08
Liana Hadarean
first draft implementation of uf proofs with holes
commit
|
commitdiff
|
tree
2013-10-07
Liana Hadarean
merged golden
commit
|
commitdiff
|
tree
2013-09-30
Liana Hadarean
merged golden
commit
|
commitdiff
|
tree
2013-07-16
Liana Hadarean
fixed seg fault when bv equality is turned off
commit
|
commitdiff
|
tree
2013-07-16
Liana Hadarean
fixed bug520
commit
|
commitdiff
|
tree
2013-05-14
lianah
added some extra options to the bit-vector theory
commit
|
commitdiff
|
tree
2013-05-10
lianah
now proofs print mapping between atom and propositional...
commit
|
commitdiff
|
tree
2013-05-10
lianah
fixes to the proof system so it works with theory lemmas...
commit
|
commitdiff
|
tree
2013-05-07
lianah
added type checking rule to check for bit-vector constants...
commit
|
commitdiff
|
tree
2013-05-07
lianah
one more fix for rewrites
commit
|
commitdiff
|
tree
2013-05-07
lianah
fixed bv rewrite blow-up
commit
|
commitdiff
|
tree
2013-05-07
Liana Hadarean
fixed bv rewrite rule bug
commit
|
commitdiff
|
tree
2013-05-03
lianah
changed the shifting bit-blasting to potentially be...
commit
|
commitdiff
|
tree
2013-05-02
lianah
merged master
commit
|
commitdiff
|
tree
2013-05-02
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2013-05-01
lianah
removed tracing code causing slowdown; cleaned up some...
commit
|
commitdiff
|
tree
2013-05-01
lianah
added back BitwiseEq rule
commit
|
commitdiff
|
tree
2013-04-30
lianah
fixed merge conflicts
commit
|
commitdiff
|
tree
2013-04-30
lianah
merged cvc4 master
commit
|
commitdiff
|
tree
2013-04-30
lianah
updated the author name
commit
|
commitdiff
|
tree
2013-04-30
lianah
added several rewrite rules (BitwiseSlicing, Ule/SleEliminat...
commit
|
commitdiff
|
tree
2013-04-30
lianah
added bvule, bvsle operator elimination rulesl; added...
commit
|
commitdiff
|
tree
2013-04-30
lianah
added some bv rewrite rules
commit
|
commitdiff
|
tree
2013-04-30
lianah
innd examples are solved fast, but destruction assertion...
commit
|
commitdiff
|
tree
2013-04-30
Liana Hadarean
fixed compile error
commit
|
commitdiff
|
tree
2013-04-30
lianah
uncompiling new bv to bool lifting
commit
|
commitdiff
|
tree
2013-04-30
lianah
finished implementing bv to bool lifting and added...
commit
|
commitdiff
|
tree
2013-04-30
Liana Hadarean
more work on boolean lifting
commit
|
commitdiff
|
tree
2013-04-30
lianah
started work on bv1 to boolean lifting
commit
|
commitdiff
|
tree
2013-04-30
lianah
added support for dumping the SAT problem the sat solver...
commit
|
commitdiff
|
tree
2013-04-30
lianah
updated the author name
commit
|
commitdiff
|
tree
2013-04-30
lianah
added several rewrite rules (BitwiseSlicing, Ule/SleEliminat...
commit
|
commitdiff
|
tree
2013-04-25
lianah
added bvule, bvsle operator elimination rulesl; added...
commit
|
commitdiff
|
tree
2013-04-21
lianah
added some bv rewrite rules
commit
|
commitdiff
|
tree
2013-04-18
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2013-04-18
lianah
making sure sat context is zero when user context is...
commit
|
commitdiff
|
tree
2013-04-18
lianah
fixing destruction order in SmtEngine
commit
|
commitdiff
|
tree
2013-04-17
lianah
innd examples are solved fast, but destruction assertion...
commit
|
commitdiff
|
tree
2013-04-16
Liana Hadarean
fixed compile error
commit
|
commitdiff
|
tree
2013-04-16
lianah
uncompiling new bv to bool lifting
commit
|
commitdiff
|
tree
2013-04-12
lianah
finished implementing bv to bool lifting and added...
commit
|
commitdiff
|
tree
2013-04-11
lianah
fixed getModelValue to only query the value of leaves...
commit
|
commitdiff
|
tree
2013-04-10
Liana Hadarean
more work on boolean lifting
commit
|
commitdiff
|
tree
2013-04-10
lianah
started work on bv1 to boolean lifting
commit
|
commitdiff
|
tree
2013-04-08
lianah
added support for dumping the SAT problem the sat solver...
commit
|
commitdiff
|
tree
2013-04-03
Liana Hadarean
updated NEWS to include inequality solver
commit
|
commitdiff
|
tree
2013-04-01
lianah
fixed TheoryBool rewriter bug
commit
|
commitdiff
|
tree
2013-04-01
lianah
fixed bug 502; now the core bv solver only gives the...
commit
|
commitdiff
|
tree
2013-03-31
Liana Hadarean
changed option to run inequality solver by default
commit
|
commitdiff
|
tree
2013-03-27
lianah
reverted the core solver to do static slicing, added...
commit
|
commitdiff
|
tree
next