From: vijay_ganesh Date: Wed, 9 Sep 2009 20:06:17 +0000 (+0000) Subject: For-construct seems to be working X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=921e87ee728b7eada7b0c941cbf4191a84b902d0;p=francis%2Fstp.git For-construct seems to be working git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@213 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index d30be78..efd7c20 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -5,7 +5,7 @@ #emacs #OPTIMIZE = -g -pg # Debugging and gprof-style profiling -#OPTIMIZE = -g # Debugging +OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization CFLAGS_BASE = $(OPTIMIZE) diff --git a/src/AST/AST.h b/src/AST/AST.h index dd864fc..09721e0 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1565,8 +1565,12 @@ namespace BEEV 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); diff --git a/src/AST/Makefile b/src/AST/Makefile index ba6331f..e9ecc95 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -23,4 +23,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend +#-include depend diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index 2044c16..c00271a 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -174,17 +174,25 @@ namespace printer 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: diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index 03f45ac..e830bf6 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -323,37 +323,50 @@ namespace BEEV 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 = @@ -369,7 +382,8 @@ namespace BEEV // 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) { @@ -380,7 +394,7 @@ namespace BEEV { //ComputeFormulaUsingModel can either return ASTFalse or //ASTTrue - AllLoopsAreTrue++; + ThisForLoopAllTrue++; } //Update ParamToCurrentValMap with parameter and its current @@ -388,11 +402,13 @@ namespace BEEV // //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; } @@ -435,34 +451,50 @@ namespace BEEV //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 = @@ -484,10 +516,11 @@ namespace BEEV //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) { diff --git a/src/abstraction-refinement/Makefile b/src/abstraction-refinement/Makefile index c1543c1..68f2884 100644 --- a/src/abstraction-refinement/Makefile +++ b/src/abstraction-refinement/Makefile @@ -13,5 +13,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend - \ No newline at end of file +#-include depend \ No newline at end of file diff --git a/src/bitvec/Makefile b/src/bitvec/Makefile index c83b8c5..a1849a5 100644 --- a/src/bitvec/Makefile +++ b/src/bitvec/Makefile @@ -14,5 +14,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend - \ No newline at end of file +#-include depend diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile index fef9b48..306d418 100644 --- a/src/c_interface/Makefile +++ b/src/c_interface/Makefile @@ -14,5 +14,5 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend +#-include depend diff --git a/src/constantbv/Makefile b/src/constantbv/Makefile index 7a4fcd6..e56c8f4 100644 --- a/src/constantbv/Makefile +++ b/src/constantbv/Makefile @@ -14,4 +14,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend +#-include depend \ No newline at end of file diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp index 24f2311..dd35947 100644 --- a/src/main/Globals.cpp +++ b/src/main/Globals.cpp @@ -16,38 +16,54 @@ namespace BEEV // //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; diff --git a/src/main/Globals.h b/src/main/Globals.h index abd66df..6d1b4ae 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -42,40 +42,57 @@ namespace BEEV // //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; diff --git a/src/main/Makefile b/src/main/Makefile index d8e7979..401acc4 100644 --- a/src/main/Makefile +++ b/src/main/Makefile @@ -38,4 +38,4 @@ depend: $(SRCS) --include depend +#-include depend \ No newline at end of file diff --git a/src/main/main.cpp b/src/main/main.cpp index 9efb839..808b717 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -19,7 +19,7 @@ extern int cvcparse(void*); // 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. @@ -28,7 +28,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; * 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; @@ -44,22 +44,21 @@ int main(int argc, char ** argv) { } //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++) { @@ -80,6 +79,9 @@ int main(int argc, char ** argv) { construct_counterexample_flag = true; check_counterexample_flag = true; break; + case 'e': + expand_finitefor_flag = true; + break; case 'h': fprintf(stderr,usage,prog); cout << helpstring; diff --git a/src/parser/Makefile b/src/parser/Makefile index 2769085..82f9920 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -31,5 +31,4 @@ parseSMT_defs.h parseSMT.cpp:smtlib.y @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 diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile index 318b0eb..9d03c88 100644 --- a/src/simplifier/Makefile +++ b/src/simplifier/Makefile @@ -15,5 +15,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend - +#-include depend \ No newline at end of file diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 701351f..d538f11 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -48,8 +48,13 @@ ASTNode Flatten(const ASTNode& a) 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(); @@ -77,11 +82,18 @@ ASTNode Flatten(const ASTNode& a) // 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); @@ -303,7 +315,7 @@ ASTNode Flatten(const ASTNode& a) if (smtlib_parser_flag) BuildReferenceCountMap(b); - ASTNode out = SimplifyFormula(b, pushNeg); + ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); ResetSimplifyMaps(); return out; } @@ -331,7 +343,7 @@ ASTNode Flatten(const ASTNode& a) } ASTNode output; - if (CheckSimplifyMap(a, output, pushNeg)) + if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; a = PullUpITE(a); @@ -375,7 +387,7 @@ ASTNode Flatten(const ASTNode& a) } //memoize - UpdateSimplifyMap(a, output, pushNeg); + UpdateSimplifyMap(a, output, pushNeg, VarConstMap); return output; } @@ -383,7 +395,8 @@ ASTNode Flatten(const ASTNode& a) 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; } @@ -395,7 +408,7 @@ ASTNode Flatten(const ASTNode& a) return a; ASTNode output; - if (CheckSimplifyMap(a, output, pushNeg)) + if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) { return output; } @@ -480,7 +493,7 @@ ASTNode Flatten(const ASTNode& a) } //memoize - UpdateSimplifyMap(a, output, pushNeg); + UpdateSimplifyMap(a, output, pushNeg, VarConstMap); return output; } //end of SimplifyAtomicFormula() @@ -757,7 +770,7 @@ ASTNode Flatten(const ASTNode& a) output = CreateNode(EQ, in1, in2); } - UpdateSimplifyMap(in, output, false); + UpdateSimplifyMap(in, output, false, VarConstMap); return output; } //End of ITEOpts_InEqs() @@ -865,7 +878,7 @@ ASTNode Flatten(const ASTNode& a) ASTNode output; //cerr << "input:\n" << a << endl; - if (CheckSimplifyMap(a, output, pushNeg)) + if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; ASTVec c, outvec; @@ -893,8 +906,8 @@ ASTNode Flatten(const ASTNode& a) 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; } @@ -910,7 +923,7 @@ ASTNode Flatten(const ASTNode& a) 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; } @@ -947,8 +960,11 @@ ASTNode Flatten(const ASTNode& a) } 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; } @@ -959,7 +975,7 @@ ASTNode Flatten(const ASTNode& a) // output = RemoveContradictionsFromAND(output); //memoize - UpdateSimplifyMap(a, output, pushNeg); + UpdateSimplifyMap(a, output, pushNeg, VarConstMap); //cerr << "output:\n" << output << endl; return output; } //end of SimplifyAndOrFormula @@ -970,7 +986,7 @@ ASTNode Flatten(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() == 1 && NOT == a.GetKind())) @@ -1013,15 +1029,15 @@ ASTNode Flatten(const ASTNode& a) 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) @@ -1044,14 +1060,14 @@ ASTNode Flatten(const ASTNode& a) } //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 @@ -1070,14 +1086,14 @@ ASTNode Flatten(const ASTNode& a) } //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 @@ -1096,14 +1112,14 @@ ASTNode Flatten(const ASTNode& a) } //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())) @@ -1139,14 +1155,17 @@ ASTNode Flatten(const ASTNode& a) //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 @@ -1166,14 +1185,14 @@ ASTNode Flatten(const ASTNode& a) } //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())) @@ -1233,7 +1252,7 @@ ASTNode Flatten(const ASTNode& a) } //memoize - UpdateSimplifyMap(a, output, pushNeg); + UpdateSimplifyMap(a, output, pushNeg, VarConstMap); return output; } @@ -1243,7 +1262,7 @@ ASTNode Flatten(const ASTNode& a) return b; ASTNode output; - if (CheckSimplifyMap(b, output, pushNeg)) + if (CheckSimplifyMap(b, output, pushNeg, VarConstMap)) return output; if (!(b.Degree() == 3 && ITE == b.GetKind())) @@ -1313,7 +1332,7 @@ ASTNode Flatten(const ASTNode& a) } //memoize - UpdateSimplifyMap(a, output, pushNeg); + UpdateSimplifyMap(a, output, pushNeg, VarConstMap); return output; } @@ -1392,7 +1411,7 @@ ASTNode Flatten(const ASTNode& a) return SimplifyTerm(output); } - if (CheckSimplifyMap(inputterm, output, false)) + if (CheckSimplifyMap(inputterm, output, false, VarConstMap)) { //cerr << "SimplifierMap:" << inputterm << " output: " << output << endl; return output; @@ -2019,7 +2038,7 @@ ASTNode Flatten(const ASTNode& a) { output = annihilator; //memoize - UpdateSimplifyMap(inputterm, output, false); + UpdateSimplifyMap(inputterm, output, false, VarConstMap); //cerr << "output of SimplifyTerm: " << output << endl; return output; } @@ -2182,7 +2201,7 @@ ASTNode Flatten(const ASTNode& a) assert(NULL != output); //memoize - UpdateSimplifyMap(inputterm, output, false); + UpdateSimplifyMap(inputterm, output, false, VarConstMap); //cerr << "SimplifyTerm: output" << output << endl; // CheckSimplifyInvariant(inputterm,output); diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile index e8de198..28fd9be 100644 --- a/src/to-sat/Makefile +++ b/src/to-sat/Makefile @@ -15,5 +15,4 @@ clean: depend: $(SRCS) @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ --include depend - \ No newline at end of file +#-include depend \ No newline at end of file