-
Notifications
You must be signed in to change notification settings - Fork 273
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Put one line functions in a format compatible with clang-format to give a more consistent formatting to the code in prop_conv header.
- Loading branch information
1 parent
b6caa91
commit c61a5d8
Showing
1 changed file
with
50 additions
and
18 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -27,10 +27,13 @@ Author: Daniel Kroening, [email protected] | |
class prop_convt:public decision_proceduret | ||
{ | ||
public: | ||
explicit prop_convt( | ||
const namespacet &_ns): | ||
decision_proceduret(_ns) { } | ||
virtual ~prop_convt() { } | ||
explicit prop_convt(const namespacet &_ns) : decision_proceduret(_ns) | ||
{ | ||
} | ||
|
||
virtual ~prop_convt() | ||
{ | ||
} | ||
|
||
// conversion to handle | ||
virtual literalt convert(const exprt &expr)=0; | ||
|
@@ -49,15 +52,27 @@ class prop_convt:public decision_proceduret | |
virtual void set_frozen(literalt a); | ||
virtual void set_frozen(const bvt &); | ||
virtual void set_assumptions(const bvt &_assumptions); | ||
virtual bool has_set_assumptions() const { return false; } | ||
virtual void set_all_frozen() {} | ||
|
||
virtual bool has_set_assumptions() const | ||
{ | ||
return false; | ||
} | ||
|
||
virtual void set_all_frozen() | ||
{ | ||
} | ||
|
||
// returns true if an assumption is in the final conflict | ||
virtual bool is_in_conflict(literalt l) const; | ||
virtual bool has_is_in_conflict() const { return false; } | ||
virtual bool has_is_in_conflict() const | ||
{ | ||
return false; | ||
} | ||
|
||
// Resource limits: | ||
virtual void set_time_limit_seconds(uint32_t) {} | ||
virtual void set_time_limit_seconds(uint32_t) | ||
{ | ||
} | ||
}; | ||
|
||
// | ||
|
@@ -70,9 +85,10 @@ class prop_convt:public decision_proceduret | |
class prop_conv_solvert:public prop_convt | ||
{ | ||
public: | ||
prop_conv_solvert(const namespacet &_ns, propt &_prop): | ||
prop_convt(_ns), | ||
prop(_prop) { } | ||
prop_conv_solvert(const namespacet &_ns, propt &_prop) | ||
: prop_convt(_ns), prop(_prop) | ||
{ | ||
} | ||
|
||
virtual ~prop_conv_solvert() = default; | ||
|
||
|
@@ -81,34 +97,50 @@ class prop_conv_solvert:public prop_convt | |
decision_proceduret::resultt dec_solve() override; | ||
void print_assignment(std::ostream &out) const override; | ||
std::string decision_procedure_text() const override | ||
{ return "propositional reduction"; } | ||
{ | ||
return "propositional reduction"; | ||
} | ||
exprt get(const exprt &expr) const override; | ||
|
||
// overloading from prop_convt | ||
using prop_convt::set_frozen; | ||
virtual tvt l_get(literalt a) const override { return prop.l_get(a); } | ||
virtual tvt l_get(literalt a) const override | ||
{ | ||
return prop.l_get(a); | ||
} | ||
void set_frozen(literalt a) override | ||
{ | ||
prop.set_frozen(a); | ||
} | ||
void set_assumptions(const bvt &_assumptions) override | ||
{ prop.set_assumptions(_assumptions); } | ||
{ | ||
prop.set_assumptions(_assumptions); | ||
} | ||
bool has_set_assumptions() const override | ||
{ return prop.has_set_assumptions(); } | ||
{ | ||
return prop.has_set_assumptions(); | ||
} | ||
void set_all_frozen() override | ||
{ | ||
freeze_all = true; | ||
} | ||
literalt convert(const exprt &expr) override; | ||
bool is_in_conflict(literalt l) const override | ||
{ return prop.is_in_conflict(l); } | ||
{ | ||
return prop.is_in_conflict(l); | ||
} | ||
bool has_is_in_conflict() const override | ||
{ return prop.has_is_in_conflict(); } | ||
{ | ||
return prop.has_is_in_conflict(); | ||
} | ||
|
||
// get literal for expression, if available | ||
virtual optionalt<literalt> literal(const exprt &expr) const; | ||
|
||
virtual void clear_cache() { cache.clear();} | ||
virtual void clear_cache() | ||
{ | ||
cache.clear(); | ||
} | ||
|
||
bool use_cache = true; | ||
bool equality_propagation = true; | ||
|