undefined | Better HN

0 pointsAnimats3mo ago0 comments

Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.

0 comments

porcoda3mo ago

I assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.

j / k navigate · click thread line to collapse

0 pointsAnimats3mo ago0 comments

Yes. Been there, done that, with the pre-ACL2 Boyer-Moore prover. We had the Oppen-Nelson prover (the first SAT solver) handling the easy stuff, and used the Boyer-Moore prover for the hard stuff. Not that much manual work.

0 comments

porcoda3mo ago

I assume you mean first SMT solver when you refer to Oppen-Nelson? I thought their contribution was the basis for SMT methods.

j / k navigate · click thread line to collapse