Home
last modified time | relevance | path

Searched refs:unfixed_vars (Results 1 – 4 of 4) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_solver.cpp4371 bool_var_set unfixed_vars; in get_bounded_consequences() local
4374 unfixed_vars.insert(v); in get_bounded_consequences()
4395 extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); in get_bounded_consequences()
4413 extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); in get_bounded_consequences()
4433 bool_var_set unfixed_vars; in get_consequences() local
4435 unfixed_vars.insert(lit.var()); in get_consequences()
4457 update_unfixed_literals(unfixed_lits, unfixed_vars); in get_consequences()
4514 delete_unfixed(unfixed_lits, unfixed_vars); in get_consequences()
4516 update_unfixed_literals(unfixed_lits, unfixed_vars); in get_consequences()
4540 unfixed_vars.remove(lit.var()); in delete_unfixed()
[all …]
H A Dsat_solver.h764 void delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
774 void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_solver.cpp4319 bool_var_set unfixed_vars;
4322 unfixed_vars.insert(v);
4343 extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
4361 extract_fixed_consequences(num_units, asms, unfixed_vars, conseq);
4381 bool_var_set unfixed_vars;
4383 unfixed_vars.insert(lit.var());
4405 update_unfixed_literals(unfixed_lits, unfixed_vars);
4462 delete_unfixed(unfixed_lits, unfixed_vars);
4464 update_unfixed_literals(unfixed_lits, unfixed_vars);
4488 unfixed_vars.remove(lit.var());
[all …]
H A Dsat_solver.h722 void delete_unfixed(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
732 void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);