From 129fe727b36c3c9223d64cb12a9ff915c14d5f92 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 8 Jun 2010 14:18:04 +0000 Subject: [PATCH] Bugfix. Avoid creating cycles with the bvsolver. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@817 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/bvsolver.cpp | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index dad5d27..e1d9edd 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -617,19 +617,25 @@ namespace BEEV else c = input.GetChildren(); ASTVec eveneqns; - ASTNode solved = ASTFalse; + bool any_solved = false; for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) { //_bm->ASTNodeStats("Printing before calling simplifyformula //inside the solver:", *it); - ASTNode aaa = - (ASTTrue == solved - && EQ == it->GetKind()) ? - _simp->SimplifyFormula(*it, false) : - *it; + + // Calling simplifyFormula 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. + ASTNode aaa = + (any_solved + && EQ == it->GetKind()) ? + _simp->SimplifyFormula(*it, false) : + *it; //_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); @@ -644,7 +650,8 @@ namespace BEEV o.push_back(aaa); } } - solved = aaa; + if (ASTTrue == aaa) + any_solved=true; } ASTNode evens; -- 2.47.3