| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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). | |||
| 2018-10-08 | Address slow sygus regressions (#2598) | Andrew Reynolds | |
| 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 | New C++ API: Add checks for Sorts. (#2519) | Aina Niemetz | |
| 2018-10-04 | Infrastructure for string length entailments via approximations (#2514) | Andrew Reynolds | |
| 2018-10-04 | Only use SKIP_RETURN_CODE with CMake 3.9.0+ (#2590) | Andres Noetzli | |
| With older versions of CMake, skipped tests are reported as failures, which is undesirable. This commit changes the CMakeLists file to only use the `SKIP_RETURN_CODE` property if a newer version of CMake is used. | |||
| 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 mem leak in sha1_collision example. (#2588) | Aina Niemetz | |
| 2018-10-03 | Fix mem leak in sets_translate example. (#2589) | Aina Niemetz | |
| 2018-10-03 | Simplify datatypes printing (#2573) | Andrew Reynolds | |
| 2018-10-03 | Fix compiler warnings. (#2585) | Aina Niemetz | |
| 2018-10-03 | Fix regress (#2575) | Andrew Reynolds | |
| 2018-10-03 | Add actively generated sygus enumerators (#2552) | Andrew Reynolds | |
| 2018-10-03 | Make CegisUnif with condition independent robust to var agnostic (#2565) | Haniel Barbosa | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback