SRI-CSL / yices2 / 15622981081
65%
master: 65%

LAST BUILD BRANCH: 2.7.0
DEFAULT BRANCH: master
Ran
Jobs 1
Files 492
Run time 125min
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: 64.502% (-0.9%) from 65.37%
15622981081

push

github

web-flow 
L2 o submission merge into smtcomp2025 (#562)

* Add L2O module

* fix bug no vars to hill_climbing

* +l2o TODOs file

* Fixed some code issues.

* Fixed some code issues.

* Fixed code formatting for some files

* Fixed memory leak in hill climbing, removed hill climbing dl list, code improvements

* Removed unused files

* Moved EMPTY_KEY and DELTED_KEY of hmaps in .c files.

* Renamed eval_hash_map to double_hash_map

* +l2o_apply_ls: classical local search cost fx

* assert

* removed redundant code with apply_l2o_ls

* Fixed some breask in l2o_apply

* Added proper conversion from double to mcsat_value

* minor code updates

* Update function signature for l2o

* Portfolio 1

* Portfolio 2

* Portfolio 2 + delayed start

* Portfolio with start L2O

* Start, no portfolio

* Portfolio mod 13

* L2O only at restarts

* Increased initial delay

* No initial delay, cache clear every 2nd l2o run

* Fixed cache memory leak

* Fixed another memory leak

* Fix

* fup

# Conflicts:
#	src/mcsat/l2o/evaluator.c

* baa

* Added l2o_search_state_t and update evaluator.c

* Clean-up evaluator_t

* asserting cache variable comparison

* Update cache

* Cleanup l2o structs

* Cleanup header file

* Cleanup header files and includes

* Variable order sorting by activity in L2O

* Using prio in hill climb

* Using prio in hill climb w/o sorting

* Fixed var selection in hill climbing

* Fixed var selection in hill climbing

* another bugfix

* Update hill_climbing for boolean and bugfix

* enable variable ordering again

* added nra cache statistics

* don't do var order sorting

* L2O always use the cache

* Ever 25th recache, the cache is cleared instead of L2O

* do a % 10 for cache use in l2o

* Clear cache the first time only

* moved L2O call beyond propagation

* l2o after prop with % 2 cache usage

* Reworked hill_climbing.c

* 50/50

* Fixed new hill_climbing.c

* 50/50 %3

* first version of fs_jumping implemented

* Not just base level

* l2o init only ... (continued)

231 of 1972 new or added lines in 19 files covered. (11.71%)

5 existing lines in 3 files now uncovered.

81263 of 125986 relevant lines covered (64.5%)

1412845.33 hits per line

New Missed Lines in Diff

Lines Coverage ∆ File
1
84.74
 0.06% src/mcsat/trail.c
2
0.0
 src/mcsat/l2o/l2o_internal.h
2
90.58
 0.32% src/terms/terms.c
5
34.21
 -0.07% src/frontend/yices_smt2.c
5
78.77
 -0.03% src/mcsat/solver.c
5
69.74
 -4.91% src/utils/int_queues.c
6
76.87
 -0.34% src/mcsat/nra/nra_plugin.c
6
69.63
 -0.47% src/terms/rationals.c
13
50.02
 -0.17% src/frontend/smt2/smt2_commands.c
14
83.47
 -11.81% src/utils/int_hash_sets.c
18
80.46
 -0.22% src/terms/term_manager.c
108
16.28
 src/mcsat/l2o/varset_table.c
134
0.0
 src/mcsat/l2o/hill_climbing.c
161
10.06
 src/utils/double_hash_map.c
496
0.0
 src/mcsat/l2o/evaluator.c
765
5.32
 src/mcsat/l2o/l2o.c

Uncovered Existing Lines

Lines Coverage ∆ File
1
83.47
 -11.81% src/utils/int_hash_sets.c
2
50.02
 -0.17% src/frontend/smt2/smt2_commands.c
2
78.77
 -0.03% src/mcsat/solver.c
Jobs
ID Job ID Ran Files Coverage
1 15622981081.1 492
64.5
 GitHub Action Run
Source Files on build 15622981081