mirror of
https://github.com/Jaxan/satuio.git
synced 2025-04-26 22:27:46 +02:00
More consistent, and less output
This commit is contained in:
Joshua Moerman
parent
6660c8c3ed
commit
8e5553e8b1
6 changed files with 72 additions and 64 deletions
|
|
@ -48,7 +48,14 @@ python3 satuio/ads-core.py --help
|
|||
|
||||
The solver can be specified (as long as pysat supports it). The default is
|
||||
[Glucose3](https://www.labri.fr/perso/lsimon/glucose/), as that worked
|
||||
well on the examples.
|
||||
well on the examples. After a bit more testing, these work well: `g3`, `mc`,
|
||||
`m22`. These are okay: `gc3`, `gc4`, `g4`, `mgh`. And these were slow for me:
|
||||
`cd`, `lgl`, `mcb`, `mcm`, `mpl`, `mg3`.
|
||||
|
||||
The encoding currectly defaults to `seqcounter` for cardinality constraints.
|
||||
This seems to work just fine, and I am not even sure the encodings are really
|
||||
different for cardinality of `k=1`. It could be worth doing more testing to
|
||||
see which is the fastest.
|
||||
|
||||
|
||||
## Copyright
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
"""
|
||||
WIP script for returning the unsat core in the case an ADS does
|
||||
*not* exist. This could be merged into the main ads script,
|
||||
although there is an additional cost (presumably). Usage:
|
||||
although there is an additional cost (presumably). For now, this
|
||||
is mostyl copy-pasted from ads.py. Usage:
|
||||
|
||||
python3 ads-core.py --help
|
||||
|
||||
|
|
@ -21,6 +22,10 @@ from utils.parser import read_machine
|
|||
from utils.utils import *
|
||||
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(highlight=False)
|
||||
|
||||
|
||||
# *****************
|
||||
# Reading the input
|
||||
# *****************
|
||||
|
|
@ -41,7 +46,7 @@ if args.states == None or len(args.states) <= 1:
|
|||
states = args.states
|
||||
length = args.length
|
||||
|
||||
measure_time('Constructed automaton with', len(all_states), 'states and', len(alphabet), 'symbols')
|
||||
console.print(now(), f'Constructed automaton with [bold blue]{len(all_states)} states[/bold blue], [bold green]{len(alphabet)} symbols[/bold green] and Q_0 has [bold blue]{len(states)} states[/bold blue]')
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -100,7 +105,7 @@ def unique(lits):
|
|||
cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
|
||||
solver.append_formula(cnf.clauses)
|
||||
|
||||
measure_time('Setup solver', args.solver)
|
||||
console.print(now(), f'Solver {args.solver} ready for clauses')
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -114,7 +119,7 @@ measure_time('Setup solver', args.solver)
|
|||
# used to decide whether we found a different output.
|
||||
possible_outputs = {}
|
||||
possible_states = {}
|
||||
for s in tqdm(states, desc="CNF paths"):
|
||||
for s in tqdm(states, desc="CNF paths", leave=False):
|
||||
# current set of possible states we're in
|
||||
current_set = set([s])
|
||||
# set of successors for the next iteration of i
|
||||
|
|
@ -162,7 +167,7 @@ for s in tqdm(states, desc="CNF paths"):
|
|||
|
||||
# Now we will encode differences in outputs (and equal inputs, as
|
||||
# long as there is no difference).
|
||||
for s in tqdm(states, desc="CNF diffs"):
|
||||
for s in tqdm(states, desc="CNF diffs", leave=False):
|
||||
for t in states:
|
||||
# We skip s == t, since those state are equivalent.
|
||||
# I am not sure whether we can skip s <= t, since our construction
|
||||
|
|
@ -231,7 +236,7 @@ for s in tqdm(states, desc="CNF diffs"):
|
|||
solver.add_clause(enable_for_core + [-dvar(s, t, i), -ovar(s, i, o), -ovar(t, i, o)])
|
||||
|
||||
|
||||
measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
|
||||
console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
|
||||
|
||||
|
||||
# ******************
|
||||
|
|
@ -239,7 +244,6 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
|
|||
# ******************
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(markup=False, highlight=False)
|
||||
max_state_length = max([len(str) for str in states])
|
||||
|
||||
# Solve it!
|
||||
|
|
@ -249,17 +253,17 @@ solution = False
|
|||
while current_states and not solution:
|
||||
enabled_states = [evar(s) for s in current_states]
|
||||
solution = solver.solve(assumptions=enabled_states)
|
||||
measure_time('Solver finished')
|
||||
console.print(now(), 'Solver finished')
|
||||
|
||||
# If there is no solution, we can exit. As far as I know
|
||||
# there is no relevant information in the "core", as there
|
||||
# are no assumptions used in our encoding.
|
||||
if solution:
|
||||
console.print('! ADS of length', length, 'for', len(current_states), 'states exists', style='bold green')
|
||||
measure_total_time('Done')
|
||||
console.print(f'! ADS of length {length} for {len(current_states)} states exists', style='bold green')
|
||||
console.print(now(), 'Done')
|
||||
exit()
|
||||
|
||||
console.print('! no ADS of length', length, 'for', len(current_states), 'states', style='bold red')
|
||||
console.print(f'! no ADS of length {length} for {len(current_states)} states', style='bold red')
|
||||
|
||||
core = solver.get_core()
|
||||
core_set = set()
|
||||
|
|
@ -269,11 +273,11 @@ while current_states and not solution:
|
|||
|
||||
core_states = [s for s in states if evar(s) in core_set]
|
||||
fine_states = [s for s in states if evar(s) not in core_set]
|
||||
print(len(core_states), 'states in the unsat core')
|
||||
print('core states =', core_states)
|
||||
print('fine states =', fine_states)
|
||||
console.print(f'{len(core_states)} states in the unsat core')
|
||||
console.print(f'core states = {core_states}')
|
||||
console.print(f'fine states = {fine_states}')
|
||||
|
||||
current_states = fine_states
|
||||
|
||||
|
||||
measure_total_time('Done')
|
||||
console.print(now(), 'Done')
|
||||
|
|
|
|||
|
|
@ -26,6 +26,11 @@ from tqdm import tqdm # Import fancy progress bars
|
|||
|
||||
from utils.parser import read_machine
|
||||
from utils.utils import *
|
||||
import random
|
||||
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(highlight=False)
|
||||
|
||||
|
||||
# *****************
|
||||
|
|
@ -38,19 +43,25 @@ parser.add_argument('filename', help='File of the mealy machine (dot format)')
|
|||
parser.add_argument('length', help='Length of the ADS', type=int)
|
||||
parser.add_argument('-v', '--verbose', help='Show more output', action='store_true')
|
||||
parser.add_argument('--show-differences', help='Show even more output', action='store_true')
|
||||
parser.add_argument('--random-base', help='Chooses a random base', action='store_true')
|
||||
parser.add_argument('--base-size', type=int)
|
||||
parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3')
|
||||
parser.add_argument('--states', help='For which states to compute an ADS', nargs='+')
|
||||
args = parser.parse_args()
|
||||
|
||||
if args.states == None or len(args.states) <= 1:
|
||||
raise ValueError('Should specify at least 2 states')
|
||||
|
||||
# reading the automaton
|
||||
(alphabet, outputs, all_states, delta, labda) = read_machine(args.filename)
|
||||
states = args.states
|
||||
length = args.length
|
||||
|
||||
measure_time('Constructed automaton with', len(all_states), 'states and', len(alphabet), 'symbols')
|
||||
if args.random_base and args.base_size > 1:
|
||||
states = random.sample(all_states, k=args.base_size)
|
||||
elif len(args.states) > 1:
|
||||
states = args.states
|
||||
else:
|
||||
raise ValueError('Should specify at least 2 states')
|
||||
|
||||
console.print(now(), f'Constructed automaton with [bold blue]{len(all_states)} states[/bold blue], [bold green]{len(alphabet)} symbols[/bold green] and Q_0 has [bold blue]{len(states)} states[/bold blue]')
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -102,7 +113,7 @@ def unique(lits):
|
|||
cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
|
||||
solver.append_formula(cnf.clauses)
|
||||
|
||||
measure_time('Setup solver', args.solver)
|
||||
console.print(now(), f'Solver {args.solver} ready for clauses')
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -116,7 +127,7 @@ measure_time('Setup solver', args.solver)
|
|||
# used to decide whether we found a different output.
|
||||
possible_outputs = {}
|
||||
possible_states = {}
|
||||
for s in tqdm(states, desc="CNF paths"):
|
||||
for s in tqdm(states, desc="CNF paths", leave=False):
|
||||
# current set of possible states we're in
|
||||
current_set = set([s])
|
||||
# set of successors for the next iteration of i
|
||||
|
|
@ -164,7 +175,7 @@ for s in tqdm(states, desc="CNF paths"):
|
|||
|
||||
# Now we will encode differences in outputs (and equal inputs, as
|
||||
# long as there is no difference).
|
||||
for s in tqdm(states, desc="CNF diffs"):
|
||||
for s in tqdm(states, desc="CNF diffs", leave=False):
|
||||
for t in states:
|
||||
# We skip s == t, since those state are equivalent.
|
||||
# I am not sure whether we can skip s <= t, since our construction
|
||||
|
|
@ -230,7 +241,7 @@ for s in tqdm(states, desc="CNF diffs"):
|
|||
solver.add_clause([-dvar(s, t, i), -ovar(s, i, o), -ovar(t, i, o)])
|
||||
|
||||
|
||||
measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
|
||||
console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
|
||||
|
||||
|
||||
# ******************
|
||||
|
|
@ -238,19 +249,18 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
|
|||
# ******************
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(markup=False, highlight=False)
|
||||
max_state_length = max([len(str) for str in states])
|
||||
|
||||
# Solve it!
|
||||
solution = solver.solve()
|
||||
measure_time('Solver finished')
|
||||
console.print(now(), 'Solver finished')
|
||||
|
||||
# If there is no solution, we can exit. As far as I know
|
||||
# there is no relevant information in the "core", as there
|
||||
# are no assumptions used in our encoding.
|
||||
if not solution:
|
||||
console.print('! no ADS of length', length, style='bold red')
|
||||
measure_total_time('Done')
|
||||
console.print(now(), 'Done')
|
||||
exit()
|
||||
|
||||
# Get the set of true variables
|
||||
|
|
@ -351,17 +361,14 @@ def extract_tree(initial_set, level):
|
|||
def print_tree(console, tree, left=''):
|
||||
# The leaf is inlined in the printing
|
||||
if 'leaf' in tree:
|
||||
console.print('> state', end=' ')
|
||||
console.print(tree['leaf'], style='bold blue')
|
||||
console.print(f'> state [bold blue]{tree["leaf"]}[/bold blue]')
|
||||
else:
|
||||
# The next input symbol is also inlined
|
||||
console.print('> ', end='')
|
||||
console.print(tree['split_symbol'], end='', style='bold green')
|
||||
console.print(f'> [bold green]{tree["split_symbol"]}[/bold green]', end='')
|
||||
# We contract single-successor paths in the tree
|
||||
while len(tree['subtree']) == 1:
|
||||
tree = some_elem(tree['subtree'].values())
|
||||
console.print(' - ', end='')
|
||||
console.print(tree['split_symbol'], end='', style='bold green')
|
||||
console.print(f' - [bold green]{tree["split_symbol"]}[/bold green]', end='')
|
||||
else:
|
||||
console.print()
|
||||
counter = len(tree['subtree'])
|
||||
|
|
@ -381,7 +388,7 @@ print_tree(console, extract_tree(states, 0))
|
|||
print('')
|
||||
|
||||
# Report some final stats
|
||||
measure_total_time('Done')
|
||||
console.print(now(), 'Done')
|
||||
|
||||
|
||||
# TODO: we know that dvar(s, t, i) is an equivalence relation for
|
||||
|
|
|
|||
|
|
@ -44,6 +44,7 @@ parser.add_argument('--time', help='Upper bound on search time (ms)', type=int)
|
|||
parser.add_argument('--solver', help='Which solver to use (default g3)', default='g3')
|
||||
parser.add_argument('--bases', help='For which states to compute an UIO (leave empty for all states)', nargs='*')
|
||||
parser.add_argument('--log', help='Enable the additional log file', action='store_true')
|
||||
parser.add_argument('-v', '--verbose', help='Show more output', action='store_true')
|
||||
args = parser.parse_args()
|
||||
|
||||
# reading the automaton
|
||||
|
|
@ -255,7 +256,7 @@ while True:
|
|||
# and we also record the outputs along this path. The outputs are later
|
||||
# used to decide whether we found a different output.
|
||||
possible_outputs = {}
|
||||
for s in tqdm(states, desc="CNF paths", leave=False):
|
||||
for s in tqdm(states, desc="CNF paths", leave=args.verbose):
|
||||
# current set of possible states we're in
|
||||
current_set = set([s])
|
||||
# set of successors for the next iteration of i
|
||||
|
|
@ -307,7 +308,7 @@ while True:
|
|||
# Also note, we only encode the converse: if there is a difference claimed
|
||||
# and base has a certain output, than the state should not have that output.
|
||||
# This means that the solver doesn't report all differences, but at least one.
|
||||
for s in tqdm(states, desc="CNF diffs", leave=False):
|
||||
for s in tqdm(states, desc="CNF diffs", leave=args.verbose):
|
||||
# Constraint: there is a place, such that there is a difference in output
|
||||
# \/_i x_('e', s, i)
|
||||
# If s is our base, we don't care (this can be done, because only
|
||||
|
|
@ -347,7 +348,7 @@ while True:
|
|||
# We want to find an UIO for each base. We have already constructed
|
||||
# the CNF. So it remains to add assumptions to the solver, this is
|
||||
# called "incremental solving" in SAT literature.
|
||||
for base in tqdm(bases, desc='solving', leave=False):
|
||||
for base in tqdm(bases, desc='solving', leave=args.verbose):
|
||||
# If we run out of time, stop solving (but finish other stuff)
|
||||
if args.time and time_since_start() * 1000 > args.time:
|
||||
break
|
||||
|
|
@ -393,7 +394,7 @@ for (s, uio) in uios.items():
|
|||
console.print('')
|
||||
|
||||
# Report some final stats
|
||||
measure_total_time('\nDone')
|
||||
console.print(now(), 'Done')
|
||||
console.print(f'uios found: {100*len(uios)/len(states):.0f}%')
|
||||
console.print(f'avg length: {sum([len(uio) for uio in uios.values()])/len(uios):.3}')
|
||||
|
||||
|
|
|
|||
|
|
@ -23,6 +23,10 @@ from utils.parser import read_machine
|
|||
from utils.utils import *
|
||||
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(highlight=False)
|
||||
|
||||
|
||||
# *****************
|
||||
# Reading the input
|
||||
# *****************
|
||||
|
|
@ -47,7 +51,7 @@ else:
|
|||
|
||||
length = args.length
|
||||
|
||||
measure_time('Constructed automaton with', len(states), 'states and', len(alphabet), 'symbols')
|
||||
console.print(now(), f'Constructed automaton with {len(states)} states and {len(alphabet)} symbols')
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -104,7 +108,7 @@ def unique(lits):
|
|||
cnf = CardEnc.equals(lits, 1, vpool=vpool, encoding=EncType.seqcounter)
|
||||
solver.append_formula(cnf.clauses)
|
||||
|
||||
measure_time('Setup solver', args.solver)
|
||||
console.print(now(), 'Setup solver', args.solver)
|
||||
|
||||
|
||||
# ********************
|
||||
|
|
@ -125,7 +129,7 @@ unique([bvar(base) for base in bases])
|
|||
# and we also record the outputs along this path. The outputs are later
|
||||
# used to decide whether we found a different output.
|
||||
possible_outputs = {}
|
||||
for s in tqdm(states, desc="CNF paths"):
|
||||
for s in tqdm(states, desc="CNF paths", leave=args.verbose):
|
||||
# current set of possible states we're in
|
||||
current_set = set([s])
|
||||
# set of successors for the next iteration of i
|
||||
|
|
@ -177,7 +181,7 @@ for s in tqdm(states, desc="CNF paths"):
|
|||
# Also note, we only encode the converse: if there is a difference claimed
|
||||
# and base has a certain output, than the state should not have that output.
|
||||
# This means that the solver doesn't report all differences, but at least one.
|
||||
for s in tqdm(states, desc="CNF diffs"):
|
||||
for s in tqdm(states, desc="CNF diffs", leave=args.verbose):
|
||||
# Constraint: there is a place, such that there is a difference in output
|
||||
# \/_i x_('e', s, i)
|
||||
# If s is our base, we don't care (this can be done, because only
|
||||
|
|
@ -207,7 +211,7 @@ for s in tqdm(states, desc="CNF diffs"):
|
|||
if o in outputs_s:
|
||||
solver.add_clause([-bv, -evar(s, i), -ovar(base, i, o), -ovar(s, i, o)])
|
||||
|
||||
measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver.nof_vars(), 'variables')
|
||||
console.print(now(), f'Constructed CNF with {solver.nof_clauses()} clauses and {solver.nof_vars()} variables')
|
||||
|
||||
|
||||
# ******************
|
||||
|
|
@ -215,7 +219,6 @@ measure_time('Constructed CNF with', solver.nof_clauses(), 'clauses and', solver
|
|||
# ******************
|
||||
|
||||
# We set up some things for nice output
|
||||
console = Console(markup=False, highlight=False)
|
||||
max_state_length = max([len(str) for str in states])
|
||||
|
||||
# We count the number of uios
|
||||
|
|
@ -225,20 +228,17 @@ num_uios = {True: 0, False: 0}
|
|||
# the CNF. So it remains to add assumptions to the solver, this is
|
||||
# called "incremental solving" in SAT literature.
|
||||
for base in bases:
|
||||
console.print('')
|
||||
console.print('*** UIO for state', base, style='bold blue')
|
||||
|
||||
# Solve with bvar(base) being true
|
||||
b = solver.solve(assumptions=[bvar(base)])
|
||||
num_uios[b] = num_uios[b] + 1
|
||||
measure_time('Solver finished')
|
||||
console.print(now(), f'Solved for [bold blue]{base}[/bold blue]')
|
||||
|
||||
if b:
|
||||
# Get the set of true variables
|
||||
truth = get_truth(solver)
|
||||
|
||||
# We print the word
|
||||
console.print('! UIO of length', length, style='bold green')
|
||||
console.print(f' UIO of length {length}: ', end='')
|
||||
for i in range(length):
|
||||
for a in alphabet:
|
||||
if avar(i, a) in truth:
|
||||
|
|
@ -269,13 +269,13 @@ for base in bases:
|
|||
console.print('')
|
||||
|
||||
else:
|
||||
console.print('! no UIO of length', length, style='bold red')
|
||||
console.print(f' no UIO of length {length}', style='bold red')
|
||||
# The core returned by the solver is not interesting:
|
||||
# It is only the assumption (i.e. bvar).
|
||||
|
||||
print('')
|
||||
|
||||
# Report some final stats
|
||||
measure_total_time('\nDone')
|
||||
print('With UIO:', num_uios[True])
|
||||
print('without: ', num_uios[False])
|
||||
console.print(now(), 'Done')
|
||||
console.print('With UIO:', num_uios[True])
|
||||
console.print('without: ', num_uios[False])
|
||||
|
|
|
|||
|
|
@ -13,17 +13,6 @@ from time import time
|
|||
start = time()
|
||||
start_total = start
|
||||
|
||||
def measure_time(*str):
|
||||
global start
|
||||
now = time()
|
||||
print('***', *str, "in %.3f seconds" % (now - start))
|
||||
start = now
|
||||
|
||||
def measure_total_time(*str):
|
||||
global start_total
|
||||
now = time()
|
||||
print('***', *str, ": total time = %.3f seconds" % (now - start_total))
|
||||
|
||||
def time_since_start():
|
||||
return time() - start_total
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue