SRI-CSL / yices2 / 9784126858

65%

Build Type

push

github

Committed by web-flow

Commit Message

Finite Field support (#513)

* Symbols created, eval_ff_* to be done

* Added ff_plugin stub

* Registered ff plugin to mcsat

* Added further type support for FF type

* Added printing support for the ff type

* fixed warning

* actual missing error strings

* Parsing of (as (_ ff3 13) FF0) done

* reformat indentions

* reformat indentions

* Front-end parsing done

* mod_rba_buffer_t and TAG_ARITH_FF_BUFFER

* Code Formatting

* Finite Field term generation done

* Fixed print_elem in term_stack2.c

* Code Formatting

* Removed unnecessary todos

* Support arbitrary finite field size

* Some optimization for ff eq term generation

* Code Formatting and Warning fixes

* Added exceptions when ff is solved with non-mcsat context.

* fixed model_eval to handle finite field terms (and return unknown).

* Term manager update (added further ff code to term_manager)

* Added FF support to MCSAT preprocessor

* Added FF support to model printing

* fix

* Fixed printing and added value_ff_t.

* WIP: ff_plugin_new_term_notify

* Code Formatting fixes

* extracted lp_data handling from NRA plugin

* moved trail_variable_compare to trail and added lp_data in ff_plugin

* extracted poly_constraint from nra to lp_constraint_db

* fixed bug in non mcsat part

* using lp_data in explanation

* store term_t in lp_data instead of variable_t

* Consolidated libpoly_utils.c

* update nra_plugin_explain to support lp_data

* fixed context_config bug

* added mcsat only checks to makefile

* rework done: extracted lib_poly code from nra.

* rework done: extracted unit_info from nra and bv

* implementation of term_notify in ff done

* fixed Makefile whitespaces

* ff_poly_constraint_create implemented and minor improvements in the nra plugin.

* Build system update to use static libpoly for all builds when configured

* fixed term printing issue

* make lp_data_t finite field ord... (continued)

Run Details

2302 of 3292 new or added lines in 66 files covered. (69.93%)

19 existing lines in 13 files now uncovered.

81585 of 123750 relevant lines covered (65.93%)

1494894.38 hits per line