Loading...

Searching...

No Matches

counterexample_found.cpp File Reference

Counterexample Found. More...

#include "counterexample_found.h"
#include <util/cout_message.h>
#include <util/simplify_expr.h>
#include <solvers/sat/satcheck.h>
#include "axioms.h"
#include "bv_pointers_wide.h"
#include "simplify_state_expr.h"
#include "state.h"

+ Include dependency graph for counterexample_found.cpp:

[フレーム]

Go to the source code of this file.

Functions

void show_assignment (const bv_pointers_widet &solver)

static exprt evaluator_rec (const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)

static exprt evaluator (const std::unordered_map< exprt, exprt, irep_hash > &memory, const decision_proceduret &solver, exprt src, const namespacet &ns)

propertyt::tracet counterexample (const std::vector< framet > &frames, const workt &work, const bv_pointers_widet &solver, const axiomst &axioms, const namespacet &ns)

std::optional< propertyt::tracet > counterexample_found (const std::vector< framet > &frames, const workt &work, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, bool verbose, const namespacet &ns)

Detailed Description

Counterexample Found.

Definition in file counterexample_found.cpp.

Function Documentation

◆ counterexample()

propertyt::tracet counterexample ( const std::vector< framet > & frames,

const workt & work,

const bv_pointers_widet & solver,

const axiomst & axioms,

const namespacet & ns

)

Definition at line 106 of file counterexample_found.cpp.

◆ counterexample_found()

std::optional< propertyt::tracet > counterexample_found ( const std::vector< framet > & frames,

const workt & work,

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

bool verbose,

const namespacet & ns

)

Definition at line 173 of file counterexample_found.cpp.

◆ evaluator()

static exprt evaluator ( const std::unordered_map< exprt, exprt, irep_hash > & memory,

const decision_proceduret & solver,

exprt src,

const namespacet & ns

)

static

Definition at line 96 of file counterexample_found.cpp.

◆ evaluator_rec()

static exprt evaluator_rec ( const std::unordered_map< exprt, exprt, irep_hash > & memory,

const decision_proceduret & solver,

exprt src,

const namespacet & ns

)

static

Definition at line 59 of file counterexample_found.cpp.

◆ show_assignment()

void show_assignment ( const bv_pointers_widet & solver )

Definition at line 24 of file counterexample_found.cpp.