CBMC
Loading...
Searching...
No Matches
Classes | Functions
solver.cpp File Reference

Solver. More...

#include "solver.h"
#include <util/format_expr.h>
#include "address_taken.h"
#include "generalization.h"
#include "inductiveness.h"
#include "report_properties.h"
#include "report_traces.h"
#include "solver_progress.h"
#include "solver_types.h"
#include <iostream>
+ Include dependency graph for solver.cpp:

Go to the source code of this file.

Classes

class   take_time_resourcet
 

Functions

void  solver (std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
 
solver_resultt  solver (const std::vector< exprt > &constraints, const solver_optionst &solver_options, const namespacet &ns)
 

Detailed Description

Solver.

Definition in file solver.cpp.

Function Documentation

◆  solver() [1/2]

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

Definition at line 107 of file solver.cpp.

◆  solver() [2/2]

void solver ( std::vector< framet > &  frames,
const std::unordered_set< symbol_exprt, irep_hash > &  address_taken,
const solver_optionst &  solver_options,
const namespacet &  ns,
std::vector< propertyt > &  properties,
std::size_t  property_index 
)

Definition at line 44 of file solver.cpp.

AltStyle によって変換されたページ (->オリジナル) /