CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
solvers Directory Reference
+ Directory dependency graph for solvers:

Directories

 bdd
 
 flattening
 
 floatbv
 
 lowering
 
 prop
 
 qbf
 
 refinement
 
 sat
 
 smt2
 
 smt2_incremental
 
 strings
 

Files

 conflict_provider.h
 Capability to check whether an expression is a reason for the solver returning UNSAT.
 
 decision_procedure.cpp
 Decision Procedure Interface.
 
 decision_procedure.h
 Decision Procedure Interface.
 
 hardness_collector.h
 Capability to collect the statistics of the complexity of individual solver queries.
 
 stack_decision_procedure.h
 Decision procedure with incremental solving with contexts and assumptions.