#emacs
#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
-#OPTIMIZE = -g # Debugging
+OPTIMIZE = -g # Debugging
OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
CFLAGS_BASE = $(OPTIMIZE)
bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
//functions for checking and updating simplifcation map
- bool CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg);
- void UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg);
+ bool CheckSimplifyMap(const ASTNode& key,
+ ASTNode& output,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ void UpdateSimplifyMap(const ASTNode& key,
+ const ASTNode& value,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
void ResetSimplifyMaps();
bool CheckAlwaysTrueFormMap(const ASTNode& key);
void UpdateAlwaysTrueFormMap(const ASTNode& val);
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
+#-include depend
os << endl << "ENDIF";
break;
case FOR:
- os << "FOR(";
- PL_Print1(os, c[0], indentation, letize);
- os << ";";
- PL_Print1(os, c[1], indentation, letize);
- os << ";";
- PL_Print1(os, c[2], indentation, letize);
- os << ";";
- PL_Print1(os, c[3], indentation, letize);
- os << "){ \n";
- PL_Print1(os, c[4], indentation, letize);
- os << "} \n";
+ if(expand_finitefor_flag)
+ {
+ ASTNode expandedfor = bm.Expand_FiniteLoop_TopLevel(n);
+ PL_Print1(os, expandedfor, indentation, letize);
+ }
+ else
+ {
+ os << "FOR(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ";";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ";";
+ PL_Print1(os, c[2], indentation, letize);
+ os << ";";
+ PL_Print1(os, c[3], indentation, letize);
+ os << "){ \n";
+ PL_Print1(os, c[4], indentation, letize);
+ os << "} \n";
+ }
break;
case BVLT:
case BVLE:
int paramCurrentValue = paramInit;
//Update ParamToCurrentValMap with parameter and its current
- //value. Here paramCurrentValue is the initial value
- unsigned width = 32;
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ //value. Here paramCurrentValue is the initial value
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+ SOLVER_RETURN_TYPE ret;
//Go recursively thru' all the FOR-constructs.
if(FOR == formulabody.GetKind())
{
while(paramCurrentValue < paramLimit)
{
- SATBased_FiniteLoop_Refinement(SatSolver,
- original_input,
- formulabody,
- ParamToCurrentValMap);
- paramCurrentValue = paramCurrentValue + paramIncrement;
+ ret = SATBased_FiniteLoop_Refinement(SatSolver,
+ original_input,
+ formulabody,
+ ParamToCurrentValMap);
+ if(SOLVER_VALID == ret)
+ {
+ //If formula is valid, return immediately
+ return ret;
+ }
+
//Update ParamToCurrentValMap with parameter and its current
//value
//
//FIXME: Possible leak since I am not freeing the previous
- //'value' for the same 'key'
+ //'value' for the same 'key'
+ paramCurrentValue = paramCurrentValue + paramIncrement;
(*ParamToCurrentValMap)[parameter] =
- CreateBVConst(32,paramCurrentValue);
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
} //end of While
+
+ //The last 'ret' value is the truthvalue of the formula. If it
+ //is SOLVER_INVALID then the formula is indeed INVALID, else
+ //ret can only be SOLVER_UNDECIDED at this point. Hence return
+ //UNDECIDED.
+ return ret;
} //end of recursion FORs
//ASTVec forloopFormulaVector;
//Expand the leaf level FOR-construct completely
- int AllLoopsAreTrue = 0;
- for(;
- paramCurrentValue < paramLimit;
- paramCurrentValue = paramCurrentValue + paramIncrement)
+ int ThisForLoopAllTrue = 0;
+ for(;paramCurrentValue < paramLimit;
+ //increment of paramCurrentValue done inside loop
+ )
{
ASTNode currentFormula;
currentFormula =
// CreateNode(AND, forloopFormulaVector) :
// forloopFormulaVector[0];
- SOLVER_RETURN_TYPE result =
+ currentFormula = TransformFormula_TopLevel(currentFormula);
+ SOLVER_RETURN_TYPE result =
CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
if(result != SOLVER_UNDECIDED)
{
{
//ComputeFormulaUsingModel can either return ASTFalse or
//ASTTrue
- AllLoopsAreTrue++;
+ ThisForLoopAllTrue++;
}
//Update ParamToCurrentValMap with parameter and its current
//
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
+ paramCurrentValue = paramCurrentValue + paramIncrement;
(*ParamToCurrentValMap)[parameter] =
- CreateBVConst(32,paramCurrentValue);
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+ //cout << (*ParamToCurrentValMap)[parameter];
} //end of expanding the FOR loop
- if(AllLoopsAreTrue == paramLimit)
+ if(ThisForLoopAllTrue == paramLimit)
{
return SOLVER_INVALID;
}
//Update ParamToCurrentValMap with parameter and its current
//value. Here paramCurrentValue is the initial value
- unsigned width = 32;
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+ ASTNode ret = ASTTrue;
+ ASTVec returnVec;
//Go recursively thru' all the FOR-constructs.
if(FOR == formulabody.GetKind())
{
while(paramCurrentValue < paramLimit)
{
- Check_FiniteLoop_UsingModel(formulabody,
- ParamToCurrentValMap,
- checkusingmodel_flag);
- paramCurrentValue = paramCurrentValue + paramIncrement;
+ ret = Check_FiniteLoop_UsingModel(formulabody,
+ ParamToCurrentValMap,
+ checkusingmodel_flag);
+ if(ASTFalse == ret)
+ {
+ //no more expansion needed. Return immediately
+ return ret;
+ }
+ else
+ {
+ returnVec.push_back(ret);
+ }
//Update ParamToCurrentValMap with parameter and its current
//value
//
//FIXME: Possible leak since I am not freeing the previous
- //'value' for the same 'key'
+ //'value' for the same 'key'
+ paramCurrentValue = paramCurrentValue + paramIncrement;
(*ParamToCurrentValMap)[parameter] =
- CreateBVConst(32,paramCurrentValue);
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
} //end of While
+
+ ASTNode retFormula =
+ (returnVec.size() != 1) ?
+ CreateNode(AND, returnVec) : returnVec[0];
+ return retFormula;
}
ASTVec forloopFormulaVector;
//Expand the leaf level FOR-construct completely
- for(;
- paramCurrentValue < paramLimit;
- paramCurrentValue = paramCurrentValue + paramIncrement)
+ for(;paramCurrentValue < paramLimit;
+ //incrementing of paramCurrentValue is done inside loop
+ )
{
ASTNode currentFormula;
currentFormula =
//value
//FIXME: Possible leak since I am not freeing the previous
//'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] =
- CreateBVConst(32,paramCurrentValue);
- }
-
+ paramCurrentValue = paramCurrentValue + paramIncrement;
+ (*ParamToCurrentValMap)[parameter] =
+ CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue);
+ //cout << (*ParamToCurrentValMap)[parameter];
+ } //end of For
if(checkusingmodel_flag)
{
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
-
\ No newline at end of file
+#-include depend
\ No newline at end of file
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
-
\ No newline at end of file
+#-include depend
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
+#-include depend
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
+#-include depend
\ No newline at end of file
//
//collect statistics on certain functions
bool stats_flag = false;
+
//print DAG nodes
bool print_nodes_flag = false;
+
//run STP in optimized mode
bool optimize_flag = true;
+
//do sat refinement, i.e. underconstraint the problem, and feed to
//SAT. if this works, great. else, add a set of suitable constraints
//to re-constraint the problem correctly, and call SAT again, until
//all constraints have been added.
bool arrayread_refinement_flag = true;
+
//flag to control write refinement
bool arraywrite_refinement_flag = true;
+
//check the counterexample against the original input to STP
bool check_counterexample_flag = false;
+
//construct the counterexample in terms of original variable based
//on the counterexample returned by SAT solver
bool construct_counterexample_flag = true;
bool print_counterexample_flag = false;
bool print_binary_flag = false;
+
+ //Expands out the finite for-construct completely
+ bool expand_finitefor_flag;
+
//if this option is true then print the way dawson wants using a
//different printer. do not use this printer.
bool print_arrayval_declaredorder_flag = false;
+
//flag to decide whether to print "valid/invalid" or not
bool print_output_flag = false;
+
//print the variable order chosen by the sat solver while it is
//solving.
bool print_sat_varorder_flag = false;
+
//turn on word level bitvector solver
bool wordlevel_solve_flag = true;
+
//turn off XOR flattening
bool xor_flatten_flag = false;
+
//Flag to switch on the smtlib parser
bool smtlib_parser_flag = false;
+
//print the input back
bool print_STPinput_back_flag = false;
//
//collect statistics on certain functions
extern bool stats_flag;
+
//print DAG nodes
extern bool print_nodes_flag;
+
//run STP in optimized mode
extern bool optimize_flag;
+
//do sat refinement, i.e. underconstraint the problem, and feed to
//SAT. if this works, great. else, add a set of suitable constraints
//to re-constraint the problem correctly, and call SAT again, until
//all constraints have been added.
extern bool arrayread_refinement_flag;
+
//switch to control write refinements
extern bool arraywrite_refinement_flag;
+
//check the counterexample against the original input to STP
extern bool check_counterexample_flag;
+
//construct the counterexample in terms of original variable based
//on the counterexample returned by SAT solver
extern bool construct_counterexample_flag;
extern bool print_counterexample_flag;
extern bool print_binary_flag;
+
+ //Expands out the finite for-construct completely
+ extern bool expand_finitefor_flag;
+
//if this option is true then print the way dawson wants using a
//different printer. do not use this printer.
extern bool print_arrayval_declaredorder_flag;
+
//flag to decide whether to print "valid/invalid" or not
extern bool print_output_flag;
+
//print the variable order chosen by the sat solver while it is
//solving.
extern bool print_sat_varorder_flag;
+
//turn on word level bitvector solver
extern bool wordlevel_solve_flag;
+
//XOR flattening optimizations.
extern bool xor_flatten_flag;
+
//this flag indicates that the BVSolver() succeeded
extern bool toplevel_solved_flag;
+
//print the input back
extern bool print_STPinput_back_flag;
+
//Flag to switch on the smtlib parser
extern bool smtlib_parser_flag;
--include depend
+#-include depend
\ No newline at end of file
// Amount of memory to ask for at beginning of main.
static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
-/******************************************************************************
+/********************************************************************
* MAIN FUNCTION:
*
* step 0. Parse the input into an ASTVec.
* step 3. Convert to CNF
* step 4. Convert to SAT
* step 5. Call SAT to determine if input is SAT or UNSAT
- ******************************************************************************/
+ ********************************************************************/
int main(int argc, char ** argv) {
char * infile;
extern FILE *cvcin;
}
//populate the help string
- helpstring += "version: " + version + "\n\n";
- helpstring += "-r : switch refinement off (optimizations are ON by default)\n";
- helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n";
+ helpstring += "STP version: " + version + "\n\n";
helpstring += "-a : switch optimizations off (optimizations are ON by default)\n";
- helpstring += "-s : print function statistics\n";
- helpstring += "-v : print nodes \n";
+ helpstring += "-b : print STP input back to cout\n";
helpstring += "-c : construct counterexample\n";
helpstring += "-d : check counterexample\n";
- helpstring += "-p : print counterexample\n";
- helpstring += "-y : print counterexample in binary\n";
- helpstring += "-b : print STP input back to cout\n";
- helpstring += "-x : flatten nested XORs\n";
+ helpstring += "-e : expand finite-for construct\n";
helpstring += "-h : help\n";
helpstring += "-m : use the SMTLIB parser\n";
-
-
+ helpstring += "-p : print counterexample\n";
+ helpstring += "-r : switch refinement off (optimizations are ON by default)\n";
+ helpstring += "-s : print function statistics\n";
+ helpstring += "-v : print nodes \n";
+ helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n";
+ helpstring += "-x : flatten nested XORs\n";
+ helpstring += "-y : print counterexample in binary\n";
for(int i=1; i < argc;i++)
{
construct_counterexample_flag = true;
check_counterexample_flag = true;
break;
+ case 'e':
+ expand_finitefor_flag = true;
+ break;
case 'h':
fprintf(stderr,usage,prog);
cout << helpstring;
@cp y.tab.h parseSMT_defs.h
clean:
- rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser y.tab.* lex.yy.c .#*
-
+ rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser y.tab.* lex.yy.c .#*
\ No newline at end of file
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
-
+#-include depend
\ No newline at end of file
bool BeevMgr::CheckSimplifyMap(const ASTNode& key,
- ASTNode& output, bool pushNeg)
+ ASTNode& output,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
+ if(NULL != VarConstMap)
+ {
+ return false;
+ }
ASTNodeMap::iterator it, itend;
it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end();
// Push any reference count used by the key to the value.
void BeevMgr::UpdateSimplifyMap(const ASTNode& key,
- const ASTNode& value, bool pushNeg)
+ const ASTNode& value,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
- // Don't add leaves. Leaves are easy to recalculate, no need to cache.
- if (0 == key.Degree())
- return;
+ if(NULL != VarConstMap)
+ {
+ return;
+ }
+
+ // 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);
if (smtlib_parser_flag)
BuildReferenceCountMap(b);
- ASTNode out = SimplifyFormula(b, pushNeg);
+ ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
ResetSimplifyMaps();
return out;
}
}
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
a = PullUpITE(a);
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
BeevMgr::SimplifyForFormula(const ASTNode& a,
bool pushNeg, ASTNodeMap* VarConstMap)
{
- //FIXME: Code this up properly later. Mainly pushing the negation down
+ //FIXME: Code this up properly later. Mainly pushing the negation
+ //down
return a;
}
return a;
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
{
return output;
}
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
} //end of SimplifyAtomicFormula()
output = CreateNode(EQ, in1, in2);
}
- UpdateSimplifyMap(in, output, false);
+ UpdateSimplifyMap(in, output, false, VarConstMap);
return output;
} //End of ITEOpts_InEqs()
ASTNode output;
//cerr << "input:\n" << a << endl;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
ASTVec c, outvec;
if (annihilator == aaa)
{
//memoize
- UpdateSimplifyMap(*i, annihilator, pushNeg);
- UpdateSimplifyMap(a, annihilator, pushNeg);
+ UpdateSimplifyMap(*i, annihilator, pushNeg, VarConstMap);
+ UpdateSimplifyMap(a, annihilator, pushNeg, VarConstMap);
//cerr << "annihilator1: output:\n" << annihilator << endl;
return annihilator;
}
else if (nextexists && ((bbb.GetKind() == NOT && bbb[0] == aaa)))
{
//memoize
- UpdateSimplifyMap(a, annihilator, pushNeg);
+ UpdateSimplifyMap(a, annihilator, pushNeg, VarConstMap);
//cerr << "annihilator2: output:\n" << annihilator << endl;
return annihilator;
}
}
default:
{
- output = (isAnd) ? (pushNeg ? CreateNode(OR, outvec) : CreateNode(AND, outvec)) : (pushNeg ? CreateNode(AND, outvec) : CreateNode(OR,
- outvec));
+ output =
+ (isAnd) ? (pushNeg ?
+ CreateNode(OR, outvec) :
+ CreateNode(AND, outvec)) :
+ (pushNeg ? CreateNode(AND, outvec) : CreateNode(OR,outvec));
//output = FlattenOneLevel(output);
break;
}
// output = RemoveContradictionsFromAND(output);
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
//cerr << "output:\n" << output << endl;
return output;
} //end of SimplifyAndOrFormula
bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (!(a.Degree() == 1 && NOT == a.GetKind()))
output = SimplifyFormula(o, pn, VarConstMap);
}
//memoize
- UpdateSimplifyMap(o, output, pn);
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(o, output, pn, VarConstMap);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (a.GetChildren().size() > 2)
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output, a0, a1;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
//the two NOTs cancel out
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output, a0, a1;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
//the two NOTs cancel out
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (!(a.Degree() == 2 && IMPLIES == a.GetKind()))
//applying modus ponens
output = c1;
}
- else if (CheckAlwaysTrueFormMap(c1) || CheckAlwaysTrueFormMap(CreateNode(NOT, c0)) || (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0])))
+ else if (CheckAlwaysTrueFormMap(c1) ||
+ CheckAlwaysTrueFormMap(CreateNode(NOT, c0)) ||
+ (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0])))
{
//(~c0 AND (~c0 OR c1)) <==> TRUE
//
//(c0 AND ~c0->c1) <==> TRUE
output = ASTTrue;
}
- else if (CheckAlwaysTrueFormMap(CreateNode(NOT, c1)) || (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0])))
+ else if (CheckAlwaysTrueFormMap(CreateNode(NOT, c1)) ||
+ (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0])))
{
//(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0
//(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
- if (CheckSimplifyMap(a, output, pushNeg))
+ if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
return output;
if (!(a.Degree() == 2 && IFF == a.GetKind()))
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
return b;
ASTNode output;
- if (CheckSimplifyMap(b, output, pushNeg))
+ if (CheckSimplifyMap(b, output, pushNeg, VarConstMap))
return output;
if (!(b.Degree() == 3 && ITE == b.GetKind()))
}
//memoize
- UpdateSimplifyMap(a, output, pushNeg);
+ UpdateSimplifyMap(a, output, pushNeg, VarConstMap);
return output;
}
return SimplifyTerm(output);
}
- if (CheckSimplifyMap(inputterm, output, false))
+ if (CheckSimplifyMap(inputterm, output, false, VarConstMap))
{
//cerr << "SimplifierMap:" << inputterm << " output: " << output << endl;
return output;
{
output = annihilator;
//memoize
- UpdateSimplifyMap(inputterm, output, false);
+ UpdateSimplifyMap(inputterm, output, false, VarConstMap);
//cerr << "output of SimplifyTerm: " << output << endl;
return output;
}
assert(NULL != output);
//memoize
- UpdateSimplifyMap(inputterm, output, false);
+ UpdateSimplifyMap(inputterm, output, false, VarConstMap);
//cerr << "SimplifyTerm: output" << output << endl;
// CheckSimplifyInvariant(inputterm,output);
depend: $(SRCS)
@$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
--include depend
-
\ No newline at end of file
+#-include depend
\ No newline at end of file
projects / francis / stp.git / commitdiff