# This is a -*- makefile -*-, Emacs
+#
#Please refer LICENSE FILE in the home directory for licensing
#information always use full screen mode to view/edit this file in
#emacs
#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
-#OPTIMIZE = -g # Debugging
-OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
+OPTIMIZE = -g # Debugging
+#OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
CFLAGS_BASE = $(OPTIMIZE)
-# You can compile using make STATIC=true to compile a statically linked executable
-# Note that you should execute liblinks.sh first.
+
+# You can compile using make STATIC=true to compile a statically
+# linked executable Note that you should execute liblinks.sh first.
+
ifdef STATIC
LDFLAGS_BASE = -static-libgcc -static
else
endif
# PKT: support for universal binaries
-# NB: static libraries are poorly supported in Mac OS X. More specifically
-# -static has different semantics than on ELF based systems
-# Also, building mac os x universal binaries is a tad tricky
-# 1. you cannot use ar on a library after calling ranlib
-# 2. -MM dependency tracking does not work
+# NB: static libraries are poorly supported in Mac OS X. More
+# specifically -static has different semantics than on ELF based
+# systems Also, building mac os x universal binaries is a tad tricky
+# 1. you cannot use ar on a library after calling ranlib 2. -MM
+# dependency tracking does not work
# the architectures to compile for
UNIVERSAL_ARCH = -arch i386 -arch ppc -arch ppc64
return n;
}
- ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyFormula_TopLevel(const ASTNode& a, bool pushNeg);
+ ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyFormula_TopLevel(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
ASTNode SimplifyTerm_TopLevel(const ASTNode& b);
- ASTNode SimplifyFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyTerm(const ASTNode& inputterm, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyTerm(const ASTNode& inputterm,
+ ASTNodeMap* VarConstMap=NULL);
void CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output);
void BuildReferenceCountMap(const ASTNode& b);
ASTNodeMap* ParamToCurrentValMap,
bool CheckUsingModel_Or_Expand);
ASTNode Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop);
-
+ ASTNode Check_FiniteLoop_UsingModel(const ASTNode& finiteloop);
+
//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
void ASTNodeStats(const char * c, const ASTNode& a);
//Check the map passed to SimplifyTerm
- bool CheckMap(ASTNodeMap* VarConstMap, const ASTNode& key, ASTNode& output);
+ bool CheckMap(ASTNodeMap* VarConstMap,
+ const ASTNode& key, ASTNode& output);
//substitution
* it compares with other approaches (e.g., one false axiom at a
* time or all the false axioms each time).
*****************************************************************/
- SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
- const ASTNode& inputAlreadyInSAT,
- const ASTNode& original_input) {
+ SOLVER_RETURN_TYPE
+ BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
+ const ASTNode& inputAlreadyInSAT,
+ const ASTNode& original_input) {
//printf("doing array read refinement\n");
if (!arrayread_refinement_flag)
FatalError("SATBased_ArrayReadRefinement: Control should not reach here");
//get the arrayname
ASTNode ArrName = iset->first;
// if(SYMBOL != ArrName.GetKind())
- // FatalError("SATBased_ArrayReadRefinement: arrname is not a SYMBOL",ArrName);
- ASTNode arr_read1 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
+ // FatalError("SATBased_ArrayReadRefinement: "\
+ // "arrname is not a SYMBOL",ArrName);
+ ASTNode arr_read1 =
+ CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
//get the variable corresponding to the array_read1
ASTNode arrsym1 = _arrayread_symbol[arr_read1];
if (!(SYMBOL == arrsym1.GetKind() || BVCONST == arrsym1.GetKind()))
//first construct the antecedent for the LA axiom
ASTNode eqOfIndices =
(exprless(the_index, compare_index)) ?
- CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ(compare_index, the_index);
+ CreateSimplifiedEQ(the_index, compare_index) :
+ CreateSimplifiedEQ(compare_index, the_index);
- ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
+ ASTNode arr_read2 =
+ CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
//get the variable corresponding to the array_read2
ASTNode arrsym2 = _arrayread_symbol[arr_read2];
if (!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind()))
//if (FalseAxiomsVec.size() > 0)
if (FalseAxiomsVec.size() > oldFalseAxiomsSize)
{
- res2 = CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input);
+ res2 =
+ CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input);
oldFalseAxiomsSize = FalseAxiomsVec.size();
}
//printf("spot 02, res2 = %d\n", res2);
*
* FIXME: Write Detailed Comment
*****************************************************************/
- SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver,
- const ASTNode& original_input)
+ SOLVER_RETURN_TYPE
+ BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver,
+ const ASTNode& original_input)
{
ASTNode writeAxiom;
ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin();
{
if (READ != term.GetKind() && WRITE != term[0].GetKind())
{
- FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE", term);
+ FatalError("Create_ArrayWriteAxioms: "\
+ "Input must be a READ over a WRITE", term);
}
ASTNode lhs = newvar;
* if the 'done' flag is true, then we terminate this refinement
* loop.
*****************************************************************/
- SOLVER_RETURN_TYPE BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver,
- const ASTNode& original_input)
+ SOLVER_RETURN_TYPE
+ BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver,
+ const ASTNode& original_input)
{
- for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),iend=GlobalList_Of_FiniteLoops.end();
- i!=iend;i++)
+ SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED;
+ std::vector<SOLVER_RETURN_TYPE> retvec;
+ for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
+ iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
{
- ASTNodeMap ParamToCurrentValMap;
- SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver,
- original_input,
- *i,&ParamToCurrentValMap);
- if(SOLVER_UNDECIDED != ret)
+ //ASTNodeMap * ParamToCurrentValMap = new ASTNodeMap;
+ ASTNodeMap ParamToCurrentValMap;
+ ret = SATBased_FiniteLoop_Refinement(SatSolver,
+ original_input,
+ *i,
+ &ParamToCurrentValMap);
+ if(SOLVER_VALID == ret)
{
return ret;
}
+ retvec.push_back(ret);
+ } //End of For()
+
+ //Even if one of the for loops results in SOLVER_UNDECIDED, then
+ //it means that the constructed model is bogus. Return this fact.
+ for(vector<SOLVER_RETURN_TYPE>::iterator i=retvec.begin(),
+ iend=retvec.end();i!=iend;i++)
+ {
+ if(SOLVER_UNDECIDED == *i)
+ {
+ return SOLVER_UNDECIDED;
+ }
}
- return SOLVER_UNDECIDED;
+
+ //All for loops are true in the model
+ return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input);
} //end of SATBased_AllFiniteLoops_Refinement()
//
//Expand the finite loop, check against model, and add false
//formulas to the SAT solver
- SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver,
- const ASTNode& original_input,
- const ASTNode& finiteloop,
- ASTNodeMap* ParamToCurrentValMap)
+ SOLVER_RETURN_TYPE
+ BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver,
+ const ASTNode& original_input,
+ const ASTNode& finiteloop,
+ ASTNodeMap* ParamToCurrentValMap)
{
//BVTypeCheck should have already checked the sanity of the input
//FOR-formula
{
while(paramCurrentValue < paramLimit)
{
- SATBased_FiniteLoop_Refinement(SatSolver, original_input,
- formulabody, ParamToCurrentValMap);
+ SATBased_FiniteLoop_Refinement(SatSolver,
+ original_input,
+ formulabody,
+ ParamToCurrentValMap);
paramCurrentValue = paramCurrentValue + paramIncrement;
//Update ParamToCurrentValMap with parameter and its current
//
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(32,paramCurrentValue);
} //end of While
} //end of recursion FORs
- ASTVec forloopFormulaVector;
+ //ASTVec forloopFormulaVector;
//Expand the leaf level FOR-construct completely
+ int AllLoopsAreTrue = 0;
for(;
paramCurrentValue < paramLimit;
paramCurrentValue = paramCurrentValue + paramIncrement)
{
ASTNode currentFormula;
- currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap);
+ currentFormula =
+ SimplifyFormula(formulabody, false, ParamToCurrentValMap);
//Check the currentformula against the model, and add it to the
//SAT solver if it is false against the model
if(ASTFalse == ComputeFormulaUsingModel(currentFormula))
{
- forloopFormulaVector.push_back(currentFormula);
- ASTNode forloopFormulas =
- (forloopFormulaVector.size() != 1) ?
- CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0];
+ // forloopFormulaVector.push_back(currentFormula); ASTNode
+ // forloopFormulas =
+ // (forloopFormulaVector.size() != 1) ?
+ // CreateNode(AND, forloopFormulaVector) :
+ // forloopFormulaVector[0];
SOLVER_RETURN_TYPE result =
- CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input);
+ CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
if(result != SOLVER_UNDECIDED)
{
return result;
}
}
+ else
+ {
+ //ComputeFormulaUsingModel can either return ASTFalse or
+ //ASTTrue
+ AllLoopsAreTrue++;
+ }
//Update ParamToCurrentValMap with parameter and its current
//value
//
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(32,paramCurrentValue);
} //end of expanding the FOR loop
+ if(AllLoopsAreTrue == paramLimit)
+ {
+ return SOLVER_INVALID;
+ }
+
return SOLVER_UNDECIDED;
} //end of the SATBased_FiniteLoop_Refinement()
//SATBased_FiniteLoop_Refinement_UsingModel
//
- //Expand the finite loop, check against model, and add false
- //formulas to the SAT solver
- ASTNode BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
- ASTNodeMap* ParamToCurrentValMap,
- bool CheckUsingModel_Or_Expand = true)
+ //Expand the finite loop, check against model
+ ASTNode
+ BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
+ ASTNodeMap* ParamToCurrentValMap,
+ bool checkusingmodel_flag = true)
{
/*
* 'finiteloop' is the finite loop to be expanded
while(paramCurrentValue < paramLimit)
{
Check_FiniteLoop_UsingModel(formulabody,
- ParamToCurrentValMap, CheckUsingModel_Or_Expand);
+ ParamToCurrentValMap,
+ checkusingmodel_flag);
paramCurrentValue = paramCurrentValue + paramIncrement;
//Update ParamToCurrentValMap with parameter and its current
//
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(32,paramCurrentValue);
} //end of While
}
paramCurrentValue = paramCurrentValue + paramIncrement)
{
ASTNode currentFormula;
- currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap);
+ currentFormula =
+ SimplifyFormula(formulabody, false, ParamToCurrentValMap);
- if(CheckUsingModel_Or_Expand)
+ if(checkusingmodel_flag)
{
//Check the currentformula against the model, and add it to the
//SAT solver if it is false against the model
//value
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(32,paramCurrentValue);
}
- if(CheckUsingModel_Or_Expand)
+ if(checkusingmodel_flag)
{
- ASTNode retFormula =
- (forloopFormulaVector.size() != 1) ? CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0];
- return retFormula;
+ return ASTTrue;
}
else
{
- return ASTTrue;
+ ASTNode retFormula =
+ (forloopFormulaVector.size() != 1) ?
+ CreateNode(AND, forloopFormulaVector) :
+ forloopFormulaVector[0];
+ return retFormula;
}
} //end of the Check_FiniteLoop_UsingModel()
//Expand_FiniteLoop_For_ModelCheck
- ASTNode BeevMgr::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop)
+ ASTNode
+ BeevMgr::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop)
{
ASTNodeMap ParamToCurrentValMap;
- return Check_FiniteLoop_UsingModel(finiteloop, &ParamToCurrentValMap, false);
+ return Check_FiniteLoop_UsingModel(finiteloop,
+ &ParamToCurrentValMap, false);
} //end of Expand_FiniteLoop_TopLevel()
+ ASTNode
+ BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop)
+ {
+ ASTNodeMap ParamToCurrentValMap;
+ return Check_FiniteLoop_UsingModel(finiteloop,
+ &ParamToCurrentValMap, true);
+ } //end of Check_FiniteLoop_UsingModel
+
};// end of namespace BEEV
}
- bool BeevMgr::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg)
+ bool BeevMgr::CheckSimplifyMap(const ASTNode& key,
+ ASTNode& output, bool pushNeg)
{
ASTNodeMap::iterator it, itend;
it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
}
// Push any reference count used by the key to the value.
- void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg)
+ void BeevMgr::UpdateSimplifyMap(const ASTNode& key,
+ const ASTNode& value, bool pushNeg)
{
// Don't add leaves. Leaves are easy to recalculate, no need to cache.
if (0 == key.Degree())
return;
-
// If there are references to the key, add them to the references of the value.
ASTNodeCountMap::const_iterator itKey, itValue;
itKey = ReferenceCount->find(key);
//e0 is of the form var, and e1 is const
if (1 == i && !CheckSubstitutionMap(e0))
{
- assert((e1.GetKind() == TRUE) || (e1.GetKind() == FALSE) || (e1.GetKind() == BVCONST));
+ assert((e1.GetKind() == TRUE) ||
+ (e1.GetKind() == FALSE) ||
+ (e1.GetKind() == BVCONST));
SolverMap[e0] = e1;
return true;
}
//e1 is of the form var, and e0 is const
if (-1 == i && !CheckSubstitutionMap(e1))
{
- assert((e0.GetKind() == TRUE) || (e0.GetKind() == FALSE) || (e0.GetKind() == BVCONST));
+ assert((e0.GetKind() == TRUE) ||
+ (e0.GetKind() == FALSE) ||
+ (e0.GetKind() == BVCONST));
SolverMap[e1] = e0;
return true;
}
//a is of the form READ(Arr,const), and b is const, or
//a is of the form var, and b is const
- if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST && (k2 == BVCONST)))
- // ||
- // k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
+ if ((k1 == READ &&
+ a[0].GetKind() == SYMBOL &&
+ a[1].GetKind() == BVCONST &&
+ (k2 == BVCONST)))
+ // || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind()
+ // == BVCONST)))
return 1;
if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
//b is of the form READ(Arr,const), and a is const, or
//b is of the form var, and a is const
- if ((k1 == BVCONST) && ((k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
+ if ((k1 == BVCONST) &&
+ ((k2 == READ &&
+ b[0].GetKind() == SYMBOL &&
+ b[1].GetKind() == BVCONST)))
return -1;
if (SYMBOL == k2 && (BVCONST == k1 || TRUE == k1 || FALSE == k1))
}
}
- ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode
+ BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
Begin_RemoveWrites = false;
ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
}
}
- ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg)
+ ASTNode
+ BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
ResetSimplifyMaps();
return out;
}
- ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode
+ BeevMgr::SimplifyFormula(const ASTNode& b,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
if (!optimize_flag)
return b;
Kind kind = b.GetKind();
if (BOOLEAN_TYPE != b.GetType())
{
- FatalError(" SimplifyFormula: You have input a nonformula kind: ", ASTUndefined, kind);
+ FatalError(" SimplifyFormula: "\
+ "You have input a nonformula kind: ", ASTUndefined, kind);
}
ASTNode a = b;
{
case AND:
case OR:
- output = SimplifyAndOrFormula(a, pushNeg);
+ output = SimplifyAndOrFormula(a, pushNeg, VarConstMap);
break;
case NOT:
- output = SimplifyNotFormula(a, pushNeg);
+ output = SimplifyNotFormula(a, pushNeg, VarConstMap);
break;
case XOR:
- output = SimplifyXorFormula(a, pushNeg);
+ output = SimplifyXorFormula(a, pushNeg, VarConstMap);
break;
case NAND:
- output = SimplifyNandFormula(a, pushNeg);
+ output = SimplifyNandFormula(a, pushNeg, VarConstMap);
break;
case NOR:
- output = SimplifyNorFormula(a, pushNeg);
+ output = SimplifyNorFormula(a, pushNeg, VarConstMap);
break;
case IFF:
- output = SimplifyIffFormula(a, pushNeg);
+ output = SimplifyIffFormula(a, pushNeg, VarConstMap);
break;
case IMPLIES:
- output = SimplifyImpliesFormula(a, pushNeg);
+ output = SimplifyImpliesFormula(a, pushNeg, VarConstMap);
break;
case ITE:
- output = SimplifyIteFormula(a, pushNeg);
+ output = SimplifyIteFormula(a, pushNeg, VarConstMap);
break;
case FOR:
- output = SimplifyForFormula(a, pushNeg);
+ output = SimplifyForFormula(a, pushNeg, VarConstMap);
break;
default:
//kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable
- output = SimplifyAtomicFormula(a, pushNeg);
+ output = SimplifyAtomicFormula(a, pushNeg, VarConstMap);
//output = pushNeg ? CreateNode(NOT,a) : a;
break;
}
return output;
}
- ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) {
+ ASTNode
+ BeevMgr::SimplifyForFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap)
+ {
//FIXME: Code this up properly later. Mainly pushing the negation down
return a;
}
- ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode
+ BeevMgr::SimplifyAtomicFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
if (!optimize_flag)
return a;
if (a.Degree() == 2)
{
//cerr << "Input to simplifyterm: left: " << a[0] << endl;
- left = SimplifyTerm(a[0]);
+ left = SimplifyTerm(a[0], VarConstMap);
//cerr << "Output of simplifyterm:left: " << left << endl;
//cerr << "Input to simplifyterm: right: " << a[1] << endl;
- right = SimplifyTerm(a[1]);
+ right = SimplifyTerm(a[1], VarConstMap);
//cerr << "Output of simplifyterm:left: " << right << endl;
}
ASTNode thebit = a[1];
ASTNode zero = CreateZeroConst(1);
ASTNode one = CreateOneConst(1);
- ASTNode getthebit = SimplifyTerm(CreateTerm(BVEXTRACT, 1, term, thebit, thebit));
+ ASTNode getthebit =
+ SimplifyTerm(CreateTerm(BVEXTRACT, 1, term, thebit, thebit));
if (getthebit == zero)
output = pushNeg ? ASTTrue : ASTFalse;
else if (getthebit == one)
break;
}
default:
- FatalError("SimplifyAtomicFormula: NO atomic formula of the kind: ", ASTUndefined, kind);
+ FatalError("SimplifyAtomicFormula: "\
+ "NO atomic formula of the kind: ", ASTUndefined, kind);
break;
}
return output;
} //end of SimplifyAtomicFormula()
- ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, const ASTNode& left, const ASTNode& right, bool pushNeg)
+ ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k,
+ const ASTNode& left,
+ const ASTNode& right, bool pushNeg)
{
ASTNode output;
if (BVCONST == left.GetKind() && BVCONST == right.GetKind())
}
else
{
- output = pushNeg ? CreateNode(BVLE, right, left) : CreateNode(BVLT, left, right);
+ output =
+ pushNeg ?
+ CreateNode(BVLE, right, left) :
+ CreateNode(BVLT, left, right);
}
break;
case BVLE:
}
else
{
- output = pushNeg ? CreateNode(BVLT, right, left) : CreateNode(BVLE, left, right);
+ output =
+ pushNeg ?
+ CreateNode(BVLT, right, left) :
+ CreateNode(BVLE, left, right);
}
break;
case BVGT:
}
else
{
- output = pushNeg ? CreateNode(BVLE, left, right) : CreateNode(BVLT, right, left);
+ output =
+ pushNeg ?
+ CreateNode(BVLE, left, right) :
+ CreateNode(BVLT, right, left);
}
break;
case BVGE:
}
else
{
- output = pushNeg ? CreateNode(BVLT, left, right) : CreateNode(BVLE, right, left);
+ output =
+ pushNeg ?
+ CreateNode(BVLT, left, right) :
+ CreateNode(BVLE, right, left);
}
break;
case BVSLT:
{
if (BVLT != in[j].GetKind())
continue;
- if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) // parameters are swapped.
+ // parameters are swapped.
+ if (in[i][0] == in[j][1] && in[i][1] == in[j][0])
return ASTFalse;
}
}
return in;
}
- // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e))
- // Expensive. But makes some other simplifications possible.
+ // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d)
+ // (bvslt c e)) Expensive. But makes some other simplifications
+ // possible.
ASTNode BeevMgr::PullUpITE(const ASTNode& in)
{
if (2 != in.GetChildren().size())
//be semantically equal.
output = ASTFalse;
}
- else if (ITE == k1 && BVCONST == in1[1].GetKind() && BVCONST == in1[2].GetKind() && BVCONST == k2)
+ else if (ITE == k1 &&
+ BVCONST == in1[1].GetKind() &&
+ BVCONST == in1[2].GetKind() && BVCONST == k2)
{
//if one side is a BVCONST and the other side is an ITE over
//BVCONST then we can do the following optimization:
output = CreateNode(EQ, in1, in2);
}
}
- else if (ITE == k2 && BVCONST == in2[1].GetKind() && BVCONST == in2[2].GetKind() && BVCONST == k1)
+ else if (ITE == k2 &&
+ BVCONST == in2[1].GetKind() &&
+ BVCONST == in2[2].GetKind() && BVCONST == k1)
{
ASTNode cond = in2[0];
if (in2[1] == in1)
}
//accepts cond == t1, then part is t2, and else part is t3
- ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2)
+ ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0,
+ const ASTNode& in1,
+ const ASTNode& in2)
{
ASTNode t0 = in0;
ASTNode t1 = in1;
if (t1.GetValueWidth() != t2.GetValueWidth())
{
cerr << "t2 is : = " << t2;
- FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match", t1);
+ FatalError("CreateSimplifiedTermITE: "\
+ "the lengths of the two branches don't match", t1);
}
if (t1.GetIndexWidth() != t2.GetIndexWidth())
{
cerr << "t2 is : = " << t2;
- FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match", t1);
+ FatalError("CreateSimplifiedTermITE: "\
+ "the lengths of the two branches don't match", t1);
}
return CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2);
}
} //end of SimplifyAndOrFormula
- ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode
+ BeevMgr::SimplifyNotFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg))
}
//This function simplifies terms based on their kind
- ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap)
+ ASTNode
+ BeevMgr::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap)
{
ASTNode inputterm(actualInputterm); // mutable local copy.
CONSTANTBV::BitVector_Bit_On(maskedPlusOne, i);
}
CONSTANTBV::BitVector_increment(maskedPlusOne);
- ASTNode temp = CreateTerm(BVMULT, inputValueWidth, CreateBVConst(maskedPlusOne, inputValueWidth), other);
+ ASTNode temp =
+ CreateTerm(BVMULT, inputValueWidth,
+ CreateBVConst(maskedPlusOne, inputValueWidth), other);
output = CreateTerm(BVNEG, inputValueWidth, temp);
}
}
{
//arr is a SYMBOL for sure
ASTNode arr = inputterm[0];
- ASTNode index = SimplifyTerm(inputterm[1]);
+ ASTNode index = SimplifyTerm(inputterm[1], VarConstMap);
out1 = CreateTerm(READ, inputValueWidth, arr, index);
}
}
//Call the SAT solver, and check the result before returning. This
//can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED
SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
- const ASTNode& modified_input,
+ const ASTNode& modified_input,
const ASTNode& original_input)
{
ASTNode BBFormula = BBForm(modified_input);
ASTNode writeIndex = TermToConstTermUsingModel(write[1], false);
ASTNode writeVal = TermToConstTermUsingModel(write[2], false);
- ASTNode cond = ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex, readIndex));
+ ASTNode cond =
+ ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex, readIndex));
if (ASTTrue == cond)
{
//found the write-value. return it
else if (ASTFalse == t0)
output = ComputeFormulaUsingModel(form[2]);
else
- FatalError("ComputeFormulaUsingModel: ITE: something is wrong with the formula: ", form);
+ FatalError("ComputeFormulaUsingModel: ITE: "\
+ "something is wrong with the formula: ", form);
break;
+ case FOR:
+ output = Check_FiniteLoop_UsingModel(form);
+ break;
default:
- FatalError(" ComputeFormulaUsingModel: the kind has not been implemented", ASTUndefined);
+ FatalError(" ComputeFormulaUsingModel: "\
+ "the kind has not been implemented", ASTUndefined);
break;
}
do
{
inputToSAT = simplified_solved_InputToSAT;
+
simplified_solved_InputToSAT =
CreateSubstitutionMap(simplified_solved_InputToSAT);
//printf("##################################################\n");
ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+
simplified_solved_InputToSAT =
SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+
simplified_solved_InputToSAT =
bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
- } while (inputToSAT != simplified_solved_InputToSAT);
+
+ }
+ while (inputToSAT != simplified_solved_InputToSAT);
ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT);
SimplifyWrites_InPlace_Flag = true;
simplified_solved_InputToSAT =
CreateSubstitutionMap(simplified_solved_InputToSAT);
ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
- simplified_solved_InputToSAT =
+
+ simplified_solved_InputToSAT =
SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
- simplified_solved_InputToSAT =
+
+ simplified_solved_InputToSAT =
bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
- } while (inputToSAT != simplified_solved_InputToSAT);
+
+ }
+ while (inputToSAT != simplified_solved_InputToSAT);
ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT);
delete bvsolver;
do
{
inputToSAT = simplified_solved_InputToSAT;
- //simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT);
- //Begin_RemoveWrites = true;
- //ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+ //simplified_solved_InputToSAT =
+ //CreateSubstitutionMap(simplified_solved_InputToSAT);
+ //Begin_RemoveWrites = true; ASTNodeStats("after pure
+ //substitution: ", simplified_solved_InputToSAT);
simplified_solved_InputToSAT =
SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
- //ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
- //simplified_solved_InputToSAT = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
- //ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+ //ASTNodeStats("after simplification: ",
+ //simplified_solved_InputToSAT); simplified_solved_InputToSAT
+ //= bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+ //ASTNodeStats("after solving: ",
+ //simplified_solved_InputToSAT);
} while (inputToSAT != simplified_solved_InputToSAT);
if (start_abstracting)
SimplifyWrites_InPlace_Flag = false;
Begin_RemoveWrites = false;
- simplified_solved_InputToSAT = TransformFormula_TopLevel(simplified_solved_InputToSAT);
+ simplified_solved_InputToSAT =
+ TransformFormula_TopLevel(simplified_solved_InputToSAT);
ASTNodeStats("after transformation: ", simplified_solved_InputToSAT);
TermsAlreadySeenMap.clear();
return res;
}
+ res = SATBased_AllFiniteLoops_Refinement(newS, orig_input);
+ if (SOLVER_UNDECIDED != res)
+ {
+ CountersAndStats("print_func_stats");
+ return res;
+ }
+
res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
if (SOLVER_UNDECIDED != res)
{
projects / francis / stp.git / commitdiff