From eb4ea606d55bd404a5d36a1eb9a4ae457a63f131 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 21 Jul 2023 14:55:29 +0200 Subject: [PATCH] notes on pvar justifications --- src/math/polysat/slicing.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index 6c4e011ea..24fa325ac 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -33,6 +33,13 @@ TODO: - implement query functions - when solver assigns value of a variable v, add equations with v substituted by its value? +TODO: better conflicts with pvar justification +- pvar justification is only introduced by add_value (when a variable is assigned in the model) +- so there can be at most two pvar justifications in a single conflict +- when explaining a conflict that contains pvars: + - single pvar x: the egraph has derived that x must have a different value c, learn literal x = c (instead of x != value(x) as is done now by the naive integration) + - two pvars x, y: learn literal x = y + */