Hi guy, I am author of Spur , I want to share the Spur solver which is backed by z3 for neuro-symbolic reasoning, combining probabilistic language models with mathematical constraint solvingThe ideal here : LLM will give out constranst and translate the constranst to the z3 SMT language, then give out feedback loop between LLM model and neuro-symbolic reasoning to give out better reasioninglooking for feedback and comments from HNsThanks and best regards Kevin