Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-10-18 | Merge branch 'master' into fixDumpfixDump | Andres Noetzli | |
2018-10-18 | update | Andres Noetzli | |
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 | Merge branch 'master' into fixDump | Andres Noetzli | |
2018-10-18 | fix typo | Andres Noetzli | |
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. | |||
2018-10-09 | Allow multiple synthesis conjectures. (#2593) | Andrew Reynolds | |
2018-10-08 | Fix compiler warnings. (#2601) | Aina Niemetz | |
2018-10-08 | BV instantiator: Factor out util functions. (#2604) | Aina Niemetz | |
Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this. | |||
2018-10-08 | BV inverter: Factor out util functions. (#2603) | Aina Niemetz | |
Previously, all invertibility condition functions were static functions in theory/quantifiers/bv_inverter.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/bv_inverter_utils.(cpp|h). | |||
2018-10-08 | Fix string register extended terms (#2597) | Andrew Reynolds | |
A regress2 benchmark was failing, due to a recent change in our strings rewriter. The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings. The fix is to ensure that extended function terms in any assertions *or shared terms* are registered. This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed. | |||
2018-10-08 | Cmake: Fix ctest call for example/translator. (#2600) | Aina Niemetz | |
example/translator expects an input file to translate but none was provided in the ctest call. This caused the ctest call to hang and wait for input on stdin in some configurations (in particular in the nightlies). |