From 10082b3b379b45f12a78b1302bd2a44407c79d3a Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 6 Apr 2023 10:37:47 -0700 Subject: [PATCH 1/2] give more weightage to bool reasons during clause learning --- src/mcsat/bool/bool_plugin.c | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/mcsat/bool/bool_plugin.c b/src/mcsat/bool/bool_plugin.c index 1285fcf85..85c2d5484 100644 --- a/src/mcsat/bool/bool_plugin.c +++ b/src/mcsat/bool/bool_plugin.c @@ -94,6 +94,9 @@ typedef struct { /** Increase of the lemma limit after gc */ float lemma_limit_factor; + /** bump factor for bool vars -- geq 1. Higher number means more weightage **/ + uint32_t bool_var_bump_factor; + } heuristic_params; struct { @@ -126,6 +129,9 @@ void bool_plugin_heuristics_init(bool_plugin_t* bp) { // Clause database compact bp->heuristic_params.lemma_limit_init = 1000; bp->heuristic_params.lemma_limit_factor = 1.02; + + // Bool var scoring + bp->heuristic_params.bool_var_bump_factor = 5; } static @@ -749,8 +755,9 @@ term_t bool_plugin_explain_propagation(plugin_t* plugin, variable_t var, ivector } ivector_push(reasons, opposite_term(t_i)); - // Bump the reason variable - bp->ctx->bump_variable(bp->ctx, x_i); + // Bump the reason variable -- give more weightage to boolean reasons + bp->ctx->bump_variable_n(bp->ctx, x_i, + bp->heuristic_params.bool_var_bump_factor); } // Bump the clause as useful From 1c8923f4ba1cbbd4bec2914fcd2a1f7e60c47b25 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Thu, 6 Apr 2023 11:01:46 -0700 Subject: [PATCH 2/2] don't string match the produced interpolant -- it can change --- tests/regress/mcsat/nra/assumptions/issue261.smt2 | 2 +- tests/regress/mcsat/nra/assumptions/issue261.smt2.gold | 10 ---------- 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/tests/regress/mcsat/nra/assumptions/issue261.smt2 b/tests/regress/mcsat/nra/assumptions/issue261.smt2 index 4960cf8b7..9749609b9 100644 --- a/tests/regress/mcsat/nra/assumptions/issue261.smt2 +++ b/tests/regress/mcsat/nra/assumptions/issue261.smt2 @@ -1984,4 +1984,4 @@ e1979 )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (check-sat-assuming-model (v0) ((/ (- 75) 58))) -(get-unsat-model-interpolant) +;;(get-unsat-model-interpolant) diff --git a/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold b/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold index fe591fcf7..3f65111b0 100644 --- a/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold +++ b/tests/regress/mcsat/nra/assumptions/issue261.smt2.gold @@ -1,11 +1 @@ unsat -(or (< (+ -180841357257/2612 (* 444710031/2 (^ v0 2))) 0) (>= (* -1 (^ v0 2)) 0) (< (+ 2568250217007/5224 (* -1 v0)) 0) (= (^ v0 2) -1/27794700) - (>= (+ -1 (* -1 (^ v0 2))) 0) (>= (+ -3379123281/8 v0 (* -8906187/4 (^ v0 2))) 0) (>= (+ 222194717/3379123281 (* -2 (^ v0 2))) 0) - (>= (+ -162883/3379123281 (* -2 (^ v0 2))) 0) (< (+ -1/27794700 (* -1 v0)) 0) (= (^ v0 2) 222194717/3379123281) (= (^ v0 2) -6892) (< (^ v0 2) 0) - (= v0 104957259/1306) (= (^ v0 2) 180841357257/2612) (>= (+ -3379123281/8 v0) 0) (>= (+ 16152313/55589400 (* -3 (^ v0 2))) 0) (= (^ v0 2) 0) - (< (+ 6892 (* -1 (^ v0 2))) 0) (< (+ 1/27794700 (^ v0 2)) 0) (= (^ v0 2) -1/222357600) (= (^ v0 2) -1723/13516493124) (= (^ v0 2) 3379123281/16) - (>= (+ -3379123281/8 (* -1 (^ v0 2))) 0) (= (^ v0 2) 34985753/96798550081) (= (^ v0 2) -3446) - (>= (+ -22313794156579651/62614478572273800 (* -2 (^ v0 2))) 0) (< (+ -1/27794700 (* 3 (^ v0 2))) 0) (< (+ 18310751/34985753 (^ v0 2)) 0) - (< (+ -653/111178800 (* -1 v0)) 0) (>= (+ 1 (* -1 (^ v0 2))) 0) (< (+ 18310751/34985753 (* 3 (^ v0 2))) 0) (>= v0 0) (>= (+ -3379123281 (* 8 v0)) 0) - (>= (+ -180841357257 (* 2612 v0)) 0) (>= (+ -3379116389 (* 8 v0)) 0) (>= (+ -3379123281 (* 2612 (^ v0 2))) 0) (>= (+ 3446 (* -162883 (^ v0 2))) 0) - (>= (+ 162883 (* -6758246562 (^ v0 2))) 0) (>= (+ 16152313 (* -375686871433642800 (^ v0 2))) 0) (>= (+ 222194717 (* -751373742867285600 (^ v0 2))) 0))