SMT2 parser: lambda expressions

This uses the existing code for parsing bindings to parse lambda
expressions.

Author: kroening

regression/smt2_solver/function-applications/lambda1.desc

@@ -0,0 +1,7 @@
+CORE
+lambda1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/function-applications/lambda1.smt2

@@ -0,0 +1,14 @@
+(set-logic QF_BV)
+
+(define-const min (-> (_ BitVec 8) (_ BitVec 8) (_ BitVec 8))
+  (lambda ((a (_ BitVec 8)) (b (_ BitVec 8))) 
+    (ite (bvule a b) a b)))
+
+(define-fun p1 () Bool (= (min #x01 #x02) #x01))
+(define-fun p2 () Bool (= (min #xff #xfe) #xfe))
+
+; all must be true
+
+(assert (not (and p1 p2)))
+
+(check-sat)

src/solvers/smt2/smt2_parser.cpp

@@ -275,6 +275,12 @@ std::pair<binding_exprt::variablest, exprt> smt2_parsert::binding(irep_idt id)
   return {std::move(bindings), std::move(expr)};
 }
 
+exprt smt2_parsert::lambda_expression()
+{
+  auto binding = this->binding(ID_lambda);
+  return lambda_exprt(binding.first, binding.second);
+}
+
 exprt smt2_parsert::quantifier_expression(irep_idt id)
 {
   auto binding = this->binding(id);
@@ -972,6 +978,7 @@ void smt2_parsert::setup_expressions()
     return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32));
   };
 
+  expressions["lambda"] = [this] { return lambda_expression(); };
   expressions["let"] = [this] { return let_expression(); };
   expressions["exists"] = [this] { return quantifier_expression(ID_exists); };
   expressions["forall"] = [this] { return quantifier_expression(ID_forall); };

src/solvers/smt2/smt2_parser.h

@@ -164,6 +164,7 @@ class smt2_parsert
   exprt unary(irep_idt, const exprt::operandst &);
 
   std::pair<binding_exprt::variablest, exprt> binding(irep_idt);
+  exprt lambda_expression();
   exprt let_expression();
   exprt quantifier_expression(irep_idt);
   exprt function_application(