gymbo::PSExecutor Struct Reference

Represents a derived class for symbolic execution engine for probabilistic programs. More...

#include <psymbolic.h>

Inheritance diagram for gymbo::PSExecutor:

Collaboration diagram for gymbo::PSExecutor:

Public Member Functions
void	register_random_var (int var_id)
bool	solve (bool is_target, int pc, SymState &state)
	Solves path constraints and updates the symbolic state. More...
Trace	run (Prog &prog, std::unordered_set< int > &target_pcs, SymState &state, int maxDepth=256)
	Run probabilistic symbolic execution on a program. More...
	BaseExecutor (GDOptimizer optimizer, int maxSAT=256, int maxUNSAT=256, int max_num_trials=10, bool ignore_memory=false, bool use_dpll=false, int verbose_level=0, bool return_trace=false)
	Constructor for BaseExecutor. More...
Public Member Functions inherited from gymbo::BaseExecutor
	BaseExecutor (GDOptimizer optimizer, int maxSAT=256, int maxUNSAT=256, int max_num_trials=10, bool ignore_memory=false, bool use_dpll=false, int verbose_level=0, bool return_trace=false)
	Constructor for BaseExecutor. More...

Public Attributes
std::unordered_set< int >	random_vars
	Set of random variables'IDs. More...
PathConstraintsTable	constraints_cache
	Cache for storing and reusing path constraints. More...
ProbPathConstraintsTable	prob_constraints_table
Public Attributes inherited from gymbo::BaseExecutor
GDOptimizer	optimizer
int	maxSAT
	The maximum number of SAT constraints to collect. More...
int	maxUNSAT
	The maximum number of UNSAT constraints to collect. More...
int	max_num_trials
int	verbose_level
	The level of verbosity. More...
bool	ignore_memory
bool	use_dpll
bool	return_trace

Detailed Description

Represents a derived class for symbolic execution engine for probabilistic programs.

Member Function Documentation

BaseExecutor()

gymbo::BaseExecutor::BaseExecutor

inline

Constructor for BaseExecutor.

Parameters

optimizer	The gradient descent optimizer for parameter optimization.
maxSAT	The maximum number of SAT constraints to collect.
maxUNSAT	The maximum number of UNSAT constraints to collect.
max_num_trials	The maximum number of trials for each gradient descent.
ignore_memory	If set to true, constraints derived from memory will be ignored.
use_dpll	If set to true, use DPLL to decide the initial assignment for each term.
verbose_level	The level of verbosity.
return_trace	If set to true, save the trace at each pc and return them (default false).

register_random_var()

void gymbo::PSExecutor::register_random_var ( int  var_id )

inline

run()

Trace gymbo::PSExecutor::run ( Prog &  prog, std::unordered_set< int > &  target_pcs, SymState &  state, int  maxDepth = 256  )

inlinevirtual

Run probabilistic symbolic execution on a program.

This function performs probabilistic symbolic execution on a given program, considering variable distributions, symbolic states, and path constraints. It explores different execution paths and updates the constraints and probabilities accordingly.

Parameters

prog	The program to symbolically execute.
target_pcs	Set of pc where gymbo executes path-constraints solving. If this set is empty or contains -1, gymbo solves all path-constraints.
state	The initial symbolic state for execution.
maxDepth	Maximum exploration depth during symbolic execution.

Returns

The symbolic execution trace containing states and child traces.

Implements gymbo::BaseExecutor.

solve()

bool gymbo::PSExecutor::solve ( bool  is_target, int  pc, SymState &  state  )

inlinevirtual

Solves path constraints and updates the symbolic state.

This function checks the satisfiability of the path constraints using an SMT solver or a probabilistic branching algorithm. It updates the symbolic state based on the result and stores the solution in a cache for future use.

Parameters

is_target	Whether the program counter is a target.
pc	The program counter.
state	The symbolic state.

Returns

Flag indicating satisfifiability.

Implements gymbo::BaseExecutor.

Member Data Documentation

constraints_cache

PathConstraintsTable gymbo::PSExecutor::constraints_cache

Cache for storing and reusing path constraints.

prob_constraints_table

ProbPathConstraintsTable gymbo::PSExecutor::prob_constraints_table

Table for storing probabilistic path constraints.

random_vars

std::unordered_set<int> gymbo::PSExecutor::random_vars

Set of random variables'IDs.

---

The documentation for this struct was generated from the following file:

• libgymbo/psymbolic.h