Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-10-20 | Merge branch 'master' into strRewritesstrRewrites | Andrew Reynolds | |
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 | Add substr, contains and equality rewrites | Andres Noetzli | |
This commit adds three new rewrites: - `(str.contains (str.replace x y z) w) ---> (str.contains (str.replace x y "") w)` if `(str.contains z w) ---> false` and `(str.len w) = 1` - `(= (str.replace x y z) z) ---> (or (= x y) (= x z))` if `(str.len y) = (str.len z)` - `(str.substr s x y) --> ""` if `0 < y |= x >= str.len(s)` | |||
2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
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 | 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 | Constant length regular expression elimination (#2646) | Andrew Reynolds | |
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 | 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 | Add more (str.replace x y z) rewrites (#2628) | 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 | 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 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 | 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 | Disable extended rewriter when applicable with var agnostic enumeration (#2594) | Andrew Reynolds | |
2018-10-05 | Fix unif trace (#2550) | Haniel Barbosa | |
2018-10-05 | Fix cache for sygus post-condition inference (#2592) | Andrew Reynolds | |
2018-10-05 | Update default options for sygus (#2586) | Andrew Reynolds | |
2018-10-04 | Fix rewrite rule filtering. (#2591) | Andrew Reynolds | |
2018-10-04 | Infrastructure for string length entailments via approximations (#2514) | Andrew Reynolds | |
2018-10-04 | Fix end constraint for regexp elimination (#2571) | Andrew Reynolds | |
2018-10-04 | Clean remaining references to getNextDecisionRequest and simplify (#2500) | Andrew Reynolds | |
2018-10-03 | Fix compiler warnings. (#2585) | Aina Niemetz | |
2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |