24 std::cout <<
"enter: No Lit.=" <<
no_variables() <<
"\n";
32 out <<
"# PBType: E" <<
"\n";
33 out <<
"# PBGoal: " <<
goal <<
"\n";
37 out <<
"# PBType: SE" <<
"\n";
38 out <<
"# PBGoal: " <<
d_sum <<
"\n";
39 out <<
"# PBObj : MIN" <<
"\n";
43 out <<
"# PBType: GE" <<
"\n";
44 out <<
"# PBGoal: " << 0 <<
"\n";
45 out <<
"# PBObj : MAX" <<
"\n";
64 std::cout <<
"solve: No Lit.=" <<
no_variables() <<
"\n";
72 if(command.substr(command.length(), 1) !=
"/")
79 std::cout <<
"PBS COMMAND IS: " << command <<
"\n";
84 command=
getenv(
"PBS_PATH");
88 error (
"Unable to read PBS_PATH environment variable.\n");
93 command +=
" -f temp.cnf";
100 command +=
" -S 1000 -D 1 -H -I -a";
105 std::cout <<
"NO BINARY SEARCH"
108 command +=
" -S 1000 -D 1 -I -a";
113 command +=
" -S 1000 -D 1 -a";
119 command +=
" -a > temp.out";
124 std::ifstream file(
"temp.out");
137 while(file && !file.eof())
139 std::getline(file, line);
141 strstr(line.c_str(),
"Variable Assignments Satisfying CNF Formula:") !=
145 std::cout <<
"Reading assignments...\n";
156 std::cout << v <<
" ";
163 std::cout <<
"Finished reading assignments.\n";
166 else if(
strstr(line.c_str(),
"SAT... SUM") !=
nullptr)
173 else if(
strstr(line.c_str(),
"SAT - All implied") !=
nullptr)
180 "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d",
183 else if(
strstr(line.c_str(),
"SAT... Solution") !=
nullptr)
190 else if(
strstr(line.c_str(),
"Optimal Soln") !=
nullptr)
195 if(
strstr(line.c_str(),
"time out") !=
nullptr)
197 log.
status() <<
"WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT."
212 std::ofstream file(
"temp.cnf");
216 std::ofstream
pbfile(
"temp.cnf.pb");
235 log.
status() <<
"PBS checker: system is SATISFIABLE";
266 std::cout <<
"FALSE\n";
273 std::cout <<
"TRUE\n";
283 std::cout <<
"FALSE\n";
290 std::cout <<
"TRUE\n";
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
virtual size_t no_variables() const override
virtual void write_dimacs_cnf(std::ostream &out) const
mstreamt & statistics() const
mstreamt & status() const
tvt l_get(literalt a) const override
resultt do_prop_solve(const bvt &assumptions) override
virtual void write_dimacs_pb(std::ostream &out)
std::map< literalt, unsigned > pb_constraintmap
std::vector< literalt > bvt
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
int sscanf(const char *restrict s, const char *restrict format,...)
char * getenv(const char *name)