SRI-CSL / yices2 / 9784126858
65%

DEFAULT BRANCH: master
Ran
Jobs 1
Files 486
Run time 6min
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst
coverage: 65.927% (+0.2%) from 65.726%
9784126858

push

github

web-flow 
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)

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

New Missed Lines in Diff

Lines Coverage ∆ File
1
91.52
 0.21% src/frontend/smt2/smt2_lexer.c
1
83.65
 0.0% src/mcsat/watch_list_manager.c
2
86.07
 -1.43% src/context/shared_terms.c
2
84.27
 -0.22% src/context/symmetry_breaking.c
2
77.34
 1.58% src/frontend/smt2/smt2_parser.c
2
96.15
 src/mcsat/ff/ff_plugin_internal.c
2
90.3
 0.14% src/mcsat/preprocessor.c
2
94.87
 src/mcsat/unit_info.c
2
89.14
 -0.05% src/solvers/simplex/simplex.c
3
88.3
 -0.21% src/context/context_simplifier.c
3
82.69
 1.04% src/model/model_eval.c
3
0.0
 0.0% src/solvers/simplex/diophantine_systems.c
3
70.33
 3.35% src/terms/rationals.c
5
64.36
 0.91% src/model/concrete_values.c
5
90.26
 0.23% src/terms/terms.c
6
85.52
 -1.76% src/frontend/smt2/smt2_printer.c
6
77.65
 0.72% src/mcsat/nra/nra_plugin.c
6
67.19
 -2.17% src/model/val_to_term.c
6
62.66
 -1.24% src/terms/polynomials.c
7
59.7
 -6.97% src/frontend/smt2/smt2_type_printer.c
7
30.11
 -1.06% src/terms/term_explorer.c
8
80.46
 -0.24% src/terms/term_utils.c
11
69.09
 -2.29% src/mcsat/value.c
12
10.83
 -0.43% src/io/concrete_value_printer.c
13
33.09
 0.51% src/frontend/yices_smt2.c
13
14.72
 -0.13% src/io/term_printer.c
13
92.9
 src/mcsat/utils/lp_utils.c
13
73.66
 -3.31% src/mcsat/utils/value_hash_map.c
13
40.82
 1.39% src/terms/types.c
15
75.51
 1.27% src/frontend/smt2/smt2_term_stack.c
15
0.0
 0.0% src/io/type_printer.c
18
0.0
 0.0% src/api/yices_error.c
20
32.15
 0.11% src/api/yices_api.c
20
80.95
 src/mcsat/utils/lp_data.c
23
57.41
 src/mcsat/ff/ff_libpoly.c
26
49.39
 -0.03% src/frontend/smt2/smt2_commands.c
30
80.98
 -0.25% src/terms/term_manager.c
33
51.24
 -2.6% src/io/yices_pp.c
36
56.16
 -6.81% src/mcsat/utils/substitution.c
37
62.95
 -0.77% src/mcsat/nra/feasible_set_db.c
43
59.35
 -1.31% src/terms/balanced_arith_buffers.c
51
72.13
 src/mcsat/utils/lp_constraint_db.c
52
72.87
 0.18% src/parser_utils/term_stack2.c
54
65.16
 src/mcsat/nra/nra_libpoly.c
78
78.63
 src/mcsat/ff/ff_plugin_explain.c
86
63.54
 -4.65% src/mcsat/nra/nra_plugin_explain.c
90
79.91
 src/mcsat/ff/ff_plugin.c
91
67.27
 src/mcsat/ff/ff_feasible_set_db.c

Uncovered Existing Lines

Lines Coverage ∆ File
1
77.65
 0.72% src/mcsat/nra/nra_plugin.c
1
66.12
 0.0% src/mcsat/variable_db.c
1
0.0
 0.0% src/solvers/simplex/diophantine_systems.c
1
10.83
 -0.43% src/io/concrete_value_printer.c
1
86.07
 -1.43% src/context/shared_terms.c
1
63.54
 -4.65% src/mcsat/nra/nra_plugin_explain.c
1
72.87
 0.18% src/parser_utils/term_stack2.c
1
30.11
 -1.06% src/terms/term_explorer.c
1
0.0
 0.0% src/io/type_printer.c
2
75.51
 1.27% src/frontend/smt2/smt2_term_stack.c
2
49.39
 -0.03% src/frontend/smt2/smt2_commands.c
2
59.35
 -1.31% src/terms/balanced_arith_buffers.c
4
79.53
 -0.17% src/mcsat/solver.c
Jobs
ID Job ID Ran Files Coverage
1 9784126858.1 1696
66.67
 GitHub Action Run
Source Files on build 9784126858