Gymbo

Public Member Functions | Public Attributes | List of all members
gymbo::BaseExecutor Struct Referenceabstract

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

`#include <symbolic.h>`

Inheritance diagram for gymbo::BaseExecutor:
[legend]
Collaboration diagram for gymbo::BaseExecutor:
[legend]

## 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