search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

How to determine if a `Term` requires SMT Theories #1340

Open weaversa opened 3 years ago

weaversa commented 3 years ago

Would it be possible for SAW to determine whether or not a Term is capable of being turned into an AIG or CNF? Some constructs such as the Integer type mean we can’t use SAT, we have to use SMT instead, but we don't currently have a way to know that. I’m wondering if SAW could have a function to determine if SMT is necessary.

Simple API could be just a SAWScript function like is_sat_predicate : Term -> Bool.

However, in talking with @robdockins, we identified a small extension - What4 already has a way to examine terms to see what SMT theories they require (CF https://github.com/GaloisInc/what4/blob/master/what4/src/What4/ProblemFeatures.hs). So, SAW could translate a Term to What4 and return a sequence of necessary SMT theories. If the list is empty, we would know that the Term is SAT-able. And, others may find the sequence of SMT theories useful in the future.

robdockins commented 3 years ago

1366 adds a new command that computes the features required for a problem, as translated by What4. It doesn't correctly identify uses of uninterpreted functions yet due to https://github.com/GaloisInc/what4/issues/139. I will leave this ticket open to track work on fixing this.

robdockins commented 3 years ago

https://github.com/GaloisInc/what4/issues/139 now has a fix. Once we bump the What4 submodule, it should be easy to add cases for uses of uninterpreted and defined functions.

robdockins commented 3 years ago

The what4 module has now been updated, so this should be pretty easy to fix now.