summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
AgeCommit message (Collapse)Author
2017-03-28Fix bug 787.ajreynol
2017-03-28Fix for bug 733Clark Barrett
2017-03-24Add some regressions. Minor.ajreynol
2017-01-05Disabling a regression test that assumes CVC4 is configured with proofs on. ↵Tim King
Modifying the travis rules so there are instances with proofs disabled.
2016-12-16Fix dependency tracing for fewerPreprocessingHolesAndres Notzli
Previously, dependency tracing in `ite_removal.cpp` was only done with the `unsatCores` option but `fewerPreprocessingHoles` requires dependencies, too. This lead to errors during proof construction when `fewerPreprocessingHoles` was active. This commit fixes the condition and includes a test case that previously failed. Additionally, it fixes a similar issue in the theory engine. NOTE: this commit might not fix all instances of this problem. `smt_engine.cpp` turns certain flags off with `unsatCores`. Compatibility between those flags and `fewerPreprocessingHoles` needs to be checked separately.
2016-12-02Fix for bug 734Clark Barrett
2016-11-30Remove wrong `ExtractMultLeadingBit` ruleAndres Notzli
The rule `ExtractMultLeadingBit` estimated the number of leading zeros wrong: when there were ones in the leading constant parts of the factors, it was using the length of the non-zero part instead of the length of the zero part. This commit includes an example for which the previous version of the rule would cause a wrong answer.
2016-11-17Fix Makefiles in testAndres Notzli
With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-11-11Add simple inferences for extended bitvector functions, add a few related ↵ajreynol
options. Use bv2nat, int2bv as triggers. Add regressions.
2016-10-26Enable bv2nat regressionsajreynol
2016-10-21Move slow regress0 benchmarks to regress1, increment regress1 through regress3.ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback