cloud9_root/src/third_party/stp/src/STPManager/STP.cpp
// The absolute TopLevel function that invokes STP on the input
// formula
The absolute TopLevel function that invokes STP on the input
formula
The absolute TopLevel function that invokes STP on the input formula
SOLVER_RETURN_TYPE STP::TopLevelSTP(const ASTNode& inputasserts, 
				      const ASTNode& query)
  {      
    ASTNode original_input;
    if (query != bm->ASTFalse)
      original_input = bm->CreateNode(AND,
					    inputasserts, 
					    bm->CreateNode(NOT, query));
    else
      original_input = inputasserts;
    SATSolver *newS;
    if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER)
		newS = new SimplifyingMinisat();
    else if (bm->UserFlags.solver_to_use == UserDefinedFlags::CRYPTOMINISAT_SOLVER)
                    newS = new CryptoMinisat();
    else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER)
      newS = new MinisatCore<Minisat::Solver>();
    else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
      newS = new MinisatCore_prop<Minisat::Solver_prop>();
    SATSolver& NewSolver = *newS;
    if(bm->UserFlags.stats_flag)
      {
	NewSolver.setVerbosity(1);
      }
	SOLVER_RETURN_TYPE result;
    result = TopLevelSTPAux(NewSolver,
			      original_input);
    delete newS;
    return result;
  }
SOLVER_RETURN_TYPE STP :: TopLevelSTP ( const ASTNode & inputasserts , const ASTNode & query ) { ASTNode original_input ; if ( query != bm -> ASTFalse ) original_input = bm -> CreateNode ( AND , inputasserts , bm -> CreateNode ( NOT , query ) ) ; else original_input = inputasserts ; SATSolver * newS ; if ( bm -> UserFlags . solver_to_use == UserDefinedFlags :: SIMPLIFYING_MINISAT_SOLVER ) newS = new SimplifyingMinisat ( ) ; else if ( bm -> UserFlags . solver_to_use == UserDefinedFlags :: CRYPTOMINISAT_SOLVER ) newS = new CryptoMinisat ( ) ; else if ( bm -> UserFlags . solver_to_use == UserDefinedFlags :: MINISAT_SOLVER ) newS = new MinisatCore < Minisat :: Solver > ( ) ; else if ( bm -> UserFlags . solver_to_use == UserDefinedFlags :: MINISAT_PROPAGATORS ) newS = new MinisatCore_prop < Minisat :: Solver_prop > ( ) ; SATSolver & NewSolver = * newS ; if ( bm -> UserFlags . stats_flag ) { NewSolver . setVerbosity ( 1 ) ; } SOLVER_RETURN_TYPE result ; result = TopLevelSTPAux ( NewSolver , original_input ) ; delete newS ; return result ; }
The absolute TopLevel function that invokes STP on the input
formula
The absolute TopLevel function that invokes STP on the input formula
//solver instantiated here //#if defined CRYPTOMINISAT2 //MINISAT::Solver NewSolver; //if(bm->UserFlags.print_cnf_flag) //{ //NewSolver.needLibraryCNFFile(bm->UserFlags.cnf_dump_filename); //} //#endif