From 823166d849e5117762d8b6a7457339ae78c4a452 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 11 May 2011 04:23:04 +0000 Subject: [PATCH] Improvement. Exit-after-cnf would exit after sending the CNF to the SAT solver. We used to read the CNF back out of the SAT solver, but don't any longer, so there's no reason to do this. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1328 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/AIG/ToSATAIG.cpp | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 011e5b2..63b9659 100644 --- a/src/to-sat/AIG/ToSATAIG.cpp +++ b/src/to-sat/AIG/ToSATAIG.cpp @@ -72,6 +72,18 @@ namespace BEEV } first = false; + if (bm->UserFlags.exit_after_CNF) + { + if (bm->UserFlags.quick_statistics_flag) + bm->GetRunTimes()->print(); + + if (needAbsRef) + cerr << "Warning: STP is exiting after generating the first CNF. But the CNF" + " is probably partial which you probably don't want. You probably want to disable" + " refinement with the \"-r\" command line option." << endl; + + exit(0); + } bm->GetRunTimes()->start(RunTimes::SendingToSAT); @@ -119,18 +131,6 @@ namespace BEEV toCNF.setPrior(cnfData); } - if (bm->UserFlags.exit_after_CNF) - { - if (bm->UserFlags.quick_statistics_flag) - bm->GetRunTimes()->print(); - - if (needAbsRef) - cerr << "Warning: STP is exiting after generating the first CNF. But the CNF" - "is probably partial which you probably don't want. You probably want to disable" - "refinement with the \"-r\" command line option." << endl; - - exit(0); - } bm->GetRunTimes()->start(RunTimes::Solving); satSolver.solve(); -- 2.47.3