controlling-the-randomness

[MortezaRezaalipour]

There's a way that we can make the experiments more isolated; constant optimize vs. constant never.

When running the following script (which is essentially runs constant never and constant optimize for the benchmark abs_diff_i20_o10.v) I get two different type of subgraph in the subgraph extraction, also surprisingly, labeling time is not the same as well. To fix this problem, right before defining a Solver (or Optimize) object, we can set a the random seed manually using this command set_param('sat.random_seed', 42) and it will control the randomness of z3; I did it and both commands resulted the same Verilogs, subgraphs, etc.

PYTHON='python3'
SCRIPT='main.py'
BENCH='input/ver/abs_diff_i20_o10.v'
IMAX=6
OMAX=3
LPP=6
PPO=6
MODE=55
N_MODELS=1
ENCODING='z3bvec'
ET_PARTITIONING='asc'
TEMPLATE='nonshared'
ET8=512

CONSTANTS='optimize'
$PYTHON $SCRIPT $BENCH --subxpat --template=$TEMPLATE --parallel --min-labeling  --error-partitioning=$ET_PARTITIONING --encoding=$ENCODING --constants=$CONSTANTS --wanted-models=$N_MODELS --output-max=$OMAX --input-max=$IMAX  --max-lpp=$LPP --max-ppo=$PPO --extraction-mode=$MODE -e=$ET8 --clean

CONSTANTS='never'
$PYTHON $SCRIPT $BENCH --subxpat --template=$TEMPLATE --parallel --min-labeling  --error-partitioning=$ET_PARTITIONING --encoding=$ENCODING --constants=$CONSTANTS --wanted-models=$N_MODELS --output-max=$OMAX --input-max=$IMAX  --max-lpp=$LPP --max-ppo=$PPO --extraction-mode=$MODE -e=$ET8

HERE ARE THE RESULTS FOR TWO CASES:

1.W/O SEED SET (the current version of the code we have)

2.WITH SEED SET