summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2013-05-07fix for bug500Dejan Jovanović
2013-05-03Fixing compilation of unit tests. These problems were due to splitLemma() ↵Tim King
being pure virtual.
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
2013-05-01Adding a missing makefile to the dist (fixes distcheck)Morgan Deters
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-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-25Add ability to run different regression levels with "make check"Morgan Deters
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-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
2013-04-05Fix unit test (compile error) for new SatSolver interfaceMorgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Fixes for two bugs:Morgan Deters
* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both.
2013-04-01Adding tests for the previous commit.Tim King
2013-04-01Merging some cleanup work:Morgan Deters
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-04-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵Morgan Deters
previously-failing testcase.
2013-04-01fixed TheoryBool rewriter buglianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-21added regression test for constant evallianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-20added more testslianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ↵lianah
inequalities
2013-03-20Fix to bug 497: make justification heuristic's ITE cache context-dependent.Morgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-03-20one more ineq regressionLiana Hadarean
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not ↵Liana Hadarean
incremental); currently disabled though
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-03-16started work on the inequality bv subtheorylianah
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-02-26Merge branch '1.0.x'lianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-07Merge branch '1.0.x'Morgan Deters
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-04Merge branch '1.0.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback