SRI-CSL / yices2 / 8303521702

66%

Build Type

push

github

Committed by web-flow

Commit Message

Decision hint queue (#494)

* Fixed typos

* rename int_queue_t size with capacity

* enhanced int_queue

* added queue for next decision

* Clear hint queue on conflict

* Added two queues (top and hint)

* fixed bug

* added solver hints in NRA

* model_interpolation questions

* model_interpolation does not perform request_top_decision

* Remove shortcut variables from the queue

* regression prints execution time

* nra_plugin.c hint only on real solution

* variable selection forces decision on hint

* fix random decision

* trace printing

* changed the gold of a model interpolant

* added option for test issue204.smt2

* Removed ToDo

* avoid dupplication in top_decision_queue

* Revert "regression prints execution time"

This reverts commit aec6c21e4.

* Update mcsat_decision (fixed aux decision problems) and moved hinted queue reset to pop.

* Added force_decision for top_variables

---------

Co-authored-by: Thomas Hader <thomas.hader@sri.com>
Co-authored-by: Thomas Hader <tom@hader.email>

Run Details

96 of 132 new or added lines in 7 files covered. (72.73%)

15 existing lines in 4 files now uncovered.

79752 of 121708 relevant lines covered (65.53%)

1481502.14 hits per line