Alex Ozdemir 368f3c3ed6 ff: connect sub-theories to main solver & test (#9218) ...

Organizing the PR a bit:

we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.

2022-12-16 16:36:41 +00:00

..

bags.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

bitvectors_and_arrays.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

bitvectors.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

CMakeLists.txt

ff: connect sub-theories to main solver & test (#9218)

2022-12-16 16:36:41 +00:00

combination.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

datatypes.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

extract.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

finite_field.cpp

ff: connect sub-theories to main solver & test (#9218)

2022-12-16 16:36:41 +00:00

floating_point_arith.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

helloworld.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

linear_arith.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

quickstart.cpp

docs: Do not use explicit line numbers in literalinclude. (#8690)

2022-05-02 20:13:00 +00:00

relations.cpp

Add Relation and Table types to SMTLib parser (#8605)

2022-04-13 13:54:27 -05:00

sequences.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

sets.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

strings.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

sygus-fun.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

sygus-grammar.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

sygus-inv.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

transcendentals.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

utils.cpp

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00

utils.h

Update copyright headers for release 1.0 (#8539)

2022-04-05 20:38:57 +00:00