summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Collapse)Author
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2014-06-13fixed BVMinisat bug due to not clearing seen properlylianah
2014-06-10Merging CAV14 paper bit-vector work.lianah
2014-03-12Some standardization of regression Makefiles that got out of sync. Fixes ↵Morgan Deters
cases of nonterminating rewrite-rules regressions.
2014-03-11Minor cleanup.Morgan Deters
* Reenable parts of bvsimple test * Fix typo in #endif comment
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-09-18Support a personal build configuration and make rules.Morgan 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-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-21added regression test for constant evallianah
2013-03-20added more testslianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ↵lianah
inequalities
2013-03-20one more ineq regressionLiana Hadarean
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not ↵Liana Hadarean
incremental); currently disabled though
2013-03-16started work on the inequality bv subtheorylianah
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2012-11-13Testcases for fixed bugsClark Barrett
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-08added reduced bv model failing test caseLiana Hadarean
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions ↵Morgan Deters
should work now
2012-06-28Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2Clark Barrett
2012-06-14fix for clark's bugDejan Jovanović
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()
2012-06-13enabling regressions from last night, all fixedDejan Jovanović
2012-06-13!(*child_it).isConst() assertion failDejan Jovanović
this is delta minimal with the same assertion
2012-06-13r2.node == response.node failure Dejan Jovanović
2012-06-13!current[0].isConst() failureDejan Jovanović
2012-06-13benchmark to show that we don't rewrite bvsmod correctlyDejan Jovanović
the definition in smtlib was buggy and was changed on 2011-06-15 check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2
2012-06-12wrong answer for bvDejan Jovanović
2012-06-12bv reduced with decision: sat instead of unsatKshitij Bansal
2012-06-12wrong answer benchmarksDejan Jovanović
these should be simple constant propagation problems
2012-06-11another benchmark that used to fail Dejan Jovanović
2012-06-11fixing bitvector bugsDejan Jovanović
* clauses shouldn't be erased when they could be a reason for outside propagation * propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
2012-06-11failing bv examplesDejan Jovanović
2012-06-08very small fast example for the bv failDejan Jovanović
2012-06-08small fuzz examples where bv fails Dejan Jovanović
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ↵Dejan Jovanović
are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
This should also fix bug 325.
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ↵Morgan Deters
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
* modified BVMinisat to work incrementally * added more bv regressions
2012-02-20portfolio mergeMorgan Deters
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-05-02adding some previously-failing "bug" test cases for bitvectorsMorgan Deters
2011-05-02updating bv regressionsDejan Jovanović
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
* Fixed hole in arrays typechecking. * Fixed "make dist". * Better ouroborous test, and some printer fixes. * Continued cleanup in CVC parser, removed some warnings. * Better output.
2011-04-20Tuesday end-of-day commit.Morgan Deters
Expected performance impact outside of datatypes/CVC parser is negligible. * CVC language LAMBDA, functional LET, type LET, precedence fixes, bitvectors, and arrays, with partial parsing support also for quantifiers, tuples, subranges, subtypes, and records * support for complex recursive DATATYPE selectors, e.g. tree = node(children:ARRAY INT OF tree) | leaf(data:INT) these are complicated because they have to be left unresolved at parse time and dealt with in a second pass. * bugfix for Exprs/Types that occurred when setting them to null (not Nodes/TypeNodes, just Exprs/Types). * Cleanup/code review items
2011-04-18more work on CVC languageMorgan Deters
2011-04-11fix "make dist" issues in makefilesMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback