summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2018-10-09Allow multiple synthesis conjectures. (#2593)Andrew Reynolds
2018-10-08Fix compiler warnings. (#2601)Aina Niemetz
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-08Cmake: 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).
2018-10-08Address slow sygus regressions (#2598)Andrew Reynolds
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-04New C++ API: Add checks for Sorts. (#2519)Aina Niemetz
2018-10-04Infrastructure for string length entailments via approximations (#2514)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback