endif
$(MAKE) -C $(SRC)/parser
$(MAKE) -C $(SRC)/main
- $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \
- $(SRC)/to-sat/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o \
- $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o \
- $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
+ $(AR) rc libstp.a $(SRC)/AST/*.o \
+ $(SRC)/STPManager/*.o \
+ $(SRC)/printer/*.o \
+ $(SRC)/absrefine_counterexample/*.o \
+ $(SRC)/to-sat/*.o \
+ $(SRC)/sat/*.o \
+ $(SRC)/simplifier/*.o \
+ $(SRC)/extlib-constbv/*.o \
+ $(SRC)/c_interface/*.o \
+ $(SRC)/parser/let-funcs.o \
+ $(SRC)/parser/parseCVC.o \
+ $(SRC)/parser/lexCVC.o \
+ $(SRC)/main/*.o
$(RANLIB) libstp.a
@mkdir -p lib
@mv libstp.a lib/
# * LICENSE: Please view LICENSE file in the home dir of this Program
# ********************************************************************/
-#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
-OPTIMIZE = -g # Debugging
-OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
-#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE
-CFLAGS_BASE = $(OPTIMIZE)
-#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT
-#CFLAGS_M32 = -m32
+#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
+OPTIMIZE = -g # Debugging
+OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
+#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE
+CFLAGS_BASE = $(OPTIMIZE)
+#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT
+#CRYPTOMINISAT = true
+#CFLAGS_M32 = -m32
SHELL=/bin/bash
endif
$(MAKE) -C $(SRC)/parser
$(MAKE) -C $(SRC)/main
- $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \
- $(SRC)/to-sat/*.o $(SRC)/sat/*.or $(SRC)/simplifier/*.o \
- $(SRC)/extlib-constbv/*.o $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o \
- $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o $(SRC)/main/*.o
+ $(AR) rc libstp.a $(SRC)/AST/*.o \
+ $(SRC)/STPManager/*.o \
+ $(SRC)/printer/*.o \
+ $(SRC)/absrefine_counterexample/*.o \
+ $(SRC)/to-sat/*.o \
+ $(SRC)/sat/*.o \
+ $(SRC)/simplifier/*.o \
+ $(SRC)/extlib-constbv/*.o \
+ $(SRC)/c_interface/*.o \
+ $(SRC)/parser/let-funcs.o \
+ $(SRC)/parser/parseCVC.o \
+ $(SRC)/parser/lexCVC.o \
+ $(SRC)/main/*.o
$(RANLIB) libstp.a
@mkdir -p lib
@mv libstp.a lib/
ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin();
ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end();
for(;it!=itend;it++)
- {
- ((*it).second).clear();
- }
+ {
+ ((*it).second).clear();
+ }
Arrayname_ReadindicesMap->clear();
delete Arrayname_ReadindicesMap;
}
void RunTimes::print()
{
if (0 != category_stack.size())
- {
- std::cerr << "size:" << category_stack.size() << std::endl;
- std::cerr << "top:" << CategoryNames[category_stack.top().first] << std::endl;
- BEEV::FatalError("category stack is not yet empty!!");
- }
+ {
+ std::cerr << "size:" << category_stack.size() << std::endl;
+ std::cerr << "top:" << CategoryNames[category_stack.top().first] << std::endl;
+ BEEV::FatalError("category stack is not yet empty!!");
+ }
std::ostringstream result;
result << "statistics\n";
delete arrayTransformer;
delete tosat;
delete simp;
-// delete bm;
+ // delete bm;
}
/****************************************************************
vector<ASTVec*>::iterator it = _asserts.begin();
vector<ASTVec*>::iterator itend = _asserts.end();
for(;it!=itend;it++)
- {
- ASTVec * j = (*it);
- j->clear();
- }
+ {
+ ASTVec * j = (*it);
+ j->clear();
+ }
_asserts.clear();
_interior_unique_table.clear();
}
ASTNode newRead = term;
- const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false);
+ const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false);
//iteratively expand read-over-write, and evaluate against the
//model at every iteration
- ASTNode write = newRead[0];
+ ASTNode write = newRead[0];
do
{
ASTNode writeIndex = TermToConstTermUsingModel(write[1], false);
- if (writeIndex == readIndex)
+ if (writeIndex == readIndex)
{
//found the write-value. return it
- output = TermToConstTermUsingModel(write[2], false);
+ output = TermToConstTermUsingModel(write[2], false);
CounterExampleMap[term] = output;
return output;
}
- write = write[0];
- } while (WRITE == write.GetKind());
+ write = write[0];
+ } while (WRITE == write.GetKind());
- const unsigned int width = term.GetValueWidth();
- newRead = bm->CreateTerm(READ, width, write, readIndex);
+ const unsigned int width = term.GetValueWidth();
+ newRead = bm->CreateTerm(READ, width, write, readIndex);
output = TermToConstTermUsingModel(newRead, arrayread_flag);
//memoize
CounterExampleMap[term] = output;
return output;
- } //Expand_ReadOverWrite_UsingModel()
+ } //Expand_ReadOverWrite_UsingModel()
/* FUNCTION: accepts a non-constant formula, and checks if the
* formula is ASTTrue or ASTFalse w.r.t to a model
// callback for SIGALRM.
void handle_time_out(int parameter){
- printf("Timed Out.\n");
- exit(0);
+ printf("Timed Out.\n");
+ exit(0);
}
.PHONY: core
core:
$(MAKE) -C core lib all
+ mv Solver.or Solver.o
.PHONY: simp
simp:
$(MAKE) -C simp lib all
+ mv SimpSolver.or SimpSolver.o
.PHONY: unsound
unsound:
$(MAKE) -C unsound lib all
+ mv UnsoundSimpSolver.or UnsoundSimpSolver.o
.PHONY: cryptominisat
cryptominisat:
$(MAKE) -C cryptominisat
cp cryptominisat/libminisat.a .
+ cp cryptominisat/CMakeFiles/minisat.dir/Solver/*.o .
.PHONY: clean
clean:
- rm -rf *.or *~ libminisat.a
+ rm -rf *.o *~ libminisat.a
$(MAKE) -C core clean
$(MAKE) -C simp clean
$(MAKE) -C unsound clean
#include "SolverTypes.h"
#ifdef _MSC_VER
-#include <ctime>
-
+ #include <ctime>
#else
-
-#include <sys/time.h>
-#include <sys/resource.h>
-#include <unistd.h>
+ #include <sys/time.h>
+ #include <sys/resource.h>
+ #include <unistd.h>
#endif
namespace MINISAT {
#define SAT_H_
#ifdef CRYPTOMINISAT
- #include "cryptominisat/Solver/Solver.h"
- #include "cryptominisat/Solver/SolverTypes.h"
+#include "cryptominisat/Solver/Solver.h"
+#include "cryptominisat/Solver/SolverTypes.h"
#else
- #include "core/Solver.h"
- #include "core/SolverTypes.h"
- //#include "simp/SimpSolver.h"
- //#include "unsound/UnsoundSimpSolver.h"
+#include "core/Solver.h"
+#include "core/SolverTypes.h"
+//#include "simp/SimpSolver.h"
+//#include "unsound/UnsoundSimpSolver.h"
#endif
#endif
// FIXME: Don't bother computing i+1 carry, which is discarded.
for (int i = 0; i < n; i++)
{
- ASTNode nextcin;
- if(i != n-1)
- {
- //Compute this only for i=0 to n-2
- nextcin = Majority(sum[i], y[i], cin);
- }
+ ASTNode nextcin;
+ if(i != n-1)
+ {
+ //Compute this only for i=0 to n-2
+ nextcin = Majority(sum[i], y[i], cin);
+ }
sum[i] = Sum(sum[i], y[i], cin);
- if(i != n-1)
- {
- //Compute this only for i=0 to n-2
- cin = nextcin;
- }
+ if(i != n-1)
+ {
+ //Compute this only for i=0 to n-2
+ cin = nextcin;
+ }
}
// cout << "----------------" << endl << "Result: " << endl;
// worth doing explicitly (e.g., a = b, a = ~b, etc.)
else
{
- // return _bm->CreateSimpForm(OR,
- // _bm->CreateSimpForm(AND, a, b),
- // _bm->CreateSimpForm(AND, b, c),
- // _bm->CreateSimpForm(AND, a, c));
- return _bm->CreateSimpForm(AND,
+ // return _bm->CreateSimpForm(OR,
+ // _bm->CreateSimpForm(AND, a, b),
+ // _bm->CreateSimpForm(AND, b, c),
+ // _bm->CreateSimpForm(AND, a, c));
+ return _bm->CreateSimpForm(AND,
_bm->CreateSimpForm(OR, a, b),
_bm->CreateSimpForm(OR, b, c),
_bm->CreateSimpForm(OR, a, c));
}
ASTNode BitBlaster::Sum(const ASTNode& xi,
- const ASTNode& yi,
- const ASTNode& cin)
+ const ASTNode& yi,
+ const ASTNode& cin)
{
// For some unexplained reason, XORs are faster than converting
// them to cluases at this point
ASTNode S0 = _bm->CreateSimpForm(XOR,
- _bm->CreateSimpForm(XOR, xi, yi),
- cin);
+ _bm->CreateSimpForm(XOR, xi, yi),
+ cin);
return S0;
// ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin);
// ASTNode S2 = _bm->CreateSimpForm(OR,
- // _bm->CreateSimpForm(NOT,xi),
- // _bm->CreateSimpForm(NOT,yi),
- // cin);
+ // _bm->CreateSimpForm(NOT,xi),
+ // _bm->CreateSimpForm(NOT,yi),
+ // cin);
// ASTNode S3 = _bm->CreateSimpForm(OR,
- // _bm->CreateSimpForm(NOT,xi),
- // yi,
- // _bm->CreateSimpForm(NOT,cin));
+ // _bm->CreateSimpForm(NOT,xi),
+ // yi,
+ // _bm->CreateSimpForm(NOT,cin));
// ASTNode S4 = _bm->CreateSimpForm(OR,
- // xi,
- // _bm->CreateSimpForm(NOT,yi),
- // _bm->CreateSimpForm(NOT,cin));
+ // xi,
+ // _bm->CreateSimpForm(NOT,yi),
+ // _bm->CreateSimpForm(NOT,cin));
// ASTVec S;
// S.push_back(S1);
// S.push_back(S2);
// complementing the result bit.
ASTNode BitBlaster::BBBVLE(const ASTVec& left,
const ASTVec& right,
- bool is_signed,
- bool is_bvlt)
+ bool is_signed,
+ bool is_bvlt)
{
ASTVec::const_reverse_iterator lit = left.rbegin();
ASTVec::const_reverse_iterator litend = left.rend();
for(lit++, rit++; lit < litend; lit++, rit++)
{
this_compare_bit =
- _bm->CreateSimpForm(AND, _bm->CreateSimpNot(*lit), *rit);
-
- ASTNode thisbit_output =
- _bm->CreateSimpForm(AND, this_compare_bit, prev_eq_bit);
- bit_comparisons.push_back(thisbit_output);
-
- // (neg(lit) OR rit)(lit OR neg(rit))
- ASTNode this_eq_bit =
- _bm->CreateSimpForm(AND,
- _bm->CreateSimpForm(IFF,*lit,*rit),
- prev_eq_bit);
- prev_eq_bit = this_eq_bit;
+ _bm->CreateSimpForm(AND, _bm->CreateSimpNot(*lit), *rit);
+
+ ASTNode thisbit_output =
+ _bm->CreateSimpForm(AND, this_compare_bit, prev_eq_bit);
+ bit_comparisons.push_back(thisbit_output);
+
+ // (neg(lit) OR rit)(lit OR neg(rit))
+ ASTNode this_eq_bit =
+ _bm->CreateSimpForm(AND,
+ _bm->CreateSimpForm(IFF,*lit,*rit),
+ prev_eq_bit);
+ prev_eq_bit = this_eq_bit;
}
if(!is_bvlt)
{
- bit_comparisons.push_back(prev_eq_bit);
+ bit_comparisons.push_back(prev_eq_bit);
}
ASTNode output =
_bm->CreateSimpForm(OR, bit_comparisons);
return output;
-// // "thisbit" represents BVLE of the suffixes of the BVs
-// // from that position . if R < L, return TRUE, else if L < R
-// // return FALSE, else return BVLE of lower-order bits. MSB is
-// // treated separately, because signed comparison is done by
-// // complementing the MSB of each BV, then doing an unsigned
-// // comparison.
-// ASTVec::const_iterator lit = left.rbegin();
-// ASTVec::const_iterator litend = left.rend();
-// ASTVec::const_iterator rit = right.rbegin();
-// ASTNode prevbit = ASTTrue;
-// for (; lit < litend - 1; lit++, rit++)
-// {
-// ASTNode neglit = _bm->CreateSimpNot(*lit);
-// ASTNode thisbit =
-// _bm->CreateSimpForm(OR,
-// _bm->CreateSimpForm(AND, neglit, *rit),
-// _bm->CreateSimpForm(AND,
-// _bm->CreateSimpForm(OR,
-// neglit,
-// *rit),
-// prevbit));
-// prevbit = thisbit;
-// }
-
-// // Handle MSB -- negate MSBs if signed comparison
-// // FIXME: make into refs after it's debugged.
-// ASTNode lmsb = *lit;
-// ASTNode rmsb = *rit;
-// if (is_signed)
-// {
-// lmsb = _bm->CreateSimpNot(*lit);
-// rmsb = _bm->CreateSimpNot(*rit);
-// }
-
-// ASTNode neglmsb = _bm->CreateSimpNot(lmsb);
-// ASTNode msb =
-// // TRUE if l < r
-// _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb),
-// _bm->CreateSimpForm(AND,
-// _bm->CreateSimpForm(OR,
-// neglmsb,
-// rmsb),
-// prevbit)); // else prevbit
-// return msb;
+ // // "thisbit" represents BVLE of the suffixes of the BVs
+ // // from that position . if R < L, return TRUE, else if L < R
+ // // return FALSE, else return BVLE of lower-order bits. MSB is
+ // // treated separately, because signed comparison is done by
+ // // complementing the MSB of each BV, then doing an unsigned
+ // // comparison.
+ // ASTVec::const_iterator lit = left.rbegin();
+ // ASTVec::const_iterator litend = left.rend();
+ // ASTVec::const_iterator rit = right.rbegin();
+ // ASTNode prevbit = ASTTrue;
+ // for (; lit < litend - 1; lit++, rit++)
+ // {
+ // ASTNode neglit = _bm->CreateSimpNot(*lit);
+ // ASTNode thisbit =
+ // _bm->CreateSimpForm(OR,
+ // _bm->CreateSimpForm(AND, neglit, *rit),
+ // _bm->CreateSimpForm(AND,
+ // _bm->CreateSimpForm(OR,
+ // neglit,
+ // *rit),
+ // prevbit));
+ // prevbit = thisbit;
+ // }
+
+ // // Handle MSB -- negate MSBs if signed comparison
+ // // FIXME: make into refs after it's debugged.
+ // ASTNode lmsb = *lit;
+ // ASTNode rmsb = *rit;
+ // if (is_signed)
+ // {
+ // lmsb = _bm->CreateSimpNot(*lit);
+ // rmsb = _bm->CreateSimpNot(*rit);
+ // }
+
+ // ASTNode neglmsb = _bm->CreateSimpNot(lmsb);
+ // ASTNode msb =
+ // // TRUE if l < r
+ // _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb),
+ // _bm->CreateSimpForm(AND,
+ // _bm->CreateSimpForm(OR,
+ // neglmsb,
+ // rmsb),
+ // prevbit)); // else prevbit
+ // return msb;
}
// Left shift within fixed field inserting zeros at LSB.
// Internal bit blasting routines.
ASTNode BBBVLE(const ASTVec& x,
- const ASTVec& y, bool is_signed, bool is_bvlt = false);
+ const ASTVec& y, bool is_signed, bool is_bvlt = false);
// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
ASTNode BBcompare(const ASTNode& form);
// (pos) AND ~> UNION
//****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- ClauseList* psi = COPY(*(info[*it]->clausespos));
-
- for (it++; it != varphi.GetChildren().end(); it++) {
- convertFormulaToCNF(*it, defs);
- CNFInfo* x = info[*it];
-
- if (sharesPos(*x) == 1) {
- psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end());
- delete (x->clausespos);
- x->clausespos = NULL;
- if (x->clausesneg == NULL) {
- delete x;
- info.erase(*it);
- }
- } else {
- INPLACE_UNION(psi, *(x->clausespos));
- reduceMemoryFootprintPos(*it);
- }
- }
- info[varphi]->clausespos = psi;
-} //End of convertFormulaToCNFPosAND()
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ ClauseList* psi = COPY(*(info[*it]->clausespos));
+
+ for (it++; it != varphi.GetChildren().end(); it++) {
+ convertFormulaToCNF(*it, defs);
+ CNFInfo* x = info[*it];
+
+ if (sharesPos(*x) == 1) {
+ psi->insert(psi->end(),x->clausespos->begin(), x->clausespos->end());
+ delete (x->clausespos);
+ x->clausespos = NULL;
+ if (x->clausesneg == NULL) {
+ delete x;
+ info.erase(*it);
+ }
+ } else {
+ INPLACE_UNION(psi, *(x->clausespos));
+ reduceMemoryFootprintPos(*it);
+ }
+ }
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosAND()
void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi,
ClauseList* defs)
int input_clauselist_size = cll.size();
if (cll.size() == 0)
{
- FatalError("toSATandSolve: Nothing to Solve", ASTUndefined);
+ FatalError("toSATandSolve: Nothing to Solve", ASTUndefined);
}
#ifdef CRYPTOMINISAT
MINISAT::vec<MINISAT::Lit> satSolverClause;
satSolverClause.capacity((*i)->size());
vector<const ASTNode*>::const_iterator j = (*i)->begin();
- vector<const ASTNode*>::const_iterator jend = (*i)->end();
- //ASTVec clauseVec;
+ vector<const ASTNode*>::const_iterator jend = (*i)->end();
+ //ASTVec clauseVec;
//j is a disjunct in the ASTclause (*i)
for (; j != jend; j++)
- {
+ {
ASTNode node = **j;
- //clauseVec.push_back(node);
+ //clauseVec.push_back(node);
bool negate = (NOT == node.GetKind()) ? true : false;
ASTNode n = negate ? node[0] : node;
MINISAT::Var v = LookupOrCreateSATVar(newS, n);
}
// ASTNode theClause = bm->CreateNode(OR, clauseVec);
- // if(flag
- // && ASTTrue == CheckBBandCNF(newS, theClause))
- // {
- // continue;
- // }
-
- newS.addClause(satSolverClause);
- float percentage=0.6;
- if(count++ >= input_clauselist_size*percentage)
- {
- //Arbitrary adding only 60% of the clauses in the hopes of
- //terminating early
- // cout << "Percentage clauses added: "
- // << percentage << endl;
- bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
- bm->GetRunTimes()->start(RunTimes::Solving);
- newS.solve();
- bm->GetRunTimes()->stop(RunTimes::Solving);
- if(!newS.okay())
- {
- return false;
- }
- count = 0;
- flag = 1;
- bm->GetRunTimes()->start(RunTimes::SendingToSAT);
- }
+ // if(flag
+ // && ASTTrue == CheckBBandCNF(newS, theClause))
+ // {
+ // continue;
+ // }
+#ifdef CRYPTOMINISAT
+ newS.addClause(satSolverClause,0,"z");
+#else
+ newS.addClause(satSolverClause);
+#endif
+ float percentage=0.6;
+ if(count++ >= input_clauselist_size*percentage)
+ {
+ //Arbitrary adding only 60% of the clauses in the hopes of
+ //terminating early
+ // cout << "Percentage clauses added: "
+ // << percentage << endl;
+ bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
+ bm->GetRunTimes()->start(RunTimes::Solving);
+ newS.solve();
+ bm->GetRunTimes()->stop(RunTimes::Solving);
+ if(!newS.okay())
+ {
+ return false;
+ }
+ count = 0;
+ flag = 1;
+ bm->GetRunTimes()->start(RunTimes::SendingToSAT);
+ }
if (newS.okay())
{
- continue;
- }
+ continue;
+ }
else
{
bm->PrintStats(newS);
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
return false;
- }
+ }
} // End of For-loop adding the clauses
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
ASTNode ToSAT::CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form)
{
// cout << "++++++++++++++++"
- // << endl
- // << "CheckBBandCNF_int form = "
- // << form << endl;
+ // << endl
+ // << "CheckBBandCNF_int form = "
+ // << form << endl;
ASTNodeMap::iterator memoit = CheckBBandCNFMemo.find(form);
if (memoit != CheckBBandCNFMemo.end())
{
result = SymbolTruthValue(newS, form);
- // cout << "================"
- // << endl
- // << "Checking BB formula:"
- // << form << endl;
- // cout << "----------------"
- // << endl
- // << "Result:" << result << endl;
+ // cout << "================"
+ // << endl
+ // << "Checking BB formula:"
+ // << form << endl;
+ // cout << "----------------"
+ // << endl
+ // << "Result:" << result << endl;
break;
}
default:
}
result = bm->CreateSimpForm(k, eval_children);
- // cout << "================"
- // << endl
- // << "Checking BB formula:" << form << endl;
- // cout << "----------------"
- // << endl
- // << "Result:" << result << endl;
-
+ // cout << "================"
+ // << endl
+ // << "Checking BB formula:" << form << endl;
+ // cout << "----------------"
+ // << endl
+ // << "Result:" << result << endl;
+
ASTNode replit_eval;
// Compare with replit, if there is one.
ASTNodeMap::iterator replit_it = RepLitMap.find(form);
bm->CreateSimpNot(SymbolTruthValue(newS, replit[0]));
}
- // cout << "----------------"
- // << endl
- // << "Rep lit: " << replit << endl;
- // cout << "----------------"
- // << endl
- // << "Rep lit value: " << replit_eval << endl;
+ // cout << "----------------"
+ // << endl
+ // << "Rep lit: " << replit << endl;
+ // cout << "----------------"
+ // << endl
+ // << "Rep lit value: " << replit_eval << endl;
if (result != replit_eval)
{
projects / francis / stp.git / commitdiff