summaryrefslogtreecommitdiff
path: root/src/smt/dump.cpp
AgeCommit message (Collapse)Author
2019-06-11Disable dumping regression for non-dumping builds (#3046)Andres Noetzli
`let_shadowing.smt2` uses dumping to test our printing infrastructure. Since some builds do not support dumping, this commit disables that regression for non-dumping builds. Additionally, it enables an error message when trying to dump with a muzzled build and corrects the output of `--show-config` to indicate that muzzled builds cannot dump. Previously, the dumping output of a muzzled build was just silently empty. Most of the changes in `dump.cpp` are due to reformatting.
2019-03-26Update copyright headers.Aina Niemetz
2018-10-01 Fix dumping pre/post preprocessing passes (#2469)Andres Noetzli
This commit changes the hard-coded list of checks for preprocessing-related dump tags to take advantage of the new preprocessing pass registration mechanism from PR #2468. It also fixes a typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()` and adds a list of available passes to the `--dump help` output.
2018-06-25Updated copyright headers.Aina Niemetz
2017-07-07Update copyright headers.Mathias Preiner
2017-03-06Adding support for bool-to-bvClark Barrett
Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass.
2016-12-05Added "dump=raw-benchmark" option for dumping all user commands exactly as ↵Clark Barrett
received.
2016-08-19Fixed two bugsClark Barrett
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-17fix for windows buildsKshitij Bansal
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ↵Tim King
Breaking an edge between the sat solver and command.h.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback