lundi 8 juillet 2019

How to add new constraint for existing declared function in z3 using c++?

I would like to know is there any way to add some new constraints for existing declared variables in the solver without getting the model.

For example, if I have 2 declare functions:

(declare-fun k!648 () (_ BitVec 8)) (declare-fun k!647 () (_ BitVec 8)) and some constraint with it.

How can I get their declared names generally?

Aucun commentaire:

Enregistrer un commentaire