summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-06Merge branch 'master' into fixDestrOrderfixDestrOrderAlex Ozdemir
2018-12-06 Take into account minimality and types for cached PBE solutions (#2738)Andrew Reynolds
2018-12-05Fix use-after-free due to destruction orderAndres Noetzli
2018-12-04Apply extended rewriting on PBE static symmetry breaking. (#2735)Andrew Reynolds
2018-12-04Enable regular expression elimination by default. (#2736)Andrew Reynolds
2018-12-03 Skip non-cardinality types in sets min card inference (#2734)Andrew Reynolds
2018-12-03Bit vector proof superclass (#2599)Alex Ozdemir
2018-12-02Optimizations for PBE strings (#2728)Andrew Reynolds
2018-11-29 Infrastructure for sygus side conditions (#2729)Andrew Reynolds
2018-11-29Combine sygus stream with PBE (#2726)Andrew Reynolds
2018-11-28Improve interface for sygus grammar cons (#2727)Andrew Reynolds
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-27LRA proof signature fixes and a first proof for linear polynomials (#2713)Alex Ozdemir
2018-11-22Use https for antlr3.org downloads (#2701)Tom Smeding
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-20Fix real2int regression. (#2716)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-14cmake: Require boost 1.50.0 for examples. (#2710)Mathias Preiner
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-05New C++ API: Split unit tests. (#2688)Aina Niemetz
2018-11-05Increasing coverage (#2683)yoni206
2018-11-05API: Fix assignment operators (#2680)Andres Noetzli
2018-11-05configure.sh: Fix option parsing to match --help (#2611)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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback