summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2019-04-20new rewritecav2019strings_expAndres Noetzli
2019-04-17Add rewrite for splitting equalitiesAndres Noetzli
2019-04-17mergeAndres Noetzli
2019-04-16Add interface for term enumeration (#2956)Andrew Reynolds
2019-04-16Stratify enumerative instantiation (#2954)Andrew Reynolds
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-05fix fp issue (#2940)Haniel Barbosa
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-03Update copyright headers.Aina Niemetz
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-04-01FP: Fix wrong model due to partial assignment (#2910)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
2019-04-01Modify strategy in sets+cardinality (#2909)Andrew Reynolds
2019-03-29Apply empty splits more aggressively in sets+cardinality (#2907)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-26Fix a few warnings (#2898)Andrew Reynolds
2019-03-24 Split regular expression solver (#2891)Andrew Reynolds
2019-03-23BV: Fix typerules for rotate operators. (#2895)Aina Niemetz
2019-03-23Fix memory leak when using subsolvers (#2893)Andres Noetzli
2019-03-23Strip non-matching beginning from indexof operator (#2885)Andres Noetzli
2019-03-22Revisit strings extended function decomposition (#2892)Andrew Reynolds
2019-03-22Fix instantiation stat for fmf (#2889)Andrew Reynolds
2019-03-22More fixes for PBE with datatypes (#2882)Andrew Reynolds
2019-03-22Fix stripConstantEndpoints in strings rewriter (#2883)Andres Noetzli
2019-03-21 Fix bad comparison in RE solver's addMembership (#2880)Andrew Reynolds
2019-03-21Rewrite selectors correctly applied to constructors (#2875)Andrew Reynolds
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2019-03-15New beta-reduction for HOL solving (#2869)Haniel Barbosa
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-05Make stripConstantEndpoints() less aggressiveAndres Noetzli
2019-02-04mergeAndres Noetzli
2019-02-04Formatajreynol
2019-02-04Minorajreynol
2019-02-04Generalize sygus rr verify feature.ajreynol
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-03Merge branch 'REtoCtn' into cav2019stringsAndres Noetzli
2019-02-03Merge branch 'ctnRew' into cav2019stringsAndres Noetzli
2019-02-03Fix issueAndres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback