40 #ifndef __SAT_SOLVER__
41 #define __SAT_SOLVER__
44 #include <sys/resource.h>
50 #ifndef __SAT_STATUS__
51 #define __SAT_STATUS__
157 vector<pair<int,pair< HookFunPtrT, int> > >
_hooks;
211 vector<CLitPoolElement *> & neg_ht_clauses);
213 vector<CLitPoolElement*> & neg_ht_clauses);
289 getrusage(RUSAGE_SELF, &ru);
290 return ( ru.ru_utime.tv_sec*1000 +
291 ru.ru_utime.tv_usec/1000+
292 ru.ru_stime.tv_sec*1000 +
293 ru.ru_stime.tv_usec/1000 );
299 gettimeofday(&tv,&tz);
300 return (tv.tv_sec * 1000 + tv.tv_usec/1000) ;
331 int mem_assignment = 0;
335 return mem_dbase + mem_assignment;
341 pair<HookFunPtrT, int> a(fun, interval);
342 _hooks.push_back(pair<
int, pair<HookFunPtrT, int> > (0, a));
346 CHECK (cout <<
"\t\t\t\t\t\tQueueing " << (lit&0x01?
" -":
" +") << (lit>>1) ;
347 cout <<
" because of " << ante_clause <<
endl; );
360 cout <<
"Restarting ... " <<
endl;
363 for (
unsigned i=1; i<
variables().size(); ++i) {
374 int solve(
bool allowNewClauses);
381 void dump(ostream & os = cout ) {