Add lazy approach for handling lambdas in the HO extension (#7625)

This adds a new option --uf-lazy-ll for not applying lambda lifting eagerly. This is motivated by HO operators in theory of bags, e.g. bag.map, which cannot answer "sat" for simple problems where lambdas are mapped to bags, due to the introduction of quantified formulas for eliminating lambdas.

It moves lambda lifting from term formula removal to a utility module within TheoryUF. If lazy lambda lifting is enabled, this module does not introduce quantified formulas for lambdas eagerly.

It adds 2 lemma schemas for reasoning about quantifier-free constraints with lambdas natively in TheoryUF. It extends the model construction in the HoExtension to assign lambdas in the case that an equivalence class contains a variable that is defined by a lambda.

1 files changed, 16 insertions, 0 deletions

diff --git a/test/regress/regress0/ho/lazy-lambda-model.smt2 b/test/regress/regress0/ho/lazy-lambda-model.smt2
new file mode 100644
index 000000000..71df017e9
--- /dev/null
+++ b/test/regress/regress0/ho/lazy-lambda-model.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --uf-lazy-ll
+; EXPECT: sat
+(set-logic HO_ALL)
+(declare-fun g (Int) Int)
+(declare-fun h (Int) Int)
+(define-fun f ((x Int)) Int (ite (> x 0) (* 2 x) x))
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+
+(assert (or (= f g) (= f h)))
+
+(assert (and (= (h a) 26) (= (g b) 26)))
+
+(check-sat)