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/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-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 7091b6f844d..b4a5474146b 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 @@ -69,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/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.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/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 57% rename from src/util/decision_procedure.cpp rename to src/solvers/prop/decision_procedure.cpp index d611fe7f24f..0b7bf603e4f 100644 --- a/src/util/decision_procedure.cpp +++ b/src/solvers/prop/decision_procedure.cpp @@ -14,3 +14,18 @@ Author: Daniel Kroening, kroening@kroening.com decision_proceduret::~decision_proceduret() { } + +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 new file mode 100644 index 00000000000..818b9cd1952 --- /dev/null +++ b/src/solvers/prop/decision_procedure.h @@ -0,0 +1,83 @@ +/*******************************************************************\ + +Module: Decision Procedure Interface + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Decision Procedure Interface + +#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H +#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H + +#include +#include + +#include "literal.h" + +class exprt; +class tvt; + +class decision_proceduret +{ +public: + /// 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; + + /// For a Boolean expression \p expr, add the constraint 'expr' + void set_to_true(const exprt &expr); + + /// 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 + virtual literalt convert(const exprt &expr) = 0; + + /// Result of running the decision procedure + enum class resultt + { + D_SATISFIABLE, + D_UNSATISFIABLE, + D_ERROR + }; + + /// Run the decision procedure to solve the problem + resultt operator()(); + + /// 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; + + /// Return value of literal \p l from satisfying assignment. + /// Return tvt::UNKNOWN if not available + virtual tvt l_get(literalt l) const = 0; + + /// Print satisfying assignment to \p out + virtual void print_assignment(std::ostream &out) const = 0; + + /// Return a textual description of the decision procedure + virtual std::string decision_procedure_text() const = 0; + + /// 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; +}; + +/// 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; +} + +#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H 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(); } } diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index da134f8992f..11046ae2732 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" @@ -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 &); @@ -56,9 +45,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; }; // 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 \ diff --git a/src/util/decision_procedure.h b/src/util/decision_procedure.h deleted file mode 100644 index 5654e0e1740..00000000000 --- a/src/util/decision_procedure.h +++ /dev/null @@ -1,65 +0,0 @@ -/*******************************************************************\ - -Module: Decision Procedure Interface - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Decision Procedure Interface - -#ifndef CPROVER_UTIL_DECISION_PROCEDURE_H -#define CPROVER_UTIL_DECISION_PROCEDURE_H - -#include -#include - -class exprt; - -class decision_proceduret -{ -public: - virtual ~decision_proceduret(); - - // get a value from satisfying instance if satisfiable - // returns nil if not available - virtual exprt get(const exprt &expr) const=0; - - // print satisfying assignment - virtual void print_assignment(std::ostream &out) const=0; - - // add constraints - // the expression must be of Boolean type - virtual void set_to(const exprt &expr, bool value)=0; - - void set_to_true(const exprt &expr) - { set_to(expr, true); } - - void set_to_false(const exprt &expr) - { set_to(expr, false); } - - // 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(); - } - - // return a textual description of the decision procedure - virtual std::string decision_procedure_text() const=0; -}; - -inline decision_proceduret &operator<<( - decision_proceduret &dest, - const exprt &src) -{ - dest.set_to_true(src); - return dest; -} - -#endif // CPROVER_UTIL_DECISION_PROCEDURE_H