From: trevor_hansen Date: Thu, 5 Jan 2012 13:04:33 +0000 (+0000) Subject: Probably a refactor. This comments out the write-refinement loop that I broke >1... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8d618b8c3916084b2b62e1646c4d1e6bc70a070b;p=francis%2Fstp.git Probably a refactor. This comments out the write-refinement loop that I broke >1 year ago without realising. I'm commenting it out to prevent confusion to others. If it worked I don't know how useful it'd be. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1473 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 9c71222..13fbad6 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -353,6 +353,7 @@ namespace BEEV { bm->ASTNodeStats("After AIG Core: ", simplified_solved_InputToSAT); } +#if 0 bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT); bm->SimplifyWrites_InPlace_Flag = true; @@ -401,6 +402,7 @@ namespace BEEV { while (inputToSAT != simplified_solved_InputToSAT); bm->ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT); +#endif if (bm->UserFlags.isSet("enable-unconstrained", "1")) { @@ -534,6 +536,7 @@ namespace BEEV { return res; } + #if 0 res = Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, original_input, satBase); if (SOLVER_UNDECIDED != res) { @@ -553,18 +556,14 @@ namespace BEEV { CountersAndStats("print_func_stats", bm); return res; } + #endif + + FatalError("TopLevelSTPAux: reached the end without proper conclusion:" + "either a divide by zero in the input or a bug in STP"); + //bogus return to make the compiler shut up + return SOLVER_ERROR; + -// if (!bm->UserFlags.num_absrefine_flag) - { - FatalError("TopLevelSTPAux: reached the end without proper conclusion:" - "either a divide by zero in the input or a bug in STP"); - //bogus return to make the compiler shut up - return SOLVER_ERROR; - } - // else - { - // return res; - } } //End of TopLevelSTPAux #if 0 diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index 0fc6942..c7437fc 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -130,12 +130,6 @@ namespace BEEV ToSATBase* tosat, bool refinement); - //creates array write axiom only for the input term or formula, if - //necessary. If there are no axioms to produce then it simply - //generates TRUE - ASTNode - Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, - const ASTNode& array_newname); SOLVER_RETURN_TYPE SATBased_ArrayReadRefinement(SATSolver& newS, @@ -143,11 +137,21 @@ namespace BEEV const ASTNode& original_input, ToSATBase* tosat); +#if 0 SOLVER_RETURN_TYPE SATBased_ArrayWriteRefinement(SATSolver& newS, const ASTNode& orig_input, ToSATBase *tosat); + //creates array write axiom only for the input term or formula, if + //necessary. If there are no axioms to produce then it simply + //generates TRUE + ASTNode + Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term, + const ASTNode& array_newname); + +#endif + void ClearAllTables(void) { CounterExampleMap.clear(); diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index 4de6756..3209b6e 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -418,6 +418,9 @@ namespace BEEV } //end of SATBased_ArrayReadRefinement +#if 0 + // This isn't currently wired up. + /****************************************************************** * ARRAY WRITE ABSTRACTION REFINEMENT * @@ -497,5 +500,5 @@ namespace BEEV ASTNode arraywrite_axiom = simp->CreateSimplifiedEQ(lhs, rhs); return arraywrite_axiom; }//end of Create_ArrayWriteAxioms() - +#endif };// end of namespace BEEV diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 5a88368..fa3c59b 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -2872,8 +2872,10 @@ namespace BEEV //process only if not in the substitution map. simplifymap //has been checked already +#if 0 if (!CheckSubstitutionMap(out1, out1) && out1.GetKind() == READ && WRITE == out1[0].GetKind()) out1 = RemoveWrites_TopLevel(out1); +#endif //it is possible that after all the procesing the READ term //reduces to READ(Symbol,const) and hence we should check the @@ -3325,6 +3327,7 @@ namespace BEEV return output; } //end of distributemultoverplus() +#if 0 //converts the BVSX(len, a0) operator into ITE( check top bit, //extend a0 by 1, extend a0 by 0) ASTNode @@ -3389,7 +3392,9 @@ namespace BEEV UpdateSimplifyMap(a, output, false); return output; } //end of ConvertBVSXToITE() +#endif +#if 0 ASTNode Simplifier::RemoveWrites_TopLevel(const ASTNode& term) { @@ -3412,6 +3417,7 @@ namespace BEEV return RemoveWrites(term); } } //end of RemoveWrites_TopLevel() +#endif // recursively simplify things that are of type array. @@ -3459,6 +3465,7 @@ namespace BEEV return output; } +#if 0 ASTNode Simplifier::SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap) { @@ -3605,6 +3612,7 @@ namespace BEEV return output; } //end of RemoveWrites() + ASTNode Simplifier::ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap) { @@ -3692,6 +3700,7 @@ namespace BEEV //UpdateSimplifyMap(term,output,false); return output; } //ReadOverWrite_To_ITE() +#endif //compute the multiplicative inverse of the input ASTNode @@ -3834,10 +3843,13 @@ namespace BEEV cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl; cerr << "AlwaysTrueFormSet" << AlwaysTrueHashSet.size() << ":" << AlwaysTrueHashSet.bucket_count() << endl; cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl; + +#if 0 cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" << ReadOverWrite_NewName_Map->bucket_count() << endl; cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" << NewName_ReadOverWrite_Map.bucket_count() << endl; +#endif cerr << "substn_map" << substitutionMap.Return_SolverMap()->size() << ":" << substitutionMap.Return_SolverMap()->bucket_count() << endl; diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 2aebf64..f3e938e 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -41,11 +41,11 @@ namespace BEEV // For ArrayWrite Abstraction: map from read-over-write term to // newname. - ASTNodeMap * ReadOverWrite_NewName_Map; + //ASTNodeMap * ReadOverWrite_NewName_Map; // For ArrayWrite Refinement: Map new arraynames to // Read-Over-Write terms - ASTNodeMap NewName_ReadOverWrite_Map; + //ASTNodeMap NewName_ReadOverWrite_Map; //Ptr to STP Manager STPMgr * _bm; @@ -73,7 +73,7 @@ namespace BEEV { SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE); SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); - ReadOverWrite_NewName_Map = new ASTNodeMap(); + //ReadOverWrite_NewName_Map = new ASTNodeMap(); ASTTrue = bm->CreateNode(TRUE); ASTFalse = bm->CreateNode(FALSE); @@ -86,7 +86,7 @@ namespace BEEV { delete SimplifyMap; delete SimplifyNegMap; - delete ReadOverWrite_NewName_Map; + //delete ReadOverWrite_NewName_Map; delete nf; } @@ -213,7 +213,7 @@ namespace BEEV ASTNode DistributeMultOverPlus(const ASTNode& a, bool startdistribution = false); - ASTNode ConvertBVSXToITE(const ASTNode& a); + //ASTNode ConvertBVSXToITE(const ASTNode& a); ASTNode BVConstEvaluator(const ASTNode& t); @@ -231,17 +231,19 @@ namespace BEEV ASTNode SimplifyArrayTerm(const ASTNode& term,ASTNodeMap* VarConstMap); - ASTNode ReadOverWrite_To_ITE(const ASTNode& term, - ASTNodeMap* VarConstMap=NULL); + //ASTNode ReadOverWrite_To_ITE(const ASTNode& term, + // ASTNodeMap* VarConstMap=NULL); void printCacheStatus(); +#if 0 //FIXME: Get rid of this horrible function const ASTNodeMap * ReadOverWriteMap() { return ReadOverWrite_NewName_Map; } // End of ReadOverWriteMap() - +#endif + bool hasUnappliedSubstitutions() { return substitutionMap.hasUnappliedSubstitutions(); @@ -262,8 +264,8 @@ namespace BEEV { SimplifyMap->clear(); SimplifyNegMap->clear(); - ReadOverWrite_NewName_Map->clear(); - NewName_ReadOverWrite_Map.clear(); + //ReadOverWrite_NewName_Map->clear(); + //NewName_ReadOverWrite_Map.clear(); AlwaysTrueHashSet.clear(); MultInverseMap.clear(); substitutionMap.clear();