Uses channels to add a timeout functionality for the read() function of the SMTProcess. This enables us to wait until we receive a signal on the channel before the timeout. We add a new error type SMTError::Timeout to enable the user to check if the solver timed out on the current set of constraints.
solver.solve_with_timeout(smt_proc, time_in_milliseconds) now allows us to provide an argument for time in ms. This has not been added to the SMTBackend trait and can be added in future versions. Also added a similar check_sat_with_timeout. This now makes read() take a Option argument for the timeout period.
Also fixes a bunch of compiler warnings.
Fixes an error in real_insts.rs where the string "s" was being written instead of the variable.
This PR aims to achieve the following:
Uses channels to add a timeout functionality for the read() function of the SMTProcess. This enables us to wait until we receive a signal on the channel before the timeout. We add a new error type
SMTError::Timeoutto enable the user to check if the solver timed out on the current set of constraints.solver.solve_with_timeout(smt_proc, time_in_milliseconds)now allows us to provide an argument for time in ms. This has not been added to the SMTBackend trait and can be added in future versions. Also added a similarcheck_sat_with_timeout. This now makesread()take a OptionAlso fixes a bunch of compiler warnings.
Fixes an error in
real_insts.rswhere the string "s" was being written instead of the variable.