ConstraintSolver Class Reference

The class uses the Z3 solver to generate packing for a set of PHV fields given a set of constraints. More...

#include <bridged_packing.h>

Public Member Functions
	ConstraintSolver (const PhvInfo &p, z3::context &context, z3::optimize &solver, PackingConstraints &pc, AllConstraints &constraints, DebugInfo &dbg)
void	add_constraints (cstring, ordered_set< const PHV::Field * > &)
void	add_mutually_aligned_constraints (ordered_set< const PHV::Field * > &)
void	print_assertions ()
ordered_map< cstring, std::vector< const PHV::Field * > >	solve (ordered_map< cstring, ordered_set< const PHV::Field * > > &)

Detailed Description

The class uses the Z3 solver to generate packing for a set of PHV fields given a set of constraints.

The constraints for the Z3 solver are determined using the information from PhvInfo for the set of PHV fields delivered using the ConstraintSolver::add_constraints and ConstraintSolver::add_mutually_aligned_constraints methods.

The method ConstraintSolver::solve executes the Z3 solver and it returns, for each header, a vector of fields whose offset is adjusted based on the solution of the Z3 solver with padding fields inserted where necessary.

Logging options

-Tbridged_packing:1	The fields the constraints are being added for to the Z3 solver The constraints being added to the Z3 solver
-Tbridged_packing:3	The Z3 solver model in the case of a satisfied solution The Z3 solver core in the case of an unsatisfied solution
-Tbridged_packing:5	The Z3 solver assertions

Precondition

Up-to-date PhvInfo.

Member Function Documentation

add_constraints()

void ConstraintSolver::add_constraints	(	cstring	hdr,
		ordered_set< const PHV::Field * > &	fields )

Initializes the Z3 solver with constraints from PhvInfo (except for the mutually aligned constraint, which is handled with ConstraintSolver::add_mutually_aligned_constraints).

Computes upper bound of the overall size of all fields, which is used as a constraint to Z3 solver in the ConstraintSolver::add_field_alignment_constraints method. It assumes that each field is padded to next byte boundary.

When a 'small' bridged field must be packed into a large container, we must extend the upper bound by the size of the large container, instead of the round-up value based on the bridge field size.

add_mutually_aligned_constraints()

void ConstraintSolver::add_mutually_aligned_constraints

(

ordered_set< const PHV::Field * > &

fields

)

Initializes the Z3 solver with mutually aligned constraints from PhvInfo.

solve()

ordered_map< cstring, std::vector< const PHV::Field * > > ConstraintSolver::solve

(

ordered_map< cstring, ordered_set< const PHV::Field * > > &

fields

)

Executes the Z3 solver.

Parameters

[in]

fields

For each header, an ordered set of fields to be packed based on the solution of the Z3 solver.

Returns

For each header, a vector of fields whose offset is adjusted based on the solution of the Z3 solver with padding fields inserted where necessary.