Loading...

Searching...

No Matches

inductiveness.cpp File Reference

Inductiveness. More...

#include "inductiveness.h"
#include <util/console.h>
#include <util/cout_message.h>
#include <util/format_expr.h>
#include <solvers/sat/satcheck.h>
#include "axioms.h"
#include "bv_pointers_wide.h"
#include "counterexample_found.h"
#include "propagate.h"
#include "solver.h"
#include <algorithm>
#include <iomanip>
#include <iostream>

+ Include dependency graph for inductiveness.cpp:

[フレーム]

Go to the source code of this file.

Functions

bool is_subsumed (const std::unordered_set< exprt, irep_hash > &a1, const std::unordered_set< exprt, irep_hash > &a2, const std::unordered_set< exprt, irep_hash > &a3, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)

std::size_t count_frame (const workt::patht &path, frame_reft f)

inductiveness_resultt inductiveness_check (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)

Detailed Description

Inductiveness.

Definition in file inductiveness.cpp.

Function Documentation

◆ count_frame()

std::size_t count_frame ( const workt::patht & path,

frame_reft f

)

Definition at line 91 of file inductiveness.cpp.

◆ inductiveness_check()

inductiveness_resultt inductiveness_check ( 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 98 of file inductiveness.cpp.

◆ is_subsumed()

bool is_subsumed ( const std::unordered_set< exprt, irep_hash > & a1,

const std::unordered_set< exprt, irep_hash > & a2,

const std::unordered_set< exprt, irep_hash > & a3,

const exprt & b,

const std::unordered_set< symbol_exprt, irep_hash > & address_taken,

bool verbose,

const namespacet & ns

)

Definition at line 30 of file inductiveness.cpp.