diff --git a/jbmc/src/jbmc/all_properties.cpp b/jbmc/src/jbmc/all_properties.cpp index 6b6ec88b441..ca0cd584e42 100644 --- a/jbmc/src/jbmc/all_properties.cpp +++ b/jbmc/src/jbmc/all_properties.cpp @@ -105,8 +105,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()() { // Our goal is to falsify a property, i.e., we will // add the negation of the property as goal. - literalt p = !solver.convert(g.second.as_expr()); - cover_goals.add(p); + cover_goals.add(not_exprt(g.second.as_expr())); } status() << "Running " << solver.decision_procedure_text() << eom; diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 239db6bf68c..7f5c7ea2c6d 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "literal_expr.h" -#include "prop_conv.h" cover_goalst::~cover_goalst() { @@ -29,8 +28,9 @@ void cover_goalst::mark() o->satisfying_assignment(); for(auto &g : goals) - if(g.status==goalt::statust::UNKNOWN && - prop_conv.l_get(g.condition).is_true()) + if( + g.status == goalt::statust::UNKNOWN && + decision_procedure.get(g.condition).is_true()) { g.status=goalt::statust::COVERED; _number_covered++; @@ -48,27 +48,12 @@ void cover_goalst::constraint() // cover at least one unknown goal - for(std::list::const_iterator - g_it=goals.begin(); - g_it!=goals.end(); - g_it++) - if(g_it->status==goalt::statust::UNKNOWN && - !g_it->condition.is_false()) - disjuncts.push_back(literal_exprt(g_it->condition)); + for(const auto &g : goals) + if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false()) + disjuncts.push_back(g.condition); // this is 'false' if there are no disjuncts - prop_conv.set_to_true(disjunction(disjuncts)); -} - -/// Build clause -void cover_goalst::freeze_goal_variables() -{ - for(std::list::const_iterator - g_it=goals.begin(); - g_it!=goals.end(); - g_it++) - if(!g_it->condition.is_constant()) - prop_conv.set_frozen(g_it->condition); + decision_procedure.set_to_true(disjunction(disjuncts)); } /// Try to cover all goals @@ -79,17 +64,13 @@ operator()(message_handlert &message_handler) decision_proceduret::resultt dec_result; - // We use incremental solving, so need to freeze some variables - // to prevent them from being eliminated. - freeze_goal_variables(); - do { // We want (at least) one of the remaining goals, please! _iterations++; constraint(); - dec_result = prop_conv(); + dec_result = decision_procedure(); switch(dec_result) { diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index 8c4593313a2..b72b2df1b16 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -15,20 +15,20 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "decision_procedure.h" -#include "literal.h" + +#include class message_handlert; -class prop_convt; /// Try to cover some given set of goals incrementally. This can be seen as a /// heuristic variant of SAT-based set-cover. No minimality guarantee. class cover_goalst { public: - explicit cover_goalst(prop_convt &_prop_conv): - _number_covered(0), - _iterations(0), - prop_conv(_prop_conv) + explicit cover_goalst(decision_proceduret &_decision_procedure) + : _number_covered(0), + _iterations(0), + decision_procedure(_decision_procedure) { } @@ -41,10 +41,11 @@ class cover_goalst struct goalt { - literalt condition; + exprt condition; enum class statust { UNKNOWN, COVERED, UNCOVERED, ERROR } status; - goalt():status(statust::UNKNOWN) + explicit goalt(exprt _condition) + : condition(std::move(_condition)), status(statust::UNKNOWN) { } }; @@ -71,10 +72,9 @@ class cover_goalst // managing the goals - void add(const literalt condition) + void add(exprt condition) { - goals.push_back(goalt()); - goals.back().condition=condition; + goals.emplace_back(std::move(condition)); } // register an observer if you want to be told @@ -95,7 +95,7 @@ class cover_goalst protected: std::size_t _number_covered; unsigned _iterations; - prop_convt &prop_conv; + decision_proceduret &decision_procedure; typedef std::vector observerst; observerst observers; @@ -103,7 +103,6 @@ class cover_goalst private: void mark(); void constraint(); - void freeze_goal_variables(); }; #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 73609bfecbc..9c3484a65ea 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -15,10 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "literal.h" - class exprt; -class tvt; class decision_proceduret { @@ -33,10 +30,6 @@ class decision_proceduret /// For a Boolean expression \p expr, add the constraint 'not expr' void set_to_false(const exprt &expr); - /// Convert a Boolean expression and return the corresponding literal - /// This will go away, use handle(expr) instead - virtual literalt convert(const exprt &expr) = 0; - /// Generate a handle for an expression; this offers an efficient way /// to refer to the expression in subsequent calls to \ref get or /// \ref set_to @@ -58,11 +51,6 @@ class decision_proceduret /// Return `nil` if not available virtual exprt get(const exprt &expr) const = 0; - /// Return value of literal \p l from satisfying assignment. - /// Return tvt::UNKNOWN if not available - /// This will go away, use get instead. - virtual tvt l_get(literalt l) const = 0; - /// Print satisfying assignment to \p out virtual void print_assignment(std::ostream &out) const = 0; diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 38792212e5c..9b9e15d2e85 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -10,11 +10,30 @@ Author: Daniel Kroening, kroening@kroening.com #include "literal_expr.h" +#include + #include exprt prop_convt::handle(const exprt &expr) { - return literal_exprt(convert(expr)); + // We can only improve Booleans. + if(expr.type().id() != ID_bool) + return expr; + + // We convert to a literal to obtain a 'small' handle + literalt l = convert(expr); + + // The literal may be a constant as a result of non-trivial + // propagation. We return constants as such. + if(l.is_true()) + return true_exprt(); + else if(l.is_false()) + return false_exprt(); + + // freeze to enable incremental use + set_frozen(l); + + return literal_exprt(l); } /// determine whether a variable is in the final conflict diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index db1981f55c5..31435874a3d 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -11,6 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_PROP_PROP_CONV_H #include "decision_procedure.h" +#include "literal.h" + +class tvt; // API that provides a "handle" in the form of a literalt // for expressions. @@ -29,6 +32,13 @@ class prop_convt:public decision_proceduret /// but solver-specific representation. exprt handle(const exprt &expr) override; + /// Convert a Boolean expression and return the corresponding literal + virtual literalt convert(const exprt &expr) = 0; + + /// Return value of literal \p l from satisfying assignment. + /// Return tvt::UNKNOWN if not available + virtual tvt l_get(literalt l) const = 0; + // incremental solving virtual void set_frozen(literalt a); virtual void set_frozen(const bvt &); @@ -41,9 +51,4 @@ class prop_convt:public decision_proceduret virtual bool has_is_in_conflict() const { return false; } }; -// -// an instance of the above that converts the -// propositional skeleton by passing it to a propt -// - #endif // CPROVER_SOLVERS_PROP_PROP_CONV_H