FunctionDefinition.h

 
#pragma once
 
#include <concepts>
#include <cstddef>
#include <vector>
 
#include "dlinear/parser/smt2/Sort.h"
#include "dlinear/parser/smt2/Term.h"
#include "dlinear/symbolic/literal.h"
 
namespace dlinear::smt2 {
 
class FunctionDefinition {
 public:
  FunctionDefinition(std::vector<Variable> parameters, Sort return_type, Term body);
 
  Term operator()(const std::vector<Term>& arguments) const;
  Term operator()(std::same_as<Term> auto... arguments) const {
    if (parameters_.size() != sizeof...(arguments)) {
      throw std::runtime_error("This function definition expects #" + std::to_string(parameters_.size()) +
                               " arguments ({}). Provided #" + std::to_string(sizeof...(arguments)) + " arguments.");
    }
    Term t = body_;
 
    std::size_t i = 0;
    for (const Term& arg_i : {arguments...}) {
      const Variable& param_i{parameters_[i]};
      arg_i.Check(param_i.get_type());
      t = t.Substitute(param_i, arg_i);
      ++i;
    }
 
    return t;
  }
 
 private:
  std::vector<Variable> parameters_;  
  Sort return_type_;                  
  Term body_;                         
};
 
}  // namespace dlinear::smt2