- Apr 22, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Directly add memory constraints for init states.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
maybe_sat seems to be broken (see assume_regression test)
-
Marek Chalupa authored
(at least some)
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
In joining states, just assume that the state is feasible after some time of solving.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We do not know what to do else.
-
Marek Chalupa authored
The check was not called as it was in a wrong instance of method.
-
Marek Chalupa authored
Forgot to add this to git.
-
Marek Chalupa authored
Not in parser, the calls may be unreachable.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We store 1b values into 1B values, which is not nice and must be taken care of.
-
- Apr 21, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
We must remember the initial value of reads so that we can do the substitutions correctly.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We must match together only inputs, not all nondets.
-
Marek Chalupa authored
Every subclass just will call _copy_to that copies the new attributes and the old attributes are copied in super()._copy_to.
-
Marek Chalupa authored
-
Marek Chalupa authored
Always do eval, we did that internally too.
-
Marek Chalupa authored
It reveals a bug in BSE.
-
- Apr 20, 2021
-
-
Marek Chalupa authored
Call is_sat() from state, not from the solver. Otherwise we'll get no try_hard.
-
Marek Chalupa authored
-
Marek Chalupa authored
This was an artifact of past times.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-