From 088f1e888d25bcc2b68580b97ab362df6cd38f3f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 11 Apr 2019 16:38:24 -0700 Subject: [PATCH 1/5] elaborate prop_convt::handle(expr) This change adds three features: 1) Non-boolean expressions are returned verbatim. 2) Boolean expressions that are determined to be a constant (e.g., by means of constant folding) are returned as constants, to enable further optimisation by users. 3) Literals returned are frozen, to simplify incremental usage. --- src/solvers/prop/prop_conv.cpp | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) 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 From 101c775e5c7f0e846ac6496ed3edc0bec1c18081 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 11 Apr 2019 19:58:23 -0700 Subject: [PATCH 2/5] introduce ranged for in cover_goals --- src/solvers/prop/cover_goals.cpp | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 239db6bf68c..9f6651d44fe 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -48,13 +48,9 @@ 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(literal_exprt(g.condition)); // this is 'false' if there are no disjuncts prop_conv.set_to_true(disjunction(disjuncts)); @@ -63,12 +59,9 @@ void cover_goalst::constraint() /// 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); + for(const auto &g : goals) + if(!g.condition.is_constant()) + prop_conv.set_frozen(g.condition); } /// Try to cover all goals From 4869a95996a0a0bf3bdcd752720df5e8b1484a06 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 11 Apr 2019 20:00:21 -0700 Subject: [PATCH 3/5] use new handle interface in cover_goals The literal-based interface is more specific, and cover_goals doesn't require anything beyond what decision_proceduret offers. --- jbmc/src/jbmc/all_properties.cpp | 3 +-- src/solvers/prop/cover_goals.cpp | 19 ++++--------------- src/solvers/prop/cover_goals.h | 14 +++++++------- 3 files changed, 12 insertions(+), 24 deletions(-) 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 9f6651d44fe..341bafa54e7 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -29,8 +29,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 && + prop_conv.get(g.condition).is_true()) { g.status=goalt::statust::COVERED; _number_covered++; @@ -50,20 +51,12 @@ void cover_goalst::constraint() for(const auto &g : goals) if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false()) - disjuncts.push_back(literal_exprt(g.condition)); + 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(const auto &g : goals) - if(!g.condition.is_constant()) - prop_conv.set_frozen(g.condition); -} - /// Try to cover all goals decision_proceduret::resultt cover_goalst:: operator()(message_handlert &message_handler) @@ -72,10 +65,6 @@ 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! diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index 8c4593313a2..5e8160985ac 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -15,7 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "decision_procedure.h" -#include "literal.h" + +#include class message_handlert; class prop_convt; @@ -41,10 +42,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 +73,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 @@ -103,7 +104,6 @@ class cover_goalst private: void mark(); void constraint(); - void freeze_goal_variables(); }; #endif // CPROVER_SOLVERS_PROP_COVER_GOALS_H From 283fa83216ad851b9a0b9232407043e4f7a3903b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 11 Apr 2019 20:39:38 -0700 Subject: [PATCH 4/5] cover_goalst does not need prop_convt No methods of prop_convt are used. --- src/solvers/prop/cover_goals.cpp | 7 +++---- src/solvers/prop/cover_goals.h | 11 +++++------ 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 341bafa54e7..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() { @@ -31,7 +30,7 @@ void cover_goalst::mark() for(auto &g : goals) if( g.status == goalt::statust::UNKNOWN && - prop_conv.get(g.condition).is_true()) + decision_procedure.get(g.condition).is_true()) { g.status=goalt::statust::COVERED; _number_covered++; @@ -54,7 +53,7 @@ void cover_goalst::constraint() disjuncts.push_back(g.condition); // this is 'false' if there are no disjuncts - prop_conv.set_to_true(disjunction(disjuncts)); + decision_procedure.set_to_true(disjunction(disjuncts)); } /// Try to cover all goals @@ -71,7 +70,7 @@ operator()(message_handlert &message_handler) _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 5e8160985ac..b72b2df1b16 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -19,17 +19,16 @@ Author: Daniel Kroening, kroening@kroening.com #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) { } @@ -96,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; From b885981a6053f96c0712d042dc525cd17cc838f0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 11 Apr 2019 20:23:55 -0700 Subject: [PATCH 5/5] move l_get and convert back into prop_convt prop_convt is an instance of decision_proceduret that uses propositional logic. --- src/solvers/prop/decision_procedure.h | 12 ------------ src/solvers/prop/prop_conv.h | 15 ++++++++++----- 2 files changed, 10 insertions(+), 17 deletions(-) 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.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