Made the solver use the results of partial solving.

libraries/pbes/include/mcrl2/pbes/pbesreach.h

@@ -607,15 +607,21 @@ class pbesreach_algorithm
     virtual void on_end_while_loop()
     { }
 
-    /// \returns True iff the solution was already found.
-    virtual bool solution_found(const sylvan::ldds::ldd&)
+    /// \returns True iff the solution for the given vertex is known.
+    virtual bool solution_found(const sylvan::ldds::ldd&) const
     {
       return false;
     }
 
-    virtual bool solution() const
+    /// \returns True iff the vertex is won by even and nothing if the solution has not been determined.
+    virtual sylvan::ldds::ldd W0() const
     {
-      return false;
+      return sylvan::ldds::empty_set();
+    }
+
+    virtual sylvan::ldds::ldd W1() const
+    {
+      return sylvan::ldds::empty_set();
     }
 
     const std::vector<summand_group>& summand_groups() const

libraries/pbes/include/mcrl2/pbes/symbolic_pbessolve.h

@@ -425,14 +425,16 @@ class symbolic_pbessolve_algorithm
 
     bool solve(const ldd& V,
                const ldd& initial_vertex,
-               const ldd& Vdeadlock = sylvan::ldds::empty_set())
+               const ldd& Vdeadlock = sylvan::ldds::empty_set(),
+               const ldd& W0 = sylvan::ldds::empty_set(),
+               const ldd& W1 = sylvan::ldds::empty_set())
     {
-      auto const& [W0, W1] = solve_impl(V, initial_vertex, Vdeadlock);
-      if (includes(W0, initial_vertex))
+      auto const& [solved0, solved1] = solve_impl(V, initial_vertex, Vdeadlock, W0, W1);
+      if (includes(solved0, initial_vertex))
       {
         return true;
       }
-      else if (includes(W1, initial_vertex))
+      else if (includes(solved1, initial_vertex))
       {
         return false;
       }

tools/developer/pbessolvesymbolic/pbessolvesymbolic.cpp

@@ -103,31 +103,33 @@ class pbesreach_algorithm_partial : public pbes_system::pbesreach_algorithm
     }
   }
 
-  bool solution_found(const sylvan::ldds::ldd& initial_state) override
+  bool solution_found(const ldd& initial_state) const override
   {
     if (includes(m_Vwon[0], initial_state))
     {
-      m_result = true;
       return true;
     }
     else if (includes(m_Vwon[1], initial_state))
     {
-      m_result = false;
       return true;
     }
 
     return false;
   }
 
-  bool solution() const override
+  ldd W0() const override
   {
-    return m_result;
+    return m_Vwon[0];
+  }
+
+  ldd W1() const override
+  {
+    return m_Vwon[1];
   }
 
 private:
   // States for which winners have already been determined.
   std::array<sylvan::ldds::ldd, 2> m_Vwon;
-  bool m_result = false;
   std::size_t iteration_count = 0;
 };
 
@@ -290,15 +292,15 @@ class pbessolvesymbolic_tool: public rewriter_tool<input_output_tool>
 
         if (reach.solution_found(reach.initial_state()))
         {
-          std::cout << (reach.solution() ? "true" : "false") << std::endl;
+          std::cout << (includes(reach.W0(), (reach.initial_state())) ? "true" : "false") << std::endl;
         }
         else
         {
           auto equation_info = compute_equation_info(reach.pbes(), reach.data_index());
           pbes_system::symbolic_pbessolve_algorithm solver(V, reach.summand_groups(), equation_info, options.no_relprod, options.chaining, reach.data_index());
           mCRL2log(log::debug) << pbes_system::print_pbes_info(reach.pbes()) << std::endl;
           timer().start("solving");
-          bool result = solver.solve(V, reach.initial_state(), reach.deadlocks());
+          bool result = solver.solve(V, reach.initial_state(), reach.deadlocks(), reach.W0(), reach.W1());
           timer().finish("solving");
 
           std::cout << (result ? "true" : "false") << std::endl;