summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2018-10-20Merge branch 'master' into strRewritesstrRewritesAndrew Reynolds
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-19Add substr, contains and equality rewritesAndres 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-19Remove autotools build system. (#2639)Mathias Preiner
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-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-18Constant length regular expression elimination (#2646)Andrew Reynolds
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-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-15Add more (str.replace x y z) rewrites (#2628)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-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 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.
2018-10-09Allow multiple synthesis conjectures. (#2593)Andrew Reynolds
2018-10-08BV 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-05Fix unif trace (#2550)Haniel Barbosa
2018-10-05 Fix cache for sygus post-condition inference (#2592)Andrew Reynolds
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-04Fix rewrite rule filtering. (#2591)Andrew Reynolds
2018-10-04Infrastructure for string length entailments via approximations (#2514)Andrew Reynolds
2018-10-04Fix end constraint for regexp elimination (#2571)Andrew Reynolds
2018-10-04Clean remaining references to getNextDecisionRequest and simplify (#2500)Andrew Reynolds
2018-10-03Fix compiler warnings. (#2585)Aina Niemetz
2018-10-03Add actively generated sygus enumerators (#2552)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback