10 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H 11 #define CPROVER_SOLVERS_PROP_PROP_CONV_H 43 using decision_proceduret::operator();
73 equality_propagation(true),
75 post_processing_done(false),
81 virtual void set_to(
const exprt &expr,
bool value)
override;
85 {
return "propositional reduction"; }
86 virtual exprt get(
const exprt &expr)
const override;
93 { prop.set_assumptions(_assumptions); }
95 {
return prop.has_set_assumptions(); }
99 {
return prop.is_in_conflict(l); }
101 {
return prop.has_is_in_conflict(); }
104 virtual bool literal(
const exprt &expr,
literalt &literal)
const;
113 typedef std::unordered_map<exprt, literalt, irep_hash>
cachet;
119 virtual void post_process();
124 virtual bool get_bool(
const exprt &expr,
tvt &value)
const;
129 virtual bool set_equality_to_true(
const equal_exprt &expr);
139 virtual void ignoring(
const exprt &expr);
145 #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H virtual void set_all_frozen()
bool equality_propagation
literalt operator()(const exprt &expr)
virtual bool has_is_in_conflict() const
virtual void print_assignment(std::ostream &out) const =0
virtual ~prop_conv_solvert()
Decision Procedure Interface.
virtual bool is_in_conflict(literalt l) const
determine whether a variable is in the final conflict
virtual void set_frozen(literalt a) override
const symbolst & get_symbols() const
std::map< irep_idt, literalt > symbolst
virtual void set_assumptions(const bvt &_assumptions) override
virtual void clear_cache()
virtual resultt dec_solve()=0
const cachet & get_cache() const
API to expression classes.
virtual bool has_set_assumptions() const override
virtual bool has_is_in_conflict() const override
std::unordered_map< exprt, literalt, irep_hash > cachet
virtual literalt convert(const exprt &expr)=0
virtual void set_to(const exprt &expr, bool value)=0
virtual std::string decision_procedure_text() const override
virtual bool has_set_assumptions() const
virtual tvt l_get(literalt a) const =0
virtual tvt l_get(literalt a) const override
virtual bool is_in_conflict(literalt l) const override
determine whether a variable is in the final conflict
Base class for all expressions.
bool post_processing_done
virtual void set_frozen(literalt a)
prop_conv_solvert(const namespacet &_ns, propt &_prop)
std::vector< literalt > bvt
prop_convt(const namespacet &_ns)
virtual void set_all_frozen() override
virtual void set_assumptions(const bvt &_assumptions)