spot  2.12
satsolver.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <spot/misc/common.hh>
22 #include <spot/misc/tmpfile.hh>
23 #include <vector>
24 #include <stdexcept>
25 #include <iosfwd>
26 #include <initializer_list>
27 
28 struct PicoSAT; // forward
29 
30 namespace spot
31 {
32  class printable;
33 
43  {
44  private:
45  const char* satsolver;
46 
47  public:
49 
51  bool command_given();
52 
54  int run(printable* in, printable* out);
55 
56  };
57 
69  class SPOT_API satsolver
70  {
71  public:
76  ~satsolver();
77 
79  void adjust_nvars(int nvars);
80 
82  void set_nassumptions_vars(int nassumptions_vars);
83 
85  void add(std::initializer_list<int> values);
86 
88  void add(int v);
89 
91  int get_nb_clauses() const;
92 
94  int get_nb_vars() const;
95 
97  std::pair<int, int> stats() const;
98 
101  template<typename T>
102  void comment_rec(T single);
103 
106  template<typename T, typename... Args>
107  void comment_rec(T first, Args... args);
108 
111  template<typename T>
112  void comment(T single);
113 
116  template<typename T, typename... Args>
117  void comment(T first, Args... args);
118 
121  void assume(int lit);
122 
123  typedef std::vector<bool> solution;
124  typedef std::pair<int, solution> solution_pair;
125 
127  solution_pair get_solution();
128 
129  private: // methods
131  void start();
132 
134  void end_clause();
135 
138  satsolver::solution
139  picosat_get_sol(int res);
140 
142  satsolver::solution
143  satsolver_get_sol(const char* filename);
144 
146  bool
147  xcnf_mode();
148 
149  private: // variables
151  satsolver_command cmd_;
152 
153  // cnf streams and associated clause counter.
154  // The next 2 pointers will be != nullptr if SPOT_SATSOLVER is given.
155  temporary_file* cnf_tmp_;
156  std::ostream* cnf_stream_;
157  int nclauses_;
158  int nvars_;
159  int nassumptions_vars_; // Surplus of vars (for 'assume' algorithm).
160 
163  int nsols_;
164 
166  PicoSAT* psat_;
167 
168  // The next 2 pointers will be initialized if SPOT_XCNF env var
169  // is set. This requires SPOT_SATSOLVER to be set as well.
170  std::ofstream* xcnf_tmp_;
171  std::ofstream* xcnf_stream_;
172  std::string path_;
173  };
174 
175  template<typename T>
176  void
178  {
179  if (!psat_)
180  *cnf_stream_ << ' ' << single;
181  }
182 
183  template<typename T, typename... Args>
184  void
185  satsolver::comment_rec(T first, Args... args)
186  {
187  if (!psat_)
188  {
189  *cnf_stream_ << ' ' << first;
190  comment_rec(args...);
191  }
192  }
193 
194  template<typename T>
195  void
197  {
198  if (!psat_)
199  *cnf_stream_ << "c " << single;
200  }
201 
202  template<typename T, typename... Args>
203  void
204  satsolver::comment(T first, Args... args)
205  {
206  if (!psat_)
207  {
208  *cnf_stream_ << "c " << first;
209  comment_rec(args...);
210  }
211  }
212 
213 }
Definition: formater.hh:112
Definition: formater.hh:30
Interface with a given sat solver.
Definition: satsolver.hh:43
bool command_given()
Return true if a satsolver is given, false otherwise.
int run(printable *in, printable *out)
Run the given satsolver.
Interface with a SAT solver.
Definition: satsolver.hh:70
std::pair< int, int > stats() const
Returns std::pair<nvars, nclauses>;.
void add(std::initializer_list< int > values)
Add a list of lit. to the current clause.
void add(int v)
Add a single lit. to the current clause.
solution_pair get_solution()
Return std::vector<solving_return_code, solution>.
satsolver()
Construct the sat solver and initialize variables. If no satsolver is provided through SPOT_SATSOLVER...
int get_nb_vars() const
Get the current number of variables.
void comment(T single)
Add a comment. It will start with "c ". It should be used only in debug mode after providing a satsol...
Definition: satsolver.hh:196
void comment_rec(T single)
Add a comment. It should be used only in debug mode after providing a satsolver.
Definition: satsolver.hh:177
void set_nassumptions_vars(int nassumptions_vars)
Declare the number of vars reserved for assumptions.
int get_nb_clauses() const
Get the current number of clauses.
void assume(int lit)
Assume a literal value. Must only be used with distributed picolib.
void adjust_nvars(int nvars)
Adjust the number of variables used in the cnf formula.
Temporary file name.
Definition: tmpfile.hh:49
Definition: automata.hh:26

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1