CBMC
solver.h File Reference

Equality Propagation. More...

#include <vector>
+ Include dependency graph for solver.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  solver_optionst
 

Enumerations

enum class  solver_resultt { ALL_PASS , SOME_FAIL , ERROR }
 

Functions

solver_resultt solver (const std::vector< exprt > &, const solver_optionst &, const namespacet &)
 

Detailed Description

Equality Propagation.

Definition in file solver.h.

Enumeration Type Documentation

◆ solver_resultt

enum solver_resultt
strong
Enumerator
ALL_PASS 
SOME_FAIL 
ERROR 

Definition at line 20 of file solver.h.

Function Documentation

◆ solver()

solver_resultt solver ( const std::vector< exprt > &  constraints,
const solver_optionst solver_options,
const namespacet ns 
)

Definition at line 107 of file solver.cpp.