Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-10-20 | Add substr, contains and equality rewrites (#2665) | Andres Noetzli | |
2018-10-20 | Disable dumping test for non-dumping builds (#2662) | Andres Noetzli | |
2018-10-20 | Travis: run examples and avoid building them twice (#2663) | Andres Noetzli | |
`make check` builds the examples but does not run them. This commit changes our Travis script to run the examples after building them and removes `makeExamples()` to avoid building them twice. | |||
2018-10-19 | BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. ↵ | Aina Niemetz | |
(#2647) Simplifications based on the special const is now delegated down, only the concat is pulled up. | |||
2018-10-19 | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special ↵ | Aina Niemetz | |
const. (#2647) | |||
2018-10-19 | Sygus streaming non-implied predicates (#2660) | Andrew Reynolds | |
2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
2018-10-19 | Fix util::Random for macOS builds (#2655) | Andres Noetzli | |
2018-10-19 | Add helper to detect length one string terms (#2654) | Andres Noetzli | |
This commit introduces a helper function to detect string terms that have exactly/at most length one. This is useful for a lot of rewrites because strings of at most length one are guaranteed to not overlap multiple components in a concatenation, which allows for more aggressive rewriting. This commit has been tested with --sygus-rr-synth-check for >1h on the string term grammar. | |||
2018-10-18 | Add OptionException handling during initialization (#2466) | Andres Noetzli | |
The initial motivation for this commit was that dump with an invalid tag was leading to a segfault. The reason for the segfault was as follows: 1. `api::Solver` creates an `ExprManager`, which is stored in a `unique_ptr` as a class member 2. The `api::Solver` tries to create an SmtEngine instance 3. The `SmtEnginePrivate` constructor subscribes to events in the NodeManager and starts registering option listeners 4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it registers and notifies the DumpModeListener which calls Dump::setDumpFromString, which fails with an `OptionException` due to the invalid tag 5. While propagating the exception through `api::Solver`, the `ExprManager` is deleted but the non-existent `SmtEnginePrivate` is still subscribed to its events and there are still option listeners registered. This leads to a segfault because the NodeManager tries to notify the `SmtEnginePrivate` about deleted nodes This commit fixes the issue by catching the `OptionException` in `SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the NodeManager events and deleting its option listener registrations before rethrowing the exception. In addition, it changes the `Options::registerAndNotify()` method to immediately delete a registration if notifying the registration resulted in an ``OptionException`` (otherwise only the `ListenerCollection` knows about the registration and complains about it in its destructor). Finally, the commit adds a simple regression test for invalid dump tags. | |||
2018-10-18 | cmake: Run regression level 2 for make check. (#2645) | Mathias Preiner | |
2018-10-18 | Non-implied mode for model cores (#2653) | Andrew Reynolds | |
2018-10-18 | Non-contributing find replace rewrite (#2652) | Andrew Reynolds | |
2018-10-18 | Improve reduction for str.to.int (#2636) | Andrew Reynolds | |
2018-10-18 | Introducing internal commands for SyGuS commands (#2627) | Haniel Barbosa | |
2018-10-18 | Constant length regular expression elimination (#2646) | Andrew Reynolds | |
2018-10-17 | Skip sygus-rr-synth-check regressions when ASAN on (#2651) | Andres Noetzli | |
This commit disables three regressions when using an ASAN build. The regressions are all leaking memory when invoking the subsolver (see issue #2649). Debugging the issue will take a while but is not very critical since this feature is currently only used by CVC4 developers but it prevents our nightly builds from going through. | |||
2018-10-17 | Show if ASAN build in --show-config (#2650) | Andres Noetzli | |
This commit extends `--show-config` to show whether the current build is an ASAN build or not. This is done by moving a detection that was previously done for the unit tests into base/configuration_private.h. In addition to being convenient, this allows us to easily exclude regression tests from ASAN builds. | |||
2018-10-17 | Sygus query generator (#2465) | Andrew Reynolds | |
2018-10-17 | Fix context-dependent for positive contains reduction (#2644) | Andrew Reynolds | |
2018-10-16 | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special ↵ | Aina Niemetz | |
const. (#2643) Match: `x_m | concat(y_my, 0_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)` Match: `x_m | concat(y_my, 1_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)` Match: `x_m | concat(y_my, ~0_n, z_mz)` Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)` On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s): ``` | CVC4-base | CVC4-concatpullup-or | BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] | totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 | ``` | |||
2018-10-16 | cmake: Add CxxTest include directory to unit test includes. (#2642) | Mathias Preiner | |
2018-10-16 | BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵ | Aina Niemetz | |
ones (#2596). | |||
2018-10-16 | BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵ | Aina Niemetz | |
1 (#2596). | |||
2018-10-16 | BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵ | Aina Niemetz | |
0 (#2596). | |||
2018-10-16 | BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596). | Aina Niemetz | |
2018-10-16 | Improve strings reductions including skolem caching for contains (#2641) | Andrew Reynolds | |
2018-10-16 | Improve reduction for int.to.str (#2629) | Andrew Reynolds | |
2018-10-16 | Option for shuffling condition pool in CegisUnif (#2587) | Haniel Barbosa | |
2018-10-15 | cmake: Generate git_versioninfo.cpp on build time. (#2640) | Mathias Preiner | |
2018-10-15 | Delay initialization of theory engine (#2621) | Andrew Reynolds | |
This implements solution number 2 for issue #2613. | |||
2018-10-15 | Add more (str.replace x y z) rewrites (#2628) | Andres Noetzli | |
2018-10-13 | Fix fp-bool.sy grammar and require symfpu (#2631) | Andres Noetzli | |
2018-10-12 | Reset input language for ExprMiner subsolver (#2624) | Andres Noetzli | |
2018-10-12 | Improvements to rewrite rules from inputs (#2625) | Andrew Reynolds | |
2018-10-12 | Add rewrites for str.replace in str.contains (#2623) | Andres Noetzli | |
This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`. | |||
2018-10-11 | Fix heuristic for string length approximation (#2622) | Andrew Reynolds | |
2018-10-11 | Refactor printing of parameterized operators in smt2 (#2609) | Andrew Reynolds | |
2018-10-11 | Improve reasoning about empty strings in rewriter (#2615) | Andres Noetzli | |
2018-10-11 | Fix partial operator elimination in sygus grammar normalization (#2620) | Andrew Reynolds | |
2018-10-11 | Fix string ext inference for rewrites that introduce negation (#2618) | Andrew Reynolds | |
2018-10-10 | Fix default setting of CegisUnif options (#2605) | Haniel Barbosa | |
2018-10-10 | cmake: Use gcovr instead lcov for coverage report generation. (#2617) | Mathias Preiner | |
2018-10-10 | Fix compiler warnings (#2602) | Andres Noetzli | |
2018-10-10 | Synthesize rewrite rules from inputs (#2608) | Andrew Reynolds | |
2018-10-10 | Fix cegis so that evaluation unfolding is not interleaved. (#2614) | Andrew Reynolds | |
2018-10-10 | Optimize regular expression elimination (#2612) | Andrew Reynolds | |
2018-10-10 | Add length-based rewrites for (str.substr _ _ _) (#2610) | Andres Noetzli | |
2018-10-09 | Support for basic actively-generated enumerators (#2606) | Andrew Reynolds | |
2018-10-09 | Random: support URNG interface (#2595) | Aina Niemetz | |
Use std::shuffle (with Random as the unified random generator) instead of std::random_shuffle for deterministic, reproducable random shuffling. |