These do more or less the same thing, so generalizing the mechanism to create constraints to cover axioms can be nice. I did an attempt to do this in the generalizedConstraints branch; alas it complicated things a lot since constrain can no longer take a simple boolean, forcing us to create a class around it, which then generated unnecessarily complicated code. Since constrain is a very common call, I'd like the existing uses of it to generate the exact same code. It feels like this should be doable, but it's a tricky thing to pull off.
The current story is simpler, since addAxiom generates a definition that we pretty much spit out (after tope-sorting with all other user given definitions). When merged with constraints, we lose that, as it needs to return an SBool that can be passed around, which proved difficult. So, perhaps keeping SBool and a forall/exists construct separate has its benefits too. In a sense, we're generalizing SBool to mean a quantified term; which is probably not worth the cost.
Still, it might be worth revisiting this at some point.
LeventErkok
commented
1 year ago
Can we unify
addAxiomandconstrain?These do more or less the same thing, so generalizing the mechanism to create constraints to cover axioms can be nice. I did an attempt to do this in the
generalizedConstraintsbranch; alas it complicated things a lot since constrain can no longer take a simple boolean, forcing us to create a class around it, which then generated unnecessarily complicated code. Sinceconstrainis a very common call, I'd like the existing uses of it to generate the exact same code. It feels like this should be doable, but it's a tricky thing to pull off.The current story is simpler, since
addAxiomgenerates a definition that we pretty much spit out (after tope-sorting with all other user given definitions). When merged with constraints, we lose that, as it needs to return anSBoolthat can be passed around, which proved difficult. So, perhaps keepingSBooland aforall/existsconstruct separate has its benefits too. In a sense, we're generalizingSBoolto mean a quantified term; which is probably not worth the cost.Still, it might be worth revisiting this at some point.