mudathirmahgoub 13cf41801f Remove subtyping for sets theory (#5179) ...

This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:

Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON

2020-10-04 15:10:24 -05:00

..

bitvectors_and_arrays.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

bitvectors.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

CMakeLists.txt

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

combination.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

datatypes.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

exceptions.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

extract.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

floating_point.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

helloworld.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

linear_arith.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

sequences.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

sets.py

Remove subtyping for sets theory (#5179)

2020-10-04 15:10:24 -05:00

strings.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

sygus-fun.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

sygus-grammar.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00

sygus-inv.py

Update copyright header script to support CMake and Python files (#5067)

2020-09-22 09:51:56 -07:00