cprover
qbf_quantor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "qbf_quantor.h"
10 
11 #include <cassert>
12 #include <cstdlib>
13 #include <fstream>
14 
16 {
17 }
18 
20 {
21 }
22 
24 {
25  assert(false);
26  return tvt::unknown();
27 }
28 
29 const std::string qbf_quantort::solver_text()
30 {
31  return "Quantor";
32 }
33 
35 {
36  {
37  messaget::status() <<
38  "Quantor: " <<
39  no_variables() << " variables, " <<
40  no_clauses() << " clauses" << eom;
41  }
42 
43  std::string qbf_tmp_file="quantor.qdimacs";
44  std::string result_tmp_file="quantor.out";
45 
46  {
47  std::ofstream out(qbf_tmp_file.c_str());
48 
49  // write it
50  write_qdimacs_cnf(out);
51  }
52 
53  // solve it
54  int res=system((
55  "quantor "+qbf_tmp_file+" -o "+result_tmp_file).c_str());
56  CHECK_RETURN(0==res);
57 
58  bool result=false;
59 
60  // read result
61  {
62  std::ifstream in(result_tmp_file.c_str());
63 
64  bool result_found=false;
65  while(in)
66  {
67  std::string line;
68 
69  std::getline(in, line);
70 
71  if(line!="" && line[line.size()-1]=='\r')
72  line.resize(line.size()-1);
73 
74  if(line=="s TRUE")
75  {
76  result=true;
77  result_found=true;
78  break;
79  }
80  else if(line=="s FALSE")
81  {
82  result=false;
83  result_found=true;
84  break;
85  }
86  }
87 
88  if(!result_found)
89  {
90  messaget::error() << "Quantor failed: unknown result" << eom;
91  return resultt::P_ERROR;
92  }
93  }
94 
95  if(result)
96  {
97  messaget::status() << "Quantor: TRUE" << eom;
99  }
100  else
101  {
102  messaget::status() << "Quantor: FALSE" << eom;
104  }
105 
106  return resultt::P_ERROR;
107 }
static tvt unknown()
Definition: threeval.h:33
virtual tvt l_get(literalt a) const
Definition: qbf_quantor.cpp:23
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Definition: threeval.h:19
mstreamt & error() const
Definition: message.h:302
resultt
Definition: prop.h:96
virtual size_t no_clauses() const
virtual ~qbf_quantort()
Definition: qbf_quantor.cpp:19
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
virtual const std::string solver_text()
Definition: qbf_quantor.cpp:29
virtual size_t no_variables() const override
Definition: cnf.h:38
virtual resultt prop_solve()
Definition: qbf_quantor.cpp:34
virtual void write_qdimacs_cnf(std::ostream &out)
Definition: qdimacs_cnf.cpp:14