summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-11-29minornormalizeStringsSkolemAggAndres Noetzli
2018-11-29minorAndres Noetzli
2018-11-28more aggressiv string skolem normalizationAndres Noetzli
2018-11-28Information gain heuristic for PBE (#2719)Andrew Reynolds
2018-11-28Optimize re-elim for re.allchar components (#2725)Andrew Reynolds
2018-11-28Improve skolem caching by normalizing skolem args (#2723)Andres Noetzli
2018-11-28Generalize sygus stream solution filtering to logical strength (#2697)Andrew Reynolds
2018-11-27Improve cegqi engine trace. (#2714)Andrew Reynolds
2018-11-27Make (T)NodeTrie a general utility (#2489)Andrew Reynolds
2018-11-27Fix coverity warnings in datatypes (#2553)Andrew Reynolds
2018-11-27Lazy model construction in TheoryEngine (#2633)Andrew Reynolds
2018-11-27Reduce lookahead when parsing string literals (#2721)Andres Noetzli
2018-11-21Move ss-combine rewrite to extended rewriter (#2703)Andres Noetzli
2018-11-21Add rewrite for (str.substr s x y) --> "" (#2695)Andres Noetzli
2018-11-21Cache evaluations for PBE (#2699)Andrew Reynolds
2018-11-21Quickly recognize when PBE conjectures are infeasible (#2718)Andrew Reynolds
2018-11-21Obvious rewrites to floating-point < and <=. (#2706)Martin
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-11-21 Fix type enumerator for FP (#2717)Andrew Reynolds
2018-11-19Change lemma proof step storage & iterators (#2712)Alex Ozdemir
2018-11-19 Clausify context-dependent simplifications in ext theory (#2711)Andrew Reynolds
2018-11-19Fix E-matching for case where candidate generator is not properly initialized...Andrew Reynolds
2018-11-15 Expand definitions prior to model core computation (#2707)Andrew Reynolds
2018-11-08cmake: Add option to explicitely enable/disable static binaries. (#2698)Mathias Preiner
2018-11-07Evaluator: add support for str.code (#2696)Andres Noetzli
2018-11-07Adding default SyGuS grammar construction for arrays (#2685)Haniel Barbosa
2018-11-07Fix collectEmptyEqs in string rewriter (#2692)Andres Noetzli
2018-11-07 Fix for itos reduction (#2691)Andrew Reynolds
2018-11-06Incorporate static PBE symmetry breaking lemmas into SygusEnumerator (#2690)Andrew Reynolds
2018-11-05Change default sygus enumeration mode to auto (#2689)Andrew Reynolds
2018-11-05Fix coverity warnings in sygus enumerator (#2687)Andrew Reynolds
2018-11-05API: Fix assignment operators (#2680)Andres Noetzli
2018-11-05Allow partial models with optimized sygus enumeration (#2682)Andrew Reynolds
2018-11-04 Implement option to turn off symmetry breaking for basic enumerators (#2686)Andrew Reynolds
2018-11-03Refactor default grammars construction (#2681)Haniel Barbosa
2018-10-31Add optimized sygus enumeration (#2677)Andrew Reynolds
2018-10-31Record assumption info in AssertionPipeline (#2678)Andres Noetzli
2018-10-24Minor improvement to sygus trace (#2675)Andrew Reynolds
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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback