summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-20Add substr, contains and equality rewrites (#2665)Andres Noetzli
2018-10-20Disable dumping test for non-dumping builds (#2662)Andres Noetzli
2018-10-20Travis: 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-19BV 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-19BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special ↵Aina Niemetz
const. (#2647)
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-19Fix util::Random for macOS builds (#2655)Andres Noetzli
2018-10-19Add 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-18Add 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-18cmake: Run regression level 2 for make check. (#2645)Mathias Preiner
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Non-contributing find replace rewrite (#2652)Andrew Reynolds
2018-10-18Improve reduction for str.to.int (#2636)Andrew Reynolds
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-18Constant 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-17Show 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-17Sygus query generator (#2465)Andrew Reynolds
2018-10-17 Fix context-dependent for positive contains reduction (#2644)Andrew Reynolds
2018-10-16BV 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-16cmake: Add CxxTest include directory to unit test includes. (#2642)Mathias Preiner
2018-10-16BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵Aina Niemetz
ones (#2596).
2018-10-16BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵Aina Niemetz
1 (#2596).
2018-10-16BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ↵Aina Niemetz
0 (#2596).
2018-10-16BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).Aina Niemetz
2018-10-16Improve strings reductions including skolem caching for contains (#2641)Andrew Reynolds
2018-10-16Improve reduction for int.to.str (#2629)Andrew Reynolds
2018-10-16Option for shuffling condition pool in CegisUnif (#2587)Haniel Barbosa
2018-10-15cmake: Generate git_versioninfo.cpp on build time. (#2640)Mathias Preiner
2018-10-15Delay initialization of theory engine (#2621)Andrew Reynolds
This implements solution number 2 for issue #2613.
2018-10-15Add more (str.replace x y z) rewrites (#2628)Andres Noetzli
2018-10-13Fix fp-bool.sy grammar and require symfpu (#2631)Andres Noetzli
2018-10-12Reset input language for ExprMiner subsolver (#2624)Andres Noetzli
2018-10-12Improvements 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-11Improve 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-10Fix default setting of CegisUnif options (#2605)Haniel Barbosa
2018-10-10cmake: Use gcovr instead lcov for coverage report generation. (#2617)Mathias Preiner
2018-10-10Fix compiler warnings (#2602)Andres Noetzli
2018-10-10Synthesize rewrite rules from inputs (#2608)Andrew Reynolds
2018-10-10Fix cegis so that evaluation unfolding is not interleaved. (#2614)Andrew Reynolds
2018-10-10Optimize regular expression elimination (#2612)Andrew Reynolds
2018-10-10Add length-based rewrites for (str.substr _ _ _) (#2610)Andres Noetzli
2018-10-09 Support for basic actively-generated enumerators (#2606)Andrew Reynolds
2018-10-09Random: 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback