summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-12-07Strings: Make EXTF_d inference more conservative (#2740)Andres Noetzli
2018-12-06Arith Constraint Proof Loggin (#2732)Alex Ozdemir
2018-12-06Enable BV proofs when using an eager bitblaster (#2733)Alex Ozdemir
2018-12-06Fix use-after-free due to destruction order (#2739)Andres Noetzli
2018-12-06 Take into account minimality and types for cached PBE solutions (#2738)Andrew Reynolds
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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback