Skip to content

Commit

Permalink
clang format, and minor fixes to is_query, is_fact
Browse files Browse the repository at this point in the history
  • Loading branch information
@yvizel
yvizel committed Feb 24, 2025
1 parent 0f6a42a commit ad717ba
Showing 1 changed file with 104 additions and 62 deletions.
166 changes: 104 additions & 62 deletions src/cprover/chc_db.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,16 @@
#ifndef CBMC_CHC_DB_H
#define CBMC_CHC_DB_H

#include <util/find_symbols.h>
#include <util/mathematical_expr.h>
#include <util/std_expr.h>
#include <util/find_symbols.h>

#include <vector>
#include "expr_iterator.h"

#include <functional>
#include <map>
#include <set>
#include <functional>
#include <vector>

class chc_dbt;

Expand All @@ -30,57 +32,54 @@ class horn_clauset
forall_exprt m_chc;

public:
horn_clauset(forall_exprt f) : m_chc(f) {}

horn_clauset(std::vector<symbol_exprt> & vars, exprt clause) : m_chc(vars, clause) {
horn_clauset(forall_exprt f) : m_chc(f)
{
}

horn_clauset(std::vector<symbol_exprt> &vars, exprt clause)
: m_chc(vars, clause)
{
}

const forall_exprt & get_chc() const
const forall_exprt &get_chc() const
{
return m_chc;
}

const exprt* body() const {
if (can_cast_expr<implies_exprt>(m_chc.where()))
const exprt *body() const
{
if(can_cast_expr<implies_exprt>(m_chc.where()))
{
return &to_implies_expr(m_chc.where()).op0();
}
return &m_chc.where();
}

const exprt* head() const {
if (can_cast_expr<implies_exprt>(m_chc.where()))
const exprt *head() const
{
if(can_cast_expr<implies_exprt>(m_chc.where()))
{
return &to_implies_expr(m_chc.where()).op1();
}
return nullptr;
}

bool is_fact() const {
bool is_fact() const
{
auto b = body();
bool not_fact = false;
b->visit_pre(
[&not_fact](const exprt &expr) {
if(can_cast_expr<function_application_exprt>(expr))
{
not_fact = true;
}
});
return !not_fact;
}

bool is_query() const {
if (can_cast_expr<implies_exprt>(m_chc.where()))
const std::function<bool(const exprt &)> pred = [](const exprt &subexpr) {
return can_cast_expr<function_application_exprt>(subexpr);
};
auto it = std::find_if(b->depth_begin(), b->depth_end(), pred);

return (it == b->depth_end());
}

bool is_query() const
{
if(can_cast_expr<implies_exprt>(m_chc.where()))
{
auto h = head();
bool res = true;
h->visit_pre(
[&res](const exprt &expr) {
if(can_cast_expr<function_application_exprt>(expr))
res = false;
});
return res;
return (can_cast_expr<function_application_exprt>(*head()));
}
return false;
}
Expand All @@ -92,7 +91,7 @@ class horn_clauset

bool operator!=(const horn_clauset &other) const
{
return !(*this==other);
return !(*this == other);
}

bool operator<(const horn_clauset &other) const
Expand All @@ -112,12 +111,19 @@ class horn_clauset
class chc_dbt
{
friend class horn_clauset;

public:
struct is_state_pred : public std::__unary_function<exprt, bool> {
struct is_state_pred : public std::__unary_function<exprt, bool>
{
const chc_dbt &m_db;
is_state_pred(const chc_dbt &db) : m_db(db) {}
is_state_pred(const chc_dbt &db) : m_db(db)
{
}

bool operator()(symbol_exprt state) { return m_db.has_state_pred(state); }
bool operator()(symbol_exprt state)
{
return m_db.has_state_pred(state);
}
};

typedef std::unordered_set<std::size_t> chc_sett;
Expand All @@ -136,37 +142,50 @@ class chc_dbt
static chc_sett m_empty_set;

public:
chc_dbt() {}
chc_dbt()
{
}

void add_state_pred(const symbol_exprt & state) { m_state_preds.insert(state); }
const std::unordered_set<symbol_exprt, irep_hash> &get_state_preds() { return m_state_preds; }
bool has_state_pred(const symbol_exprt & state) const { return m_state_preds.count(state) > 0; }
void add_state_pred(const symbol_exprt &state)
{
m_state_preds.insert(state);
}
const std::unordered_set<symbol_exprt, irep_hash> &get_state_preds()
{
return m_state_preds;
}
bool has_state_pred(const symbol_exprt &state) const
{
return m_state_preds.count(state) > 0;
}

void build_indices();
void reset_indices();

const chc_sett & use(const exprt & state) const {
const chc_sett &use(const exprt &state) const
{
auto it = m_body_idx.find(state);
if (it == m_body_idx.end())
if(it == m_body_idx.end())
return m_empty_set;
return it->second;
}

const chc_sett & def(const exprt & state) const {
const chc_sett &def(const exprt &state) const
{
auto it = m_head_idx.find(state);
if (it == m_head_idx.end())
if(it == m_head_idx.end())
return m_empty_set;
return it->second;
}

void add_clause(const forall_exprt & f)
void add_clause(const forall_exprt &f)
{
if (f.is_true())
if(f.is_true())
return;
auto new_cls = horn_clauset(f);
// Equivalent (semantic) queries may represent
// different properties
if (!new_cls.is_query())
if(!new_cls.is_query())
{
for(auto &c : m_clauses)
{
Expand All @@ -178,16 +197,28 @@ class chc_dbt
reset_indices();
}

[[nodiscard]] const horn_clauset & get_clause(std::size_t idx) const
[[nodiscard]] const horn_clauset &get_clause(std::size_t idx) const
{
INVARIANT(idx < m_clauses.size(), "Index in range");
return m_clauses[idx];
}

chcst::iterator begin() { return m_clauses.begin(); }
chcst::iterator end() { return m_clauses.end(); }
chcst::const_iterator begin() const { return m_clauses.begin(); }
chcst::const_iterator end() const { return m_clauses.end(); }
chcst::iterator begin()
{
return m_clauses.begin();
}
chcst::iterator end()
{
return m_clauses.end();
}
chcst::const_iterator begin() const
{
return m_clauses.begin();
}
chcst::const_iterator end() const
{
return m_clauses.end();
}
};

/*
Expand All @@ -197,7 +228,7 @@ class chc_dbt
*/
class chc_grapht
{
chc_dbt & m_db;
chc_dbt &m_db;
typedef std::map<exprt, std::unordered_set<exprt, irep_hash>> grapht;
grapht m_incoming;
grapht m_outgoing;
Expand All @@ -207,25 +238,36 @@ class chc_grapht
static std::unordered_set<exprt, irep_hash> m_expr_empty_set;

public:
chc_grapht(chc_dbt & db) : m_db(db), m_entry(nullptr) {}
chc_grapht(chc_dbt &db) : m_db(db), m_entry(nullptr)
{
}

void build_graph();

bool has_entry() const { return m_entry != nullptr; }
const symbol_exprt *entry() const {
bool has_entry() const
{
return m_entry != nullptr;
}
const symbol_exprt *entry() const
{
INVARIANT(has_entry(), "Entry must exist.");
return m_entry; }
return m_entry;
}

const std::unordered_set<exprt, irep_hash> &outgoing(const symbol_exprt &state) const {
const std::unordered_set<exprt, irep_hash> &
outgoing(const symbol_exprt &state) const
{
auto it = m_outgoing.find(state);
if (it == m_outgoing.end())
if(it == m_outgoing.end())
return m_expr_empty_set;
return it->second;
}

const std::unordered_set<exprt, irep_hash> &incoming(const symbol_exprt &state) const {
const std::unordered_set<exprt, irep_hash> &
incoming(const symbol_exprt &state) const
{
auto it = m_incoming.find(state);
if (it == m_incoming.end())
if(it == m_incoming.end())
return m_expr_empty_set;
return it->second;
}
Expand Down

0 comments on commit ad717ba

Please sign in to comment.