From ecf25a4fe267cc7151a0f42ae0c7bbd8b6664b4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Dec 2022 14:57:52 -0800 Subject: [PATCH] outline scheme Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_eqs.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 1117ad0bcc..ad58239c3a 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -13,6 +13,24 @@ Module Name: Nikolaj Bjorner (nbjorner) 2022-11-2. +Notes: + +extract_subst is inefficient. +It traverses the same sub-terms many times. + +Outline of a presumably better scheme: + +1. maintain map FV: term -> bit-set where bitset reprsents set of free variables. Assume the number of variables is bounded. + FV is built from initial terms. +2. maintain parent: term -> term-list of parent occurrences. +3. repeat + pick x = t, such that x not in FV(t) + orient x -> t + for p in parent*(x): + FV(p) := FV(p) u FV(t) + if y = s is processed and x in FV(s) order y < x + if y = s is processed and x in FV(t) order x < y + --*/