Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
11 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
43 using decision_proceduret::operator();
80 void set_to(
const exprt &expr,
bool value)
override;
84 {
return "propositional reduction"; }
118 typedef std::unordered_map<exprt, literalt, irep_hash>
cachet;
155 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool equality_propagation
virtual void set_assumptions(const bvt &_assumptions)
virtual bool has_is_in_conflict() const
virtual void set_all_frozen()
virtual void set_assumptions(const bvt &)
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
void set_assumptions(const bvt &_assumptions) override
std::vector< literalt > bvt
virtual void set_time_limit_seconds(uint32_t)
Base class for all expressions.
virtual tvt l_get(literalt a) const override
virtual bool has_is_in_conflict() const
virtual literalt convert_bool(const exprt &expr)
Expression to hold a symbol (variable)
virtual bool has_set_assumptions() const
virtual void ignoring(const exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool literal(const symbol_exprt &expr, literalt &literal) const
bool post_processing_done
virtual void clear_cache()
virtual literalt convert(const exprt &expr)=0
virtual bool get_bool(const exprt &expr, tvt &value) const
get a boolean value from counter example if not valid
virtual void post_process()
const cachet & get_cache() const
exprt get(const exprt &expr) const override
bool has_set_assumptions() const override
bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
virtual void set_frozen(literalt)
std::unordered_map< exprt, literalt, irep_hash > cachet
bool has_is_in_conflict() const override
virtual literalt get_literal(const irep_idt &symbol)
prop_conv_solvert(const namespacet &_ns, propt &_prop)
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
virtual tvt l_get(literalt a) const =0
literalt convert(const exprt &expr) override
virtual literalt convert_rest(const exprt &expr)
virtual void set_frozen(literalt a)
std::map< irep_idt, literalt > symbolst
virtual ~prop_conv_solvert()=default
virtual tvt l_get(literalt a) const =0
virtual bool has_set_assumptions() const
std::string decision_procedure_text() const override
void set_frozen(literalt a) override
decision_proceduret::resultt dec_solve() override
const symbolst & get_symbols() const
void print_assignment(std::ostream &out) const override
prop_convt(const namespacet &_ns)
void set_all_frozen() override
void set_time_limit_seconds(uint32_t lim) override
virtual void set_time_limit_seconds(uint32_t)
literalt operator()(const exprt &expr)
void set_to(const exprt &expr, bool value) override
virtual bool set_equality_to_true(const equal_exprt &expr)