diff options
Diffstat (limited to 'src/theory/arith/dio_solver.h')
-rw-r--r-- | src/theory/arith/dio_solver.h | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 677040615..c5a0f534f 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -338,22 +338,8 @@ private: /** Returns true if the queue of nodes to process is empty. */ bool queueEmpty() const; - bool queueConditions(TrailIndex t){ - /* debugPrintTrail(t); */ - - /* std::cout << !inConflict() << std::endl; */ - /* std::cout << gcdIsOne(t) << std::endl; */ - /* std::cout << !debugAnySubstitionApplies(t) << std::endl; */ - /* std::cout << !triviallySat(t) << std::endl; */ - /* std::cout << !triviallyUnsat(t) << std::endl; */ - - return - !inConflict() && - gcdIsOne(t) && - !debugAnySubstitionApplies(t) && - !triviallySat(t) && - !triviallyUnsat(t); - } + bool queueConditions(TrailIndex t); + void pushToQueueBack(TrailIndex t){ Assert(queueConditions(t)); |