Repository: sympy/sympy

Issue:
simplification of ConditionSet with FiniteSet
Should the following just simplify (automatically) to {0}?

```
>>> ConditionSet(x, And(x < 1, x > -3), FiniteSet(0, 1, 2))
ConditionSet(x, And(x < 1, x > -3), {0, 1, 2})
```

If the set (last arg) is a FiniteSet, and all elements cause the condition to be evaluated (True or False) then perhaps the filtered FIniteSet should be returned.

Discussion:
asmeurer: Does this do the right thing if the condition doesn't evaluate to True or False for some element of the finite set? 
AnishShah: > Does this do the right thing if the condition doesn't evaluate to True or False for some element of the finite set?

Yes, It does the right thing. I have added a test for that.
AnishShah: I have updated the PR. I have added some more tests and I used `fuzzy_bool` & `sift` instead of `intersect`.
AnishShah: test_pretty_ConditionSet fails .. I might be because of my changes. I will have a look.
Should I include those changes in this PR itself?
AnishShah: @asmeurer @smichr I have changed `test_pretty_Condition` because those tests were failing because of my changes. Let me know if it is OK to include it in this PR itself.  
AnishShah: @smichr I have updated the PR

Patch:
diff --git a/sympy/combinatorics/perm_groups.py b/sympy/combinatorics/perm_groups.py
index 37f07c0bc0..b1565fd52f 100644
--- a/sympy/combinatorics/perm_groups.py
+++ b/sympy/combinatorics/perm_groups.py
@@ -1306,14 +1306,14 @@ def generate_schreier_sims(self, af=False):
                     yield x._array_form
                 else:
                     yield x
-            return
+            raise StopIteration
         if len(u) == 1:
             for i in basic_orbits[0]:
                 if af:
                     yield u[0][i]._array_form
                 else:
                     yield u[0][i]
-            return
+            raise StopIteration
 
         u = list(reversed(u))
         basic_orbits = basic_orbits[::-1]
@@ -1327,7 +1327,7 @@ def generate_schreier_sims(self, af=False):
             # backtrack when finished iterating over coset
             if pos[h] >= posmax[h]:
                 if h == 0:
-                    return
+                    raise StopIteration
                 pos[h] = 0
                 h -= 1
                 stg.pop()
diff --git a/sympy/core/expr.py b/sympy/core/expr.py
index 32954b2e7a..55ed6db91e 100644
--- a/sympy/core/expr.py
+++ b/sympy/core/expr.py
@@ -2622,7 +2622,7 @@ def _eval_lseries(self, x, logx=None):
                 yield series.removeO()
             else:
                 yield series
-            return
+            raise StopIteration
 
         while series.is_Order:
             n += 1
diff --git a/sympy/geometry/polygon.py b/sympy/geometry/polygon.py
index e3b65055dd..fbc93fbaf0 100644
--- a/sympy/geometry/polygon.py
+++ b/sympy/geometry/polygon.py
@@ -1648,7 +1648,6 @@ class Triangle(Polygon):
     incircle
     medians
     medial
-    nine_point_circle
 
     Raises
     ======
@@ -2250,38 +2249,6 @@ def medial(self):
         s = self.sides
         return Triangle(s[0].midpoint, s[1].midpoint, s[2].midpoint)
 
-    @property
-    def nine_point_circle(self):
-        """The nine-point circle of the triangle.
-
-        Nine-point circle is the circumcircle of the medial triangle, which
-        passes through the feet of altitudes and the middle points of segments
-        connecting the vertices and the orthocenter.
-
-        Returns
-        =======
-
-        nine_point_circle : Circle
-
-        See also
-        ========
-
-        sympy.geometry.line.Segment.midpoint
-        sympy.geometry.polygon.Triangle.medial
-        sympy.geometry.polygon.Triangle.orthocenter
-
-        Examples
-        ========
-
-        >>> from sympy.geometry import Point, Triangle
-        >>> p1, p2, p3 = Point(0, 0), Point(1, 0), Point(0, 1)
-        >>> t = Triangle(p1, p2, p3)
-        >>> t.nine_point_circle
-        Circle(Point2D(1/4, 1/4), sqrt(2)/4)
-
-        """
-        return Circle(*self.medial.vertices)
-
 
 def rad(d):
     """Return the radian value for the given degrees (pi = 180 degrees)."""
diff --git a/sympy/polys/subresultants_qq_zz.py b/sympy/polys/subresultants_qq_zz.py
index a8bc77be1c..1d71909588 100644
--- a/sympy/polys/subresultants_qq_zz.py
+++ b/sympy/polys/subresultants_qq_zz.py
@@ -1,214 +1,13 @@
 # -*- coding: utf-8 -*-
 """
-This module contains functions for the computation
-of Euclidean, generalized Sturmian and (modified) subresultant
-polynomial remainder sequences (prs's).
-
-The pseudo-remainder function prem() of sympy is _not_ used
-by any of the functions in the module.
-
-Instead of prem() we use the function
-
-rem_z().
-
-Included is also the function quo_z().
-
-1. Theoretical background:
-==========================
-Consider the polynomials f, g ∈ Z[x] of degrees deg(f) = n and
-deg(g) = m with n ≥ m.
-
-Definition 1:
-=============
-The sign sequence of a polynomial remainder sequence (prs) is the
-sequence of signs of the leading coefficients of its polynomials.
-
-Sign sequences can be computed with the function:
-
-sign_seq(poly_seq, x)
-
-Definition 2:
-=============
-A polynomial remainder sequence (prs) is called complete if the
-degree difference between any two consecutive polynomials is 1;
-otherwise, it called incomplete.
-
-It is understood that f, g belong to the sequences mentioned in
-the two definitions.
-
-1A. Euclidean and subresultant prs's:
-=====================================
-The subresultant prs of f, g is a sequence of polynomials in Z[x]
-analogous to the Euclidean prs, the sequence obtained by applying
-on f, g Euclid’s algorithm for polynomial greatest common divisors
-(gcd) in Q[x].
-
-The subresultant prs differs from the Euclidean prs in that the
-coefficients of each polynomial in the former sequence are determinants
---- also referred to as subresultants --- of appropriately selected
-sub-matrices of sylvester1(f, g, x), Sylvester’s matrix of 1840 of
-dimensions (n + m) × (n + m).
-
-Recall that the determinant of sylvester1(f, g, x) itself is
-called the resultant of f, g and serves as a criterion of whether
-the two polynomials have common roots or not.
-
-For complete prs’s the sign sequence of the Euclidean prs of f, g
-is identical to the sign sequence of the subresultant prs of f, g
-and the coefficients of one sequence  are easily computed from the
-coefficients of the  other.
-
-For incomplete prs’s the polynomials in the subresultant prs, generally
-differ in sign from those of the Euclidean prs, and --- unlike the
-case of complete prs’s --- it is not at all obvious how to compute
-the coefficients of one sequence from the coefficients of the  other.
-
-1B. Sturmian and modified subresultant prs's:
-=============================================
-For the same polynomials f, g ∈ Z[x] mentioned above, their ``modified''
-subresultant prs is a sequence of polynomials similar to the Sturmian
-prs, the sequence obtained by applying in Q[x] Sturm’s algorithm on f, g.
-
-The two sequences differ in that the coefficients of each polynomial
-in the modified subresultant prs are the determinants --- also referred
-to as modified subresultants --- of appropriately selected  sub-matrices
-of sylvester2(f, g, x), Sylvester’s matrix of 1853 of dimensions 2n × 2n.
-
-The determinant of sylvester2 itself is called the modified resultant
-of f, g and it also can serve as a criterion of whether the two
-polynomials have common roots or not.
-
-For complete prs’s the  sign sequence of the Sturmian prs of f, g is
-identical to the sign sequence of the modified subresultant prs of
-f, g and the coefficients of one sequence  are easily computed from
-the coefficients of the other.
-
-For incomplete prs’s the polynomials in the modified subresultant prs,
-generally differ in sign from those of the Sturmian prs, and --- unlike
-the case of complete prs’s --- it is not at all obvious how to compute
-the coefficients of one sequence from the coefficients of the  other.
-
-As Sylvester pointed out, the coefficients of the polynomial remainders
-obtained as (modified) subresultants are the smallest possible without
-introducing rationals and without computing (integer) greatest common
-divisors.
-
-1C. On terminology:
-===================
-Whence the terminology? Well generalized Sturmian prs's are
-``modifications'' of Euclidean prs's; the hint came from the title
-of the Pell-Gordon paper of 1917.
-
-In the literature one also encounters the name ``non signed'' and
-``signed'' prs for Euclidean and Sturmian prs respectively.
-
-Likewise ``non signed'' and ``signed'' subresultant prs for
-subresultant and modified subresultant prs respectively.
-
-2. Functions in the module:
-===========================
-No function utilizes sympy's function prem().
-
-2A. Matrices:
-=============
-The functions sylvester(f, g, x, method=1) and
-sylvester(f, g, x, method=2) compute either Sylvester matrix.
-They can be used to compute (modified) subresultant prs's by
-direct determinant evaluation.
-
-The function bezout(f, g, x, method='prs') provides a matrix of
-smaller dimensions than either Sylvester matrix. It is the function
-of choice for computing (modified) subresultant prs's by direct
-determinant evaluation.
-
-sylvester(f, g, x, method=1)
-sylvester(f, g, x, method=2)
-bezout(f, g, x, method='prs')
-
-The following identity holds:
-
-bezout(f, g, x, method='prs') =
-backward_eye(deg(f))*bezout(f, g, x, method='bz')*backward_eye(deg(f))
-
-2B. Subresultant and modified subresultant prs's by
-===================================================
-determinant evaluation:
-=======================
-Instead of utilizing the Sylvester matrices, we employ
-the Bezout matrix of smaller dimensions.
-
-subresultants_bezout(f, g, x)
-modified_subresultants_bezout(f, g, x)
-
-2C. Subresultant prs's by ONE determinant evaluation:
-=====================================================
-All three functions in this section evaluate one determinant
-per remainder polynomial; this is the determinant of an
-appropriately selected sub-matrix of sylvester1(f, g, x),
-Sylvester’s matrix of 1840.
-
-To compute the remainder polynomials the function
-subresultants_rem(f, g, x) employs rem(f, g, x).
-By contrast, the other two functions implement Van Vleck’s ideas
-of 1900 and compute the remainder polynomials by trinagularizing
-sylvester2(f, g, x), Sylvester’s matrix of 1853.
-
-
-subresultants_rem(f, g, x)
-subresultants_vv(f, g, x)
-subresultants_vv_2(f, g, x).
-
-2E. Euclidean, Sturmian prs's in Q[x]:
-======================================
-euclid_q(f, g, x)
-sturm_q(f, g, x)
-
-2F. Euclidean, Sturmian and (modified) subresultant prs's P-G:
-==============================================================
-All functions in this section are based on the Pell-Gordon (P-G)
-theorem of 1917.
-Computations are done in Q[x], employing the function rem(f, g, x)
-for the computation of the remainder polynomials.
-
-euclid_pg(f, g, x)
-sturm pg(f, g, x)
-subresultants_pg(f, g, x)
-modified_subresultants_pg(f, g, x)
-
-2G. Euclidean, Sturmian and (modified) subresultant prs's A-M-V:
-================================================================
-All functions in this section are based on the Akritas-Malaschonok-
-Vigklas (A-M-V) theorem of 2015.
-Computations are done in Z[x], employing the function rem_z(f, g, x)
-for the computation of the remainder polynomials.
-
-euclid_amv(f, g, x)
-sturm_amv(f, g, x)
-subresultants_amv(f, g, x)
-modified_subresultants_amv(f, g, x)
-
-2Ga. Exception:
-===============
-subresultants_amv_q(f, g, x)
-
-This function employs rem(f, g, x) for the computation of
-the remainder polynomials, despite the fact that it implements
-the A-M-V Theorem.
-
-It is included in our module in order to show that theorems P-G
-and A-M-V can be implemented utilizing either the function
-rem(f, g, x) or the function rem_z(f, g, x).
-
-For clearly historical reasons --- since the Collins-Brown-Traub
-coefficients-reduction factor β_i was not available in 1917 ---
-we have implemented the Pell-Gordon theorem with the function
-rem(f, g, x) and the A-M-V Theorem  with the function rem_z(f, g, x).
-"""
+Created on Mon Dec 28 13:25:02 2015
 
+@author: alkis
+"""
 
 from __future__ import print_function, division
 
-from sympy import (Abs, degree, expand, eye, floor, LC, Matrix, nan, Poly, pprint)
+from sympy import (Abs, degree, expand, floor, LC, Matrix, nan, Poly, pprint)
 from sympy import (QQ, quo, rem, S, sign, simplify, summation, var, zeros)
 
 def sylvester(f, g, x, method = 1):
@@ -324,251 +123,6 @@ def sign_seq(poly_seq, x):
     """
     return [sign(LC(poly_seq[i], x)) for i in range(len(poly_seq))]
 
-def bezout(p, q, x, method='bz'):
-    """
-    The input polynomials p, q are in Z[x] or in Q[x]. It is assumed
-    that degree(p, x) >= degree(q, x).
-
-    The default option bezout(p, q, x, method='bz') returns Bezout's
-    symmetric matrix of p and q, of dimensions deg(p) x deg(p). The
-    determinant of this matrix is equal to the determinant of sylvester2,
-    Sylvester's matrix of 1853, whose dimensions are 2*deg(p) x 2*deg(p);
-    however, the subresultants of these two matrices may vary in sign.
-
-    The other option, bezout(p, q, x, 'prs'), is of interest to us
-    in this module because it returns a matrix equivalent to sylvester2.
-    In this case all subresultants of the two matrices are identical.
-
-    Both the subresultant polynomial remainder sequence (prs) and
-    the modified subresultant prs of p and q can be computed by
-    evaluating determinants of appropriately selected submatrices of
-    bezout(p, q, x, 'prs') --- one determinant per coefficient of the
-    remainder polynomials.
-
-    The matrices bezout(p, q, x, 'bz') and bezout(p, q, x, 'prs')
-    are related by the formula
-
-    bezout(p, q, x, 'prs') =
-    backward_eye(deg(p)) * bezout(p, q, x, 'bz') * backward_eye(deg(p)),
-
-    where backward_eye() is the backward identity function.
-
-    References:
-    ===========
-    1. G.M.Diaz-Toca,L.Gonzalez-Vega: Various New Expressions for Subresultants
-    and Their Applications. Appl. Algebra in Engin., Communic. and Comp.,
-    Vol. 15, 233–266, 2004.
-
-    """
-    y = var('y')
-    degP = degree(p, x)
-
-    # expr is 0 when x = y
-    expr = p * q.subs({x:y}) - p.subs({x:y}) * q
-
-    # hence expr is exactly divisible by x - y
-    poly = Poly( quo(expr, x-y), x, y)
-
-    # form Bezout matrix and store them in B as indicated to get
-    # the LC coefficient of each poly in the first position of each row
-    B = zeros(degP)
-    for i in range(degP):
-        for j in range(degP):
-            if method == 'prs':
-                B[degP - 1 - i, degP - 1 - j] = poly.nth(i, j)
-            else:
-                B[i, j] = poly.nth(i, j)
-    return B
-
-def backward_eye(n):
-    '''
-    Returns the backward identity matrix of dimensions n x n.
-
-    Needed to "turn" the Bezout matrices
-    so that the leading coefficients are first.
-    See docstring of the function bezout(p, q, x, method='bz').
-    '''
-    M = eye(n)  # identity matrix of order n
-
-    for i in range(int(M.rows / 2)):
-        M.row_swap(0 + i, M.rows - 1 - i)
-
-    return M
-
-def process_bezout_output(poly_seq, x):
-    """
-    poly_seq is a polynomial remainder sequence computed either by
-    subresultants_bezout or by modified_subresultants_bezout.
-
-    This function removes from poly_seq all zero polynomials as well
-    as all those whose degree is equal to the degree of a previous
-    polynomial in poly_seq, as we scan it from left to right.
-
-    """
-    L = poly_seq[:]  # get a copy of the input sequence
-    d = degree(L[1], x)
-    i = 2
-    while i < len(L):
-        d_i = degree(L[i], x)
-        if d_i < 0:          # zero poly
-            L.remove(L[i])
-            i = i - 1
-        if d == d_i:         # poly degree equals degree of previous poly
-            L.remove(L[i])
-            i = i - 1
-        if d_i >= 0:
-            d = d_i
-        i = i + 1
-
-    return L
-
-def subresultants_bezout(p, q, x):
-    """
-    The input polynomials p, q are in Z[x] or in Q[x]. It is assumed
-    that degree(p, x) >= degree(q, x).
-
-    Computes the subresultant polynomial remainder sequence
-    of p, q by evaluating determinants of appropriately selected
-    submatrices of bezout(p, q, x, 'prs'). The dimensions of the
-    latter are deg(p) x deg(p).
-
-    Each coefficient is computed by evaluating the determinant of the
-    corresponding submatrix of bezout(p, q, x, 'prs').
-
-    bezout(p, q, x, 'prs) is used instead of sylvester(p, q, x, 1),
-    Sylvester's matrix of 1840, because the dimensions of the latter
-    are (deg(p) + deg(q)) x (deg(p) + deg(q)).
-
-    If the subresultant prs is complete, then the output coincides
-    with the Euclidean sequence of the polynomials p, q.
-
-    References:
-    ===========
-    1. G.M.Diaz-Toca,L.Gonzalez-Vega: Various New Expressions for Subresultants
-    and Their Applications. Appl. Algebra in Engin., Communic. and Comp.,
-    Vol. 15, 233–266, 2004.
-
-    """
-    # make sure neither p nor q is 0
-    if p == 0 or q == 0:
-        return [p, q]
-
-    f, g = p, q
-    n = degF = degree(f, x)
-    m = degG = degree(g, x)
-
-    # make sure proper degrees
-    if n == 0 and m == 0:
-        return [f, g]
-    if n < m:
-        n, m, degF, degG, f, g = m, n, degG, degF, g, f
-    if n > 0 and m == 0:
-        return [f, g]
-
-    SR_L = [f, g]      # subresultant list
-    F = LC(f, x)**(degF - degG)
-
-    # form the bezout matrix
-    B = bezout(f, g, x, 'prs')
-
-    # pick appropriate submatrices of B
-    # and form subresultant polys
-    if degF > degG:
-        j = 2
-    if degF == degG:
-        j = 1
-    while j <= degF:
-        M = B[0:j, :]
-        k, coeff_L = j - 1, []
-        while k <= degF - 1:
-            coeff_L.append(M[: ,0 : j].det())
-            if k < degF - 1:
-                M.col_swap(j - 1, k + 1)
-            k = k + 1
-
-        # apply Theorem 2.1 in the paper by Toca & Vega 2004
-        # to get correct signs
-        SR_L.append((int((-1)**(j*(j-1)/2)) * Poly(coeff_L, x) / F).as_expr())
-        j = j + 1
-
-    return process_bezout_output(SR_L, x)
-
-def modified_subresultants_bezout(p, q, x):
-    """
-    The input polynomials p, q are in Z[x] or in Q[x]. It is assumed
-    that degree(p, x) >= degree(q, x).
-
-    Computes the modified subresultant polynomial remainder sequence
-    of p, q by evaluating determinants of appropriately selected
-    submatrices of bezout(p, q, x, 'prs'). The dimensions of the
-    latter are deg(p) x deg(p).
-
-    Each coefficient is computed by evaluating the determinant of the
-    corresponding submatrix of bezout(p, q, x, 'prs').
-
-    bezout(p, q, x, 'prs') is used instead of sylvester(p, q, x, 2),
-    Sylvester's matrix of 1853, because the dimensions of the latter
-    are 2*deg(p) x 2*deg(p).
-
-    If the modified subresultant prs is complete, and LC( p ) > 0, the output
-    coincides with the (generalized) Sturm's sequence of the polynomials p, q.
-
-    References:
-    ===========
-    1. Akritas, A. G., G.I. Malaschonok and P.S. Vigklas: ``Sturm Sequences
-    and Modified Subresultant Polynomial Remainder Sequences.''
-    Serdica Journal of Computing, Vol. 8, No 1, 29–46, 2014.
-
-    2. G.M.Diaz-Toca,L.Gonzalez-Vega: Various New Expressions for Subresultants
-    and Their Applications. Appl. Algebra in Engin., Communic. and Comp.,
-    Vol. 15, 233–266, 2004.
-
-
-    """
-    # make sure neither p nor q is 0
-    if p == 0 or q == 0:
-        return [p, q]
-
-    f, g = p, q
-    n = degF = degree(f, x)
-    m = degG = degree(g, x)
-
-    # make sure proper degrees
-    if n == 0 and m == 0:
-        return [f, g]
-    if n < m:
-        n, m, degF, degG, f, g = m, n, degG, degF, g, f
-    if n > 0 and m == 0:
-        return [f, g]
-
-    SR_L = [f, g]      # subresultant list
-
-    # form the bezout matrix
-    B = bezout(f, g, x, 'prs')
-
-    # pick appropriate submatrices of B
-    # and form subresultant polys
-    if degF > degG:
-        j = 2
-    if degF == degG:
-        j = 1
-    while j <= degF:
-        M = B[0:j, :]
-        k, coeff_L = j - 1, []
-        while k <= degF - 1:
-            coeff_L.append(M[: ,0 : j].det())
-            if k < degF - 1:
-                M.col_swap(j - 1, k + 1)
-            k = k + 1
-
-        ## Theorem 2.1 in the paper by Toca & Vega 2004 is _not needed_
-        ## in this case since
-        ## the bezout matrix is equivalent to sylvester2
-        SR_L.append(( Poly(coeff_L, x)).as_expr())
-        j = j + 1
-
-    return process_bezout_output(SR_L, x)
-
 def sturm_pg(p, q, x, method=0):
     """
     p, q are polynomials in Z[x] or Q[x].
diff --git a/sympy/sets/conditionset.py b/sympy/sets/conditionset.py
index 1fa874f219..2bb96861fc 100644
--- a/sympy/sets/conditionset.py
+++ b/sympy/sets/conditionset.py
@@ -3,9 +3,11 @@
 from sympy import S
 from sympy.core.basic import Basic
 from sympy.core.function import Lambda
+from sympy.core.logic import fuzzy_bool
 from sympy.logic.boolalg import And
 from sympy.sets.sets import (Set, Interval, Intersection, EmptySet, Union,
                              FiniteSet)
+from sympy.utilities.iterables import sift
 
 
 class ConditionSet(Set):
@@ -34,6 +36,15 @@ def __new__(cls, sym, condition, base_set):
             return S.EmptySet
         if condition == S.true:
             return base_set
+        if isinstance(base_set, EmptySet):
+            return base_set
+        if isinstance(base_set, FiniteSet):
+            sifted = sift(base_set, lambda _: fuzzy_bool(condition.subs(sym, _)))
+            if sifted[None]:
+                return Union(FiniteSet(*sifted[True]),
+                             Basic.__new__(cls, sym, condition, FiniteSet(*sifted[None])))
+            else:
+                return FiniteSet(*sifted[True])
         return Basic.__new__(cls, sym, condition, base_set)
 
     sym = property(lambda self: self.args[0])


Test patch:
diff --git a/sympy/geometry/tests/test_polygon.py b/sympy/geometry/tests/test_polygon.py
index 12365695a6..cef5a5cf05 100644
--- a/sympy/geometry/tests/test_polygon.py
+++ b/sympy/geometry/tests/test_polygon.py
@@ -228,10 +228,6 @@ def test_polygon():
     assert intersection(m[p1], m[p2], m[p3]) == [t1.centroid]
     assert t1.medial == Triangle(Point(2.5, 0), Point(0, 2.5), Point(2.5, 2.5))
 
-    # Nine-point circle
-    assert t1.nine_point_circle == Circle(Point(2.5, 0), Point(0, 2.5), Point(2.5, 2.5))
-    assert t1.nine_point_circle == Circle(Point(0, 0), Point(0, 2.5), Point(2.5, 2.5))
-
     # Perpendicular
     altitudes = t1.altitudes
     assert altitudes[p1] == Segment(p1, Point(Rational(5, 2), Rational(5, 2)))
diff --git a/sympy/polys/tests/test_subresultants_qq_zz.py b/sympy/polys/tests/test_subresultants_qq_zz.py
index a377a936c2..737bdf7752 100644
--- a/sympy/polys/tests/test_subresultants_qq_zz.py
+++ b/sympy/polys/tests/test_subresultants_qq_zz.py
@@ -1,8 +1,6 @@
 from sympy import var, sturm, subresultants, prem, pquo
-from sympy.matrices import Matrix, eye
-from sympy.polys.subresultants_qq_zz import (sylvester, bezout,
-    subresultants_bezout, modified_subresultants_bezout,
-    process_bezout_output, backward_eye,
+from sympy.matrices import Matrix
+from sympy.polys.subresultants_qq_zz import (sylvester,
     sturm_pg, sturm_q, sturm_amv, euclid_pg, euclid_q,
     euclid_amv, modified_subresultants_pg, subresultants_pg,
     subresultants_amv_q, quo_z, rem_z, subresultants_amv,
@@ -34,44 +32,6 @@ def test_sylvester():
     assert sylvester(x**3 - 7*x + 7, 3*x**2 - 7, x, 2) == Matrix([
 [1, 0, -7,  7,  0,  0], [0, 3,  0, -7,  0,  0], [0, 1,  0, -7,  7,  0], [0, 0,  3,  0, -7,  0], [0, 0,  1,  0, -7,  7], [0, 0,  0,  3,  0, -7]])
 
-def test_bezout():
-    x = var('x')
-
-    p = -2*x**5+7*x**3+9*x**2-3*x+1
-    q = -10*x**4+21*x**2+18*x-3
-    assert bezout(p, q, x, 'bz').det() == sylvester(p, q, x, 2).det()
-    assert bezout(p, q, x, 'bz').det() != sylvester(p, q, x, 1).det()
-    assert bezout(p, q, x, 'prs') == backward_eye(5) * bezout(p, q, x, 'bz') * backward_eye(5)
-
-def test_subresultants_bezout():
-    x = var('x')
-
-    p = x**8 + x**6 - 3*x**4 - 3*x**3 + 8*x**2 + 2*x - 5
-    q = 3*x**6 + 5*x**4 - 4*x**2 - 9*x + 21
-    assert subresultants_bezout(p, q, x) == subresultants(p, q, x)
-    assert subresultants_bezout(p, q, x)[-1] == sylvester(p, q, x).det()
-    assert subresultants_bezout(p, q, x) != euclid_amv(p, q, x)
-    amv_factors = [1, 1, -1, 1, -1, 1]
-    assert subresultants_bezout(p, q, x) == [i*j for i, j in zip(amv_factors, modified_subresultants_amv(p, q, x))]
-
-    p = x**3 - 7*x + 7
-    q = 3*x**2 - 7
-    assert subresultants_bezout(p, q, x) == euclid_amv(p, q, x)
-
-def test_modified_subresultants_bezout():
-    x = var('x')
-
-    p = x**8 + x**6 - 3*x**4 - 3*x**3 + 8*x**2 + 2*x - 5
-    q = 3*x**6 + 5*x**4 - 4*x**2 - 9*x + 21
-    amv_factors = [1, 1, -1, 1, -1, 1]
-    assert modified_subresultants_bezout(p, q, x) == [i*j for i, j in zip(amv_factors, subresultants_amv(p, q, x))]
-    assert modified_subresultants_bezout(p, q, x)[-1] != sylvester(p + x**8, q, x).det()
-    assert modified_subresultants_bezout(p, q, x) != sturm_amv(p, q, x)
-
-    p = x**3 - 7*x + 7
-    q = 3*x**2 - 7
-    assert modified_subresultants_bezout(p, q, x) == sturm_amv(p, q, x)
-    assert modified_subresultants_bezout(-p, q, x) != sturm_amv(-p, q, x)
 
 def test_sturm_pg():
     x = var('x')
diff --git a/sympy/printing/pretty/tests/test_pretty.py b/sympy/printing/pretty/tests/test_pretty.py
index 959c8b7fbc..941ba32cd0 100644
--- a/sympy/printing/pretty/tests/test_pretty.py
+++ b/sympy/printing/pretty/tests/test_pretty.py
@@ -3199,17 +3199,14 @@ def test_pretty_ConditionSet():
     assert pretty(ConditionSet(x, Eq(sin(x), 0), S.Reals)) == ascii_str
     assert upretty(ConditionSet(x, Eq(sin(x), 0), S.Reals)) == ucode_str
 
-    assert pretty(ConditionSet(x, Contains(x, S.Reals, evaluate=False), FiniteSet(1))) == \
-        '{x | x in {1} and Contains(x, (-oo, oo))}'
-    assert upretty(ConditionSet(x, Contains(x, S.Reals, evaluate=False), FiniteSet(1))) == u('{x | x ∊ {1} ∧ (x ∈ ℝ)}')
+    assert pretty(ConditionSet(x, Contains(x, S.Reals, evaluate=False), FiniteSet(1))) == '{1}'
+    assert upretty(ConditionSet(x, Contains(x, S.Reals, evaluate=False), FiniteSet(1))) == u('{1}')
 
-    assert pretty(ConditionSet(x, And(x > 1, x < -1), FiniteSet(1, 2, 3))) ==\
-        '{x | x in {1, 2, 3} and And(x > 1, x < -1)}'
-    assert upretty(ConditionSet(x, And(x > 1, x < -1), FiniteSet(1, 2, 3))) == \
-        u('{x | x ∊ {1, 2, 3} ∧ (x > 1 ∧ x < -1)}')
+    assert pretty(ConditionSet(x, And(x > 1, x < -1), FiniteSet(1, 2, 3))) == "EmptySet()"
+    assert upretty(ConditionSet(x, And(x > 1, x < -1), FiniteSet(1, 2, 3))) == u("∅")
 
-    assert pretty(ConditionSet(x, Or(x > 1, x < -1), FiniteSet(1, 2))) == '{x | x in {1, 2} and Or(x > 1, x < -1)}'
-    assert upretty(ConditionSet(x, Or(x > 1, x < -1), FiniteSet(1, 2))) == u('{x | x ∊ {1, 2} ∧ (x > 1 ∨ x < -1)}')
+    assert pretty(ConditionSet(x, Or(x > 1, x < -1), FiniteSet(1, 2))) == '{2}'
+    assert upretty(ConditionSet(x, Or(x > 1, x < -1), FiniteSet(1, 2))) == u('{2}')
 
 
 def test_pretty_ComplexRegion():
diff --git a/sympy/sets/tests/test_conditionset.py b/sympy/sets/tests/test_conditionset.py
index c7d02044b4..557f87ed30 100644
--- a/sympy/sets/tests/test_conditionset.py
+++ b/sympy/sets/tests/test_conditionset.py
@@ -1,5 +1,5 @@
-from sympy.sets import (ConditionSet, Intersection)
-from sympy import (Symbol, Eq, S, Abs, sin, pi, Lambda, Interval)
+from sympy.sets import (ConditionSet, Intersection, FiniteSet, EmptySet, Union)
+from sympy import (Symbol, Eq, S, Abs, sin, pi, Lambda, Interval, And, Mod)
 
 x = Symbol('x')
 
@@ -24,3 +24,13 @@ def test_CondSet_intersect():
 def test_issue_9849():
     assert ConditionSet(x, Eq(x, x), S.Naturals) == S.Naturals
     assert ConditionSet(x, Eq(Abs(sin(x)), -1), S.Naturals) == S.EmptySet
+
+def test_simplified_FiniteSet_in_CondSet():
+    assert ConditionSet(x, And(x < 1, x > -3), FiniteSet(0, 1, 2)) == FiniteSet(0)
+    assert ConditionSet(x, x < 0, FiniteSet(0, 1, 2)) == EmptySet()
+    assert ConditionSet(x, And(x < -3), EmptySet()) == EmptySet()
+    y = Symbol('y')
+    assert (ConditionSet(x, And(x > 0), FiniteSet(-1, 0, 1, y)) ==
+        Union(FiniteSet(1), ConditionSet(x, And(x > 0), FiniteSet(y))))
+    assert (ConditionSet(x, Eq(Mod(x, 3), 1), FiniteSet(1, 4, 2, y)) ==
+        Union(FiniteSet(1, 4), ConditionSet(x, Eq(Mod(x, 3), 1), FiniteSet(y))))