summaryrefslogtreecommitdiff
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-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
2018-11-01fixes to regression docs (#2679)yoni206
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-23CMake: Set RPATH on installed binary (#2671)Andres 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback