summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Collapse)Author
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after ↵Morgan Deters
final options/logic are set.
2013-12-24Minor code cleanup.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-10-09fixed options::proof() segfaultlianah
2013-09-30merged goldenLiana Hadarean
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
Some new functionality in substitutions.h/cpp
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-22Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added ↵Andrew Reynolds
infrastructure to BV collectModelInfo in preparation for bug fix.
2013-07-16fixed seg fault when bv equality is turned offLiana Hadarean
2013-07-16fixed bug520Liana Hadarean
2013-07-16Minor bugfixes to model-buildingMorgan Deters
2013-05-14added some extra options to the bit-vector theorylianah
2013-05-07added type checking rule to check for bit-vector constants of size 0lianah
2013-05-07one more fix for rewriteslianah
2013-05-07fixed bv rewrite blow-uplianah
2013-05-06fixed bv rewrite rule bugLiana Hadarean
2013-05-03changed the shifting bit-blasting to potentially be more efficientlianah
2013-05-02* splitLemma to request atomsDejan Jovanović
* normalizing in bv before bitblasting
2013-05-02merged masterlianah
2013-05-01removed tracing code causing slowdown; cleaned up some codelianah
2013-05-01added back BitwiseEq rulelianah
2013-04-30fixed merge conflictslianah
2013-04-30merged cvc4 masterlianah
2013-04-30updated the author namelianah
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ↵lianah
ExtractSignExtend) and bvurem lemma
2013-04-30added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-30added some bv rewrite ruleslianah
2013-04-30innd examples are solved fast, but destruction assertion faillianah
2013-04-30fixed compile errorLiana Hadarean
2013-04-30uncompiling new bv to bool liftinglianah
2013-04-30finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-30more work on boolean liftingLiana Hadarean
2013-04-30started work on bv1 to boolean liftinglianah
2013-04-30updated the author namelianah
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ↵lianah
ExtractSignExtend) and bvurem lemma
2013-04-26Merge experimental decisionweight branchKshitij Bansal
None of these are enabled by default, so any performance impact counts as a bug Options added are: --decision-threshold=N :default 0 + ignore all nodes greater than threshold in first attempt to pick decision --decision-use-weight bool :default false + use the weight nodes (locally, by looking at children) to direct recursive search --decision-random-weight=N int :default 0 + assign random weights to nodes between 0 and N-1 (0: disable) --decision-weight-internal=HOW + computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) Squashed commit of the following: commit 0dbae066c19abde37092517b50f23255398539db Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Fri Apr 26 16:42:36 2013 -0400 contentless cleanup commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Apr 16 21:43:55 2013 -0400 bugfixes in usr1 auto weight computation commit 9f039cba805bfd722466734920e758d48ae3b23e Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Fri Mar 29 15:01:33 2013 -0400 DECISION_WEIGHT_INTERNAL_USR1 commit 744e16d514594e5f1c69b36473b03cf501d9b9d1 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Mar 27 11:05:43 2013 -0400 split theory and decision requests commit f379d8a821df31c74b42a7722e891abc5c944f16 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Mar 27 09:51:58 2013 -0400 fix potential bug with threshold commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Feb 27 20:29:38 2013 -0500 stat bv::weightComputationTimer commit 2ab97d063e221357d2bb017af4589105777fd5a3 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Sat Feb 23 17:02:43 2013 -0500 decision: option to auto compute weight of boolean structure commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Sat Feb 23 14:53:50 2013 -0500 decision: fix design to do partial explorations * make findSplitterRec and all related helper functions' return type trivalued, to be able to distinguish between "partial exploration" vs "done exploration but found nothing" * keep additional data structure to remember to what extent the partial exploration has been completed so not to repeat it. we can use this to make multiple passes on formula with arbritrary order of thresholds for exploration commit 0815991fc1b0f1d63f0e8124d4672d782e89d671 Author: lianah <lianahady@gmail.com> Date: Fri Feb 22 17:55:40 2013 -0500 added simple node weight computation for bv. commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Wed Feb 20 02:35:21 2013 -0500 --decision-use-weight, --decision-random-weight=N commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2 Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Feb 19 23:36:49 2013 -0500 decisionThreshold option commit ac3579a52e452e3118ce116ff1823d6c6885544b Author: Kshitij Bansal <kshitij@cs.nyu.edu> Date: Tue Feb 19 20:22:51 2013 -0500 DecisionWeightAttr
2013-04-25added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-21added some bv rewrite ruleslianah
2013-04-18Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-04-17innd examples are solved fast, but destruction assertion faillianah
2013-04-16fixed compile errorLiana Hadarean
2013-04-16uncompiling new bv to bool liftinglianah
2013-04-12finished implementing bv to bool lifting and added --bv-to-bool optionlianah
2013-04-11Fixes for getModelVal in bv theoryClark Barrett
2013-04-10fixed getModelValue to only query the value of leaves and evaluate more ↵lianah
complex bv terms
2013-04-10more work on boolean liftingLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback