summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-03-14Fix non-variable function head elimination in UF. (#2864)Andrew Reynolds
2019-03-14Fix function term set for theory strings compute care graph. (#2862)Andrew Reynolds
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2019-03-14Properly handle lambdas in relevant domain (#2853)Andrew Reynolds
2019-03-14 Fix substitution step in ho matching (#2825)Andrew Reynolds
2019-03-14Generalize sygus-rr-verify for fast enumerator (#2829)Andrew Reynolds
2019-03-13Remove spurious data member. (#2857)Andrew Reynolds
2019-03-12Add option --sygus-rr-synth-rec for considering all grammar types recursively...Andrew Reynolds
2019-03-12 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)Andrew Reynolds
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
2019-01-19Fix missing-override warning (#2811)Andres Noetzli
2019-01-18Strings: Introduce checkEntailContains() (#2809)Andres Noetzli
2019-01-18 Fix ABC build (#2808)Andres Noetzli
2019-01-15Fix constant contains ITOS rewrite (#2799)Andrew Reynolds
2019-01-15Strings: Add option to change loop process mode (#2794)Andres Noetzli
2019-01-15 Fix unsound double abs rewrite rule for FP (#2792)Andrew Reynolds
2019-01-14 Only check disequal terms with sygus-rr-verify (#2793)Andrew Reynolds
2019-01-14ClausalBitvectorProof (#2786)Alex Ozdemir
2019-01-09Do not rewrite 1-constructor sygus testers to true (#2780)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback