search

runtimeverification / rv-predict

Code for improved rv-predict and installer
BSD 3-Clause "New" or "Revised" License
2 stars 3 forks source link

abstract away how we interact with the solver #222

Closed yilongli closed 9 years ago

yilongli commented 9 years ago

In my opinion, it's easier to read and write.

yilongli commented 9 years ago

So what we really need is an interface for building formula. And then there are different backends that generate SMTLIB2 format text, Z3 objects, etc.

@traiansf would you like to work on this? I think it could be a good warm-up exercise to get familiar with the code in prediction engine.

traiansf commented 9 years ago

Yes, I think I'd like to work on that.

grosu commented 9 years ago

Guys, I talked to Cesare Tinelli, the guy behind CVC4, and he told me two things:

1) That he is not going to charge us any $ if we want to use CVC4 in our RV tools; and

2) That he and his team may even consider fixing things for us, or helping with developing new decision procedures, like the partial-order one that we need to RV-Predict.

So I would say as part of this experiment we should also consider playing a bit with various constraint solvers besides Z3, including Yaces! and especially CVC4.

yilongli commented 9 years ago

@grosu Of course. Once we abstract away the solver from our code that builds formula, it should be trivial to switch between different solvers.

grosu commented 9 years ago

Great. Note, however, that this used to work this way in the past (e.g., when we submitted the PLDI paper). We even collected like tens or hundreds of SMTLIB formula files in order to evaluate solvers on them. I think we would have maximum of flexibility it we allow RV-Predict to have an option to generate either of the two types of SMTLIB formats, and then to be able to call any solver on them (again, we had that in the past at some moment).

yilongli commented 9 years ago

Well, that's not exactly what I am proposing here. I should probably change the title of this issue. What I am proposing is to completely abstract away how we interact with the solver. No matter it's using text format or the solver's API. The way it worked before was to interact with the solver through SMTLIB format text only. This is still trivial to do but wouldn't help us to improve the modularity of our code. More importantly, it doesn't allow incremental solving, which is going to be important for us in the near future.

yilongli commented 9 years ago

fixed via https://github.com/runtimeverification/rv-predict/pull/333