cprover
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.