mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

use reward as proxy for score

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-26 09:49:53 -07:00
parent 2549a2cf07
commit 62a8512401
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sat_ddfw.h
View file

@ -155,7 +155,7 @@ namespace sat {
inline void inc_reward(literal lit, double w) { reward(lit.var()) += w; }
inline void dec_reward(literal lit, double w) { if (reward(lit.var()) >= w) reward(lit.var()) -= w; }
inline void dec_reward(literal lit, double w) { reward(lit.var()) -= w; }
void check_with_plugin();
void check_without_plugin();