summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-01-03[LRA proof] Recording & Printing LRA Proofs (#2758)Alex Ozdemir
2018-12-20Clean up BV kinds and type rules. (#2766)Aina Niemetz
2018-12-20Add missing type rules for parameterized operator kinds. (#2766)Aina Niemetz
2018-12-19Fix issues with REWRITE_DONE in floating point rewriter (#2762)Andrew Reynolds
2018-12-15Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)Andres Noetzli
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
2018-12-14Fixed typos.Aina Niemetz
2018-12-14 Fix extended rewriter for binary associative operators. (#2751)Andrew Reynolds
2018-12-14Make single invocation and invariant pre/post condition templates independent...Andrew Reynolds
2018-12-13Remove spurious map (#2750)Andrew Reynolds
2018-12-12Fix compiler warnings. (#2748)Aina Niemetz
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-12-10BoolToBV modes (off, ite, all) (#2530)makaimann
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-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-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-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-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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback