Adding support for Algebraic Datatypes

[amarshah1]

Sorry for the delay with adding this. @FedericoAureliano and I have added the datatype type to UCLID. There are 18 tests that fail parsing, fail typechecking, pass verification, and fail verification. Here is an example:

module main {
    // should fail every third step
    datatype myRecord = | rec(A: integer, B: integer, C: integer);

    var t1 : myRecord;
    var t2 : myRecord;


    init {
        t1 = rec(1, 2, 3);
        t2 = rec(3, 1, 2);
    }
    
    next {
        t2' = rec(t2.C, t2.A, t2.B);
    }

    invariant test : t1 != t2;

    control {
        bmc(5);
        check;
        print_results;
    }
}

Output:

Successfully instantiated 1 module(s).
4 assertions passed.
2 assertions failed.
0 assertions indeterminate.
  PASSED -> bmc [Step #0] property test @ test/test-adt-4.ucl, line 18
  PASSED -> bmc [Step #1] property test @ test/test-adt-4.ucl, line 18
  PASSED -> bmc [Step #3] property test @ test/test-adt-4.ucl, line 18
  PASSED -> bmc [Step #4] property test @ test/test-adt-4.ucl, line 18
  FAILED -> bmc [Step #2] property test @ test/test-adt-4.ucl, line 18
  FAILED -> bmc [Step #5] property test @ test/test-adt-4.ucl, line 18
Finished execution for module: main.

Enum and record support in UCLID could be folded into this in the future. We do not currently have support for testers, mutually recursive datatypes, and parametric datatypes. Let me know if there is anything we should add to this pull request.

[polgreen]

1. please rebase against master to get rid of the CI error for MacOS.

2. Can you please check you committed all your code, because this appears to have broken lots of things in the SMTLIB interface and enums in both the SMT lib interface and the Z3 interface. Here are some tests that throw errors on my laptop (not just in the CI)
   e.g.,
   uclid test/test-assert-1 -s "z3 -in" throws an error about head of empty list.
   uclid test/test-array-1.ucl -s "z3 -in" throws error about invalid sort declaration
   uclid test/test-array-2.ucl -s "z3 -in" throws error about invalid sort declaration
   uclid test/test-array-3.ucl -s "z3 -in" throws error about invalid sort declaration
   uclid test/test-record-1.ucl -s "z3 -in" throws error about invalid sort declaration
   etc
   uclid test/test-procedure-checker-3.ucl -s "z3 -in" throws unknown identifier
   uclid test/test-procedure-checker-3.ucl throws unknown identifier
   uclid test/test-procedure-checker-4.ucl -s "z3 -in" throws unknown identifier
   uclid test/test-procedure-checker-4.ucl throws unknown identifier

[FedericoAureliano]

Moved to #239 after significant merging.