WitnessSelection.h File Reference

#include "WitgenDriver.h"
#include "llzk/Dialect/Function/IR/Ops.h"
#include "llzk/Dialect/Struct/IR/Ops.h"
#include <llvm/ADT/SmallVector.h>
#include <llvm/Support/Error.h>
#include <llvm/Support/JSON.h>
#include <string>

Include dependency graph for WitnessSelection.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	llzk::witgen::InputBinding
	Describe one JSON-visible main input binding. More...
struct	llzk::witgen::OutputBinding
	Describe one selected witness output leaf. More...

Namespaces
namespace	llzk
namespace	llzk::witgen

Functions
bool	llzk::witgen::memberIsSignal (component::StructDefOp owner, component::MemberDefOp member)
	Return true iff the member is considered a witness signal.
llvm::SmallVector< InputBinding >	llzk::witgen::collectInputBindings (function::FuncDefOp computeFunc)
	Collect stable JSON bindings for the main compute inputs.
mlir::FailureOr< llvm::SmallVector< OutputBinding > >	llzk::witgen::collectOutputBindings (component::StructDefOp mainDef, mlir::SymbolTableCollection &tables, mlir::Operation *origin, OutputScope scope)
	Collect the selected output bindings for the requested scope.
llvm::json::Value	llzk::witgen::buildSignalsJSONObject (llvm::ArrayRef< OutputBinding > bindings, llvm::ArrayRef< llvm::json::Value > serializedLeaves)
	Assemble a nested JSON object from selected witness leaves.