summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-10-23Sketch of refactoring the Commands to use new APInewApiForCommandsAndres Noetzli
2018-10-22Do not use lazy trie for sygus-rr-verify (#2668)Andrew Reynolds
2018-10-22Fail for SWIG 3.0.8 (#2656)makaimann
2018-10-22CMake: Set PORTFOLIO_BUILD when building pcvc4 (#2666)Andres Noetzli
2018-10-22Only build CryptoMiniSat library, no binary (#2657)Andres Noetzli
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
2018-10-20Remove antlr_undefines.h. (#2664)Mathias Preiner
2018-10-20Add substr, contains and equality rewrites (#2665)Andres Noetzli
2018-10-20Disable dumping test for non-dumping builds (#2662)Andres Noetzli
2018-10-20Travis: run examples and avoid building them twice (#2663)Andres Noetzli
2018-10-19BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2...Aina Niemetz
2018-10-19BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_XOR) with special const...Aina Niemetz
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-19Fix util::Random for macOS builds (#2655)Andres Noetzli
2018-10-19Add helper to detect length one string terms (#2654)Andres Noetzli
2018-10-18Add OptionException handling during initialization (#2466)Andres Noetzli
2018-10-18cmake: Run regression level 2 for make check. (#2645)Mathias Preiner
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-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
2018-10-17Show if ASAN build in --show-config (#2650)Andres Noetzli
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 const....Aina Niemetz
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 o...Aina Niemetz
2018-10-16BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1...Aina Niemetz
2018-10-16BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 0...Aina Niemetz
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
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
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback