Represents the base class for symbolic execution engine. More...

#include <symbolic.h>

Inheritance diagram for gymbo::BaseExecutor:

Collaboration diagram for gymbo::BaseExecutor:

Public Member Functions
	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...

virtual bool	solve (bool is_target, int pc, SymState &state)=0

virtual Trace	run (Prog &prog, std::unordered_set< int > &target_pcs, SymState &state, int maxDepth)=0

Public Attributes
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 the base class for symbolic execution engine.

Constructor & Destructor Documentation

◆ BaseExecutor()

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`
	)

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).

Member Function Documentation

◆ run()

virtual Trace gymbo::BaseExecutor::run	(	Prog &	prog,
		std::unordered_set< int > &	target_pcs,
		SymState &	state,
		int	maxDepth
	)

pure virtual

Implemented in gymbo::SExecutor, and gymbo::PSExecutor.

◆ solve()

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

pure virtual

Implemented in gymbo::SExecutor, and gymbo::PSExecutor.

Member Data Documentation

◆ ignore_memory

bool gymbo::BaseExecutor::ignore_memory

If set to true, constraints derived from memory will be ignored.

◆ max_num_trials

int gymbo::BaseExecutor::max_num_trials

The maximum number of trials for each gradient descent.

◆ maxSAT

int gymbo::BaseExecutor::maxSAT

The maximum number of SAT constraints to collect.

◆ maxUNSAT

int gymbo::BaseExecutor::maxUNSAT

The maximum number of UNSAT constraints to collect.

◆ optimizer

GDOptimizer gymbo::BaseExecutor::optimizer

The gradient descent optimizer for parameter optimization.

◆ return_trace

bool gymbo::BaseExecutor::return_trace

If set to true, save the trace at each pc and return them.

◆ use_dpll

bool gymbo::BaseExecutor::use_dpll

If set to true, use DPLL to decide the initial assignment for each term.

◆ verbose_level

int gymbo::BaseExecutor::verbose_level

The level of verbosity.

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

libgymbo/symbolic.h

Public Member Functions

Public Attributes