From 66bcf44ae632d8cac5f689339a59822f9c130c78 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 17:27:38 +0000 Subject: [PATCH 1/6] Move decision_proceduret into solvers/prop All modules that use decision_proceduret also use solvers. So, there is no need to have this interface in util. --- jbmc/src/jbmc/bmc.h | 3 ++- src/goto-instrument/accelerate/scratch_program.cpp | 3 ++- src/solvers/Makefile | 1 + src/solvers/prop/cover_goals.h | 3 +-- src/{util => solvers/prop}/decision_procedure.cpp | 0 src/{util => solvers/prop}/decision_procedure.h | 6 +++--- src/solvers/prop/prop_conv.h | 2 +- src/util/Makefile | 1 - 8 files changed, 10 insertions(+), 9 deletions(-) rename src/{util => solvers/prop}/decision_procedure.cpp (100%) rename src/{util => solvers/prop}/decision_procedure.h (90%) diff --git a/jbmc/src/jbmc/bmc.h b/jbmc/src/jbmc/bmc.h index 3543103cda3..44c0754d3aa 100644 --- a/jbmc/src/jbmc/bmc.h +++ b/jbmc/src/jbmc/bmc.h @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -31,6 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + class cbmc_solverst; /// \brief Bounded model checking or path exploration for goto-programs diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 7091b6f844d..080d89efff9 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -12,7 +12,8 @@ Author: Matt Lewis #include "scratch_program.h" #include -#include + +#include #include diff --git a/src/solvers/Makefile b/src/solvers/Makefile index dbb8fe63b24..4615d5566d5 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -144,6 +144,7 @@ SRC = $(BOOLEFORCE_SRC) \ bdd/miniBDD/miniBDD.cpp \ prop/bdd_expr.cpp \ prop/cover_goals.cpp \ + prop/decision_procedure.cpp \ prop/literal.cpp \ prop/minimize.cpp \ prop/prop.cpp \ diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h index 909adeabe65..8c4593313a2 100644 --- a/src/solvers/prop/cover_goals.h +++ b/src/solvers/prop/cover_goals.h @@ -14,8 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - +#include "decision_procedure.h" #include "literal.h" class message_handlert; diff --git a/src/util/decision_procedure.cpp b/src/solvers/prop/decision_procedure.cpp similarity index 100% rename from src/util/decision_procedure.cpp rename to src/solvers/prop/decision_procedure.cpp diff --git a/src/util/decision_procedure.h b/src/solvers/prop/decision_procedure.h similarity index 90% rename from src/util/decision_procedure.h rename to src/solvers/prop/decision_procedure.h index 5654e0e1740..8d58ea4292c 100644 --- a/src/util/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Decision Procedure Interface -#ifndef CPROVER_UTIL_DECISION_PROCEDURE_H -#define CPROVER_UTIL_DECISION_PROCEDURE_H +#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H +#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H #include #include @@ -62,4 +62,4 @@ inline decision_proceduret &operator<<( return dest; } -#endif // CPROVER_UTIL_DECISION_PROCEDURE_H +#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index da134f8992f..2ba79704351 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include +#include "decision_procedure.h" #include "literal.h" #include "literal_expr.h" #include "prop.h" diff --git a/src/util/Makefile b/src/util/Makefile index ebb2a015b19..0113f6bfed4 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -8,7 +8,6 @@ SRC = allocate_objects.cpp \ cmdline.cpp \ config.cpp \ cout_message.cpp \ - decision_procedure.cpp \ dstring.cpp \ endianness_map.cpp \ expr.cpp \ From 77e12772aa28c3a4c74d26495539d9520a35602a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 17:39:44 +0000 Subject: [PATCH 2/6] Move get_number_of_solver_calls into decision_proceduret That's not specific to prop_convt. --- src/solvers/prop/decision_procedure.h | 3 +++ src/solvers/prop/prop_conv.h | 3 --- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 8d58ea4292c..14a4f355a53 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -52,6 +52,9 @@ class decision_proceduret // return a textual description of the decision procedure virtual std::string decision_procedure_text() const=0; + + /// Returns the number of incremental solver calls + virtual std::size_t get_number_of_solver_calls() const = 0; }; inline decision_proceduret &operator<<( diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index 2ba79704351..2d4972730e6 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -56,9 +56,6 @@ class prop_convt:public decision_proceduret // Resource limits: virtual void set_time_limit_seconds(uint32_t) {} - - /// Returns the number of incremental solver calls - virtual std::size_t get_number_of_solver_calls() const = 0; }; // From ab6974232ec657ff4ed8cefbc89665db66e9b5b5 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 17:50:25 +0000 Subject: [PATCH 3/6] Move literal convert/get to decision_proceduret There is no instance in the code base of using decision_proceduret without these functions. --- src/solvers/prop/decision_procedure.h | 14 ++++++++++++++ src/solvers/prop/prop_conv.h | 11 ----------- 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 14a4f355a53..5a16e400c6c 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -15,7 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "literal.h" + class exprt; +class tvt; class decision_proceduret { @@ -26,6 +29,9 @@ class decision_proceduret // returns nil if not available virtual exprt get(const exprt &expr) const=0; + // specialized variant of get + virtual tvt l_get(literalt) const = 0; + // print satisfying assignment virtual void print_assignment(std::ostream &out) const=0; @@ -39,6 +45,14 @@ class decision_proceduret void set_to_false(const exprt &expr) { set_to(expr, false); } + // conversion to handle + virtual literalt convert(const exprt &expr) = 0; + + literalt operator()(const exprt &expr) + { + return convert(expr); + } + // solve the problem enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR }; diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index 2d4972730e6..11046ae2732 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -30,19 +30,8 @@ class prop_convt:public decision_proceduret public: virtual ~prop_convt() { } - // conversion to handle - virtual literalt convert(const exprt &expr)=0; - - literalt operator()(const exprt &expr) - { - return convert(expr); - } - using decision_proceduret::operator(); - // specialised variant of get - virtual tvt l_get(literalt a) const=0; - // incremental solving virtual void set_frozen(literalt a); virtual void set_frozen(const bvt &); From 5fad3f10bdf8f143dd576bcee3f3e0460a5beff0 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 17:57:04 +0000 Subject: [PATCH 4/6] Make dec_solve protected According to comment in the code. --- jbmc/src/jbmc/bmc.cpp | 2 +- src/goto-checker/goto_symex_property_decider.cpp | 2 +- src/goto-instrument/accelerate/scratch_program.cpp | 2 +- src/solvers/prop/cover_goals.cpp | 2 +- src/solvers/prop/decision_procedure.h | 6 +++--- src/solvers/prop/minimize.cpp | 4 ++-- 6 files changed, 9 insertions(+), 9 deletions(-) diff --git a/jbmc/src/jbmc/bmc.cpp b/jbmc/src/jbmc/bmc.cpp index e9b590a8ffa..85d297b0851 100644 --- a/jbmc/src/jbmc/bmc.cpp +++ b/jbmc/src/jbmc/bmc.cpp @@ -54,7 +54,7 @@ decision_proceduret::resultt bmct::run_decision_procedure() status() << "Running " << prop_conv.decision_procedure_text() << eom; - decision_proceduret::resultt dec_result = prop_conv.dec_solve(); + decision_proceduret::resultt dec_result = prop_conv(); { auto solver_stop = std::chrono::steady_clock::now(); diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index b50f683195d..c474ad14bd5 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -103,7 +103,7 @@ void goto_symex_property_decidert::add_constraint_from_goals( decision_proceduret::resultt goto_symex_property_decidert::solve() { - return solver->prop_conv().dec_solve(); + return solver->prop_conv()(); } prop_convt &goto_symex_property_decidert::get_solver() const diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 080d89efff9..b4a5474146b 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -70,7 +70,7 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager) std::cout << "Finished symex, invoking decision procedure.\n"; #endif - return (checker->dec_solve()==decision_proceduret::resultt::D_SATISFIABLE); + return ((*checker)() == decision_proceduret::resultt::D_SATISFIABLE); } exprt scratch_programt::eval(const exprt &e) diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index 1e0cd3f504e..5099e81f80c 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -88,7 +88,7 @@ operator()(message_handlert &message_handler) _iterations++; constraint(); - dec_result=prop_conv.dec_solve(); + dec_result = prop_conv(); switch(dec_result) { diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 5a16e400c6c..978c5c90a69 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -56,9 +56,6 @@ class decision_proceduret // solve the problem enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR }; - // will eventually be protected, use below call operator - virtual resultt dec_solve()=0; - resultt operator()() { return dec_solve(); @@ -69,6 +66,9 @@ class decision_proceduret /// Returns the number of incremental solver calls virtual std::size_t get_number_of_solver_calls() const = 0; + +protected: + virtual resultt dec_solve() = 0; }; inline decision_proceduret &operator<<( diff --git a/src/solvers/prop/minimize.cpp b/src/solvers/prop/minimize.cpp index e06a9c2f946..744093a5b30 100644 --- a/src/solvers/prop/minimize.cpp +++ b/src/solvers/prop/minimize.cpp @@ -123,7 +123,7 @@ void prop_minimizet::operator()() bvt assumptions; assumptions.push_back(c); prop_conv.set_assumptions(assumptions); - dec_result=prop_conv.dec_solve(); + dec_result = prop_conv(); switch(dec_result) { @@ -153,6 +153,6 @@ void prop_minimizet::operator()() bvt assumptions; // no assumptions prop_conv.set_assumptions(assumptions); - prop_conv.dec_solve(); + (void)prop_conv(); } } From 3a68094924215f2d1e47d22943d2f6fb0c6821f8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 18:12:00 +0000 Subject: [PATCH 5/6] Clean up and document decision_proceduret Complete documentation and reorder methods to make the interface more readable. --- src/solvers/prop/decision_procedure.cpp | 20 +++++++ src/solvers/prop/decision_procedure.h | 72 +++++++++++++------------ 2 files changed, 58 insertions(+), 34 deletions(-) diff --git a/src/solvers/prop/decision_procedure.cpp b/src/solvers/prop/decision_procedure.cpp index d611fe7f24f..b6dd6e8e1e5 100644 --- a/src/solvers/prop/decision_procedure.cpp +++ b/src/solvers/prop/decision_procedure.cpp @@ -14,3 +14,23 @@ Author: Daniel Kroening, kroening@kroening.com decision_proceduret::~decision_proceduret() { } + +literalt decision_proceduret::operator()(const exprt &expr) +{ + return convert(expr); +} + +decision_proceduret::resultt decision_proceduret::operator()() +{ + return dec_solve(); +} + +void decision_proceduret::set_to_true(const exprt &expr) +{ + set_to(expr, true); +} + +void decision_proceduret::set_to_false(const exprt &expr) +{ + set_to(expr, false); +} diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 978c5c90a69..149491392da 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -23,57 +23,61 @@ class tvt; class decision_proceduret { public: - virtual ~decision_proceduret(); + /// For a Boolean expression \p expr, add the constraint 'expr' if \p value + /// is `true`, otherwise add 'not expr' + virtual void set_to(const exprt &expr, bool value) = 0; - // get a value from satisfying instance if satisfiable - // returns nil if not available - virtual exprt get(const exprt &expr) const=0; + /// For a Boolean expression \p expr, add the constraint 'expr' + void set_to_true(const exprt &expr); - // specialized variant of get - virtual tvt l_get(literalt) const = 0; + /// For a Boolean expression \p expr, add the constraint 'not expr' + void set_to_false(const exprt &expr); - // print satisfying assignment - virtual void print_assignment(std::ostream &out) const=0; + /// Convert a Boolean expression and return the corresponding literal + virtual literalt convert(const exprt &expr) = 0; - // add constraints - // the expression must be of Boolean type - virtual void set_to(const exprt &expr, bool value)=0; + /// Convert a Boolean expression and return the corresponding literal + literalt operator()(const exprt &); - void set_to_true(const exprt &expr) - { set_to(expr, true); } + /// Result of running the decision procedure + enum class resultt + { + D_SATISFIABLE, + D_UNSATISFIABLE, + D_ERROR + }; - void set_to_false(const exprt &expr) - { set_to(expr, false); } + /// Run the decision procedure to solve the problem + resultt operator()(); - // conversion to handle - virtual literalt convert(const exprt &expr) = 0; + /// Return \p expr with variables replaced by values from satisfying + /// assignment if available. + /// Return `nil` if not available + virtual exprt get(const exprt &expr) const = 0; - literalt operator()(const exprt &expr) - { - return convert(expr); - } + /// Return value of literal \p l from satisfying assignment. + /// Return tvt::UNKNOWN if not available + virtual tvt l_get(literalt l) const = 0; - // solve the problem - enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR }; + /// Print satisfying assignment to \p out + virtual void print_assignment(std::ostream &out) const = 0; - resultt operator()() - { - return dec_solve(); - } - - // return a textual description of the decision procedure - virtual std::string decision_procedure_text() const=0; + /// Return a textual description of the decision procedure + virtual std::string decision_procedure_text() const = 0; - /// Returns the number of incremental solver calls + /// Return the number of incremental solver calls virtual std::size_t get_number_of_solver_calls() const = 0; + virtual ~decision_proceduret(); + protected: + /// Run the decision procedure to solve the problem virtual resultt dec_solve() = 0; }; -inline decision_proceduret &operator<<( - decision_proceduret &dest, - const exprt &src) +/// Add Boolean constraint \p src to decision procedure \p dest +inline decision_proceduret & +operator<<(decision_proceduret &dest, const exprt &src) { dest.set_to_true(src); return dest; From c56f9929b68b4382327e160f9c77153f2720a44a Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 26 Mar 2019 18:22:02 +0000 Subject: [PATCH 6/6] Remove unused operator Operator for conversion is not intuitive anyway. --- src/solvers/prop/decision_procedure.cpp | 5 ----- src/solvers/prop/decision_procedure.h | 3 --- 2 files changed, 8 deletions(-) diff --git a/src/solvers/prop/decision_procedure.cpp b/src/solvers/prop/decision_procedure.cpp index b6dd6e8e1e5..0b7bf603e4f 100644 --- a/src/solvers/prop/decision_procedure.cpp +++ b/src/solvers/prop/decision_procedure.cpp @@ -15,11 +15,6 @@ decision_proceduret::~decision_proceduret() { } -literalt decision_proceduret::operator()(const exprt &expr) -{ - return convert(expr); -} - decision_proceduret::resultt decision_proceduret::operator()() { return dec_solve(); diff --git a/src/solvers/prop/decision_procedure.h b/src/solvers/prop/decision_procedure.h index 149491392da..818b9cd1952 100644 --- a/src/solvers/prop/decision_procedure.h +++ b/src/solvers/prop/decision_procedure.h @@ -36,9 +36,6 @@ class decision_proceduret /// Convert a Boolean expression and return the corresponding literal virtual literalt convert(const exprt &expr) = 0; - /// Convert a Boolean expression and return the corresponding literal - literalt operator()(const exprt &); - /// Result of running the decision procedure enum class resultt {