P4C
The P4 Compiler
 
Loading...
Searching...
No Matches
Public Member Functions | List of all members
P4Tools::Z3Translator Class Reference

Translates P4 expressions into Z3. Any variables encountered are declared to a Z3 instance. More...

Inheritance diagram for P4Tools::Z3Translator:
Inheritance graph
[legend]

Public Member Functions

 Z3Translator (Z3Solver &solver)
 
z3::expr getResult ()
 
bool preorder (const IR::Add *op) override
 
bool preorder (const IR::BAnd *op) override
 
bool preorder (const IR::BoolLiteral *boolLiteral) override
 
bool preorder (const IR::BOr *op) override
 
bool preorder (const IR::BXor *op) override
 
bool preorder (const IR::Cast *cast) override
 Translates casts.
 
bool preorder (const IR::Cmpl *op) override
 
bool preorder (const IR::Concat *op) override
 
bool preorder (const IR::Constant *constant) override
 Translates constants.
 
bool preorder (const IR::Div *op) override
 
bool preorder (const IR::Equ *op) override
 
bool preorder (const IR::Geq *op) override
 
bool preorder (const IR::Grt *op) override
 
bool preorder (const IR::LAnd *op) override
 
bool preorder (const IR::Leq *op) override
 
bool preorder (const IR::LNot *op) override
 
bool preorder (const IR::LOr *op) override
 
bool preorder (const IR::Lss *op) override
 
bool preorder (const IR::Mod *op) override
 
bool preorder (const IR::Mul *op) override
 
bool preorder (const IR::Mux *op) override
 Building ternary operations.
 
bool preorder (const IR::Neg *op) override
 
bool preorder (const IR::Neq *op) override
 
bool preorder (const IR::Node *node) override
 Handles unexpected nodes.
 
bool preorder (const IR::Shl *op) override
 
bool preorder (const IR::Shr *op) override
 
bool preorder (const IR::Slice *op) override
 
bool preorder (const IR::StringLiteral *stringLiteral) override
 
bool preorder (const IR::Sub *op) override
 
bool preorder (const IR::SymbolicVariable *var) override
 Translates variables.
 
z3::expr translate (const IR::Expression *expression)
 Translate an P4C IR expression and return the Z3 equivalent.
 

Detailed Description

Translates P4 expressions into Z3. Any variables encountered are declared to a Z3 instance.

Constructor & Destructor Documentation

◆ Z3Translator()

P4Tools::Z3Translator::Z3Translator ( Z3Solver & solver)
explicit

Creates a Z3 translator. Any variables encountered during translation will be declared to the Z3 instance encapsulated within the given solver.

Member Function Documentation

◆ getResult()

z3::expr P4Tools::Z3Translator::getResult ( )
Returns
the result of the translation.