From c283598289c6084cf7fa93c399c3eeea51a61df3 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 13 Jan 2011 12:54:12 +0000 Subject: [PATCH] Remove experimental code (that wasn't enabled). That doesn't help. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1063 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/bvsolver.cpp | 53 +++++-------------------------------- 1 file changed, 7 insertions(+), 46 deletions(-) diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 2a34fb1..b151e79 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -723,12 +723,12 @@ namespace BEEV for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { /* - Calling simplifyFormula makes the required substitutions. For instance, if + Calling applySubstitutionMapUntilArrays makes the required substitutions. For instance, if first was : v = x, then if the next formula is: x = v - calling simplify on the second formula will convert it into "true", avoiding a cycle. + calling applySubstitutionMapUntilArrays on the second formula will convert it into "true", avoiding a cycle. - The problem with this is that Simplify___() doesn't normally simplify into array + The problem with this is that applySubstitutionMapUntilArrays() doesn't normally simplify into array operations. So given something like : a = b b = write(A,a,a) @@ -738,53 +738,14 @@ namespace BEEV rewrite a=b through the second expression, giving: b = write(A,b,b), which shouldn't be simplified. - - Simplifying through arrays is very expensive though. I know how to fix it, but - don't have time. Trev. - */ -#if 1 + */ ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it; - #else - ASTNode aaa = *it; - - if (any_solved && EQ == aaa.GetKind()) - { - bool found = false; - - ASTNodeSet var; - SetofVarsSeenInTerm(aaa[0], var); - - for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++) - if (_simp->CheckSubstitutionMap(*it)) - { - found = true; - break; - } - - if (!found) - { - var.clear(); - SetofVarsSeenInTerm(aaa[1], var); - - for (ASTNodeSet::const_iterator it = var.begin(); it != var.end(); it++) - if (_simp->CheckSubstitutionMap(*it)) - { - found = true; - break; - } - } - if (found) - aaa = _simp->applySubstitutionMapUntilArrays(aaa); - } - -#endif + if (ASTFalse == aaa) + return ASTFalse; // shortcut. It's unsatisfiable. - //_bm->ASTNodeStats("Printing after calling simplifyformula - //inside the solver:", aaa); aaa = BVSolve_Odd(aaa); - //_bm->ASTNodeStats("Printing after oddsolver:", aaa); bool even = false; aaa = CheckEvenEqn(aaa, even); if (even) @@ -800,7 +761,7 @@ namespace BEEV } if (ASTTrue == aaa) { - any_solved=true; + any_solved=true; } } -- 2.47.3