From a3cea169ef6a8dd3d2e2b130fbe8ed9f8d39dcf7 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 3 Dec 2009 23:30:54 +0000 Subject: [PATCH] more xor-clausing for equality and BVLE/BVLT etc git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@450 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.common | 2 +- src/c_interface/c_interface.cpp | 13 ++++++++ src/c_interface/c_interface.h | 1 + src/to-sat/BitBlast.cpp | 57 ++++++--------------------------- 4 files changed, 25 insertions(+), 48 deletions(-) diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 4342f72..22c76b7 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -23,7 +23,7 @@ SOLVER_INCLUDE = ../sat/cryptominisat # OPTION to compile CRYPTOMiniSAT version 2.x #CRYPTOMINISAT2 = true -#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT2 +#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT2 #MTL = ../sat/cryptominisat2/mtl #SOLVER_INCLUDE = ../sat/cryptominisat2 diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 4a928fd..20f4bb0 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -765,6 +765,19 @@ Expr vc_orExpr(VC vc, Expr left, Expr right) { return output; } +Expr vc_xorExpr(VC vc, Expr left, Expr right) { + bmstar b = (bmstar)(((stpstar)vc)->bm); + nodestar l = (nodestar)left; + nodestar r = (nodestar)right; + + node o = b->CreateNode(BEEV::XOR,*l,*r); + BVTypeCheck(o); + nodestar output = new node(o); + //if(cinterface_exprdelete_on) created_exprs.push_back(output); + return output; +} + + Expr vc_andExprN(VC vc, Expr* cc, int n) { bmstar b = (bmstar)(((stpstar)vc)->bm); nodestar * c = (nodestar *)cc; diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index cd57735..f4a05d0 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -94,6 +94,7 @@ extern "C" { Expr vc_andExpr(VC vc, Expr left, Expr right); Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes); Expr vc_orExpr(VC vc, Expr left, Expr right); + Expr vc_xorExpr(VC vc, Expr left, Expr right); Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes); Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc); Expr vc_iffExpr(VC vc, Expr left, Expr right); diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 4193e4b..a762e07 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -940,7 +940,10 @@ namespace BEEV ASTVec bit_comparisons; bit_comparisons.push_back(this_compare_bit); - ASTNode prev_eq_bit = _bm->CreateSimpForm(IFF, *lit, *rit); + ASTNode prev_eq_bit = + _bm->CreateSimpForm(XOR, + _bm->CreateSimpForm(NOT,*lit), + *rit); for(lit++, rit++; lit < litend; lit++, rit++) { this_compare_bit = @@ -953,7 +956,9 @@ namespace BEEV // (neg(lit) OR rit)(lit OR neg(rit)) ASTNode this_eq_bit = _bm->CreateSimpForm(AND, - _bm->CreateSimpForm(IFF,*lit,*rit), + _bm->CreateSimpForm(XOR, + _bm->CreateSimpForm(NOT,*lit), + *rit), prev_eq_bit); prev_eq_bit = this_eq_bit; } @@ -966,50 +971,6 @@ namespace BEEV _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; } // Left shift within fixed field inserting zeros at LSB. @@ -1141,7 +1102,9 @@ namespace BEEV { for (; lit != litend; lit++, rit++) { - ASTNode biteq = _bm->CreateSimpForm(IFF, *lit, *rit); + ASTNode biteq = _bm->CreateSimpForm(XOR, + _bm->CreateSimpForm(NOT,*lit), + *rit); // fast path exit if (biteq == ASTFalse) { -- 2.47.3