SRI-CSL / yices2
65%
master: 65%

LAST BUILD BRANCH: 2.7.0
DEFAULT BRANCH: master
Repo Added
Files 486
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

LAST BUILD ON BRANCH smtcomp2025
branch: smtcomp2025
CHANGE BRANCH
x

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

Relevant lines Covered
125986 RELEVANT LINES 81263 COVERED LINES
1412845.33 HITS PER LINE
Source Files on smtcomp2025

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
15622981081 smtcomp2025 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 climb... push web-flow github
64.5
15622071171 smtcomp2025 Api test eager fail (#560) * fail if any api tests fail * Update run_test.sh * Update run_test.sh push web-flow github
65.37
See All Builds (1787)