search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
114 stars 43 forks source link

Boolector Backend Substitution Function #303

Closed fangwenji closed 2 years ago

fangwenji commented 2 years ago

image Currently, the subsitution function in boolector solver backend doesn't support the term-->term substitution as the Pysmt does. I would like to ask that if I want to use the term-to-term substitution, is there any potential method? And when will the boolector solver support this kind of subsititution? Thank you so much!

yoni206 commented 2 years ago

Thanks for this question. You might want to check out the SubstitutionWalker, which allows you to perform arbitrary substitutions. Here is an example of its usage: https://github.com/stanford-centaur/smt-switch/blob/master/tests/unit/unit-substitute.cpp#L108

Feel free to follow up with more questions, we are happy to help.

fangwenji commented 2 years ago

That really helps! Thank you so much for your kind assistance!