Closed dblotsky closed 6 years ago
@FedericoAureliano this should be ready for review. It actually produces valid problems now! The downside is that it sometimes adds something like (assert (not true))
or (assert (< var0 var0))
and the problem becomes doomed.
I think it warrants a catch for trivially unsat things like this eventually. :/
Other changes:
smt_sat
tosmt_check_sat
smt_model
tosmt_get_model
coin_toss()
andrandom_string()
intoutil.py
This addresses #18.
NOTE: still working on
--meaningful
flag.