summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-15minoraggSkolemSharingAltAndres Noetzli
2018-12-14Merge branch 'revertMoveSSCombine' into aggSkolemSharingaggSkolemSharingAndres Noetzli
2018-12-14Revert "Move ss-combine rewrite to extended rewriter (#2703)"revertMoveSSCombineAndres Noetzli
2018-12-14Merge branch 'master' into aggSkolemSharingAndres Noetzli
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
2018-12-14Fixed typos.Aina Niemetz
2018-12-14New C++ API: Add tests for opterm object. (#2756)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-13New C++ API: Add tests for sort functions of solver object. (#2752)Aina Niemetz
2018-12-13Remove spurious map (#2750)Andrew Reynolds
2018-12-12Fix compiler warnings. (#2748)Aina Niemetz
2018-12-12API: Add simple empty/sigma regexp unit tests (#2746)Andres Noetzli
2018-12-11[LRA proof] More complete LRA example proofs. (#2722)Alex Ozdemir
2018-12-11[LRAT] signature robust against duplicate literals (#2743)Alex Ozdemir
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-12-11LRAT signature (#2731)Alex Ozdemir
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-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-05more aggressiveAndres Noetzli
2018-12-04fixAndres Noetzli
2018-12-04aggressive skolem sharingAndres Noetzli
2018-12-04nitmergePostSuffix2Andres 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-02minorAndres Noetzli
2018-12-02Optimizations for PBE strings (#2728)Andrew Reynolds
2018-12-01stuffAndres Noetzli
2018-11-30changesAndres Noetzli
2018-11-30updateAndres Noetzli
2018-11-29Rewrite SK_FIRST_CTN_POST to SK_SUFFIX_REM skolemAndres Noetzli
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback