• Sylvain Dailler's avatar
    Q217-025 Printer to smt2: convert bool term inside type to bv · a303ae72
    Sylvain Dailler authored
    This commit solves a CVC4 limitation on boolean inside datatypes for CE.
    It converts them to bv by adding a new printer. This commit is a hack and
    it will be reverted when the bug is solved in CVC4.
    
    * Makefile.in
    (Makefile): Added new printer.
    * drivers/smtv-libv2_cvc_ce.drv:
    (printer): new printer used is smtv2_cvc_ce
    * src/driver/parse_smtv2_model_lexer.mll
    (parse): Changed the way constructor of datatype are detected.
    * src/printer/smtv2_cvc_ce.ml
    (print_constructors): Projections to bool are changed to projections
    to bitvectors. Duplicate projections are generated which returns bool and
    are used in the rest of smtv2 generated.
    
    Change-Id: Ib2eba92aa788938b0bec30f8c156e9b235896881
    a303ae72
Makefile.in 69.9 KB