summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2013-05-03changed the shifting bit-blasting to potentially be more efficientlianah
2013-05-02merged masterlianah
2013-05-02Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-05-01Comment out some debug-related things in attribute code, no longer neededMorgan Deters
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan Deters
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
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-30added support for dumping the SAT problem the sat solver is working onlianah
2013-04-30updated the author namelianah
2013-04-30Add option in quantifiers for clause splittingAndrew Reynolds
2013-04-30added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ↵lianah
ExtractSignExtend) and bvurem lemma
2013-04-30add decision_attributes.h for make distKshitij Bansal
2013-04-29Some fixes for GCC 4.2, and for Java on MacMorgan Deters
2013-04-29Merge pull request #9 from kbansal/masterKshitij Bansal
Merge experimental decisionweight branch
2013-04-29Fixes to FCSimplex for some versions of compilersMorgan Deters
2013-04-28Fixing the failure for make distcheck.Tim King
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-26FCSimplex branch mergeTim King
2013-04-25added bvule, bvsle operator elimination rulesl; added bvurem lemma generationlianah
2013-04-23Theory "alternates" supportMorgan Deters
* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete.
2013-04-22add bit0 and bit1 constants to smt-lib v1 parserMorgan Deters
2013-04-21added some bv rewrite ruleslianah
2013-04-18Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-04-18making sure sat context is zero when user context is popped to 0 in ↵lianah
SmtEngine destructor
2013-04-18fixing destruction order in SmtEnginelianah
2013-04-17bool flatten: node num_children workaroundKshitij Bansal
2013-04-17innd examples are solved fast, but destruction assertion faillianah
2013-04-17boolean flatten: bug fix in dfs searchKshitij Bansal
(this is not intended to (and doesn't) address the issue with NodeBuilder limit)
2013-04-16boolean flatten rewrite: dont re-rewriteKshitij Bansal
2013-04-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
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-11Improved speed of no redundant lemma assertion by using hash setClark Barrett
2013-04-11Fixes for getModelVal in bv theoryClark Barrett
2013-04-11Added check for infinite lemma loopClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback