ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Public Member Functions | List of all members
rrr::SatSolver< Ntk > Class Template Reference

#include <rrrSatSolver.h>

Public Member Functions

 SatSolver (Parameter const *pPar)
 
 ~SatSolver ()
 
void AssignNetwork (Ntk *pNtk_, bool fReuse)
 
SatResult CheckRedundancy (int id, int idx)
 
SatResult CheckFeasibility (int id, int fi, bool c)
 
std::vector< VarValue > GetCex ()
 
void ResetSummary ()
 
summary< int > GetStatsSummary () const
 
summary< double > GetTimesSummary () const
 

Detailed Description

template<typename Ntk>
class rrr::SatSolver< Ntk >

Definition at line 13 of file rrrSatSolver.h.

Constructor & Destructor Documentation

◆ SatSolver()

template<typename Ntk>
rrr::SatSolver< Ntk >::SatSolver ( Parameter const * pPar)

Definition at line 267 of file rrrSatSolver.h.

267 :
268 pNtk(NULL),
269 nVerbose(pPar->nSatSolverVerbose),
270 nConflictLimit(pPar->nConflictLimit),
271 pSat(sat_solver_new()),
272 status(false),
273 target(-1),
274 fUpdate(false) {
275 ResetSummary();
276 }
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
Here is the call graph for this function:

◆ ~SatSolver()

template<typename Ntk>
rrr::SatSolver< Ntk >::~SatSolver ( )

Definition at line 279 of file rrrSatSolver.h.

279 {
280 sat_solver_delete(pSat);
281 //std::cout << "SAT solver stats: calls = " << nCalls << " (SAT = " << nSats << ", UNSAT = " << nUnsats << ", UNDET = " << nCalls - nSats - nUnsats << ")" << std::endl;
282 }
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Here is the call graph for this function:

Member Function Documentation

◆ AssignNetwork()

template<typename Ntk>
void rrr::SatSolver< Ntk >::AssignNetwork ( Ntk * pNtk_,
bool fReuse )

Definition at line 285 of file rrrSatSolver.h.

285 {
286 (void)fReuse;
287 status = false;
288 target = -1;
289 fUpdate = false;
290 pNtk = pNtk_;
291 pNtk->AddCallback(std::bind(&SatSolver<Ntk>::ActionCallback, this, std::placeholders::_1));
292 }

◆ CheckFeasibility()

template<typename Ntk>
SatResult rrr::SatSolver< Ntk >::CheckFeasibility ( int id,
int fi,
bool c )

Definition at line 375 of file rrrSatSolver.h.

375 {
376 time_point timeStart = GetCurrentTime();
377 SetTarget(id);
378 if(!status) {
379 if(nVerbose) {
380 std::cout << "trivially UNSATISFIABLE" << std::endl;
381 }
382 durationFeasibility += Duration(timeStart, GetCurrentTime());
383 return UNSAT;
384 }
385 vLits.clear();
386 assert(pNtk->GetNodeType(id) == AND);
387 vLits.push_back(toLit(vVars[id]));
388 vLits.push_back(toLitCond(vVars[fi], !c));
389 if(nVerbose) {
390 std::cout << "solving with assumptions: ";
391 std::string delim = "";
392 for(int iLit: vLits) {
393 std::cout << delim << (lit_sign(iLit)? "!": "") << lit_var(iLit);
394 delim = ", ";
395 }
396 std::cout << std::endl;
397 }
398 nCalls++;
399 int res = sat_solver_solve(pSat, vLits.data(), vLits.data() + vLits.size(), nConflictLimit, 0 /*nInsLimit*/, 0 /*nConfLimitGlobal*/, 0 /*nInsLimitGlobal*/);
400 if(res == l_False) {
401 if(nVerbose) {
402 std::cout << "UNSATISFIABLE" << std::endl;
403 }
404 nUnsats++;
405 durationFeasibility += Duration(timeStart, GetCurrentTime());
406 return UNSAT;
407 }
408 if(res == l_Undef) {
409 if(nVerbose) {
410 std::cout << "UNDETERMINED" << std::endl;
411 }
412 durationFeasibility += Duration(timeStart, GetCurrentTime());
413 return UNDET;
414 }
415 assert(res == l_True);
416 if(nVerbose) {
417 std::cout << "SATISFIABLE" << std::endl;
418 }
419 nSats++;
420 vValues.clear();
421 vValues.resize(pNtk->GetNumNodes());
422 pNtk->ForEachPi([&](int id) {
423 if(sat_solver_var_value(pSat, vVars[id])) {
424 vValues[id] = TEMP_TRUE;
425 } else {
426 vValues[id] = TEMP_FALSE;
427 }
428 });
429 pNtk->ForEachInt([&](int id) {
430 if(sat_solver_var_value(pSat, vVars[id])) {
431 vValues[id] = TEMP_TRUE;
432 } else {
433 vValues[id] = TEMP_FALSE;
434 }
435 });
436 // required values
437 assert(vValues[id] == TEMP_TRUE);
438 vValues[id] = DecideVarValue(vValues[id]);
439 assert((vValues[fi] == TEMP_TRUE) ^ !c);
440 vValues[fi] = DecideVarValue(vValues[fi]);
441 durationFeasibility += Duration(timeStart, GetCurrentTime());
442 return SAT;
443 }
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
assert
#define assert(ex)
Definition util_old.h:213

◆ CheckRedundancy()

template<typename Ntk>
SatResult rrr::SatSolver< Ntk >::CheckRedundancy ( int id,
int idx )

Definition at line 299 of file rrrSatSolver.h.

299 {
300 time_point timeStart = GetCurrentTime();
301 SetTarget(id);
302 if(!status) {
303 if(nVerbose) {
304 std::cout << "trivially UNSATISFIABLE" << std::endl;
305 }
306 durationRedundancy += Duration(timeStart, GetCurrentTime());
307 return UNSAT;
308 }
309 vLits.clear();
310 assert(pNtk->GetNodeType(id) == AND);
311 pNtk->ForEachFaninIdx(id, [&](int idx2, int fi, bool c) {
312 if(idx == idx2) {
313 vLits.push_back(toLitCond(vVars[fi], !c));
314 } else {
315 vLits.push_back(toLitCond(vVars[fi], c));
316 }
317 });
318 if(nVerbose) {
319 std::cout << "solving with assumptions: ";
320 std::string delim = "";
321 for(int iLit: vLits) {
322 std::cout << delim << (lit_sign(iLit)? "!": "") << lit_var(iLit);
323 delim = ", ";
324 }
325 std::cout << std::endl;
326 }
327 nCalls++;
328 int res = sat_solver_solve(pSat, vLits.data(), vLits.data() + vLits.size(), nConflictLimit, 0 /*nInsLimit*/, 0 /*nConfLimitGlobal*/, 0 /*nInsLimitGlobal*/);
329 if(res == l_False) {
330 if(nVerbose) {
331 std::cout << "UNSATISFIABLE" << std::endl;
332 }
333 nUnsats++;
334 durationRedundancy += Duration(timeStart, GetCurrentTime());
335 return UNSAT;
336 }
337 if(res == l_Undef) {
338 if(nVerbose) {
339 std::cout << "UNDETERMINED" << std::endl;
340 }
341 durationRedundancy += Duration(timeStart, GetCurrentTime());
342 return UNDET;
343 }
344 assert(res == l_True);
345 if(nVerbose) {
346 std::cout << "SATISFIABLE" << std::endl;
347 }
348 nSats++;
349 vValues.clear();
350 vValues.resize(pNtk->GetNumNodes());
351 pNtk->ForEachPi([&](int id) {
352 if(sat_solver_var_value(pSat, vVars[id])) {
353 vValues[id] = TEMP_TRUE;
354 } else {
355 vValues[id] = TEMP_FALSE;
356 }
357 });
358 pNtk->ForEachInt([&](int id) {
359 if(sat_solver_var_value(pSat, vVars[id])) {
360 vValues[id] = TEMP_TRUE;
361 } else {
362 vValues[id] = TEMP_FALSE;
363 }
364 });
365 // required values
366 pNtk->ForEachFaninIdx(id, [&](int idx2, int fi, bool c) {
367 assert((vValues[fi] == TEMP_TRUE) ^ (idx == idx2) ^ c);
368 vValues[fi] = DecideVarValue(vValues[fi]);
369 });
370 durationRedundancy += Duration(timeStart, GetCurrentTime());
371 return SAT;
372 }

◆ GetCex()

template<typename Ntk>
std::vector< VarValue > rrr::SatSolver< Ntk >::GetCex ( )

Definition at line 450 of file rrrSatSolver.h.

450 {
451 if(nVerbose) {
452 std::cout << "cex: ";
453 pNtk->ForEachPi([&](int id) {
454 std::cout << GetVarValueChar(vValues[id]);
455 });
456 std::cout << std::endl;
457 }
458 // reverse simulation
459 pNtk->ForEachIntReverse([&](int id) {
460 switch(pNtk->GetNodeType(id)) {
461 case AND:
462 if(vValues[id] == TRUE) {
463 pNtk->ForEachFanin(id, [&](int fi, bool c) {
464 assert((vValues[fi] == TEMP_TRUE || vValues[fi] == TRUE) ^ c);
465 vValues[fi] = DecideVarValue(vValues[fi]);
466 });
467 } else if(vValues[id] == FALSE) {
468 bool fFound = false;
469 pNtk->ForEachFanin(id, [&](int fi, bool c) {
470 if(fFound) {
471 return;
472 }
473 if(c) {
474 if(vValues[fi] == TRUE) {
475 fFound = true;
476 }
477 } else {
478 if(vValues[fi] == FALSE) {
479 fFound = true;
480 }
481 }
482 });
483 if(!fFound) {
484 pNtk->ForEachFanin(id, [&](int fi, bool c) {
485 if(fFound) {
486 return;
487 }
488 if(c) {
489 if(vValues[fi] == TEMP_TRUE) {
490 fFound = true;
491 vValues[fi] = DecideVarValue(vValues[fi]);
492 }
493 } else {
494 if(vValues[fi] == TEMP_FALSE) {
495 fFound = true;
496 vValues[fi] = DecideVarValue(vValues[fi]);
497 }
498 }
499 });
500 }
501 }
502 break;
503 default:
504 assert(0);
505 }
506 });
507 if(nVerbose) {
508 std::cout << "pex: ";
509 pNtk->ForEachPi([&](int id) {
510 std::cout << GetVarValueChar(vValues[id]);
511 });
512 std::cout << std::endl;
513 }
514 // debug
515 pNtk->ForEachInt([&](int id) {
516 switch(pNtk->GetNodeType(id)) {
517 case AND:
518 if(vValues[id] == TRUE) {
519 pNtk->ForEachFanin(id, [&](int fi, bool c) {
520 assert(c || vValues[fi] == TRUE);
521 assert(!c || vValues[fi] == FALSE);
522 });
523 } else if(vValues[id] == FALSE) {
524 bool fFound = false;
525 pNtk->ForEachFanin(id, [&](int fi, bool c) {
526 if(fFound) {
527 return;
528 }
529 if(c) {
530 if(vValues[fi] == TRUE) {
531 fFound = true;
532 }
533 } else {
534 if(vValues[fi] == FALSE) {
535 fFound = true;
536 }
537 }
538 });
539 assert(fFound);
540 }
541 break;
542 default:
543 assert(0);
544 }
545 });
546 // retrieve partial cex
547 std::vector<VarValue> vPartialCex;
548 pNtk->ForEachPi([&](int id) {
549 if(vValues[id] == TRUE || vValues[id] == FALSE) {
550 vPartialCex.push_back(vValues[id]);
551 } else {
552 vPartialCex.push_back(UNDEF);
553 }
554 });
555 return vPartialCex;
556 }

◆ GetStatsSummary()

template<typename Ntk>
summary< int > rrr::SatSolver< Ntk >::GetStatsSummary ( ) const

Definition at line 572 of file rrrSatSolver.h.

572 {
573 summary<int> v;
574 v.emplace_back("sat call", nCalls);
575 v.emplace_back("sat satisfiable", nSats);
576 v.emplace_back("sat unsatisfiable", nUnsats);
577 return v;
578 }

◆ GetTimesSummary()

template<typename Ntk>
summary< double > rrr::SatSolver< Ntk >::GetTimesSummary ( ) const

Definition at line 581 of file rrrSatSolver.h.

581 {
582 summary<double> v;
583 v.emplace_back("sat redundancy", durationRedundancy);
584 v.emplace_back("sat feasibility", durationFeasibility);
585 return v;
586 }

◆ ResetSummary()

template<typename Ntk>
void rrr::SatSolver< Ntk >::ResetSummary ( )

Definition at line 563 of file rrrSatSolver.h.

563 {
564 nCalls = 0;
565 nSats = 0;
566 nUnsats = 0;
567 durationRedundancy = 0;
568 durationFeasibility = 0;
569 }
Here is the caller graph for this function:
The documentation for this class was generated from the following file: