-#!/bin/sh
-# File: my-indent
-# Opens a set of files in emacs and executes the emacs-format-function.
-# Assumes the function named emacs-format-function is defined in the
-# file named emacs-format-file.
+ #!/bin/sh
-loadpath=`pwd`
-if [ $# == 0 ]
-then
- echo "my-indent requires at least one argument." 1>&2
- echo "Usage: my-indent files-to-indent" 1>&2
- exit 1
-fi
+ # File: my-indent Opens a set of files in emacs and executes the
+ # emacs-format-function. Assumes the function named
+ # emacs-format-function is defined in the file named
+ # emacs-format-file.
-while [ $# -ge 1 ]
-do
- if [ -d $1 ]
+ loadpath=`pwd`
+ if [ $# == 0 ]
then
- echo "Argument of my-indent $1 cannot be a directory." 1>&2
- exit 1
+ echo "my-indent requires at least one argument." 1>&2
+ echo "Usage: my-indent files-to-indent" 1>&2
+ exit 1
fi
- # Check for existence of file:
- ls $1 2> /dev/null | grep $1 > /dev/null
- if [ $? != 0 ]
- then
- echo "my-indent: $1 not found." 1>&2
- exit 1
- fi
- echo "Indenting $1 with emacs in batch mode"
- emacs -batch $1 -l $loadpath/scripts/emacs-format-file -f emacs-format-function
- echo
- shift 1
-done
-exit 0
+ while [ $# -ge 1 ]
+ do
+ if [ -d $1 ]
+ then
+ echo "Argument of my-indent $1 cannot be a directory." 1>&2
+ exit 1
+ fi
+
+ # Check for existence of file:
+ ls $1 2> /dev/null | grep $1 > /dev/null
+ if [ $? != 0 ]
+ then
+ echo "my-indent: $1 not found." 1>&2
+ exit 1
+ fi
+ echo "Indenting $1 with emacs in batch mode"
+ emacs -batch $1 -l $loadpath/scripts/emacs-format-file -f emacs-format-function
+ echo
+ shift 1
+ done
+ exit 0
if(print_binary_flag) {
res = CONSTANTBV::BitVector_to_Bin(_bvconst);
if (c_friendly)
- {
- prefix = "0b";
- }
+ {
+ prefix = "0b";
+ }
else
- {
- prefix = "0bin";
- }
+ {
+ prefix = "0bin";
+ }
}
else if (_value_width % 4 == 0)
{
- res = CONSTANTBV::BitVector_to_Hex(_bvconst);
- if (c_friendly)
- {
- prefix = "0x";
- }
- else
- {
- prefix = "0hex";
- }
+ res = CONSTANTBV::BitVector_to_Hex(_bvconst);
+ if (c_friendly)
+ {
+ prefix = "0x";
+ }
+ else
+ {
+ prefix = "0hex";
+ }
}
else
{
- res = CONSTANTBV::BitVector_to_Bin(_bvconst);
- if (c_friendly)
- {
- prefix = "0b";
- }
- else
- {
- prefix = "0bin";
- }
+ res = CONSTANTBV::BitVector_to_Bin(_bvconst);
+ if (c_friendly)
+ {
+ prefix = "0b";
+ }
+ else
+ {
+ prefix = "0bin";
+ }
}
if (NULL == res)
{
- os << "nodeprint: BVCONST : could not convert to string" << _bvconst;
- FatalError("");
+ os << "nodeprint: BVCONST : could not convert to string" << _bvconst;
+ FatalError("");
}
os << prefix << res;
CONSTANTBV::BitVector_Dispose(res);
bool ASTBVConst::ASTBVConstEqual::operator()(const ASTBVConst * bvc1,
- const ASTBVConst * bvc2) const
+ const ASTBVConst * bvc2) const
{
if (bvc1->_value_width != bvc2->_value_width)
{
- return false;
+ return false;
}
return (0 ==
- CONSTANTBV::BitVector_Compare(bvc1->_bvconst,
- bvc2->_bvconst));
+ CONSTANTBV::BitVector_Compare(bvc1->_bvconst,
+ bvc2->_bvconst));
} //End of ASTBVConstEqual operator
};//End of namespace
{
public:
bool operator()(const ASTBVConst * bvc1,
- const ASTBVConst * bvc2) const;
+ const ASTBVConst * bvc2) const;
}; //End of class ASTBVConstEqual
/****************************************************************
if (bvc1._value_width != bvc2._value_width)
return false;
return (0 == CONSTANTBV::BitVector_Compare(bvc1._bvconst,
- bvc2._bvconst));
+ bvc2._bvconst));
} //End of operator==
// Call this when deleting a node that has been stored in the the
ASTVec::const_iterator iend = ch.end();
for (ASTVec::const_iterator i = ch.begin(); i != iend; i++)
{
- hashval += i->Hash();
- hashval += (hashval << 10);
- hashval ^= (hashval >> 6);
+ hashval += i->Hash();
+ hashval += (hashval << 10);
+ hashval ^= (hashval >> 6);
}
hashval += (hashval << 3);
hashval ^= (hashval >> 11);
hashval += (hashval << 15);
- return hashval;
+ return hashval;
} //End of ASTInteriorHasher operator()
//ASTInteriorEqual operator()
bool
ASTInterior::ASTInteriorEqual::
operator()(const ASTInterior *int_node_ptr1,
- const ASTInterior *int_node_ptr2) const
+ const ASTInterior *int_node_ptr2) const
{
return (*int_node_ptr1 == *int_node_ptr2);
} ///End of ASTInteriorEqual operator()
{
public:
bool operator()(const ASTInterior *int_node_ptr1,
- const ASTInterior *int_node_ptr2) const;
+ const ASTInterior *int_node_ptr2) const;
}; //End of class ASTInteriorEqual
// Used in Equality class for hash tables
friend bool operator==(const ASTInterior &int_node1,
- const ASTInterior &int_node2)
+ const ASTInterior &int_node2)
{
return ((int_node1._kind == int_node2._kind)
- && (int_node1._children == int_node2._children));
+ && (int_node1._children == int_node2._children));
} //End of operator==
// Call this when deleting a node that has been stored in the
void DecRef()
{
if (--_ref_count == 0)
- {
- // Delete node from unique table and kill it.
- CleanUp();
- }
+ {
+ // Delete node from unique table and kill it.
+ CleanUp();
+ }
}//End of DecRef()
int GetNodeNum() const
// Constructor;
//
// creates a new pointer, increments refcount of pointed-to object.
- ASTNode::ASTNode(ASTInternal *in) :
+ ASTNode::ASTNode(ASTInternal *in) :
_int_node_ptr(in)
{
if (in)
{
- in->IncRef();
+ in->IncRef();
}
} //End of Constructor
} //End of Copy Constructor for ASTNode
// ASTNode accessor function.
- Kind ASTNode::GetKind() const
+ Kind ASTNode::GetKind() const
{
//cout << "GetKind: " << _int_node_ptr;
return _int_node_ptr->GetKind();
} //End of GetKind()
// Declared here because of same ordering problem as GetKind.
- const ASTVec &ASTNode::GetChildren() const
+ const ASTVec &ASTNode::GetChildren() const
{
return _int_node_ptr->GetChildren();
} //End of GetChildren()
// Access node number
- int ASTNode::GetNodeNum() const
+ int ASTNode::GetNodeNum() const
{
return _int_node_ptr->_node_num;
} //End of GetNodeNum()
- unsigned int ASTNode::GetIndexWidth() const
+ unsigned int ASTNode::GetIndexWidth() const
{
return _int_node_ptr->_index_width;
} //End of GetIndexWidth()
- void ASTNode::SetIndexWidth(unsigned int iw) const
+ void ASTNode::SetIndexWidth(unsigned int iw) const
{
_int_node_ptr->_index_width = iw;
} //End of SetIndexWidth()
- unsigned int ASTNode::GetValueWidth() const
+ unsigned int ASTNode::GetValueWidth() const
{
return _int_node_ptr->_value_width;
} //End of GetValueWidth()
- void ASTNode::SetValueWidth(unsigned int vw) const
+ void ASTNode::SetValueWidth(unsigned int vw) const
{
_int_node_ptr->_value_width = vw;
} //End of SetValueWidth()
//return the type of the ASTNode:
//
// 0 iff BOOLEAN; 1 iff BITVECTOR; 2 iff ARRAY; 3 iff UNKNOWN;
- types ASTNode::GetType() const
+ types ASTNode::GetType() const
{
if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN
return BOOLEAN_TYPE;
} //End of GetType()
// Assignment
- ASTNode& ASTNode::operator=(const ASTNode& n)
+ ASTNode& ASTNode::operator=(const ASTNode& n)
{
if (n._int_node_ptr)
{
}
} //End of Destructor()
- STPMgr* ASTNode::GetSTPMgr() const
+ STPMgr* ASTNode::GetSTPMgr() const
{
return GlobalSTP->bm;
} //End of GetSTPMgr()
{
STPMgr * bm = GetSTPMgr();
return (bm->AlreadyPrintedSet.find(*this) !=
- bm->AlreadyPrintedSet.end());
+ bm->AlreadyPrintedSet.end());
} //End of IsAlreadyPrinted()
// Mark the node as printed if it has been already printed
friend bool operator==(const ASTNode node1, const ASTNode node2)
{
return
- ((size_t) node1._int_node_ptr) ==
- ((size_t) node2._int_node_ptr);
+ ((size_t) node1._int_node_ptr) ==
+ ((size_t) node2._int_node_ptr);
}
friend bool operator!=(const ASTNode node1, const ASTNode node2)
friend bool operator<(const ASTNode node1, const ASTNode node2)
{
return
- ((size_t) node1._int_node_ptr) <
- ((size_t) node2._int_node_ptr);
+ ((size_t) node1._int_node_ptr) <
+ ((size_t) node2._int_node_ptr);
}
public:
#ifdef TR1_UNORDERED_MAP
tr1::hash<string> h;
#else
- //hash<char *> h;
+ //hash<char *> h;
#endif
- //return h(sym_ptr->_name);
- //cerr << "ASTSymbol hasher recieved name: "
- //<< sym_ptr->_name << endl;
+ //return h(sym_ptr->_name);
+ //cerr << "ASTSymbol hasher recieved name: "
+ //<< sym_ptr->_name << endl;
return (size_t)hash((unsigned char*)(sym_ptr->_name));
};
}; // End of class ASTSymbolHasher
{
public:
bool operator()(const ASTSymbol *sym_ptr1,
- const ASTSymbol *sym_ptr2) const
+ const ASTSymbol *sym_ptr2) const
{
return (*sym_ptr1 == *sym_ptr2);
}
// comparator
friend bool operator==(const ASTSymbol &sym1,
- const ASTSymbol &sym2)
+ const ASTSymbol &sym2)
{
return (strcmp(sym1._name, sym2._name) == 0);
}
{
cout << endl;
for (function_counters::iterator
- it = s.begin(), itend = s.end();
- it != itend; it++)
+ it = s.begin(), itend = s.end();
+ it != itend; it++)
cout << "Number of times the function: "
- << it->first
- << ": is called: "
- << it->second << endl;
+ << it->first
+ << ": is called: "
+ << it->second << endl;
return;
}
s[functionname] += 1;
FatalError("BVTypeCheck: indices should be BVCONST\n", n);
if (n.GetValueWidth() != GetUnsignedConst(n[1]) - GetUnsignedConst(n[2]) + 1)
FatalError("BVTypeCheck: length mismatch\n", n);
- if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth())
- FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n);
+ if (GetUnsignedConst(n[1]) >= n[0].GetValueWidth())
+ FatalError("BVTypeCheck: Top index of select is greater or equal to the bitwidth.\n", n);
break;
case BVLEFTSHIFT:
case BVRIGHTSHIFT:
case FALSE:
case SYMBOL:
return true;
- case PARAMBOOL:
- if(2 != n.Degree())
- FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n);
- break;
+ case PARAMBOOL:
+ if(2 != n.Degree())
+ FatalError("BVTypeCheck: PARAMBOOL formula can have exactly two childNodes", n);
+ break;
case EQ:
if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth()))
{
//FIXME: Todo
break;
default:
-
+
FatalError("BVTypeCheck: Unrecognized kind: ");
break;
}
//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)))
+ && a[0].GetKind() == SYMBOL
+ && a[1].GetKind() == BVCONST
+ && (k2 == BVCONST)))
// || k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind()
// == BVCONST)))
return 1;
//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)))
+ && ((k2 == READ
+ && b[0].GetKind() == SYMBOL
+ && b[1].GetKind() == BVCONST)))
return -1;
if (SYMBOL == k2
- && (BVCONST == k1
- || TRUE == k1
- || FALSE == k1))
+ && (BVCONST == k1
+ || TRUE == k1
+ || FALSE == k1))
return -1;
return 0;
namespace BEEV
{
- // NB: This is the only function that should be called externally. It sets
- // up the cache that the others use.
+ // NB: This is the only function that should be called
+ // externally. It sets up the cache that the others use.
ASTNode ArrayTransformer::TransformFormula_TopLevel(const ASTNode& form)
{
runTimes->start(RunTimes::Transforming);
bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1));
// create the condition for the divisor
ASTNode cond_divisor =
- bm->CreateNode(EQ, one, bm->CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
+ bm->CreateNode(EQ, one,
+ bm->CreateTerm(BVEXTRACT, 1, divisor, hi1, hi1));
if (SBVREM == in.GetKind())
{
//Take absolute value.
ASTNode pos_dividend =
- bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
+ bm->CreateTerm(ITE, len,
+ cond_dividend,
+ bm->CreateTerm(BVUMINUS, len, dividend),
+ dividend);
ASTNode pos_divisor =
- bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
+ bm->CreateTerm(ITE, len,
+ cond_divisor,
+ bm->CreateTerm(BVUMINUS, len, divisor),
+ divisor);
//create the modulus term
- ASTNode modnode = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+ ASTNode modnode =
+ bm->CreateTerm(BVMOD, len,
+ pos_dividend, pos_divisor);
//If the dividend is <0 take the unary minus.
- ASTNode n = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, modnode), modnode);
+ ASTNode n =
+ bm->CreateTerm(ITE, len,
+ cond_dividend,
+ bm->CreateTerm(BVUMINUS, len, modnode),
+ modnode);
//put everything together, simplify, and return
return simp->SimplifyTerm_TopLevel(n);
// (bvneg (bvurem (bvneg s) (bvneg t)))))))
//Take absolute value.
- ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
- ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
+ ASTNode pos_dividend =
+ bm->CreateTerm(ITE, len,
+ cond_dividend,
+ bm->CreateTerm(BVUMINUS, len, dividend),
+ dividend);
+ ASTNode pos_divisor =
+ bm->CreateTerm(ITE, len,
+ cond_divisor,
+ bm->CreateTerm(BVUMINUS, len, divisor),
+ divisor);
- ASTNode urem_node = bm->CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
+ ASTNode urem_node =
+ bm->CreateTerm(BVMOD, len,
+ pos_dividend, pos_divisor);
// If the dividend is <0, then we negate the whole thing.
- ASTNode rev_node = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, urem_node), urem_node);
+ ASTNode rev_node =
+ bm->CreateTerm(ITE, len,
+ cond_dividend,
+ bm->CreateTerm(BVUMINUS, len, urem_node),
+ urem_node);
// if It's XOR <0 then add t (not its absolute value).
- ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor);
- ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
+ ASTNode xor_node =
+ bm->CreateNode(XOR, cond_dividend, cond_divisor);
+ ASTNode n =
+ bm->CreateTerm(ITE, len,
+ xor_node,
+ bm->CreateTerm(BVPLUS, len, rev_node, divisor),
+ rev_node);
return simp->SimplifyTerm_TopLevel(n);
}
//else simply output BVDIV(dividend,divisor)
//Take absolute value.
- ASTNode pos_dividend = bm->CreateTerm(ITE, len, cond_dividend, bm->CreateTerm(BVUMINUS, len, dividend), dividend);
- ASTNode pos_divisor = bm->CreateTerm(ITE, len, cond_divisor, bm->CreateTerm(BVUMINUS, len, divisor), divisor);
+ ASTNode pos_dividend =
+ bm->CreateTerm(ITE, len,
+ cond_dividend,
+ bm->CreateTerm(BVUMINUS, len, dividend),
+ dividend);
+ ASTNode pos_divisor =
+ bm->CreateTerm(ITE, len,
+ cond_divisor,
+ bm->CreateTerm(BVUMINUS, len, divisor),
+ divisor);
- ASTNode divnode = bm->CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
+ ASTNode divnode =
+ bm->CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
// A little confusing. Only negate the result if they are XOR <0.
- ASTNode xor_node = bm->CreateNode(XOR, cond_dividend, cond_divisor);
- ASTNode n = bm->CreateTerm(ITE, len, xor_node, bm->CreateTerm(BVUMINUS, len, divnode), divnode);
+ ASTNode xor_node =
+ bm->CreateNode(XOR, cond_dividend, cond_divisor);
+ ASTNode n =
+ bm->CreateTerm(ITE, len,
+ xor_node,
+ bm->CreateTerm(BVUMINUS, len, divnode),
+ divnode);
return simp->SimplifyTerm_TopLevel(n);
}
- FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in);
+ FatalError("TranslateSignedDivModRem:"\
+ "input must be signed DIV/MOD/REM", in);
return bm->CreateNode(UNDEFINED);
}//end of TranslateSignedDivModRem()
if (!(is_Form_kind(k) && BOOLEAN_TYPE == simpleForm.GetType()))
{
//FIXME: "You have inputted a NON-formula"?
- FatalError("TransformFormula: You have input a NON-formula", simpleForm);
+ FatalError("TransformFormula:"\
+ "You have input a NON-formula", simpleForm);
}
ASTNodeMap::iterator iter;
{
ASTVec vec;
ASTNode o;
- for (ASTVec::const_iterator it = simpleForm.begin(), itend = simpleForm.end(); it != itend; it++)
+ for (ASTVec::const_iterator
+ it = simpleForm.begin(),
+ itend = simpleForm.end(); it != itend; it++)
{
o = TransformFormula(*it);
vec.push_back(o);
break;
}
case FOR:
- {
- //Insert in a global list of FOR constructs. Return TRUE now
- //GlobalList_Of_FiniteLoops.push_back(simpleForm);
- return bm->CreateNode(TRUE);
- break;
- }
+ {
+ //Insert in a global list of FOR constructs. Return TRUE now
+ //GlobalList_Of_FiniteLoops.push_back(simpleForm);
+ return bm->CreateNode(TRUE);
+ break;
+ }
case PARAMBOOL:
- {
- //If the parameteric boolean variable is of the form
- //VAR(const), then convert it into a Boolean variable of the
- //form "VAR(const)".
- //
- //Else if the paramteric boolean variable is of the form
- //VAR(expression), then simply return it
- if(BVCONST == simpleForm[1].GetKind())
- {
- result = bm->NewParameterized_BooleanVar(simpleForm[0],simpleForm[1]);
- }
- else
- {
- result = simpleForm;
- }
- break;
- }
+ {
+ //If the parameteric boolean variable is of the form
+ //VAR(const), then convert it into a Boolean variable of the
+ //form "VAR(const)".
+ //
+ //Else if the paramteric boolean variable is of the form
+ //VAR(expression), then simply return it
+ if(BVCONST == simpleForm[1].GetKind())
+ {
+ result =
+ bm->NewParameterized_BooleanVar(simpleForm[0],simpleForm[1]);
+ }
+ else
+ {
+ result = simpleForm;
+ }
+ break;
+ }
default:
- {
- if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
- result = simpleForm;
- else
- {
- FatalError("TransformFormula: Illegal kind: ", bm->CreateNode(UNDEFINED), k);
- cerr << "The input is: " << simpleForm << endl;
- cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
- }
- break;
- }
+ {
+ if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
+ result = simpleForm;
+ else
+ {
+ FatalError("TransformFormula: Illegal kind: ",
+ bm->CreateNode(UNDEFINED), k);
+ cerr << "The input is: " << simpleForm << endl;
+ cerr << "The valuewidth of input is : "
+ << simpleForm.GetValueWidth() << endl;
+ }
+ break;
+ }
} //end of Switch
if (simpleForm.GetChildren().size() > 0)
ASTNode term = inputterm;
Kind k = term.GetKind();
if (!is_Term_kind(k))
- FatalError("TransformTerm: Illegal kind: You have input a nonterm:", inputterm, k);
+ FatalError("TransformTerm: Illegal kind: You have input a nonterm:",
+ inputterm, k);
ASTNodeMap::iterator iter;
if ((iter = TransformMap->find(term)) != TransformMap->end())
return iter->second;
{
case SYMBOL:
{
- // ASTNodeMap::iterator itsym;
- // if((itsym = CounterExampleMap.find(term)) != CounterExampleMap.end())
- // result = itsym->second;
+ // ASTNodeMap::iterator itsym; if((itsym =
+ // CounterExampleMap.find(term)) !=
+ // CounterExampleMap.end()) result = itsym->second;
// else
result = term;
break;
Kind k = result.GetKind();
- if (BVDIV == k || BVMOD == k || SBVDIV == k || SBVREM == k || SBVMOD == k)
+ if (BVDIV == k
+ || BVMOD == k
+ || SBVDIV == k
+ || SBVREM == k
+ || SBVMOD == k)
{
ASTNode bottom = result[1];
- if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind())
+ if (SBVDIV == result.GetKind()
+ || SBVREM == result.GetKind()
+ || SBVMOD == result.GetKind())
{
result = TranslateSignedDivModRem(result);
}
if (division_by_zero_returns_one)
{
- // This is a difficult rule to introduce in other places because it's recursive. i.e.
- // result is embedded unchanged inside the result.
+ // This is a difficult rule to introduce in other
+ // places because it's recursive. i.e. result is
+ // embedded unchanged inside the result.
unsigned inputValueWidth = result.GetValueWidth();
ASTNode zero = bm->CreateZeroConst(inputValueWidth);
ASTNode one = bm->CreateOneConst(inputValueWidth);
- result = bm->CreateTerm(ITE, inputValueWidth, bm->CreateNode(EQ, zero, bottom), one, result);
+ result =
+ bm->CreateTerm(ITE, inputValueWidth,
+ bm->CreateNode(EQ, zero, bottom),
+ one, result);
}
}
}
- ////////////////////////////////////////////////////////////////////////////////////
-
-
break;
}
if (term.GetChildren().size() > 0)
(*TransformMap)[term] = result;
if (term.GetValueWidth() != result.GetValueWidth())
- FatalError("TransformTerm: result and input terms are of different length", result);
+ FatalError("TransformTerm: "\
+ "result and input terms are of different length", result);
if (term.GetIndexWidth() != result.GetIndexWidth())
{
cerr << "TransformTerm: input term is : " << term << endl;
- FatalError("TransformTerm: result and input terms have different index length", result);
+ FatalError("TransformTerm: "\
+ "result & input terms have different index length", result);
}
return result;
} //End of TransformTerm
const unsigned int width = term.GetValueWidth();
if (READ != term.GetKind())
- FatalError("TransformArray: input term is of wrong kind: ", ASTUndefined);
+ FatalError("TransformArray: input term is of wrong kind: ",
+ ASTUndefined);
ASTNodeMap::iterator iter;
if ((iter = TransformMap->find(term)) != TransformMap->end())
*/
// Recursively transform read index, which may also contain reads.
- ASTNode processedTerm = bm->CreateTerm(READ, width, arrName, readIndex);
+ ASTNode processedTerm =
+ bm->CreateTerm(READ, width, arrName, readIndex);
//check if the 'processedTerm' has a corresponding ITE construct
//already. if so, return it. else continue processing.
ASTNodeMap::iterator it;
- if ((it = Arrayread_IteMap->find(processedTerm)) != Arrayread_IteMap->end())
+ if ((it = Arrayread_IteMap->find(processedTerm))
+ != Arrayread_IteMap->end())
{
result = it->second;
break;
//Constructing Symbolic variable corresponding to 'processedTerm'
ASTNode CurrentSymbol;
ASTNodeMap::iterator it1;
- // First, check if read index is constant and it has a constant value in the substitution map.
+ // First, check if read index is constant and it has a
+ // constant value in the substitution map.
if (simp->CheckSubstitutionMap(processedTerm, CurrentSymbol))
{
Arrayread_SymbolMap[processedTerm] = CurrentSymbol;
}
// Check if it already has an abstract variable.
- else if ((it1 = Arrayread_SymbolMap.find(processedTerm)) != Arrayread_SymbolMap.end())
+ else if ((it1 = Arrayread_SymbolMap.find(processedTerm))
+ != Arrayread_SymbolMap.end())
{
CurrentSymbol = it1->second;
}
else
{
- // Make up a new abstract variable.
- // FIXME: Make this into a method (there already may BE a method) and
- // get rid of the fixed-length buffer!
- //build symbolic name corresponding to array read. The symbolic
- //name has 2 components: stringname, and a count
+ // Make up a new abstract variable. FIXME: Make this
+ // into a method (there already may BE a method) and get
+ // rid of the fixed-length buffer! build symbolic name
+ // corresponding to array read. The symbolic name has 2
+ // components: stringname, and a count
const char * b = arrName.GetName();
std::string c(b);
char d[32];
ASTVec::const_reverse_iterator it2end = readIndices.rend();
for (; it2 != it2end; it2++)
{
- ASTNode cond = simp->CreateSimplifiedEQ(readIndex, *it2);
+ ASTNode cond =
+ simp->CreateSimplifiedEQ(readIndex, *it2);
if (ASTFalse == cond)
continue;
- ASTNode arrRead = bm->CreateTerm(READ, width, arrName, *it2);
+ ASTNode arrRead =
+ bm->CreateTerm(READ, width, arrName, *it2);
assert(BVTypeCheck(arrRead));
ASTNode arrayreadSymbol = Arrayread_SymbolMap[arrRead];
if (arrayreadSymbol.IsNull())
- FatalError("TransformArray:symbolic variable for processedTerm, p,"
- "does not exist:p = ", arrRead);
- ite = simp->CreateSimplifiedTermITE(cond, arrayreadSymbol, ite);
+ {
+ FatalError("TransformArray:"\
+ "symbolic variable for processedTerm, p,"\
+ "does not exist:p = ", arrRead);
+ }
+ ite =
+ simp->CreateSimplifiedTermITE(cond, arrayreadSymbol, ite);
}
result = ite;
//}
ASTNode writeVal = TransformTerm(arrName[2]);
if (ARRAY_TYPE != arrName[0].GetType())
- FatalError("TransformArray: An array write is being attempted on a non-array:", term);
+ FatalError("TransformArray: "\
+ "An array write is being attempted on a non-array:",
+ term);
- if ((SYMBOL == arrName[0].GetKind() || WRITE == arrName[0].GetKind()))
+ if ((SYMBOL == arrName[0].GetKind()
+ || WRITE == arrName[0].GetKind()))
{
- ASTNode cond = simp->CreateSimplifiedEQ(writeIndex, readIndex);
+ ASTNode cond =
+ simp->CreateSimplifiedEQ(writeIndex, readIndex);
BVTypeCheck(cond);
- ASTNode readTerm = bm->CreateTerm(READ, width, arrName[0], readIndex);
+ ASTNode readTerm =
+ bm->CreateTerm(READ, width, arrName[0], readIndex);
BVTypeCheck(readTerm);
ASTNode readPushedIn = TransformArray(readTerm);
BVTypeCheck(readPushedIn);
- result = simp->CreateSimplifiedTermITE(cond, writeVal, readPushedIn);
-
+ result =
+ simp->CreateSimplifiedTermITE(cond, writeVal, readPushedIn);
BVTypeCheck(result);
}
else if (ITE == arrName[0].GetKind())
{
- // pull out the ite from the write // pushes the write through.
- ASTNode writeTrue = bm->CreateNode(WRITE, (arrName[0][1]), writeIndex, writeVal);
+ // pull out the ite from the write // pushes the write
+ // through.
+ ASTNode writeTrue =
+ bm->CreateNode(WRITE, (arrName[0][1]), writeIndex, writeVal);
writeTrue.SetIndexWidth(writeIndex.GetValueWidth());
writeTrue.SetValueWidth(writeVal.GetValueWidth());
assert(ARRAY_TYPE == writeTrue.GetType());
- ASTNode writeFalse = bm->CreateNode(WRITE, (arrName[0][2]), writeIndex, writeVal);
+ ASTNode writeFalse =
+ bm->CreateNode(WRITE, (arrName[0][2]), writeIndex, writeVal);
writeFalse.SetIndexWidth(writeIndex.GetValueWidth());
writeFalse.SetValueWidth(writeVal.GetValueWidth());
assert(ARRAY_TYPE == writeFalse.GetType());
- result = simp->CreateSimplifiedTermITE(TransformFormula(arrName[0][0]), writeTrue, writeFalse);
+ result =
+ simp->CreateSimplifiedTermITE(TransformFormula(arrName[0][0]),
+ writeTrue, writeFalse);
result.SetIndexWidth(writeIndex.GetValueWidth());
result.SetValueWidth(writeVal.GetValueWidth());
assert(ARRAY_TYPE == result.GetType());
- result = bm->CreateTerm(READ, writeVal.GetValueWidth(), result, readIndex);
+ result =
+ bm->CreateTerm(READ, writeVal.GetValueWidth(),
+ result, readIndex);
BVTypeCheck(result);
result = TransformArray(result);
}
break;
}
default:
- FatalError("TransformArray: The READ is NOT over SYMBOL/WRITE/ITE", term);
+ FatalError("TransformArray: "\
+ "The READ is NOT over SYMBOL/WRITE/ITE", term);
break;
}
ASTVec c = a.GetChildren();
SortByArith(c);
if (SYMBOL != c[0].GetKind() ||
- bm->VarSeenInTerm(c[0],
- simp->SimplifyFormula_NoRemoveWrites(c[1], false)))
+ bm->VarSeenInTerm(c[0],
+ simp->SimplifyFormula_NoRemoveWrites(c[1], false)))
{
return a;
}
bool updated =
- simp->UpdateSubstitutionMap(c[0], simp->SimplifyFormula(c[1], false));
+ simp->UpdateSubstitutionMap(c[0],
+ simp->SimplifyFormula(c[1], false));
output = updated ? ASTTrue : a;
return output;
}
ASTNode c1 = simp->SimplifyTerm(c[1]);
if (SYMBOL == c[0].GetKind()
- && bm->VarSeenInTerm(c[0], c1))
+ && bm->VarSeenInTerm(c[0], c1))
{
return a;
}
if (1 == TermOrder(c[0], c[1])
- && READ == c[0].GetKind()
- && bm->VarSeenInTerm(c[0][1], c1))
+ && READ == c[0].GetKind()
+ && bm->VarSeenInTerm(c[0][1], c1))
{
return a;
}
{
ASTVec o;
ASTVec c = a.GetChildren();
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ for (ASTVec::iterator
+ it = c.begin(), itend = c.end();
+ it != itend; it++)
{
simp->UpdateAlwaysTrueFormMap(*it);
ASTNode aaa = CreateSubstitutionMap(*it);
//by a BVCONST (e1). This is necessary for later Leibnitz Axiom
//generation
void ArrayTransformer::FillUp_ArrReadIndex_Vec(const ASTNode& e0,
- const ASTNode& e1)
+ const ASTNode& e1)
{
int i = TermOrder(e0, e1);
if (0 == i)
return;
if (1 == i
- && e0.GetKind() != SYMBOL
- && !simp->CheckSubstitutionMap(e0))
+ && e0.GetKind() != SYMBOL
+ && !simp->CheckSubstitutionMap(e0))
{
(*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]);
//e0 is the array read : READ(A,i) and e1 is a bvconst
return;
}
if (-1 == i
- && e1.GetKind() != SYMBOL
- && !simp->CheckSubstitutionMap(e1))
+ && e1.GetKind() != SYMBOL
+ && !simp->CheckSubstitutionMap(e1))
{
(*Arrayname_ReadindicesMap)[e1[0]].push_back(e1[1]);
//e0 is the array read : READ(A,i) and e1 is a bvconst
bool FoundIntroducedSymbolSet(const ASTNode& in)
{
if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end())
- {
- return true;
- }
+ {
+ return true;
+ }
return false;
} // End of IntroduceSymbolSet
{
for (ASTNodeToVecMap::iterator
- iset = Arrayname_ReadindicesMap->begin(),
- iset_end = Arrayname_ReadindicesMap->end();
- iset != iset_end; iset++)
- {
- iset->second.clear();
- }
+ iset = Arrayname_ReadindicesMap->begin(),
+ iset_end = Arrayname_ReadindicesMap->end();
+ iset != iset_end; iset++)
+ {
+ iset->second.clear();
+ }
Arrayname_ReadindicesMap->clear();
Arrayread_SymbolMap.clear();
namespace BEEV
{
- void FatalError(const char * str);
+ void FatalError(const char * str);
}
long RunTimes::getCurrentTime()
{
- timeval t;
- gettimeofday(&t, NULL);
- return (1000 * t.tv_sec) + (t.tv_usec / 1000);
+ timeval t;
+ gettimeofday(&t, NULL);
+ return (1000 * t.tv_sec) + (t.tv_usec / 1000);
}
void RunTimes::print()
{
- if (0 != category_stack.size())
- BEEV::FatalError("category stack is not yet emptuy");
+ if (0 != category_stack.size())
+ BEEV::FatalError("category stack is not yet emptuy");
- std::ostringstream result;
- result << "statistics\n";
- std::map<Category, int>::const_iterator it1 = counts.begin();
- std::map<Category, long>::const_iterator it2 = times.begin();
+ std::ostringstream result;
+ result << "statistics\n";
+ std::map<Category, int>::const_iterator it1 = counts.begin();
+ std::map<Category, long>::const_iterator it2 = times.begin();
- while (it1 != counts.end())
- {
- result << " " << CategoryNames[it1->first] << ": " << it1->second;
- if ((it2 = times.find(it1->first)) != times.end())
- result << " [" << it2->second << "ms]";
- result << std::endl;
- it1++;
- }
+ while (it1 != counts.end())
+ {
+ result << " " << CategoryNames[it1->first] << ": " << it1->second;
+ if ((it2 = times.find(it1->first)) != times.end())
+ result << " [" << it2->second << "ms]";
+ result << std::endl;
+ it1++;
+ }
- std::cerr << result.str();
- // iterator
+ std::cerr << result.str();
+ // iterator
}
void RunTimes::addTime(Category c, long milliseconds)
{
- std::map<Category, long>::iterator it;
- if ((it = times.find(c)) == times.end())
- {
- times[c] = milliseconds;
- }
- else
- {
- it->second += milliseconds;
- }
+ std::map<Category, long>::iterator it;
+ if ((it = times.find(c)) == times.end())
+ {
+ times[c] = milliseconds;
+ }
+ else
+ {
+ it->second += milliseconds;
+ }
}
void RunTimes::addCount(Category c)
{
- std::map<Category, int>::iterator it;
- if ((it = counts.find(c)) == counts.end())
- {
- counts[c] = 1;
- }
- else
- {
- it->second++;
- }
+ std::map<Category, int>::iterator it;
+ if ((it = counts.find(c)) == counts.end())
+ {
+ counts[c] = 1;
+ }
+ else
+ {
+ it->second++;
+ }
}
void RunTimes::stop(Category c)
{
- Element e = category_stack.top();
- category_stack.pop();
- if (e.first != c)
- {
- std::cerr << e.first;
- std::cerr << c;
- BEEV::FatalError("Don't match");
- }
- addTime(c, getCurrentTime() - e.second);
- addCount(c);
+ Element e = category_stack.top();
+ category_stack.pop();
+ if (e.first != c)
+ {
+ std::cerr << e.first;
+ std::cerr << c;
+ BEEV::FatalError("Don't match");
+ }
+ addTime(c, getCurrentTime() - e.second);
+ addCount(c);
}
void RunTimes::start(Category c)
{
- category_stack.push(std::make_pair(c, getCurrentTime()));
+ category_stack.push(std::make_pair(c, getCurrentTime()));
}
typedef std::pair<Category, long> Element;
- private:
+private:
RunTimes& operator =(const RunTimes&);
RunTimes(const RunTimes& other);
long getCurrentTime();
void addTime(Category c, long milliseconds);
- public:
+public:
void addCount(Category c);
void start(Category c);
RunTimes(){}
void clear()
- {
- counts.clear();
- times.clear();
- category_stack.empty();
- }
+ {
+ counts.clear();
+ times.clear();
+ category_stack.empty();
+ }
};
#endif
#include "RunTimes.h"
#ifdef EXT_HASH_MAP
- #include <ext/hash_set>
- #include <ext/hash_map>
+#include <ext/hash_set>
+#include <ext/hash_map>
#elif defined(TR1_UNORDERED_MAP)
- #include <tr1/unordered_map>
- #include <tr1/unordered_set>
- #define hash_map tr1::unordered_map
- #define hash_set tr1::unordered_set
- #define hash_multiset tr1::unordered_multiset
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+#define hash_map tr1::unordered_map
+#define hash_set tr1::unordered_set
+#define hash_multiset tr1::unordered_multiset
#else
- #include <hash_set>
- #include <hash_map>
+#include <hash_set>
+#include <hash_map>
#endif
#define HASHMAP hash_map
eqstr> function_counters;
#else
typedef HASHMAP<const char*,
- int,
- hash<char *>,
- eqstr> function_counters;
+ int,
+ hash<char *>,
+ eqstr> function_counters;
#endif
// Function that computes various kinds of statistics for the phases
{
inputToSAT = simplified_solved_InputToSAT;
- if(optimize_flag)
- {
+ if(optimize_flag)
+ {
- bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
- simplified_solved_InputToSAT =
- arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
- bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
- //printf("##################################################\n");
- bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+ bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
+ simplified_solved_InputToSAT =
+ arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
+ bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
+ //printf("##################################################\n");
+ bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
- simplified_solved_InputToSAT =
- simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+ simplified_solved_InputToSAT =
+ simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
- bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
- }
+ bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+ }
- if(wordlevel_solve_flag)
- {
- simplified_solved_InputToSAT =
- bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
- bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
- }
+ if(wordlevel_solve_flag)
+ {
+ simplified_solved_InputToSAT =
+ bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+ bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+ }
}
while (inputToSAT != simplified_solved_InputToSAT);
bm->ASTNodeStats("Before SimplifyWrites_Inplace begins: ",
- simplified_solved_InputToSAT);
+ simplified_solved_InputToSAT);
bm->SimplifyWrites_InPlace_Flag = true;
bm->Begin_RemoveWrites = false;
{
inputToSAT = simplified_solved_InputToSAT;
- if(optimize_flag)
- {
- bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
- simplified_solved_InputToSAT =
- arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
- bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
- bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
-
- simplified_solved_InputToSAT =
- simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
- bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
- }
-
- if(wordlevel_solve_flag)
- {
- simplified_solved_InputToSAT =
- bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
- bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
- }
+ if(optimize_flag)
+ {
+ bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
+ simplified_solved_InputToSAT =
+ arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
+ bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
+ bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+
+ simplified_solved_InputToSAT =
+ simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+ bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+ }
+
+ if(wordlevel_solve_flag)
+ {
+ simplified_solved_InputToSAT =
+ bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
+ bm->ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+ }
} while (inputToSAT != simplified_solved_InputToSAT);
bm->ASTNodeStats("After SimplifyWrites_Inplace: ",
- simplified_solved_InputToSAT);
+ simplified_solved_InputToSAT);
bm->start_abstracting = (arraywrite_refinement_flag) ? true : false;
bm->SimplifyWrites_InPlace_Flag = false;
if (bm->start_abstracting)
{
bm->ASTNodeStats("before abstraction round begins: ",
- simplified_solved_InputToSAT);
+ simplified_solved_InputToSAT);
}
bm->TermsAlreadySeenMap_Clear();
res =
Ctr_Example->CallSAT_ResultCheck(newS,
- simplified_solved_InputToSAT,
- orig_input);
+ simplified_solved_InputToSAT,
+ orig_input);
if (SOLVER_UNDECIDED != res)
{
CountersAndStats("print_func_stats");
// res = SATBased_AllFiniteLoops_Refinement(newS, orig_input);
// if (SOLVER_UNDECIDED != res)
// {
- // CountersAndStats("print_func_stats");
+ // CountersAndStats("print_func_stats");
// return res;
// }
res =
Ctr_Example->SATBased_ArrayReadRefinement(newS,
- simplified_solved_InputToSAT,
- orig_input);
+ simplified_solved_InputToSAT,
+ orig_input);
if (SOLVER_UNDECIDED != res)
{
CountersAndStats("print_func_stats");
res =
Ctr_Example->SATBased_ArrayReadRefinement(newS,
- simplified_solved_InputToSAT,
- orig_input);
+ simplified_solved_InputToSAT,
+ orig_input);
if (SOLVER_UNDECIDED != res)
{
CountersAndStats("print_func_stats");
return SOLVER_ERROR;
} //End of TopLevelSTPAux
-// void STP::ClearAllTables(void)
-// {
-// // //Clear STPManager caches
-
-// // //Clear ArrayTransformer caches
-
-// // //Clear Simplifier caches
-
-// // //Clear BVSolver caches
-
-// // //Clear AbsRefine_CounterExample caches
-
-// // //clear all tables before calling toplevelsat
-// // //_ASTNode_to_SATVar.clear();
-// // //_SATVar_to_AST.clear();
-
-// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(),
-// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++)
-// // // {
-// // // (it->second)->clear();
-// // // delete (it->second);
-// // // }
-// // // _ASTNode_to_Bitvector.clear();
-
-// // NodeLetVarMap.clear();
-// // NodeLetVarMap1.clear();
-// // PLPrintNodeSet.clear();
-// // AlreadyPrintedSet.clear();
-// // //ReferenceCount->clear();
-// // //_arrayread_ite.clear();
-// // //_introduced_symbols.clear();
-// // //CounterExampleMap.clear();
-// // //ComputeFormulaMap.clear();
-// // StatInfoSet.clear();
-
-// // _asserts.clear();
-
-// // // for (ASTNodeToVecMap::iterator iset =
-// // // _arrayname_readindices.begin(), iset_end =
-// // // _arrayname_readindices.end(); iset != iset_end; iset++) {
-// // // iset->second.clear(); }
-// // // _arrayname_readindices.clear();
-
-// // _interior_unique_table.clear();
-// // _symbol_unique_table->clear();
-// // _bvconst_unique_table.clear();
-// }
-
-// void STP::ClearAllCaches(void)
-// {
-// // //clear all tables before calling toplevelsat
-// // //_ASTNode_to_SATVar.clear();
-// // //_SATVar_to_AST.clear();
-
-// // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(),
-// // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++)
-// // // {
-// // // (it->second)->clear();
-// // // delete (it->second);
-// // // }
-// // // _ASTNode_to_Bitvector.clear();
+ // void STP::ClearAllTables(void)
+ // {
+ // // //Clear STPManager caches
+
+ // // //Clear ArrayTransformer caches
+
+ // // //Clear Simplifier caches
+
+ // // //Clear BVSolver caches
+
+ // // //Clear AbsRefine_CounterExample caches
+
+ // // //clear all tables before calling toplevelsat
+ // // //_ASTNode_to_SATVar.clear();
+ // // //_SATVar_to_AST.clear();
+
+ // // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(),
+ // // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++)
+ // // // {
+ // // // (it->second)->clear();
+ // // // delete (it->second);
+ // // // }
+ // // // _ASTNode_to_Bitvector.clear();
+
+ // // NodeLetVarMap.clear();
+ // // NodeLetVarMap1.clear();
+ // // PLPrintNodeSet.clear();
+ // // AlreadyPrintedSet.clear();
+ // // //ReferenceCount->clear();
+ // // //_arrayread_ite.clear();
+ // // //_introduced_symbols.clear();
+ // // //CounterExampleMap.clear();
+ // // //ComputeFormulaMap.clear();
+ // // StatInfoSet.clear();
+
+ // // _asserts.clear();
+
+ // // // for (ASTNodeToVecMap::iterator iset =
+ // // // _arrayname_readindices.begin(), iset_end =
+ // // // _arrayname_readindices.end(); iset != iset_end; iset++) {
+ // // // iset->second.clear(); }
+ // // // _arrayname_readindices.clear();
+
+ // // _interior_unique_table.clear();
+ // // _symbol_unique_table->clear();
+ // // _bvconst_unique_table.clear();
+ // }
+
+ // void STP::ClearAllCaches(void)
+ // {
+ // // //clear all tables before calling toplevelsat
+ // // //_ASTNode_to_SATVar.clear();
+ // // //_SATVar_to_AST.clear();
+
+ // // // for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(),
+ // // // itend = _ASTNode_to_Bitvector.end(); it != itend; it++)
+ // // // {
+ // // // (it->second)->clear();
+ // // // delete (it->second);
+ // // // }
+ // // // _ASTNode_to_Bitvector.clear();
-// // NodeLetVarMap.clear();
-// // NodeLetVarMap1.clear();
-// // PLPrintNodeSet.clear();
-// // AlreadyPrintedSet.clear();
-// // // SimplifyMap->clear();
-// // // SimplifyNegMap->clear();
-// // // ReferenceCount->clear();
-// // // SolverMap.clear();
-// // //AlwaysTrueFormMap.clear();
-// // //_arrayread_ite.clear();
-// // //_arrayread_symbol.clear();
-// // //_introduced_symbols.clear();
-// // //CounterExampleMap.clear();
-// // //ComputeFormulaMap.clear();
-// // StatInfoSet.clear();
-
-// // // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++)
-// // // {
-// // // iset->second.clear();
-// // // }
+ // // NodeLetVarMap.clear();
+ // // NodeLetVarMap1.clear();
+ // // PLPrintNodeSet.clear();
+ // // AlreadyPrintedSet.clear();
+ // // // SimplifyMap->clear();
+ // // // SimplifyNegMap->clear();
+ // // // ReferenceCount->clear();
+ // // // SolverMap.clear();
+ // // //AlwaysTrueFormMap.clear();
+ // // //_arrayread_ite.clear();
+ // // //_arrayread_symbol.clear();
+ // // //_introduced_symbols.clear();
+ // // //CounterExampleMap.clear();
+ // // //ComputeFormulaMap.clear();
+ // // StatInfoSet.clear();
+
+ // // // for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++)
+ // // // {
+ // // // iset->second.clear();
+ // // // }
-// // // _arrayname_readindices.clear();
-// // //_interior_unique_table.clear();
-// // //_symbol_unique_table.clear();
-// // //_bvconst_unique_table.clear();
-// }
+ // // // _arrayname_readindices.clear();
+ // // //_interior_unique_table.clear();
+ // // //_symbol_unique_table.clear();
+ // // //_bvconst_unique_table.clear();
+ // }
}; //end of namespace
//Constructor
STP(STPMgr* b,
- Simplifier* s,
- BVSolver* bsolv,
- ArrayTransformer * a,
- ToSAT * ts,
- AbsRefine_CounterExample * ce)
+ Simplifier* s,
+ BVSolver* bsolv,
+ ArrayTransformer * a,
+ ToSAT * ts,
+ AbsRefine_CounterExample * ce)
{
bm = b;
simp = s;
~STP()
{
- ClearAllTables();
+ ClearAllTables();
}
/****************************************************************
// The absolute TopLevel function that invokes STP on the input
// formula
SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts,
- const ASTNode& query)
+ const ASTNode& query)
{
ASTNode q = bm->CreateNode(AND,
- inputasserts,
- bm->CreateNode(NOT, query));
+ inputasserts,
+ bm->CreateNode(NOT, query));
return TopLevelSTPAux(q);
} //End of TopLevelSTP()
n_ptr->SetNodeNum(NewNodeNum());
}
pair<ASTInteriorSet::const_iterator, bool> p =
- _interior_unique_table.insert(n_ptr);
+ _interior_unique_table.insert(n_ptr);
return *(p.first);
}
else
}
ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTVec & back_children)
+ const ASTNode& child0,
+ const ASTVec & back_children)
{
ASTInterior *n_ptr = new ASTInterior(kind);
}
ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec & back_children)
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTVec & back_children)
{
ASTInterior *n_ptr = new ASTInterior(kind);
ASTVec &front_children = n_ptr->_children;
}
ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec & back_children)
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2,
+ const ASTVec & back_children)
{
ASTInterior *n_ptr = new ASTInterior(kind);
ASTVec &front_children = n_ptr->_children;
}
ASTInterior *STPMgr::CreateInteriorNode(Kind kind,
- // children array of this node will be modified.
- ASTInterior *n_ptr,
- const ASTVec & back_children)
+ // children array of this node will be modified.
+ ASTInterior *n_ptr,
+ const ASTVec & back_children)
{
// insert back_children at end of front_children
ASTVec &front_children = n_ptr->_children;
front_children.insert(front_children.end(),
- back_children.begin(),
- back_children.end());
+ back_children.begin(),
+ back_children.end());
// check for undefined nodes.
ASTVec::const_iterator it_end = front_children.end();
for (ASTVec::const_iterator it = front_children.begin(); it != it_end; it++)
{
if (it->IsNull())
- {
- FatalError("CreateInteriorNode:"\
- "Undefined childnode in CreateInteriorNode: ",
- ASTUndefined);
- }
+ {
+ FatalError("CreateInteriorNode:"\
+ "Undefined childnode in CreateInteriorNode: ",
+ ASTUndefined);
+ }
}
return LookupOrCreateInterior(n_ptr);
s_ptr1->SetNodeNum(NewNodeNum());
s_ptr1->_value_width = s_ptr->_value_width;
pair<ASTSymbolSet::const_iterator, bool> p =
- _symbol_unique_table.insert(s_ptr1);
+ _symbol_unique_table.insert(s_ptr1);
return *p.first;
}
else
{
- // return symbol found in table.
- return *it;
+ // return symbol found in table.
+ return *it;
}
} // End of LookupOrCreateSymbol
ASTSymbol* s_ptr = &s; // it's a temporary key.
if (_symbol_unique_table.find(s_ptr) ==
- _symbol_unique_table.end())
+ _symbol_unique_table.end())
return false;
else
return true;
{
if (width > (sizeof(unsigned long long int) << 3) || width <= 0)
FatalError("CreateBVConst: "\
- "trying to create a bvconst using unsigned long long of width: ",
- ASTUndefined, width);
+ "trying to create a bvconst using unsigned long long of width: ",
+ ASTUndefined, width);
CBV bv = CONSTANTBV::BitVector_Create(width, true);
unsigned long c_val = (~((unsigned long) 0)) & bvconst;
ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width)
{
- if (bit_width <= 0)
- FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, bit_width);
+ if (bit_width <= 0)
+ FatalError("CreateBVConst: trying to create a bvconst of width: ", ASTUndefined, bit_width);
if (!(2 == base || 10 == base || 16 == base))
// Create and return an ASTNode for a term
ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTVec &children)
+ unsigned int width,
+ const ASTVec &children)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:",
- ASTUndefined, kind);
+ ASTUndefined, kind);
ASTNode n = CreateNode(kind, children);
n.SetValueWidth(width);
}
ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTVec &children)
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTVec &children)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
- ASTNode n = CreateNode(kind, child0, children);
- n.SetValueWidth(width);
- BVTypeCheck(n);
- return n;
+ ASTNode n = CreateNode(kind, child0, children);
+ n.SetValueWidth(width);
+ BVTypeCheck(n);
+ return n;
}
ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children)
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTVec &children)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
}
ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children)
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2,
+ const ASTVec &children)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
}
// //Create a new variable of ValueWidth 'n'
-// ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value)
-// {
-// std::string c("v");
-// char d[32];
-// sprintf(d, "%d", _symbol_count++);
-// std::string ccc(d);
-// c += "_writearray_" + ccc;
-
-// ASTNode CurrentSymbol = CreateSymbol(c.c_str());
-// CurrentSymbol.SetValueWidth(value);
-// CurrentSymbol.SetIndexWidth(index);
-// return CurrentSymbol;
-// } //end of NewArrayVar()
+ // ASTNode STPMgr::NewArrayVar(unsigned int index, unsigned int value)
+ // {
+ // std::string c("v");
+ // char d[32];
+ // sprintf(d, "%d", _symbol_count++);
+ // std::string ccc(d);
+ // c += "_writearray_" + ccc;
+
+ // ASTNode CurrentSymbol = CreateSymbol(c.c_str());
+ // CurrentSymbol.SetValueWidth(value);
+ // CurrentSymbol.SetIndexWidth(index);
+ // return CurrentSymbol;
+ // } //end of NewArrayVar()
//prints statistics for the ASTNode
void STPMgr::ASTNodeStats(const char * c, const ASTNode& a)
bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
{
if (READ == term.GetKind()
- && WRITE == term[0].GetKind()
- && !GetRemoveWritesFlag())
+ && WRITE == term[0].GetKind()
+ && !GetRemoveWritesFlag())
{
return false;
}
if (READ == term.GetKind()
- && WRITE == term[0].GetKind()
- && GetRemoveWritesFlag())
+ && WRITE == term[0].GetKind()
+ && GetRemoveWritesFlag())
{
return true;
}
ASTNode STPMgr::NewParameterized_BooleanVar(const ASTNode& var,
- const ASTNode& constant)
+ const ASTNode& constant)
{
ostringstream outVar;
ostringstream outNum;
// Typedef for unique Interior node table.
typedef HASHSET<
- ASTInterior *,
- ASTInterior::ASTInteriorHasher,
- ASTInterior::ASTInteriorEqual> ASTInteriorSet;
+ ASTInterior *,
+ ASTInterior::ASTInteriorHasher,
+ ASTInterior::ASTInteriorEqual> ASTInteriorSet;
// Typedef for unique Symbol node (leaf) table.
typedef HASHSET<
// nodes are not modified. Then it returns the hashed copy of the
// node, which is created if necessary.
ASTInterior *CreateInteriorNode(Kind kind,
- ASTInterior *new_node,
+ ASTInterior *new_node,
const ASTVec & back_children =
- _empty_ASTVec);
+ _empty_ASTVec);
// Create unique ASTInterior node.
ASTInterior *LookupOrCreateInterior(ASTInterior *n);
// Simplifying create functions
ASTNode CreateSimpForm(Kind kind,
- ASTVec &children);
+ ASTVec &children);
ASTNode CreateSimpForm(Kind kind,
- const ASTNode& child0);
+ const ASTNode& child0);
ASTNode CreateSimpForm(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1);
+ const ASTNode& child0,
+ const ASTNode& child1);
ASTNode CreateSimpForm(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2);
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2);
ASTNode CreateSimpNot (const ASTNode& form);
ASTNode CreateSimpXor(const ASTNode& form1,
- const ASTNode& form2);
+ const ASTNode& form2);
ASTNode CreateSimpXor(ASTVec &children);
ASTNode CreateSimpAndOr(bool isAnd,
- const ASTNode& form1,
- const ASTNode& form2);
+ const ASTNode& form1,
+ const ASTNode& form2);
ASTNode CreateSimpAndOr(bool IsAnd,
- ASTVec &children);
+ ASTVec &children);
ASTNode CreateSimpFormITE(const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2);
+ const ASTNode& child1,
+ const ASTNode& child2);
/****************************************************************
* Create Symbol and BVConst functions *
// Create and return an interior ASTNode
ASTNode CreateNode(Kind kind,
- const ASTVec &children = _empty_ASTVec);
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTVec &children = _empty_ASTVec);
+ const ASTNode& child0,
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children = _empty_ASTVec);
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children = _empty_ASTVec);
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec);
/****************************************************************
* Create Term functions *
// Create and return an ASTNode for a term
ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTVec &children = _empty_ASTVec);
+ unsigned int width,
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTVec &children = _empty_ASTVec);
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children = _empty_ASTVec);
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTVec &children = _empty_ASTVec);
ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children = _empty_ASTVec);
+ unsigned int width,
+ const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec);
/****************************************************************
bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
ASTNode NewParameterized_BooleanVar(const ASTNode& var,
- const ASTNode& constant);
+ const ASTNode& constant);
void TermsAlreadySeenMap_Clear(void)
{
namespace BEEV
{
class AbsRefine_CounterExample
- {
- private:
+ {
+ private:
- // Handy defs
- ASTNode ASTTrue, ASTFalse, ASTUndefined;
+ // Handy defs
+ ASTNode ASTTrue, ASTFalse, ASTUndefined;
- // Data structure that holds the counterexample
- ASTNodeMap CounterExampleMap;
+ // Data structure that holds the counterexample
+ ASTNodeMap CounterExampleMap;
- // This map for building/printing counterexamples. MINISAT
- // returns values for each bit (a BVGETBIT Node), and this maps
- // allows us to assemble the bits into bitvectors.
- typedef HASHMAP<
- ASTNode,
- HASHMAP<unsigned int, bool> *,
- ASTNode::ASTNodeHasher,
- ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
-
- ASTtoBitvectorMap _ASTNode_to_BitvectorMap;
-
- // This memo map is used by the ComputeFormulaUsingModel()
- ASTNodeMap ComputeFormulaMap;
+ // This map for building/printing counterexamples. MINISAT
+ // returns values for each bit (a BVGETBIT Node), and this maps
+ // allows us to assemble the bits into bitvectors.
+ typedef HASHMAP<
+ ASTNode,
+ HASHMAP<unsigned int, bool> *,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
+
+ ASTtoBitvectorMap _ASTNode_to_BitvectorMap;
+
+ // This memo map is used by the ComputeFormulaUsingModel()
+ ASTNodeMap ComputeFormulaMap;
- // Ptr to STPManager
- STPMgr * bm;
+ // Ptr to STPManager
+ STPMgr * bm;
- // Ptr to Simplifier
- Simplifier * simp;
+ // Ptr to Simplifier
+ Simplifier * simp;
- // Ptr to ArrayTransformer
- ArrayTransformer * ArrayTransform;
+ // Ptr to ArrayTransformer
+ ArrayTransformer * ArrayTransform;
- // Ptr to ToSAT
- ToSAT * tosat;
-
- // Checks if the counterexample is good. In order for the
- // counterexample to be ok, every assert must evaluate to true
- // w.r.t couner_example, and the query must evaluate to
- // false. Otherwise we know that the counter_example is bogus.
- void CheckCounterExample(bool t);
-
- // Accepts a term and turns it into a constant-term w.r.t
- // counter_example
- ASTNode TermToConstTermUsingModel(const ASTNode& term,
- bool ArrayReadFlag = true);
-
- ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term,
- bool ArrayReadFlag = true);
-
- void CopySolverMap_To_CounterExample(void);
-
- //Converts a vector of bools to a BVConst
- ASTNode BoolVectoBVConst(HASHMAP<unsigned, bool> * w, unsigned int l);
-
- public:
-
- // Constructor
- AbsRefine_CounterExample(STPMgr * b,
- Simplifier * s,
- ArrayTransformer * at,
- ToSAT * t) :
- bm(b), simp(s), ArrayTransform(at), tosat(t)
- {
- ASTTrue = bm->CreateNode(TRUE);
- ASTFalse = bm->CreateNode(FALSE);
- ASTUndefined = bm->CreateNode(UNDEFINED);
- }
-
- void ClearCounterExampleMap(void)
- {
- CounterExampleMap.clear();
- }
-
- void ClearComputeFormulaMap(void)
- {
- ComputeFormulaMap.clear();
- }
-
- //Converts MINISAT counterexample into an AST memotable (i.e. the
- //function populates the datastructure CounterExampleMap)
- void ConstructCounterExample(MINISAT::Solver& S);
+ // Ptr to ToSAT
+ ToSAT * tosat;
+
+ // Checks if the counterexample is good. In order for the
+ // counterexample to be ok, every assert must evaluate to true
+ // w.r.t couner_example, and the query must evaluate to
+ // false. Otherwise we know that the counter_example is bogus.
+ void CheckCounterExample(bool t);
+
+ // Accepts a term and turns it into a constant-term w.r.t
+ // counter_example
+ ASTNode TermToConstTermUsingModel(const ASTNode& term,
+ bool ArrayReadFlag = true);
+
+ ASTNode Expand_ReadOverWrite_UsingModel(const ASTNode& term,
+ bool ArrayReadFlag = true);
+
+ void CopySolverMap_To_CounterExample(void);
+
+ //Converts a vector of bools to a BVConst
+ ASTNode BoolVectoBVConst(HASHMAP<unsigned, bool> * w, unsigned int l);
+
+ public:
+
+ // Constructor
+ AbsRefine_CounterExample(STPMgr * b,
+ Simplifier * s,
+ ArrayTransformer * at,
+ ToSAT * t) :
+ bm(b), simp(s), ArrayTransform(at), tosat(t)
+ {
+ ASTTrue = bm->CreateNode(TRUE);
+ ASTFalse = bm->CreateNode(FALSE);
+ ASTUndefined = bm->CreateNode(UNDEFINED);
+ }
+
+ void ClearCounterExampleMap(void)
+ {
+ CounterExampleMap.clear();
+ }
+
+ void ClearComputeFormulaMap(void)
+ {
+ ComputeFormulaMap.clear();
+ }
+
+ //Converts MINISAT counterexample into an AST memotable (i.e. the
+ //function populates the datastructure CounterExampleMap)
+ void ConstructCounterExample(MINISAT::Solver& S);
- //Prints the counterexample to stdout
- void PrintCounterExample(bool t, std::ostream& os = cout);
+ //Prints the counterexample to stdout
+ void PrintCounterExample(bool t, std::ostream& os = cout);
- //Prints the counterexample to stdout
- void PrintCounterExample_InOrder(bool t);
+ //Prints the counterexample to stdout
+ void PrintCounterExample_InOrder(bool t);
- //queries the counterexample, and returns the value corresponding
- //to e
- ASTNode GetCounterExample(bool t, const ASTNode& e);
+ //queries the counterexample, and returns the value corresponding
+ //to e
+ ASTNode GetCounterExample(bool t, const ASTNode& e);
- int CounterExampleSize(void) const
- {
- return CounterExampleMap.size();
- }
-
- //FIXME: This is bloody dangerous function. Hack attack to take
- //care of requests from users who want to store complete
- //counter-examples in their own data structures.
- ASTNodeMap GetCompleteCounterExample()
- {
- return CounterExampleMap;
- }
+ int CounterExampleSize(void) const
+ {
+ return CounterExampleMap.size();
+ }
+
+ //FIXME: This is bloody dangerous function. Hack attack to take
+ //care of requests from users who want to store complete
+ //counter-examples in their own data structures.
+ ASTNodeMap GetCompleteCounterExample()
+ {
+ return CounterExampleMap;
+ }
- //Computes the truth value of a formula w.r.t counter_example
- ASTNode ComputeFormulaUsingModel(const ASTNode& form);
-
-
- // Prints MINISAT assigment one bit at a time, for debugging.
- void PrintSATModel(MINISAT::Solver& S);
-
- /****************************************************************
- * Array Refinement functions *
- ****************************************************************/
- SOLVER_RETURN_TYPE
- CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
- const ASTNode& modified_input,
- const ASTNode& original_input);
- //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
- ASTNode
- Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term,
- const ASTNode& array_newname);
+ //Computes the truth value of a formula w.r.t counter_example
+ ASTNode ComputeFormulaUsingModel(const ASTNode& form);
+
+
+ // Prints MINISAT assigment one bit at a time, for debugging.
+ void PrintSATModel(MINISAT::Solver& S);
+
+ /****************************************************************
+ * Array Refinement functions *
+ ****************************************************************/
+ SOLVER_RETURN_TYPE
+ CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
+ const ASTNode& modified_input,
+ const ASTNode& original_input);
+ //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
+ ASTNode
+ Create_ArrayWriteAxioms(const ASTNode& array_readoverwrite_term,
+ const ASTNode& array_newname);
- SOLVER_RETURN_TYPE
- SATBased_ArrayReadRefinement(MINISAT::Solver& newS,
- const ASTNode& modified_input,
- const ASTNode& original_input);
-
- SOLVER_RETURN_TYPE
- SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
- const ASTNode& orig_input);
+ SOLVER_RETURN_TYPE
+ SATBased_ArrayReadRefinement(MINISAT::Solver& newS,
+ const ASTNode& modified_input,
+ const ASTNode& original_input);
+
+ SOLVER_RETURN_TYPE
+ SATBased_ArrayWriteRefinement(MINISAT::Solver& newS,
+ const ASTNode& orig_input);
- // SOLVER_RETURN_TYPE
- // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS,
- // const ASTNode& orig_input);
+ // SOLVER_RETURN_TYPE
+ // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS,
+ // const ASTNode& orig_input);
- // ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver&
- // SatSolver, const ASTNode& original_input, const ASTNode&
- // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
- // absrefine_flag=false);
+ // ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver&
+ // SatSolver, const ASTNode& original_input, const ASTNode&
+ // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
+ // absrefine_flag=false);
- // ASTNode Check_FiniteLoop_UsingModel(const ASTNode&
- // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
- // CheckUsingModel_Or_Expand);
- //
- // ASTNode Expand_FiniteLoop_TopLevel(const ASTNode&
- // finiteloop); ASTNode Check_FiniteLoop_UsingModel(const
- // ASTNode& finiteloop);
-
- void ClearAllTables(void)
- {
- CounterExampleMap.clear();
- for (ASTtoBitvectorMap::iterator
- it = _ASTNode_to_BitvectorMap.begin(),
- itend = _ASTNode_to_BitvectorMap.end();
- it != itend; it++)
- {
- (it->second)->clear();
- delete (it->second);
- }
- _ASTNode_to_BitvectorMap.clear();
- ComputeFormulaMap.clear();
- } //End of ClearAllTables()
- };//End of Class CounterExample
+ // ASTNode Check_FiniteLoop_UsingModel(const ASTNode&
+ // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
+ // CheckUsingModel_Or_Expand);
+ //
+ // ASTNode Expand_FiniteLoop_TopLevel(const ASTNode&
+ // finiteloop); ASTNode Check_FiniteLoop_UsingModel(const
+ // ASTNode& finiteloop);
+
+ void ClearAllTables(void)
+ {
+ CounterExampleMap.clear();
+ for (ASTtoBitvectorMap::iterator
+ it = _ASTNode_to_BitvectorMap.begin(),
+ itend = _ASTNode_to_BitvectorMap.end();
+ it != itend; it++)
+ {
+ (it->second)->clear();
+ delete (it->second);
+ }
+ _ASTNode_to_BitvectorMap.clear();
+ ComputeFormulaMap.clear();
+ } //End of ClearAllTables()
+ };//End of Class CounterExample
class CompleteCounterExample
+ {
+ ASTNodeMap counterexample;
+ STPMgr * bv;
+ public:
+ CompleteCounterExample(ASTNodeMap a, STPMgr* beev) :
+ counterexample(a), bv(beev)
+ {
+ }
+ ASTNode GetCounterExample(ASTNode e)
{
- ASTNodeMap counterexample;
- STPMgr * bv;
- public:
- CompleteCounterExample(ASTNodeMap a, STPMgr* beev) :
- counterexample(a), bv(beev)
- {
- }
- ASTNode GetCounterExample(ASTNode e)
- {
- if (BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind())
- {
- FatalError("You must input a term or propositional variables\n", e);
- }
- if (counterexample.find(e) != counterexample.end())
- {
- return counterexample[e];
- }
- else
- {
- if (SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType())
- {
- return bv->CreateNode(BEEV::FALSE);
- }
-
- if (SYMBOL == e.GetKind())
- {
- ASTNode z = bv->CreateZeroConst(e.GetValueWidth());
- return z;
- }
-
- return e;
- }
- }
- };//end of Class CompleteCounterExample
+ if (BOOLEAN_TYPE == e.GetType() && SYMBOL != e.GetKind())
+ {
+ FatalError("You must input a term or propositional variables\n", e);
+ }
+ if (counterexample.find(e) != counterexample.end())
+ {
+ return counterexample[e];
+ }
+ else
+ {
+ if (SYMBOL == e.GetKind() && BOOLEAN_TYPE == e.GetType())
+ {
+ return bv->CreateNode(BEEV::FALSE);
+ }
+
+ if (SYMBOL == e.GetKind())
+ {
+ ASTNode z = bv->CreateZeroConst(e.GetValueWidth());
+ return z;
+ }
+
+ return e;
+ }
+ }
+ };//end of Class CompleteCounterExample
};//end of namespace
#endif
*****************************************************************/
SOLVER_RETURN_TYPE
AbsRefine_CounterExample::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
- const ASTNode& inputAlreadyInSAT,
- const ASTNode& original_input) {
+ 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");
//
//for each array, fetch its list of indices seen so far
for (ASTNodeToVecMap::const_iterator
- iset = ArrayTransform->ArrayName_ReadIndicesMap()->begin(),
+ iset = ArrayTransform->ArrayName_ReadIndicesMap()->begin(),
iset_end = ArrayTransform->ArrayName_ReadIndicesMap()->end();
- iset != iset_end; iset++)
+ iset != iset_end; iset++)
{
ASTVec listOfIndices = iset->second;
//loop over the list of indices for the array and create LA,
ASTNode ArrName = iset->first;
// if(SYMBOL != ArrName.GetKind())
// FatalError("SATBased_ArrayReadRefinement: "\
- // "arrname is not a SYMBOL",ArrName);
+ // "arrname is not a SYMBOL",ArrName);
ASTNode arr_read1 =
- bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
+ bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index);
//get the variable corresponding to the array_read1
//ASTNode arrsym1 = _arrayread_symbol[arr_read1];
ASTNode arrsym1 = ArrayTransform->ArrayRead_SymbolMap(arr_read1);
ASTNode eqOfIndices =
(exprless(the_index, compare_index)) ?
simp->CreateSimplifiedEQ(the_index, compare_index) :
- simp->CreateSimplifiedEQ(compare_index, the_index);
+ simp->CreateSimplifiedEQ(compare_index, the_index);
ASTNode arr_read2 =
- bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
+ bm->CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
//get the variable corresponding to the array_read2
//ASTNode arrsym2 = _arrayread_symbol[arr_read2];
- ASTNode arrsym2 = ArrayTransform->ArrayRead_SymbolMap(arr_read2);
+ ASTNode arrsym2 = ArrayTransform->ArrayRead_SymbolMap(arr_read2);
if (!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind()))
FatalError("TopLevelSAT: refinement loop:"
"term arrsym2 corresponding to READ must be a var", arrsym2);
if (FalseAxiomsVec.size() > oldFalseAxiomsSize)
{
res2 =
- CallSAT_ResultCheck(SatSolver,
- FalseAxioms,
- original_input);
+ CallSAT_ResultCheck(SatSolver,
+ FalseAxioms,
+ original_input);
oldFalseAxiomsSize = FalseAxiomsVec.size();
}
//printf("spot 02, res2 = %d\n", res2);
bm->CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
bm->ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);
return CallSAT_ResultCheck(SatSolver,
- RemainingAxioms,
- original_input);
+ RemainingAxioms,
+ original_input);
} //end of SATBased_ArrayReadRefinement
SOLVER_RETURN_TYPE
AbsRefine_CounterExample::
SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver,
- const ASTNode& original_input)
+ const ASTNode& original_input)
{
ASTNode writeAxiom;
ASTNodeMap::const_iterator it = simp->ReadOverWriteMap()->begin();
if (FalseAxioms.size() > oldFalseAxiomsSize)
{
res2 = CallSAT_ResultCheck(SatSolver,
- writeAxiom,
- original_input);
+ writeAxiom,
+ original_input);
oldFalseAxiomsSize = FalseAxioms.size();
}
if (SOLVER_UNDECIDED != res2)
bm->CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
bm->ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
res2 = CallSAT_ResultCheck(SatSolver,
- writeAxiom,
- original_input);
+ writeAxiom,
+ original_input);
if (SOLVER_UNDECIDED != res2)
{
return res2;
//bm->Creates Array Write Axioms
ASTNode AbsRefine_CounterExample::Create_ArrayWriteAxioms(const ASTNode& term,
- const ASTNode& newvar)
+ const ASTNode& newvar)
{
if (READ != term.GetKind() && WRITE != term[0].GetKind())
{
FatalError("Create_ArrayWriteAxioms: "\
- "Input must be a READ over a WRITE", term);
+ "Input must be a READ over a WRITE", term);
}
ASTNode lhs = newvar;
}//end of Create_ArrayWriteAxioms()
-// static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap,
-// const ASTNode& key, const ASTNode& value)
-// {
-// ASTNodeMap::iterator it = VarToConstMap->find(key);
-// if(it != VarToConstMap->end())
-// {
-// VarToConstMap->erase(it);
-// }
-
-// (*VarToConstMap)[key] = value;
-// return;
-// }
-
-
-// /******************************************************************
-// * FINITE FORLOOP ABSTRACTION REFINEMENT
-// *
-// * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops'
-// *
-// * Expand_FiniteLoop(finiteloop);
-// *
-// * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a
-// * counterexample-guided refinement fashion
-// *
-// * Once all the finiteloops have been expanded, we need to go back
-// * and recheck that every discarded constraint is true with the
-// * final model. A flag 'done' is set to false if atleast one
-// * constraint is false during model-check, and is set to true if all
-// * constraints are true during model-check.
-// *
-// * if the 'done' flag is true, then we terminate this refinement
-// * loop.
-// *****************************************************************/
-// SOLVER_RETURN_TYPE
-// AbsRefine_CounterExample::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver,
-// const ASTNode& original_input)
-// {
-// //cout << "The number of abs-refinement limit is " << num_absrefine << endl;
-// for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++)
-// {
-// ASTVec Allretvec0;
-// Allretvec0.push_back(ASTTrue);
-// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
-// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
-// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-// {
-// ASTVec retvec;
-// ASTNodeMap ParamToCurrentValMap;
-// retvec = SATBased_FiniteLoop_Refinement(SatSolver,
-// original_input,
-// *i,
-// &ParamToCurrentValMap,
-// true); //absrefine flag
-
-// for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++)
-// {
-// Allretvec0.push_back(*j);
-// }
-// //Allretvec0.(Allretvec0.end(),retvec.begin(),retvec.end());
-// } //End of For
-
-// ASTNode retformula =
-// (Allretvec0.size() == 1) ?
-// Allretvec0[0] : bm->CreateNode(AND,Allretvec0);
-// retformula = TransformFormula_TopLevel(retformula);
-
-// //Add the return value of all loops to the SAT Solver
-// res =
-// CallSAT_ResultCheck(SatSolver, retformula, original_input);
-// if(SOLVER_UNDECIDED != res)
-// {
-// return res;
-// }
-// } //end of absrefine count
+ // static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap,
+ // const ASTNode& key, const ASTNode& value)
+ // {
+ // ASTNodeMap::iterator it = VarToConstMap->find(key);
+ // if(it != VarToConstMap->end())
+ // {
+ // VarToConstMap->erase(it);
+ // }
+
+ // (*VarToConstMap)[key] = value;
+ // return;
+ // }
+
+
+ // /******************************************************************
+ // * FINITE FORLOOP ABSTRACTION REFINEMENT
+ // *
+ // * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops'
+ // *
+ // * Expand_FiniteLoop(finiteloop);
+ // *
+ // * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a
+ // * counterexample-guided refinement fashion
+ // *
+ // * Once all the finiteloops have been expanded, we need to go back
+ // * and recheck that every discarded constraint is true with the
+ // * final model. A flag 'done' is set to false if atleast one
+ // * constraint is false during model-check, and is set to true if all
+ // * constraints are true during model-check.
+ // *
+ // * if the 'done' flag is true, then we terminate this refinement
+ // * loop.
+ // *****************************************************************/
+ // SOLVER_RETURN_TYPE
+ // AbsRefine_CounterExample::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver,
+ // const ASTNode& original_input)
+ // {
+ // //cout << "The number of abs-refinement limit is " << num_absrefine << endl;
+ // for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++)
+ // {
+ // ASTVec Allretvec0;
+ // Allretvec0.push_back(ASTTrue);
+ // SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
+ // for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
+ // iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
+ // {
+ // ASTVec retvec;
+ // ASTNodeMap ParamToCurrentValMap;
+ // retvec = SATBased_FiniteLoop_Refinement(SatSolver,
+ // original_input,
+ // *i,
+ // &ParamToCurrentValMap,
+ // true); //absrefine flag
+
+ // for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++)
+ // {
+ // Allretvec0.push_back(*j);
+ // }
+ // //Allretvec0.(Allretvec0.end(),retvec.begin(),retvec.end());
+ // } //End of For
+
+ // ASTNode retformula =
+ // (Allretvec0.size() == 1) ?
+ // Allretvec0[0] : bm->CreateNode(AND,Allretvec0);
+ // retformula = TransformFormula_TopLevel(retformula);
+
+ // //Add the return value of all loops to the SAT Solver
+ // res =
+ // CallSAT_ResultCheck(SatSolver, retformula, original_input);
+ // if(SOLVER_UNDECIDED != res)
+ // {
+ // return res;
+ // }
+ // } //end of absrefine count
-// ASTVec Allretvec1;
-// Allretvec1.push_back(ASTTrue);
-// SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
-// for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
-// iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-// {
-// //cout << "The abs-refine didn't finish the job. Add the remaining formulas\n";
-// ASTNodeMap ParamToCurrentValMap;
-// ASTVec retvec;
-// retvec = SATBased_FiniteLoop_Refinement(SatSolver,
-// original_input,
-// *i,
-// &ParamToCurrentValMap,
-// false); //absrefine flag
-// for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++)
-// {
-// Allretvec1.push_back(*j);
-// }
-// } //End of For
-
-// ASTNode retformula =
-// (Allretvec1.size() == 1) ?
-// Allretvec1[0] : bm->CreateNode(AND,Allretvec1);
-// retformula = TransformFormula_TopLevel(retformula);
-// //Add the return value of all loops to the SAT Solver
-// res = CallSAT_ResultCheck(SatSolver, retformula, original_input);
-// return res;
-// } //end of SATBased_AllFiniteLoops_Refinement()
+ // ASTVec Allretvec1;
+ // Allretvec1.push_back(ASTTrue);
+ // SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;
+ // for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
+ // iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
+ // {
+ // //cout << "The abs-refine didn't finish the job. Add the remaining formulas\n";
+ // ASTNodeMap ParamToCurrentValMap;
+ // ASTVec retvec;
+ // retvec = SATBased_FiniteLoop_Refinement(SatSolver,
+ // original_input,
+ // *i,
+ // &ParamToCurrentValMap,
+ // false); //absrefine flag
+ // for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++)
+ // {
+ // Allretvec1.push_back(*j);
+ // }
+ // } //End of For
+
+ // ASTNode retformula =
+ // (Allretvec1.size() == 1) ?
+ // Allretvec1[0] : bm->CreateNode(AND,Allretvec1);
+ // retformula = TransformFormula_TopLevel(retformula);
+ // //Add the return value of all loops to the SAT Solver
+ // res = CallSAT_ResultCheck(SatSolver, retformula, original_input);
+ // return res;
+ // } //end of SATBased_AllFiniteLoops_Refinement()
-// /*****************************************************************
-// * SATBased_FiniteLoop_Refinement
-// *
-// * 'finiteloop' is the finite loop to be expanded
-// * Every finiteloop has three parts:
-// * 0) Parameter Name
-// * 1) Parameter initialization
-// * 2) Parameter limit value
-// * 3) Increment formula
-// * 4) Formula Body
-// *
-// * ParamToCurrentValMap contains a map from parameters to their
-// * current values in the recursion
-// *
-// * Nested FORs are allowed, but only the innermost loop can have a
-// * formula in it
-// *****************************************************************/
-// //SATBased_FiniteLoop_Refinement
-// //
-// //Expand the finite loop, check against model, and add false
-// //formulas to the SAT solver
-// ASTVec
-// AbsRefine_CounterExample::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver,
-// const ASTNode& original_input,
-// const ASTNode& finiteloop,
-// ASTNodeMap* ParamToCurrentValMap,
-// bool absrefine_flag)
-// {
-// //BVTypeCheck should have already checked the sanity of the input
-// //FOR-formula
-// ASTNode parameter = finiteloop[0];
-// int paramInit = GetUnsignedConst(finiteloop[1]);
-// int paramLimit = GetUnsignedConst(finiteloop[2]);
-// int paramIncrement = GetUnsignedConst(finiteloop[3]);
-// ASTNode exceptFormula = finiteloop[4];
-// ASTNode formulabody = finiteloop[5];
-// int paramCurrentValue = paramInit;
-// int width = finiteloop[1].GetValueWidth();
-
-// //Update ParamToCurrentValMap with parameter and its current
-// //value. Here paramCurrentValue is the initial value
-// ASTNode value =
-// bm->CreateBVConst(width,paramCurrentValue);
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+ // /*****************************************************************
+ // * SATBased_FiniteLoop_Refinement
+ // *
+ // * 'finiteloop' is the finite loop to be expanded
+ // * Every finiteloop has three parts:
+ // * 0) Parameter Name
+ // * 1) Parameter initialization
+ // * 2) Parameter limit value
+ // * 3) Increment formula
+ // * 4) Formula Body
+ // *
+ // * ParamToCurrentValMap contains a map from parameters to their
+ // * current values in the recursion
+ // *
+ // * Nested FORs are allowed, but only the innermost loop can have a
+ // * formula in it
+ // *****************************************************************/
+ // //SATBased_FiniteLoop_Refinement
+ // //
+ // //Expand the finite loop, check against model, and add false
+ // //formulas to the SAT solver
+ // ASTVec
+ // AbsRefine_CounterExample::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver,
+ // const ASTNode& original_input,
+ // const ASTNode& finiteloop,
+ // ASTNodeMap* ParamToCurrentValMap,
+ // bool absrefine_flag)
+ // {
+ // //BVTypeCheck should have already checked the sanity of the input
+ // //FOR-formula
+ // ASTNode parameter = finiteloop[0];
+ // int paramInit = GetUnsignedConst(finiteloop[1]);
+ // int paramLimit = GetUnsignedConst(finiteloop[2]);
+ // int paramIncrement = GetUnsignedConst(finiteloop[3]);
+ // ASTNode exceptFormula = finiteloop[4];
+ // ASTNode formulabody = finiteloop[5];
+ // int paramCurrentValue = paramInit;
+ // int width = finiteloop[1].GetValueWidth();
+
+ // //Update ParamToCurrentValMap with parameter and its current
+ // //value. Here paramCurrentValue is the initial value
+ // ASTNode value =
+ // bm->CreateBVConst(width,paramCurrentValue);
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-// //Go recursively thru' all the FOR-constructs.
-// if(FOR == formulabody.GetKind())
-// {
-// ASTVec retvec;
-// ASTVec retvec_innerfor;
-// retvec.push_back(ASTTrue);
-// while(paramCurrentValue < paramLimit)
-// {
-// retvec_innerfor =
-// SATBased_FiniteLoop_Refinement(SatSolver,
-// original_input,
-// formulabody,
-// ParamToCurrentValMap,
-// absrefine_flag);
-
-// for(ASTVec::iterator i=retvec_innerfor.begin(),
-// iend=retvec_innerfor.end();i!=iend;i++)
-// {
-// retvec.push_back(*i);
-// }
-
-// //Update ParamToCurrentValMap with parameter and its
-// //current value.
-// paramCurrentValue = paramCurrentValue + paramIncrement;
-// value = bm->CreateTerm(BVPLUS,
-// width,
-// (*ParamToCurrentValMap)[parameter],
-// bm->CreateOneConst(width));
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-// } //end of While
-
-// return retvec;
-// } //end of recursion FORs
-
-// //Expand the leaf level FOR-construct completely
-// //increment of paramCurrentValue done inside loop
-// int ThisForLoopAllTrue = 0;
-// ASTVec ForloopVec;
-// ForloopVec.push_back(ASTTrue);
-// for(;paramCurrentValue < paramLimit;)
-// {
-// ASTNode currentFormula;
-// ASTNode currentExceptFormula = exceptFormula;
-// currentExceptFormula =
-// SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
-// if(ASTTrue == currentExceptFormula)
-// {
-// currentFormula = ASTTrue;
-// }
-// else
-// {
-// 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(absrefine_flag
-// &&
-// ASTFalse == ComputeFormulaUsingModel(currentFormula)
-// )
-// {
-// ForloopVec.push_back(currentFormula);
-// }
-// else
-// {
-// if(ASTTrue != currentFormula)
-// {
-// ForloopVec.push_back(currentFormula);
-// }
-// if(ASTFalse == currentFormula)
-// {
-// ForloopVec.push_back(ASTFalse);
-// return ForloopVec;
-// }
-// }
+ // //Go recursively thru' all the FOR-constructs.
+ // if(FOR == formulabody.GetKind())
+ // {
+ // ASTVec retvec;
+ // ASTVec retvec_innerfor;
+ // retvec.push_back(ASTTrue);
+ // while(paramCurrentValue < paramLimit)
+ // {
+ // retvec_innerfor =
+ // SATBased_FiniteLoop_Refinement(SatSolver,
+ // original_input,
+ // formulabody,
+ // ParamToCurrentValMap,
+ // absrefine_flag);
+
+ // for(ASTVec::iterator i=retvec_innerfor.begin(),
+ // iend=retvec_innerfor.end();i!=iend;i++)
+ // {
+ // retvec.push_back(*i);
+ // }
+
+ // //Update ParamToCurrentValMap with parameter and its
+ // //current value.
+ // paramCurrentValue = paramCurrentValue + paramIncrement;
+ // value = bm->CreateTerm(BVPLUS,
+ // width,
+ // (*ParamToCurrentValMap)[parameter],
+ // bm->CreateOneConst(width));
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+ // } //end of While
+
+ // return retvec;
+ // } //end of recursion FORs
+
+ // //Expand the leaf level FOR-construct completely
+ // //increment of paramCurrentValue done inside loop
+ // int ThisForLoopAllTrue = 0;
+ // ASTVec ForloopVec;
+ // ForloopVec.push_back(ASTTrue);
+ // for(;paramCurrentValue < paramLimit;)
+ // {
+ // ASTNode currentFormula;
+ // ASTNode currentExceptFormula = exceptFormula;
+ // currentExceptFormula =
+ // SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
+ // if(ASTTrue == currentExceptFormula)
+ // {
+ // currentFormula = ASTTrue;
+ // }
+ // else
+ // {
+ // 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(absrefine_flag
+ // &&
+ // ASTFalse == ComputeFormulaUsingModel(currentFormula)
+ // )
+ // {
+ // ForloopVec.push_back(currentFormula);
+ // }
+ // else
+ // {
+ // if(ASTTrue != currentFormula)
+ // {
+ // ForloopVec.push_back(currentFormula);
+ // }
+ // if(ASTFalse == currentFormula)
+ // {
+ // ForloopVec.push_back(ASTFalse);
+ // return ForloopVec;
+ // }
+ // }
-// //Update ParamToCurrentValMap with parameter and its current
-// //value.
-// paramCurrentValue = paramCurrentValue + paramIncrement;
-// value = bm->CreateTerm(BVPLUS,
-// width,
-// (*ParamToCurrentValMap)[parameter],
-// bm->CreateOneConst(width));
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-// } //end of expanding the FOR loop
+ // //Update ParamToCurrentValMap with parameter and its current
+ // //value.
+ // paramCurrentValue = paramCurrentValue + paramIncrement;
+ // value = bm->CreateTerm(BVPLUS,
+ // width,
+ // (*ParamToCurrentValMap)[parameter],
+ // bm->CreateOneConst(width));
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+ // } //end of expanding the FOR loop
-// return ForloopVec;
-// } //end of the SATBased_FiniteLoop_Refinement()
-
-// //SATBased_FiniteLoop_Refinement_UsingModel(). Expand the finite
-// //loop, check against model
-// ASTNode
-// AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
-// ASTNodeMap* ParamToCurrentValMap,
-// bool checkusingmodel_flag = true)
-// {
-// /*
-// * 'finiteloop' is the finite loop to be expanded
-// * Every finiteloop has three parts:
-// * 0) Parameter Name
-// * 1) Parameter initialization
-// * 2) Parameter limit value
-// * 3) Increment formula
-// * 4) Formula Body
-// *
-// * ParamToCurrentValMap contains a map from parameters to their
-// * current values in the recursion
-// *
-// * Nested FORs are allowed, but only the innermost loop can have a
-// * formula in it
-// */
-
-// //BVTypeCheck should have already checked the sanity of the input
-// //FOR-formula
-// ASTNode parameter = finiteloop[0];
-// int paramInit = GetUnsignedConst(finiteloop[1]);
-// int paramLimit = GetUnsignedConst(finiteloop[2]);
-// int paramIncrement = GetUnsignedConst(finiteloop[3]);
-// ASTNode exceptFormula = finiteloop[4];
-// ASTNode formulabody = finiteloop[5];
-// int paramCurrentValue = paramInit;
-// int width = finiteloop[1].GetValueWidth();
-
-// //Update ParamToCurrentValMap with parameter and its current
-// //value. Here paramCurrentValue is the initial value
-// ASTNode value =
-// bm->CreateBVConst(width,paramCurrentValue);
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-
-// ASTNode ret = ASTTrue;
-// ASTVec returnVec;
-// //Go recursively thru' all the FOR-constructs.
-// if(FOR == formulabody.GetKind())
-// {
-// while(paramCurrentValue < paramLimit)
-// {
-// 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.
-// paramCurrentValue = paramCurrentValue + paramIncrement;
-// value = bm->CreateTerm(BVPLUS,
-// width,
-// (*ParamToCurrentValMap)[parameter],
-// bm->CreateOneConst(width));
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-// } //end of While
-
-// ASTNode retFormula =
-// (returnVec.size() > 1) ?
-// bm->CreateNode(AND, returnVec) :
-// (returnVec.size() == 1) ?
-// returnVec[0] :
-// ASTTrue;
-// return retFormula;
-// }
-
-// ASTVec forloopFormulaVector;
-// //Expand the leaf level FOR-construct completely
-// //incrementing of paramCurrentValue is done inside loop
-// for(;paramCurrentValue < paramLimit;)
-// {
-// ASTNode currentFormula;
-
-// ASTNode currentExceptFormula = exceptFormula;
-// currentExceptFormula =
-// SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
-// if(ASTTrue == currentExceptFormula)
-// {
-// currentFormula = ASTTrue;
-// //continue;
-// }
-// else
-// {
-// currentFormula =
-// SimplifyFormula(formulabody, false, ParamToCurrentValMap);
-// }
-
-// if(checkusingmodel_flag)
-// {
-// //Check the currentformula against the model, and return
-// //immediately
-// //cout << "Printing current Formula: " << currentFormula << "\n";
-// ASTNode computedForm = ComputeFormulaUsingModel(currentFormula);
-// //cout << "Printing computed Formula: " << computedForm << "\n";
-// if(ASTFalse == computedForm)
-// {
-// return ASTFalse;
-// }
-// }
-// else
-// {
-// if(ASTTrue != currentFormula)
-// {
-// forloopFormulaVector.push_back(currentFormula);
-// }
-// }
+ // return ForloopVec;
+ // } //end of the SATBased_FiniteLoop_Refinement()
+
+ // //SATBased_FiniteLoop_Refinement_UsingModel(). Expand the finite
+ // //loop, check against model
+ // ASTNode
+ // AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
+ // ASTNodeMap* ParamToCurrentValMap,
+ // bool checkusingmodel_flag = true)
+ // {
+ // /*
+ // * 'finiteloop' is the finite loop to be expanded
+ // * Every finiteloop has three parts:
+ // * 0) Parameter Name
+ // * 1) Parameter initialization
+ // * 2) Parameter limit value
+ // * 3) Increment formula
+ // * 4) Formula Body
+ // *
+ // * ParamToCurrentValMap contains a map from parameters to their
+ // * current values in the recursion
+ // *
+ // * Nested FORs are allowed, but only the innermost loop can have a
+ // * formula in it
+ // */
+
+ // //BVTypeCheck should have already checked the sanity of the input
+ // //FOR-formula
+ // ASTNode parameter = finiteloop[0];
+ // int paramInit = GetUnsignedConst(finiteloop[1]);
+ // int paramLimit = GetUnsignedConst(finiteloop[2]);
+ // int paramIncrement = GetUnsignedConst(finiteloop[3]);
+ // ASTNode exceptFormula = finiteloop[4];
+ // ASTNode formulabody = finiteloop[5];
+ // int paramCurrentValue = paramInit;
+ // int width = finiteloop[1].GetValueWidth();
+
+ // //Update ParamToCurrentValMap with parameter and its current
+ // //value. Here paramCurrentValue is the initial value
+ // ASTNode value =
+ // bm->CreateBVConst(width,paramCurrentValue);
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+
+ // ASTNode ret = ASTTrue;
+ // ASTVec returnVec;
+ // //Go recursively thru' all the FOR-constructs.
+ // if(FOR == formulabody.GetKind())
+ // {
+ // while(paramCurrentValue < paramLimit)
+ // {
+ // 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.
+ // paramCurrentValue = paramCurrentValue + paramIncrement;
+ // value = bm->CreateTerm(BVPLUS,
+ // width,
+ // (*ParamToCurrentValMap)[parameter],
+ // bm->CreateOneConst(width));
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+ // } //end of While
+
+ // ASTNode retFormula =
+ // (returnVec.size() > 1) ?
+ // bm->CreateNode(AND, returnVec) :
+ // (returnVec.size() == 1) ?
+ // returnVec[0] :
+ // ASTTrue;
+ // return retFormula;
+ // }
+
+ // ASTVec forloopFormulaVector;
+ // //Expand the leaf level FOR-construct completely
+ // //incrementing of paramCurrentValue is done inside loop
+ // for(;paramCurrentValue < paramLimit;)
+ // {
+ // ASTNode currentFormula;
+
+ // ASTNode currentExceptFormula = exceptFormula;
+ // currentExceptFormula =
+ // SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
+ // if(ASTTrue == currentExceptFormula)
+ // {
+ // currentFormula = ASTTrue;
+ // //continue;
+ // }
+ // else
+ // {
+ // currentFormula =
+ // SimplifyFormula(formulabody, false, ParamToCurrentValMap);
+ // }
+
+ // if(checkusingmodel_flag)
+ // {
+ // //Check the currentformula against the model, and return
+ // //immediately
+ // //cout << "Printing current Formula: " << currentFormula << "\n";
+ // ASTNode computedForm = ComputeFormulaUsingModel(currentFormula);
+ // //cout << "Printing computed Formula: " << computedForm << "\n";
+ // if(ASTFalse == computedForm)
+ // {
+ // return ASTFalse;
+ // }
+ // }
+ // else
+ // {
+ // if(ASTTrue != currentFormula)
+ // {
+ // forloopFormulaVector.push_back(currentFormula);
+ // }
+ // }
-// //Update ParamToCurrentValMap with parameter and its current
-// //value
-// paramCurrentValue = paramCurrentValue + paramIncrement;
-// value = bm->CreateTerm(BVPLUS,
-// width,
-// (*ParamToCurrentValMap)[parameter],
-// bm->CreateOneConst(width));
-// ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-// } //end of For
-
-// if(checkusingmodel_flag)
-// {
-// return ASTTrue;
-// }
-// else
-// {
-// ASTNode retFormula =
-// (forloopFormulaVector.size() > 1) ?
-// bm->CreateNode(AND, forloopFormulaVector) :
-// (forloopFormulaVector.size() == 1) ?
-// forloopFormulaVector[0] :
-// ASTTrue;
-// return retFormula;
-// }
-// } //end of the Check_FiniteLoop_UsingModel()
+ // //Update ParamToCurrentValMap with parameter and its current
+ // //value
+ // paramCurrentValue = paramCurrentValue + paramIncrement;
+ // value = bm->CreateTerm(BVPLUS,
+ // width,
+ // (*ParamToCurrentValMap)[parameter],
+ // bm->CreateOneConst(width));
+ // ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
+ // } //end of For
+
+ // if(checkusingmodel_flag)
+ // {
+ // return ASTTrue;
+ // }
+ // else
+ // {
+ // ASTNode retFormula =
+ // (forloopFormulaVector.size() > 1) ?
+ // bm->CreateNode(AND, forloopFormulaVector) :
+ // (forloopFormulaVector.size() == 1) ?
+ // forloopFormulaVector[0] :
+ // ASTTrue;
+ // return retFormula;
+ // }
+ // } //end of the Check_FiniteLoop_UsingModel()
-// //Expand_FiniteLoop_For_ModelCheck
-// ASTNode
-// AbsRefine_CounterExample::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop)
-// {
-// ASTNodeMap ParamToCurrentValMap;
-// return Check_FiniteLoop_UsingModel(finiteloop,
-// &ParamToCurrentValMap, false);
-// } //end of Expand_FiniteLoop_TopLevel()
-
-// ASTNode
-// AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop)
-// {
-// ASTNodeMap ParamToCurrentValMap;
-// return Check_FiniteLoop_UsingModel(finiteloop,
-// &ParamToCurrentValMap, true);
-// } //end of Check_FiniteLoop_UsingModel
+ // //Expand_FiniteLoop_For_ModelCheck
+ // ASTNode
+ // AbsRefine_CounterExample::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop)
+ // {
+ // ASTNodeMap ParamToCurrentValMap;
+ // return Check_FiniteLoop_UsingModel(finiteloop,
+ // &ParamToCurrentValMap, false);
+ // } //end of Expand_FiniteLoop_TopLevel()
+
+ // ASTNode
+ // AbsRefine_CounterExample::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop)
+ // {
+ // ASTNodeMap ParamToCurrentValMap;
+ // return Check_FiniteLoop_UsingModel(finiteloop,
+ // &ParamToCurrentValMap, true);
+ // } //end of Check_FiniteLoop_UsingModel
};// end of namespace BEEV
//'v' is the map from bit-index to bit-value
HASHMAP<unsigned, bool> * v;
if (_ASTNode_to_BitvectorMap.find(symbol) ==
- _ASTNode_to_BitvectorMap.end())
- {
- _ASTNode_to_BitvectorMap[symbol] =
- new HASHMAP<unsigned, bool> (symbolWidth);
- }
+ _ASTNode_to_BitvectorMap.end())
+ {
+ _ASTNode_to_BitvectorMap[symbol] =
+ new HASHMAP<unsigned, bool> (symbolWidth);
+ }
//v holds the map from bit-index to bit-value
v = _ASTNode_to_BitvectorMap[symbol];
//the the aggregate value of the bitvector, and populate the
//CounterExampleMap datastructure
for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(),
- itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++)
+ itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++)
{
ASTNode var = it->first;
//debugging
//cerr << var;
if (SYMBOL != var.GetKind())
- {
- FatalError("ConstructCounterExample:"\
- "error while constructing counterexample: not a variable: ", var);
- }
+ {
+ FatalError("ConstructCounterExample:"\
+ "error while constructing counterexample: not a variable: ", var);
+ }
//construct the bitvector value
HASHMAP<unsigned, bool> * w = it->second;
ASTNode value = BoolVectoBVConst(w, var.GetValueWidth());
//In this loop, we compute the value of each array read, the
//corresponding ITE against the counterexample generated above.
for (ASTNodeMap::const_iterator
- it = ArrayTransform->ArrayRead_IteMap()->begin(),
- itend = ArrayTransform->ArrayRead_IteMap()->end();
- it != itend; it++)
+ it = ArrayTransform->ArrayRead_IteMap()->begin(),
+ itend = ArrayTransform->ArrayRead_IteMap()->end();
+ it != itend; it++)
{
//the array read
ASTNode arrayread = it->first;
//counterexample
ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]);
ASTNode key = bm->CreateTerm(READ,
- arrayread.GetValueWidth(),
- arrayread[0], arrayread_index);
+ arrayread.GetValueWidth(),
+ arrayread[0], arrayread_index);
//Get the ITE corresponding to the array-read and convert it
//to a constant against the model
ASTNode writeVal = TermToConstTermUsingModel(write[2], false);
ASTNode cond =
- ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex, readIndex));
+ ComputeFormulaUsingModel(simp->CreateSimplifiedEQ(writeIndex, readIndex));
if (ASTTrue == cond)
{
//found the write-value. return it
}
}
else
- {
- CounterExampleMap[form] = ASTFalse;
- output = ASTFalse;
- }
+ {
+ CounterExampleMap[form] = ASTFalse;
+ output = ASTFalse;
+ }
break;
case EQ:
case BVLT:
//evaluate formula to false if bvdiv execption occurs while
//counterexample is being checked during refinement.
if (bm->bvdiv_exception_occured
- && bm->counterexample_checking_during_refinement)
+ && bm->counterexample_checking_during_refinement)
{
output = ASTFalse;
}
output = ComputeFormulaUsingModel(form[2]);
else
FatalError("ComputeFormulaUsingModel: ITE: "\
- "something is wrong with the formula: ", form);
+ "something is wrong with the formula: ", form);
break;
case PARAMBOOL:
- output = bm->NewParameterized_BooleanVar(form[0],form[1]);
- output = ComputeFormulaUsingModel(output);
- break;
+ output = bm->NewParameterized_BooleanVar(form[0],form[1]);
+ output = ComputeFormulaUsingModel(output);
+ break;
case FOR:
- //output = Check_FiniteLoop_UsingModel(form);
- output = ASTTrue;
- break;
+ //output = Check_FiniteLoop_UsingModel(form);
+ output = ASTTrue;
+ break;
default:
FatalError(" ComputeFormulaUsingModel: "\
- "the kind has not been implemented", ASTUndefined);
+ "the kind has not been implemented", ASTUndefined);
break;
}
if (ARRAY_TYPE == se.GetType())
{
FatalError("TermToConstTermUsingModel: "\
- "entry in counterexample is an arraytype. bogus:", se);
+ "entry in counterexample is an arraytype. bogus:", se);
}
//skip over introduced variables
if (f.GetKind() == SYMBOL &&
- (ArrayTransform->FoundIntroducedSymbolSet(f)))
- {
- continue;
- }
+ (ArrayTransform->FoundIntroducedSymbolSet(f)))
+ {
+ continue;
+ }
if (f.GetKind() == SYMBOL ||
- (f.GetKind() == READ &&
- f[0].GetKind() == SYMBOL &&
- f[1].GetKind() == BVCONST))
+ (f.GetKind() == READ &&
+ f[0].GetKind() == SYMBOL &&
+ f[1].GetKind() == BVCONST))
{
os << "ASSERT( ";
f.PL_Print(os,0);
- if(BOOLEAN_TYPE == f.GetType())
- {
- os << "<=>";
- }
- else
- {
- os << " = ";
- }
+ if(BOOLEAN_TYPE == f.GetType())
+ {
+ os << "<=>";
+ }
+ else
+ {
+ os << " = ";
+ }
if (BITVECTOR_TYPE == se.GetType())
{
TermToConstTermUsingModel(se, false).PL_Print(os, 0);
std::vector<int> out_int;
cout << "% ";
for (ASTVec::iterator it = bm->ListOfDeclaredVars.begin(),
- itend = bm->ListOfDeclaredVars.end(); it != itend; it++)
+ itend = bm->ListOfDeclaredVars.end(); it != itend; it++)
{
if (ARRAY_TYPE == it->GetType())
{
if (!simp->Return_SolverMap()->empty())
{
- CounterExampleMap.insert(simp->Return_SolverMap()->begin(),
- simp->Return_SolverMap()->end());
+ CounterExampleMap.insert(simp->Return_SolverMap()->begin(),
+ simp->Return_SolverMap()->end());
}
}
-SOLVER_RETURN_TYPE
+ SOLVER_RETURN_TYPE
AbsRefine_CounterExample::
CallSAT_ResultCheck(MINISAT::Solver& SatSolver,
- const ASTNode& modified_input,
- const ASTNode& original_input)
+ const ASTNode& modified_input,
+ const ASTNode& original_input)
{
bool sat = tosat->CallSAT(SatSolver,
- modified_input,
- original_input);
+ modified_input,
+ original_input);
if (!sat)
{
//PrintOutput(true);
BEEV::ParserBM = bm;
stpstar stp =
new BEEV::STP(bm, simp,
- bvsolver, arrayTransformer,
- tosat, Ctr_Example);
+ bvsolver, arrayTransformer,
+ tosat, Ctr_Example);
BEEV::GlobalSTP = stp;
decls = new BEEV::ASTVec();
//printf("%ull", max_n_bits);
if(v > max_n_bits) {
printf("CInterface: vc_bvConstExprFromInt: "\
- "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits);
+ "You are trying to construct a constant %llu >= %d,\n", v, max_n_bits);
BEEV::FatalError("FatalError");
}
node n = b->CreateBVConst(n_bits, v);
/* global macro definitions: */
/*****************************/
-#define BIT_VECTOR_ZERO_WORDS(target,count) \
- while (count-- > 0) *target++ = 0;
+#define BIT_VECTOR_ZERO_WORDS(target,count) \
+ while (count-- > 0) *target++ = 0;
-#define BIT_VECTOR_FILL_WORDS(target,fill,count) \
- while (count-- > 0) *target++ = fill;
+#define BIT_VECTOR_FILL_WORDS(target,fill,count) \
+ while (count-- > 0) *target++ = fill;
-#define BIT_VECTOR_FLIP_WORDS(target,flip,count) \
- while (count-- > 0) *target++ ^= flip;
+#define BIT_VECTOR_FLIP_WORDS(target,flip,count) \
+ while (count-- > 0) *target++ ^= flip;
-#define BIT_VECTOR_COPY_WORDS(target,source,count) \
- while (count-- > 0) *target++ = *source++;
+#define BIT_VECTOR_COPY_WORDS(target,source,count) \
+ while (count-- > 0) *target++ = *source++;
-#define BIT_VECTOR_BACK_WORDS(target,source,count) \
- { target += count; source += count; while (count-- > 0) *--target = *--source; }
+#define BIT_VECTOR_BACK_WORDS(target,source,count) \
+ { target += count; source += count; while (count-- > 0) *--target = *--source; }
-#define BIT_VECTOR_CLR_BIT(address,index) \
- *(address+(index>>LOGBITS)) &= ~ BITMASKTAB[index & MODMASK];
+#define BIT_VECTOR_CLR_BIT(address,index) \
+ *(address+(index>>LOGBITS)) &= ~ BITMASKTAB[index & MODMASK];
-#define BIT_VECTOR_SET_BIT(address,index) \
- *(address+(index>>LOGBITS)) |= BITMASKTAB[index & MODMASK];
+#define BIT_VECTOR_SET_BIT(address,index) \
+ *(address+(index>>LOGBITS)) |= BITMASKTAB[index & MODMASK];
-#define BIT_VECTOR_TST_BIT(address,index) \
- ((*(address+(index>>LOGBITS)) & BITMASKTAB[index & MODMASK]) != 0)
+#define BIT_VECTOR_TST_BIT(address,index) \
+ ((*(address+(index>>LOGBITS)) & BITMASKTAB[index & MODMASK]) != 0)
-#define BIT_VECTOR_FLP_BIT(address,index,mask) \
- (mask = BITMASKTAB[index & MODMASK]), \
+#define BIT_VECTOR_FLP_BIT(address,index,mask) \
+ (mask = BITMASKTAB[index & MODMASK]), \
(((*(addr+(index>>LOGBITS)) ^= mask) & mask) != 0)
-#define BIT_VECTOR_DIGITIZE(type,value,digit) \
- value = (type) ((digit = value) / 10); \
- digit -= value * 10; \
- digit += (type) '0';
+#define BIT_VECTOR_DIGITIZE(type,value,digit) \
+ value = (type) ((digit = value) / 10); \
+ digit -= value * 10; \
+ digit += (type) '0';
/*********************************************************/
/* private low-level functions (potentially dangerous!): */
unsigned int * source, unsigned int count) {
if (target != source) {
if (target < source) BIT_VECTOR_COPY_WORDS(target,source,count)
- else BIT_VECTOR_BACK_WORDS(target,source,count)
- }
+ else BIT_VECTOR_BACK_WORDS(target,source,count)
+ }
}
static void BIT_VECTOR_ins_words(unsigned int * addr,
break;
case (int) '1':
value |= BITMASKTAB[count];
- break;
+ break;
default:
ok = false;
break;
{
case (unsigned int) '0':
state = 2;
- break;
+ break;
case (unsigned int) '\0':
state = 0;
- break;
+ break;
default:
error = ErrCode_Pars;
break;
{
case (unsigned int) '-':
start = index;
- state = 3;
- break;
+ state = 3;
+ break;
case (unsigned int) ',':
BIT_VECTOR_SET_BIT(addr,index)
- state = 5;
- break;
+ state = 5;
+ break;
case (unsigned int) '\0':
BIT_VECTOR_SET_BIT(addr,index)
- state = 0;
- break;
+ state = 0;
+ break;
default:
error = ErrCode_Pars;
break;
BitVector_Interval_Fill(addr,start,index);
else if (start == index)
BIT_VECTOR_SET_BIT(addr,index)
- else error = ErrCode_Ordr;
- state = 4;
- break;
+ else error = ErrCode_Ordr;
+ state = 4;
+ break;
default:
error = ErrCode_Pars;
break;
{
case (unsigned int) ',':
state = 5;
- break;
+ break;
case (unsigned int) '\0':
state = 0;
- break;
+ break;
default:
error = ErrCode_Pars;
break;
{
case (unsigned int) '0':
state = 2;
- break;
+ break;
default:
error = ErrCode_Pars;
break;
if (index < bits_(addr))
{
if (bit) BIT_VECTOR_SET_BIT(addr,index)
- else BIT_VECTOR_CLR_BIT(addr,index)
- }
+ else BIT_VECTOR_CLR_BIT(addr,index)
+ }
}
void BitVector_LSB(unsigned int * addr, boolean bit)
BIT_VECTOR_TST_BIT(Z,indxZ) ) sum ^= 1;
}
if (sum) BIT_VECTOR_SET_BIT(X,indxX)
- else BIT_VECTOR_CLR_BIT(X,indxX)
- }
+ else BIT_VECTOR_CLR_BIT(X,indxX)
+ }
}
}
}
BIT_VECTOR_TST_BIT(Z,indxZ) ) sum |= 1;
}
if (sum) BIT_VECTOR_SET_BIT(X,indxX)
- else BIT_VECTOR_CLR_BIT(X,indxX)
- }
+ else BIT_VECTOR_CLR_BIT(X,indxX)
+ }
}
}
}
namespace MINISAT
{
- class Solver;
- typedef int Var;
+ class Solver;
+ typedef int Var;
}
namespace BEEV
ParserBM = bm;
GlobalSTP =
new STP(bm,
- simp,
- bvsolver,
- arrayTransformer,
- tosat,
- Ctr_Example);
+ simp,
+ bvsolver,
+ arrayTransformer,
+ tosat,
+ Ctr_Example);
//populate the help string
helpstring += "STP version: " + version + "\n\n";
construct_counterexample_flag = true;
check_counterexample_flag = true;
break;
- case 'e':
- expand_finitefor_flag = true;
- break;
- case 'f':
- num_absrefine_flag = true;
- num_absrefine = atoi(argv[++i]);
- break;
+ case 'e':
+ expand_finitefor_flag = true;
+ break;
+ case 'f':
+ num_absrefine_flag = true;
+ num_absrefine = atoi(argv[++i]);
+ break;
case 'h':
fprintf(stderr,usage,prog);
cout << helpstring;
stats_flag = true;
break;
case 't':
- quick_statistics_flag = true;
- break;
+ quick_statistics_flag = true;
+ break;
case 'u':
arraywrite_refinement_flag = false;
break;
case 'x':
xor_flatten_flag = true;
break;
- case 'y':
+ case 'y':
print_binary_flag = true;
break;
case 'z':
return -1;
break;
}
- } else {
- infile = argv[i];
- if (smtlib_parser_flag)
- {
- smtin = fopen(infile,"r");
- if(smtin == NULL)
- {
- fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
- FatalError("");
- }
- }
- else
- {
- cvcin = fopen(infile,"r");
- if(cvcin == NULL)
- {
- fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
- FatalError("");
- }
- }
- }
+ } else {
+ infile = argv[i];
+ if (smtlib_parser_flag)
+ {
+ smtin = fopen(infile,"r");
+ if(smtin == NULL)
+ {
+ fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+ FatalError("");
+ }
+ }
+ else
+ {
+ cvcin = fopen(infile,"r");
+ if(cvcin == NULL)
+ {
+ fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile);
+ FatalError("");
+ }
+ }
+ }
}
//want to print the output always from the commandline.
{
if(smtlib_parser_flag)
{
- // don't pass the query. It's not returned by the smtlib
- // parser.
- printer::SMTLIB_PrintBack(cout, asserts);
+ // don't pass the query. It's not returned by the smtlib
+ // parser.
+ printer::SMTLIB_PrintBack(cout, asserts);
}
else
{
{
//LET Management
class LETMgr
- {
- private:
+ {
+ private:
- // MAP: This map is from bound IDs that occur in LETs to
- // expression. The map is useful in checking replacing the IDs
- // with the corresponding expressions.
- ASTNodeMap *_letid_expr_map;
- ASTNode ASTUndefined;
+ // MAP: This map is from bound IDs that occur in LETs to
+ // expression. The map is useful in checking replacing the IDs
+ // with the corresponding expressions.
+ ASTNodeMap *_letid_expr_map;
+ ASTNode ASTUndefined;
- public:
+ public:
- LETMgr(ASTNode undefined)
- {
- _letid_expr_map = new ASTNodeMap();
- ASTUndefined = undefined;
- }
+ LETMgr(ASTNode undefined)
+ {
+ _letid_expr_map = new ASTNodeMap();
+ ASTUndefined = undefined;
+ }
- ASTNode ResolveID(const ASTNode& var);
+ ASTNode ResolveID(const ASTNode& var);
- //Functions that are used to manage LET expressions
- void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
+ //Functions that are used to manage LET expressions
+ void LetExprMgr(const ASTNode& var, const ASTNode& letExpr);
- //Delete Letid Map
- void CleanupLetIDMap(void);
+ //Delete Letid Map
+ void CleanupLetIDMap(void);
- //Allocate LetID map
- void InitializeLetIDMap(void);
+ //Allocate LetID map
+ void InitializeLetIDMap(void);
- //Substitute Let-vars with LetExprs
- ASTNode SubstituteLetExpr(ASTNode inExpr);
- };// End of class LETMgr
+ //Substitute Let-vars with LetExprs
+ ASTNode SubstituteLetExpr(ASTNode inExpr);
+ };// End of class LETMgr
}; //end of namespace
#endif
// }
// } //end of PrintClauseList()
- // //Variable Order Printer: A global function which converts a MINISAT
+ // //Variable Order Printer: A global function which converts a MINISAT
// //var into a ASTNODE var. It then prints this var along with
// //variable order dcisions taken by MINISAT.
// void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
- // int decision_level, int polarity)
+ // int decision_level, int polarity)
// {
// BEEV::ASTNode vv = BEEV::GlobalSTPMgr->_SATVar_to_AST[minisat_var];
// cout << spaces(decision_level);
BEEV::ASTNode a = *i;
switch(a.GetType()) {
case BEEV::BITVECTOR_TYPE:
- a.PL_Print(os);
- os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;
- break;
+ a.PL_Print(os);
+ os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl;
+ break;
case BEEV::ARRAY_TYPE:
- a.PL_Print(os);
- os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";
- os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;
- break;
+ a.PL_Print(os);
+ os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF ";
+ os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl;
+ break;
case BEEV::BOOLEAN_TYPE:
- a.PL_Print(os);
- os << " : BOOLEAN;" << endl;
- break;
+ a.PL_Print(os);
+ os << " : BOOLEAN;" << endl;
+ break;
default:
- BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a);
- break;
+ BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a);
+ break;
}
}
} //printVarDeclsToStream
void STPMgr::printAssertsToStream(ostream &os, int simplify_print) {
- ASTVec v = GetAsserts();
- for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
- //Begin_RemoveWrites = true;
- //ASTNode q = (simplify_print == 1) ? SimplifyFormula_TopLevel(*i,false) : *i;
- //q = (simplify_print == 1) ? SimplifyFormula_TopLevel(q,false) : q;
- ASTNode q = *i;
- //Begin_RemoveWrites = false;
- os << "ASSERT( ";
- q.PL_Print(os);
- os << ");" << endl;
+ ASTVec v = GetAsserts();
+ for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
+ //Begin_RemoveWrites = true;
+ //ASTNode q = (simplify_print == 1) ? SimplifyFormula_TopLevel(*i,false) : *i;
+ //q = (simplify_print == 1) ? SimplifyFormula_TopLevel(q,false) : q;
+ ASTNode q = *i;
+ //Begin_RemoveWrites = false;
+ os << "ASSERT( ";
+ q.PL_Print(os);
+ os << ");" << endl;
+ }
}
-}
void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query) {
(BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout);
os << endl << "ENDIF";
break;
case PARAMBOOL:
- PL_Print1(os, c[0], indentation, letize);
- os << "(";
- PL_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
+ PL_Print1(os, c[0], indentation, letize);
+ os << "(";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
case FOR:
- // 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 << ";";
- os << "EXCEPT ";
- PL_Print1(os, c[4], indentation, letize);
- os << "){ \n";
- PL_Print1(os, c[5], indentation, letize);
- os << "} \n";
- }
- break;
+ // 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 << ";";
+ os << "EXCEPT ";
+ PL_Print1(os, c[4], indentation, letize);
+ os << "){ \n";
+ PL_Print1(os, c[5], indentation, letize);
+ os << "} \n";
+ }
+ break;
case BVLT:
case BVLE:
case BVGT:
// todo : fix lets.
// : Finish mapping function names from internal names to SMTLIB names.
-// : build proper headers for PrintBack
+// : build proper headers for PrintBack
// : Letize code for each printer should be merged.
namespace printer
// Initial version intended to print the whole thing back.
void SMTLIB_PrintBack(ostream &os, const ASTNode& n) {
- // need to add fake headers into here.
- os << "(" << endl;
- os << "benchmark blah" << endl;
- printVarDeclsToStream(n.GetSTPMgr(),os);
- SMTLIB_Print(os, n, 0);
- os << ")" << endl;
+ // need to add fake headers into here.
+ os << "(" << endl;
+ os << "benchmark blah" << endl;
+ printVarDeclsToStream(n.GetSTPMgr(),os);
+ SMTLIB_Print(os, n, 0);
+ os << ")" << endl;
}
void printVarDeclsToStream( const STPMgr* mgr, ostream &os) {
- for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(),
- iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) {
- const BEEV::ASTNode& a = *i;
-
- // Should be a symbol.
- assert(a.GetKind()== SYMBOL);
-
- switch(a.GetType()) {
- case BEEV::BITVECTOR_TYPE:
-
- os << ":extrafuns (( ";
- a.nodeprint(os);
- os << " bv[" << a.GetValueWidth() << "]";
- os << " ))" << endl;
- break;
-
- case BEEV::ARRAY_TYPE:
- os << ":extrafuns (( ";
- a.nodeprint(os);
- os << " Array[" << a.GetIndexWidth();
- os << ":" << a.GetValueWidth() << "] ))" << endl;
- break;
- case BEEV::BOOLEAN_TYPE:
- os << ":extrapred (( ";
- a.nodeprint(os);
- os << "))" << endl;
- break;
- default:
- BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
- break;
- }
+ for(ASTVec::const_iterator i = mgr->ListOfDeclaredVars.begin(),
+ iend=mgr->ListOfDeclaredVars.end();i!=iend;i++) {
+ const BEEV::ASTNode& a = *i;
+
+ // Should be a symbol.
+ assert(a.GetKind()== SYMBOL);
+
+ switch(a.GetType()) {
+ case BEEV::BITVECTOR_TYPE:
+
+ os << ":extrafuns (( ";
+ a.nodeprint(os);
+ os << " bv[" << a.GetValueWidth() << "]";
+ os << " ))" << endl;
+ break;
+
+ case BEEV::ARRAY_TYPE:
+ os << ":extrafuns (( ";
+ a.nodeprint(os);
+ os << " Array[" << a.GetIndexWidth();
+ os << ":" << a.GetValueWidth() << "] ))" << endl;
+ break;
+ case BEEV::BOOLEAN_TYPE:
+ os << ":extrapred (( ";
+ a.nodeprint(os);
+ os << "))" << endl;
+ break;
+ default:
+ BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
+ break;
}
- } //printVarDeclsToStream
+ }
+ } //printVarDeclsToStream
void outputBitVec(const ASTNode n, ostream& os)
{
ostream& Dot_Print(ostream &os, const BEEV::ASTNode n);
ostream& SMTLIB_Print(ostream &os,
- const BEEV::ASTNode n, const int indentation = 0);
+ const BEEV::ASTNode n, const int indentation = 0);
ostream& C_Print(ostream &os,
- const BEEV::ASTNode n, const int indentation = 0);
+ const BEEV::ASTNode n, const int indentation = 0);
ostream& PL_Print(ostream &os,
- const BEEV::ASTNode& n, int indentation=0);
+ const BEEV::ASTNode& n, int indentation=0);
ostream& Lisp_Print(ostream &os,
- const BEEV::ASTNode& n, int indentation=0);
+ const BEEV::ASTNode& n, int indentation=0);
ostream& Lisp_Print_indent(ostream &os,
- const BEEV::ASTNode& n,int indentation=0);
+ const BEEV::ASTNode& n,int indentation=0);
void SMTLIB_PrintBack(ostream &os,
- const BEEV::ASTNode& n );
+ const BEEV::ASTNode& n );
}
{
ASTNode monom = *it;
if (SYMBOL == monom.GetKind()
- && Vars.count(monom) == 1
- && !VarSeenInTerm(monom, rhs)
- && !DoNotSolveThis(monom) && !chosen_symbol)
+ && Vars.count(monom) == 1
+ && !VarSeenInTerm(monom, rhs)
+ && !DoNotSolveThis(monom) && !chosen_symbol)
{
outmonom = monom;
chosen_symbol = true;
}
else if (BVUMINUS == monom.GetKind()
- && SYMBOL == monom[0].GetKind()
- && Vars.count(monom[0]) == 1
- && !DoNotSolveThis(monom[0])
+ && SYMBOL == monom[0].GetKind()
+ && Vars.count(monom[0]) == 1
+ && !DoNotSolveThis(monom[0])
&& !VarSeenInTerm(monom[0], rhs)
- && !chosen_symbol)
+ && !chosen_symbol)
{
//cerr << "Chosen Monom: " << monom << endl;
outmonom = monom;
{
ASTNode monom = *it;
ASTNode var =
- (BVMULT == monom.GetKind()) ?
- monom[1] :
- _bm->CreateNode(UNDEFINED);
+ (BVMULT == monom.GetKind()) ?
+ monom[1] :
+ _bm->CreateNode(UNDEFINED);
if (BVMULT == monom.GetKind()
- && BVCONST == monom[0].GetKind()
- && _simp->BVConstIsOdd(monom[0])
- && ((SYMBOL == var.GetKind()
- && Vars.count(var) == 1)
- || (BVEXTRACT == var.GetKind()
- && SYMBOL == var[0].GetKind()
- && BVCONST == var[1].GetKind()
- && zero == var[2]
- && !VarSeenInTerm(var[0], rhs)
- && !DoNotSolveThis(var[0])))
- && !DoNotSolveThis(var)
- && !VarSeenInTerm(var, rhs)
+ && BVCONST == monom[0].GetKind()
+ && _simp->BVConstIsOdd(monom[0])
+ && ((SYMBOL == var.GetKind()
+ && Vars.count(var) == 1)
+ || (BVEXTRACT == var.GetKind()
+ && SYMBOL == var[0].GetKind()
+ && BVCONST == var[1].GetKind()
+ && zero == var[2]
+ && !VarSeenInTerm(var[0], rhs)
+ && !DoNotSolveThis(var[0])))
+ && !DoNotSolveThis(var)
+ && !VarSeenInTerm(var, rhs)
&& !chosen_odd)
{
//monom[0] is odd.
//construct: rhs - (lhs without the chosen monom)
unsigned int len = lhs.GetValueWidth();
leftover_lhs =
- _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs));
+ _simp->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS, len, leftover_lhs));
ASTNode newrhs =
- _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
+ _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
lhs = chosen_monom;
rhs = newrhs;
} //end of if(BVPLUS ...)
ASTNode zero = _bm->CreateZeroConst(32);
if (!(SYMBOL == lhs[0].GetKind()
- && BVCONST == lhs[1].GetKind()
- && zero == lhs[2]
- && !VarSeenInTerm(lhs[0], rhs)
- && !DoNotSolveThis(lhs[0])))
+ && BVCONST == lhs[1].GetKind()
+ && zero == lhs[2]
+ && !VarSeenInTerm(lhs[0], rhs)
+ && !DoNotSolveThis(lhs[0])))
{
return eq;
}
//then also add another entry for x = x1@t
ASTNode var = lhs[0];
ASTNode newvar =
- _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth());
+ _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth());
newvar =
- _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs);
+ _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs);
_simp->UpdateSolverMap(var, newvar);
output = ASTTrue;
break;
ASTNode a = _simp->MultiplicativeInverse(lhs[0]);
ASTNode chosenvar = (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1];
ASTNode chosenvar_value =
- _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), a, rhs));
+ _simp->SimplifyTerm(_bm->CreateTerm(BVMULT, rhs.GetValueWidth(), a, rhs));
//if chosenvar is seen in chosenvar_value then abort
if (VarSeenInTerm(chosenvar, chosenvar_value))
{
ASTNode var = lhs[1][0];
ASTNode newvar =
- _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth());
+ _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth());
newvar =
- _bm->CreateTerm(BVCONCAT,
- var.GetValueWidth(),
- newvar, chosenvar_value);
+ _bm->CreateTerm(BVCONCAT,
+ var.GetValueWidth(),
+ newvar, chosenvar_value);
_simp->UpdateSolverMap(var, newvar);
}
output = ASTTrue;
ASTNode aaa = *it;
Kind itk = aaa.GetKind();
if (!(BVCONST == itk && !_simp->BVConstIsOdd(aaa)) && !(BVMULT == itk && BVCONST == aaa[0].GetKind() && SYMBOL == aaa[1].GetKind()
- && !_simp->BVConstIsOdd(aaa[0])))
+ && !_simp->BVConstIsOdd(aaa[0])))
{
//If the monomials of the lhs are NOT of the form 'a*x' or 'a'
//where 'a' is even, then return the eqn
bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
{
if (READ == term.GetKind()
- && WRITE == term[0].GetKind()
- && !_bm->GetRemoveWritesFlag())
+ && WRITE == term[0].GetKind()
+ && !_bm->GetRemoveWritesFlag())
{
return false;
}
if (READ == term.GetKind()
- && WRITE == term[0].GetKind()
- && _bm->GetRemoveWritesFlag())
+ && WRITE == term[0].GetKind()
+ && _bm->GetRemoveWritesFlag())
{
return true;
}
******************************************************************/
class BVSolver
- {
- private:
- // Ptr to toplevel manager that manages bit-vector expressions
- // (i.e. construct various kinds of expressions), and also has
- // member functions that simplify bit-vector expressions
- STPMgr * _bm;
+ {
+ private:
+ // Ptr to toplevel manager that manages bit-vector expressions
+ // (i.e. construct various kinds of expressions), and also has
+ // member functions that simplify bit-vector expressions
+ STPMgr * _bm;
- // Ptr to Simplifier
- Simplifier * _simp;
-
- //
- ASTNode ASTTrue, ASTFalse, ASTUndefined;
-
- //Those formulas which have already been solved. If the same
- //formula occurs twice then do not solve the second occurence, and
- //instead drop it
- ASTNodeMap FormulasAlreadySolvedMap;
-
- //this map is useful while traversing terms and uniquely
- //identifying variables in the those terms. Prevents double
- //counting.
- ASTNodeMap TermsAlreadySeenMap;
- ASTNodeMap TermsAlreadySeenMap_ForArrays;
-
- //solved variables list: If a variable has been solved for then do
- //not solve for it again
- ASTNodeSet DoNotSolve_TheseVars;
-
- //checks if var has been solved for or not. if yes, then return
- //true else return false
- bool DoNotSolveThis(const ASTNode& var);
-
- //traverses a term, and creates a multiset of all variables in the
- //term. Does memoization to avoid double counting.
- void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v);
- void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v);
-
- //choose a suitable var from the term
- ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm);
- //accepts an equation and solves for a variable or a monom in it
- ASTNode BVSolve_Odd(const ASTNode& eq);
-
- //solves equations of the form a*x=t where 'a' is even. Has a
- //return value, unlike the normal BVSolve()
- ASTNode BVSolve_Even(const ASTNode& eq);
- ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
-
- //Checks for arrayreads in a term. if yes then returns true, else
- //return false
- bool CheckForArrayReads(const ASTNode& term);
- bool CheckForArrayReads_TopLevel(const ASTNode& term);
-
- //Creates new variables used in solving
- ASTNode NewVar(unsigned int n);
-
- //this function return true if the var occurs in term, else the
- //function returns false
- bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
-
- //takes an even number "in" as input, and returns an odd number
- //(return value) and a power of 2 (as number_shifts by reference),
- //such that in = (odd_number * power_of_2).
- //
- //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on
- //bit-vector arithmetic published in DAC 1998) paper for precise
- //understanding of the algorithm
- ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in,
- unsigned int& number_shifts);
-
- //Once a formula has been solved, then update the alreadysolvedmap
- //with the formula, and the solved value. The solved value can be
- //described using the following example: Suppose input to the
- //solver is
- //
- // input key: x = 2 AND y = x + t
- //
- // output value: y = 2 + t
- void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value);
-
- //This function checks if the key (formula) has already been
- //solved for.
- //
- //If yes it returns TRUE and fills the "output" with the
- //solved-value (call by reference argument),
- //
- //else returns FALSE
- bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
-
- public:
- //constructor
- BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)
- {
- ASTTrue = _bm->CreateNode(TRUE);
- ASTFalse = _bm->CreateNode(FALSE);
- ASTUndefined = _bm->CreateNode(UNDEFINED);
- }
- ;
-
- //Destructor
- ~BVSolver()
- {
- TermsAlreadySeenMap.clear();
- DoNotSolve_TheseVars.clear();
- FormulasAlreadySolvedMap.clear();
- TermsAlreadySeenMap_ForArrays.clear();
- }
-
- //Top Level Solver: Goes over the input DAG, identifies the
- //equation to be solved, solves them,
- ASTNode TopLevelBVSolve(const ASTNode& a);
-
- void ClearAllTables(void)
- {
- DoNotSolve_TheseVars.clear();
- FormulasAlreadySolvedMap.clear();
- TermsAlreadySeenMap_ForArrays.clear();
- } //End of ClearAllTables()
-
- }; //end of class bvsolver
+ // Ptr to Simplifier
+ Simplifier * _simp;
+
+ //
+ ASTNode ASTTrue, ASTFalse, ASTUndefined;
+
+ //Those formulas which have already been solved. If the same
+ //formula occurs twice then do not solve the second occurence, and
+ //instead drop it
+ ASTNodeMap FormulasAlreadySolvedMap;
+
+ //this map is useful while traversing terms and uniquely
+ //identifying variables in the those terms. Prevents double
+ //counting.
+ ASTNodeMap TermsAlreadySeenMap;
+ ASTNodeMap TermsAlreadySeenMap_ForArrays;
+
+ //solved variables list: If a variable has been solved for then do
+ //not solve for it again
+ ASTNodeSet DoNotSolve_TheseVars;
+
+ //checks if var has been solved for or not. if yes, then return
+ //true else return false
+ bool DoNotSolveThis(const ASTNode& var);
+
+ //traverses a term, and creates a multiset of all variables in the
+ //term. Does memoization to avoid double counting.
+ void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v);
+ void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v);
+
+ //choose a suitable var from the term
+ ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm);
+ //accepts an equation and solves for a variable or a monom in it
+ ASTNode BVSolve_Odd(const ASTNode& eq);
+
+ //solves equations of the form a*x=t where 'a' is even. Has a
+ //return value, unlike the normal BVSolve()
+ ASTNode BVSolve_Even(const ASTNode& eq);
+ ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
+
+ //Checks for arrayreads in a term. if yes then returns true, else
+ //return false
+ bool CheckForArrayReads(const ASTNode& term);
+ bool CheckForArrayReads_TopLevel(const ASTNode& term);
+
+ //Creates new variables used in solving
+ ASTNode NewVar(unsigned int n);
+
+ //this function return true if the var occurs in term, else the
+ //function returns false
+ bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
+
+ //takes an even number "in" as input, and returns an odd number
+ //(return value) and a power of 2 (as number_shifts by reference),
+ //such that in = (odd_number * power_of_2).
+ //
+ //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on
+ //bit-vector arithmetic published in DAC 1998) paper for precise
+ //understanding of the algorithm
+ ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in,
+ unsigned int& number_shifts);
+
+ //Once a formula has been solved, then update the alreadysolvedmap
+ //with the formula, and the solved value. The solved value can be
+ //described using the following example: Suppose input to the
+ //solver is
+ //
+ // input key: x = 2 AND y = x + t
+ //
+ // output value: y = 2 + t
+ void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value);
+
+ //This function checks if the key (formula) has already been
+ //solved for.
+ //
+ //If yes it returns TRUE and fills the "output" with the
+ //solved-value (call by reference argument),
+ //
+ //else returns FALSE
+ bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
+
+ public:
+ //constructor
+ BVSolver(STPMgr * bm, Simplifier * simp) : _bm(bm), _simp(simp)
+ {
+ ASTTrue = _bm->CreateNode(TRUE);
+ ASTFalse = _bm->CreateNode(FALSE);
+ ASTUndefined = _bm->CreateNode(UNDEFINED);
+ }
+ ;
+
+ //Destructor
+ ~BVSolver()
+ {
+ TermsAlreadySeenMap.clear();
+ DoNotSolve_TheseVars.clear();
+ FormulasAlreadySolvedMap.clear();
+ TermsAlreadySeenMap_ForArrays.clear();
+ }
+
+ //Top Level Solver: Goes over the input DAG, identifies the
+ //equation to be solved, solves them,
+ ASTNode TopLevelBVSolve(const ASTNode& a);
+
+ void ClearAllTables(void)
+ {
+ DoNotSolve_TheseVars.clear();
+ FormulasAlreadySolvedMap.clear();
+ TermsAlreadySeenMap_ForArrays.clear();
+ } //End of ClearAllTables()
+
+ }; //end of class bvsolver
};//end of namespace BEEV
#endif
break;
}
- case BVLEFTSHIFT:
- case BVRIGHTSHIFT:
- case BVSRSHIFT:
- {
- // load in the bitWidth.
- CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
- for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
- if ((inputwidth & (0x1 << i)) != 0)
- CONSTANTBV::BitVector_Bit_On(width, i);
-
- output = CONSTANTBV::BitVector_Create(inputwidth, true);
-
- // Number of bits to shift it.
- ASTNode shiftNode = BVConstEvaluator(t[1]);
-
- bool msb = CONSTANTBV::BitVector_msb_(tmp0);
-
- // If this shift is greater than the bitWidth, make it zero.
- if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
- {
- if (k == BVSRSHIFT && msb)
- CONSTANTBV::Set_Complement(output, output);
- }
- else
- {
- // the shift is destructive, get a copy.
- CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
-
- unsigned int shift = GetUnsignedConst(shiftNode);
-
- if (k == BVLEFTSHIFT)
- CONSTANTBV::BitVector_Move_Left(output, shift);
- else
- CONSTANTBV::BitVector_Move_Right(output, shift);
-
- if (k == BVSRSHIFT && msb)
- {
- // signed shift, and the number was originally negative.
- // Shift may be larger than the inputwidth.
- for (unsigned int i = 0; i < min(shift, inputwidth); i++)
- {
- CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
- }
- assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative.
- }
- }
-
- OutputNode = _bm->CreateBVConst(output, outputwidth);
-
- CONSTANTBV::BitVector_Destroy(width);
- break;
- }
+ case BVLEFTSHIFT:
+ case BVRIGHTSHIFT:
+ case BVSRSHIFT:
+ {
+ // load in the bitWidth.
+ CBV width = CONSTANTBV::BitVector_Create(inputwidth, true);
+ for (unsigned i = 0; i < sizeof(inputwidth) * 8; i++)
+ if ((inputwidth & (0x1 << i)) != 0)
+ CONSTANTBV::BitVector_Bit_On(width, i);
+
+ output = CONSTANTBV::BitVector_Create(inputwidth, true);
+
+ // Number of bits to shift it.
+ ASTNode shiftNode = BVConstEvaluator(t[1]);
+
+ bool msb = CONSTANTBV::BitVector_msb_(tmp0);
+
+ // If this shift is greater than the bitWidth, make it zero.
+ if (CONSTANTBV::BitVector_Lexicompare(width, shiftNode.GetBVConst()) < 0)
+ {
+ if (k == BVSRSHIFT && msb)
+ CONSTANTBV::Set_Complement(output, output);
+ }
+ else
+ {
+ // the shift is destructive, get a copy.
+ CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
+
+ unsigned int shift = GetUnsignedConst(shiftNode);
+
+ if (k == BVLEFTSHIFT)
+ CONSTANTBV::BitVector_Move_Left(output, shift);
+ else
+ CONSTANTBV::BitVector_Move_Right(output, shift);
+
+ if (k == BVSRSHIFT && msb)
+ {
+ // signed shift, and the number was originally negative.
+ // Shift may be larger than the inputwidth.
+ for (unsigned int i = 0; i < min(shift, inputwidth); i++)
+ {
+ CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i));
+ }
+ assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative.
+ }
+ }
+
+ OutputNode = _bm->CreateBVConst(output, outputwidth);
+
+ CONSTANTBV::BitVector_Destroy(width);
+ break;
+ }
case BVAND:
ASTNode Simplifier::Flatten(const ASTNode& a)
{
- ASTNode n = a;
- while (true)
- {
- ASTNode& nold = n;
- n = FlattenOneLevel(n);
- if ((n == nold))
- break;
- }
-
- return n;
+ ASTNode n = a;
+ while (true)
+ {
+ ASTNode& nold = n;
+ n = FlattenOneLevel(n);
+ if ((n == nold))
+ break;
+ }
+
+ return n;
}
bool Simplifier::CheckMap(ASTNodeMap* VarConstMap,
- const ASTNode& key, ASTNode& output)
+ const ASTNode& key, ASTNode& output)
{
if(NULL == VarConstMap)
{
bool Simplifier::CheckSimplifyMap(const ASTNode& key,
- ASTNode& output,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ ASTNode& output,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
if(NULL != VarConstMap)
{
- return false;
+ return false;
}
ASTNodeMap::iterator it, itend;
it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
// Push any reference count used by the key to the value.
void Simplifier::UpdateSimplifyMap(const ASTNode& key,
- const ASTNode& value,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ const ASTNode& value,
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
if(NULL != VarConstMap)
{
- return;
+ return;
}
// Don't add leaves. Leaves are easy to recalculate, no need
if (1 == i && !CheckSubstitutionMap(e0))
{
assert((e1.GetKind() == TRUE) ||
- (e1.GetKind() == FALSE) ||
- (e1.GetKind() == BVCONST));
+ (e1.GetKind() == FALSE) ||
+ (e1.GetKind() == BVCONST));
(*SolverMap)[e0] = e1;
return true;
}
if (-1 == i && !CheckSubstitutionMap(e1))
{
assert((e0.GetKind() == TRUE) ||
- (e0.GetKind() == FALSE) ||
- (e0.GetKind() == BVCONST));
+ (e0.GetKind() == FALSE) ||
+ (e0.GetKind() == BVCONST));
(*SolverMap)[e1] = e0;
return true;
}
ASTNode
Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
_bm->Begin_RemoveWrites = false;
ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
// The SimplifyMaps on entry to the topLevel functions may contain useful entries.
// E.g. The BVSolver calls SimplifyTerm()
ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
_bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
if (smtlib_parser_flag)
- BuildReferenceCountMap(b);
+ BuildReferenceCountMap(b);
ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
ResetSimplifyMaps();
_bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel);
return out;
}
-ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b)
-{
- _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
- ASTNode out = SimplifyTerm(b);
- ResetSimplifyMaps();
- _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel);
- return out;
-}
+ ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b)
+ {
+ _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
+ ASTNode out = SimplifyTerm(b);
+ ResetSimplifyMaps();
+ _bm->GetRunTimes()->stop(RunTimes::SimplifyTopLevel);
+ return out;
+ }
ASTNode
Simplifier::SimplifyFormula(const ASTNode& b,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
-// if (!optimize_flag)
-// return b;
+ // if (!optimize_flag)
+ // return b;
Kind kind = b.GetKind();
if (BOOLEAN_TYPE != b.GetType())
{
FatalError(" SimplifyFormula: "\
- "You have input a nonformula kind: ", ASTUndefined, kind);
+ "You have input a nonformula kind: ", ASTUndefined, kind);
}
ASTNode a = b;
ASTVec ca = a.GetChildren();
if (!(IMPLIES == kind ||
- ITE == kind ||
- FOR == kind ||
- PARAMBOOL==kind ||
- isAtomic(kind)))
+ ITE == kind ||
+ FOR == kind ||
+ PARAMBOOL==kind ||
+ isAtomic(kind)))
{
SortByArith(ca);
a = _bm->CreateNode(kind, ca);
ASTNode
Simplifier::SimplifyForFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
//FIXME: Code this up properly later. Mainly pushing the negation
//down
ASTNode
Simplifier::SimplifyAtomicFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
-// if (!optimize_flag)
-// return a;
+ // if (!optimize_flag)
+ // return a;
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
output = pushNeg ? _bm->CreateNode(NOT, output) : output;
break;
case PARAMBOOL:
- {
- ASTNode term = SimplifyTerm(a[1], VarConstMap);
- output = _bm->CreateNode(PARAMBOOL, a[0], term);
- output = pushNeg ? _bm->CreateNode(NOT, output) : output;
- break;
- }
+ {
+ ASTNode term = SimplifyTerm(a[1], VarConstMap);
+ output = _bm->CreateNode(PARAMBOOL, a[0], term);
+ output = pushNeg ? _bm->CreateNode(NOT, output) : output;
+ break;
+ }
case BVGETBIT:
{
ASTNode term = SimplifyTerm(a[0], VarConstMap);
ASTNode zero = _bm->CreateZeroConst(1);
ASTNode one = _bm->CreateOneConst(1);
ASTNode getthebit =
- SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap);
+ SimplifyTerm(_bm->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap);
if (getthebit == zero)
output = pushNeg ? ASTTrue : ASTFalse;
else if (getthebit == one)
}
default:
FatalError("SimplifyAtomicFormula: "\
- "NO atomic formula of the kind: ", ASTUndefined, kind);
+ "NO atomic formula of the kind: ", ASTUndefined, kind);
break;
}
} //end of SimplifyAtomicFormula()
ASTNode Simplifier::CreateSimplifiedINEQ(Kind k,
- const ASTNode& left,
- const ASTNode& right, bool pushNeg)
+ const ASTNode& left,
+ const ASTNode& right, bool pushNeg)
{
ASTNode output;
if (BVCONST == left.GetKind() && BVCONST == right.GetKind())
else
{
output =
- pushNeg ?
- _bm->CreateNode(BVLE, right, left) :
- _bm->CreateNode(BVLT, left, right);
+ pushNeg ?
+ _bm->CreateNode(BVLE, right, left) :
+ _bm->CreateNode(BVLT, left, right);
}
break;
case BVLE:
else
{
output =
- pushNeg ?
- _bm->CreateNode(BVLT, right, left) :
- _bm->CreateNode(BVLE, left, right);
+ pushNeg ?
+ _bm->CreateNode(BVLT, right, left) :
+ _bm->CreateNode(BVLE, left, right);
}
break;
case BVGT:
else
{
output =
- pushNeg ?
- _bm->CreateNode(BVLE, left, right) :
- _bm->CreateNode(BVLT, right, left);
+ pushNeg ?
+ _bm->CreateNode(BVLE, left, right) :
+ _bm->CreateNode(BVLT, right, left);
}
break;
case BVGE:
else
{
output =
- pushNeg ?
- _bm->CreateNode(BVLT, left, right) :
- _bm->CreateNode(BVLE, right, left);
+ pushNeg ?
+ _bm->CreateNode(BVLT, left, right) :
+ _bm->CreateNode(BVLE, right, left);
}
break;
case BVSLT:
{
if (BVLT != in[j].GetKind())
continue;
- // parameters are swapped.
+ // parameters are swapped.
if (in[i][0] == in[j][1] && in[i][1] == in[j][0])
return ASTFalse;
}
output = ASTFalse;
}
else if (ITE == k1 &&
- BVCONST == in1[1].GetKind() &&
- BVCONST == in1[2].GetKind() && BVCONST == k2)
+ 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:
}
}
else if (ITE == k2 &&
- BVCONST == in2[1].GetKind() &&
- BVCONST == in2[2].GetKind() && BVCONST == k1)
+ 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 Simplifier::CreateSimplifiedTermITE(const ASTNode& in0,
- const ASTNode& in1,
- const ASTNode& in2)
+ const ASTNode& in1,
+ const ASTNode& in2)
{
ASTNode t0 = in0;
ASTNode t1 = in1;
{
cerr << "t2 is : = " << t2;
FatalError("CreateSimplifiedTermITE: "\
- "the lengths of the two branches don't match", t1);
+ "the lengths of the two branches don't match", t1);
}
if (t1.GetIndexWidth() != t2.GetIndexWidth())
{
cerr << "t2 is : = " << t2;
FatalError("CreateSimplifiedTermITE: "\
- "the lengths of the two branches don't match", t1);
+ "the lengths of the two branches don't match", t1);
}
return _bm->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2);
}
default:
{
output =
- (isAnd) ? (pushNeg ?
- _bm->CreateNode(OR, outvec) :
- _bm->CreateNode(AND, outvec)) :
- (pushNeg ? _bm->CreateNode(AND, outvec) : _bm->CreateNode(OR,outvec));
+ (isAnd) ? (pushNeg ?
+ _bm->CreateNode(OR, outvec) :
+ _bm->CreateNode(AND, outvec)) :
+ (pushNeg ? _bm->CreateNode(AND, outvec) : _bm->CreateNode(OR,outvec));
//output = FlattenOneLevel(output);
break;
}
ASTNode
Simplifier::SimplifyNotFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap)
+ bool pushNeg, ASTNodeMap* VarConstMap)
{
ASTNode output;
if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
output = c1;
}
else if (CheckAlwaysTrueFormMap(c1) ||
- CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c0)) ||
- (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0])))
+ CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c0)) ||
+ (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0])))
{
//(~c0 AND (~c0 OR c1)) <==> TRUE
//
output = ASTTrue;
}
else if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, c1)) ||
- (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0])))
+ (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0])))
{
//(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0
//(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0
ASTNode Simplifier::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap)
{
- // if (!optimize_flag)
-// return b;
+ // if (!optimize_flag)
+ // return b;
ASTNode output;
if (CheckSimplifyMap(b, output, pushNeg, VarConstMap))
output = t1;
}
else if (CheckAlwaysTrueFormMap(_bm->CreateNode(NOT, t0)) ||
- (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
+ (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0])))
{
output = t2;
}
}
CONSTANTBV::BitVector_increment(maskedPlusOne);
ASTNode temp =
- _bm->CreateTerm(BVMULT, inputValueWidth,
- _bm->CreateBVConst(maskedPlusOne, inputValueWidth), other);
+ _bm->CreateTerm(BVMULT, inputValueWidth,
+ _bm->CreateBVConst(maskedPlusOne, inputValueWidth), other);
output = _bm->CreateTerm(BVNEG, inputValueWidth, temp);
}
}
// propagate bvuminus upwards through multiplies.
if (BVMULT == output.GetKind())
- {
- ASTVec d = output.GetChildren();
- int uminus = 0;
- for (unsigned i = 0; i < d.size(); i++)
- {
- if (d[i].GetKind() == BVUMINUS)
- {
- d[i] = d[i][0];
- uminus++;
- }
- }
- if (uminus != 0)
- {
- SortByArith(d);
- output = _bm->CreateTerm(BVMULT, output.GetValueWidth(), d);
- if ((uminus & 0x1) != 0) // odd, pull up the uminus.
- {
- output = _bm->CreateTerm(BVUMINUS, output.GetValueWidth(), output);
- }
- }
- }
+ {
+ ASTVec d = output.GetChildren();
+ int uminus = 0;
+ for (unsigned i = 0; i < d.size(); i++)
+ {
+ if (d[i].GetKind() == BVUMINUS)
+ {
+ d[i] = d[i][0];
+ uminus++;
+ }
+ }
+ if (uminus != 0)
+ {
+ SortByArith(d);
+ output = _bm->CreateTerm(BVMULT, output.GetValueWidth(), d);
+ if ((uminus & 0x1) != 0) // odd, pull up the uminus.
+ {
+ output = _bm->CreateTerm(BVUMINUS, output.GetValueWidth(), output);
+ }
+ }
+ }
}
else
{
- // If the first argument to the multiply is a constant, push it through.
- // Without regard for the splitting of nodes (hmm.)
- // This is necessary because the bitvector solver can process -3*x, but
- // not -(3*x).
- if (BVCONST == a0[0].GetKind())
- {
- ASTNode a00 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]), VarConstMap);
- output = _bm->CreateTerm(BVMULT, l, a00, a0[1]);
- }
- else
- output = _bm->CreateTerm(BVUMINUS, l, a0);
+ // If the first argument to the multiply is a constant, push it through.
+ // Without regard for the splitting of nodes (hmm.)
+ // This is necessary because the bitvector solver can process -3*x, but
+ // not -(3*x).
+ if (BVCONST == a0[0].GetKind())
+ {
+ ASTNode a00 = SimplifyTerm(_bm->CreateTerm(BVUMINUS, l, a0[0]), VarConstMap);
+ output = _bm->CreateTerm(BVMULT, l, a00, a0[1]);
+ }
+ else
+ output = _bm->CreateTerm(BVUMINUS, l, a0);
}
break;
}
case BVLEFTSHIFT:
- case BVRIGHTSHIFT:
-
- { // If the shift amount is known. Then replace it by an extract.
- ASTNode a = SimplifyTerm(inputterm[0], VarConstMap);
- ASTNode b = SimplifyTerm(inputterm[1], VarConstMap);
- const unsigned int width = a.GetValueWidth();
- if (BVCONST == b.GetKind()) // known shift amount.
- {
- if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
- {
- // Intended to remove shifts by very large amounts that don't fit into the unsigned.
- // at thhe start of the "else" branch.
- output = _bm->CreateZeroConst(width);
- }
- else
- {
- const unsigned int shift = GetUnsignedConst(b);
- if (shift > width)
- {
- output = _bm->CreateZeroConst(width);
- }
- else if (shift == 0)
- {
- output = a; // unchanged.
- }
- else
- {
- if (k == BVLEFTSHIFT)
- {
- ASTNode zero = _bm->CreateZeroConst(shift);
- ASTNode hi = _bm->CreateBVConst(32, width - shift -1);
- ASTNode low = _bm->CreateBVConst(32, 0);
- ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
- BVTypeCheck(extract);
- output = _bm->CreateTerm(BVCONCAT, width, extract, zero);
- BVTypeCheck(output);
- }
- else if (k == BVRIGHTSHIFT)
- {
- ASTNode zero = _bm->CreateZeroConst(shift);
- ASTNode hi = _bm->CreateBVConst(32, width -1);
- ASTNode low = _bm->CreateBVConst(32, shift);
- ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
- BVTypeCheck(extract);
- output = _bm->CreateTerm(BVCONCAT, width, zero, extract);
- BVTypeCheck(output);
- }
- else
- FatalError("herasdf");
- }
- }
- }
- else
- output = _bm->CreateTerm(k, width, a, b);
- }
- break;
+ case BVRIGHTSHIFT:
+
+ { // If the shift amount is known. Then replace it by an extract.
+ ASTNode a = SimplifyTerm(inputterm[0], VarConstMap);
+ ASTNode b = SimplifyTerm(inputterm[1], VarConstMap);
+ const unsigned int width = a.GetValueWidth();
+ if (BVCONST == b.GetKind()) // known shift amount.
+ {
+ if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width))
+ {
+ // Intended to remove shifts by very large amounts that don't fit into the unsigned.
+ // at thhe start of the "else" branch.
+ output = _bm->CreateZeroConst(width);
+ }
+ else
+ {
+ const unsigned int shift = GetUnsignedConst(b);
+ if (shift > width)
+ {
+ output = _bm->CreateZeroConst(width);
+ }
+ else if (shift == 0)
+ {
+ output = a; // unchanged.
+ }
+ else
+ {
+ if (k == BVLEFTSHIFT)
+ {
+ ASTNode zero = _bm->CreateZeroConst(shift);
+ ASTNode hi = _bm->CreateBVConst(32, width - shift -1);
+ ASTNode low = _bm->CreateBVConst(32, 0);
+ ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+ BVTypeCheck(extract);
+ output = _bm->CreateTerm(BVCONCAT, width, extract, zero);
+ BVTypeCheck(output);
+ }
+ else if (k == BVRIGHTSHIFT)
+ {
+ ASTNode zero = _bm->CreateZeroConst(shift);
+ ASTNode hi = _bm->CreateBVConst(32, width -1);
+ ASTNode low = _bm->CreateBVConst(32, shift);
+ ASTNode extract = _bm->CreateTerm(BVEXTRACT, width - shift, a, hi, low);
+ BVTypeCheck(extract);
+ output = _bm->CreateTerm(BVCONCAT, width, zero, extract);
+ BVTypeCheck(output);
+ }
+ else
+ FatalError("herasdf");
+ }
+ }
+ }
+ else
+ output = _bm->CreateTerm(k, width, a, b);
+ }
+ break;
case BVXOR:
}
if (!_bm->Begin_RemoveWrites
- && !_bm->SimplifyWrites_InPlace_Flag
- && !_bm->start_abstracting)
+ && !_bm->SimplifyWrites_InPlace_Flag
+ && !_bm->start_abstracting)
{
return term;
}
else if (!_bm->Begin_RemoveWrites
- && _bm->SimplifyWrites_InPlace_Flag
- && !_bm->start_abstracting)
+ && _bm->SimplifyWrites_InPlace_Flag
+ && !_bm->start_abstracting)
{
//return term;
return SimplifyWrites_InPlace(term);
}
if (!_bm->start_abstracting
- && _bm->Begin_RemoveWrites)
+ && _bm->Begin_RemoveWrites)
{
output = ReadOverWrite_To_ITE(input);
}
ReferenceCount = new ASTNodeCountMap();
}
-void Simplifier::printCacheStatus()
-{
- cerr << SimplifyMap->size() << endl;
- cerr << SimplifyNegMap->size() << endl;
- cerr << ReferenceCount->size() << endl;
- //cerr << TermsAlreadySeenMap.size() << endl;
+ void Simplifier::printCacheStatus()
+ {
+ cerr << SimplifyMap->size() << endl;
+ cerr << SimplifyNegMap->size() << endl;
+ cerr << ReferenceCount->size() << endl;
+ //cerr << TermsAlreadySeenMap.size() << endl;
- cerr << SimplifyMap->bucket_count() << endl;
- cerr << SimplifyNegMap->bucket_count() << endl;
- cerr << ReferenceCount->bucket_count() << endl;
- //cerr << TermsAlreadySeenMap.bucket_count() << endl;
-} //printCacheStatus()
+ cerr << SimplifyMap->bucket_count() << endl;
+ cerr << SimplifyNegMap->bucket_count() << endl;
+ cerr << ReferenceCount->bucket_count() << endl;
+ //cerr << TermsAlreadySeenMap.bucket_count() << endl;
+ } //printCacheStatus()
};//end of namespace
namespace BEEV
{
class Simplifier
- {
- friend class counterexample;
- private:
-
- /****************************************************************
- * Private Data and TypeDefs *
- ****************************************************************/
-
- // Handy defs
- ASTNode ASTTrue, ASTFalse, ASTUndefined;
-
- // Memo table for simplifcation. Key is unsimplified node, and
- // value is simplified node.
- ASTNodeMap * SimplifyMap;
- ASTNodeMap * SimplifyNegMap;
- ASTNodeMap * SolverMap;
- ASTNodeSet AlwaysTrueFormMap;
- ASTNodeMap MultInverseMap;
-
- // For ArrayWrite Abstraction: map from read-over-write term to
- // newname.
- ASTNodeMap * ReadOverWrite_NewName_Map;
+ {
+ friend class counterexample;
+ private:
+
+ /****************************************************************
+ * Private Data and TypeDefs *
+ ****************************************************************/
+
+ // Handy defs
+ ASTNode ASTTrue, ASTFalse, ASTUndefined;
+
+ // Memo table for simplifcation. Key is unsimplified node, and
+ // value is simplified node.
+ ASTNodeMap * SimplifyMap;
+ ASTNodeMap * SimplifyNegMap;
+ ASTNodeMap * SolverMap;
+ ASTNodeSet AlwaysTrueFormMap;
+ ASTNodeMap MultInverseMap;
+
+ // For ArrayWrite Abstraction: map from read-over-write term to
+ // newname.
+ ASTNodeMap * ReadOverWrite_NewName_Map;
- // For ArrayWrite Refinement: Map new arraynames to
- // Read-Over-Write terms
- ASTNodeMap NewName_ReadOverWrite_Map;
+ // For ArrayWrite Refinement: Map new arraynames to
+ // Read-Over-Write terms
+ ASTNodeMap NewName_ReadOverWrite_Map;
- // The number of direct parents of each node. i.e. the number
- // of times the pointer is in "children". When we simplify we
- // want to be careful sometimes about using the context of a
- // node. For example, given ((x + 23) = 2), the obvious
- // simplification is to join the constants. However, if there
- // are lots of references to the plus node. Then each time we
- // simplify, we'll create an additional plus.
- // nextpoweroftwo064.smt is the motivating benchmark. The
- // splitting increased the number of pluses from 1 to 65.
- ASTNodeCountMap *ReferenceCount;
+ // The number of direct parents of each node. i.e. the number
+ // of times the pointer is in "children". When we simplify we
+ // want to be careful sometimes about using the context of a
+ // node. For example, given ((x + 23) = 2), the obvious
+ // simplification is to join the constants. However, if there
+ // are lots of references to the plus node. Then each time we
+ // simplify, we'll create an additional plus.
+ // nextpoweroftwo064.smt is the motivating benchmark. The
+ // splitting increased the number of pluses from 1 to 65.
+ ASTNodeCountMap *ReferenceCount;
- //Ptr to STP Manager
- STPMgr * _bm;
+ //Ptr to STP Manager
+ STPMgr * _bm;
- public:
+ public:
- /****************************************************************
- * Public Member Functions *
- ****************************************************************/
- Simplifier(STPMgr * bm) : _bm(bm)
- {
- SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
- SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
- SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
- ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE);
- ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE);
-
- ASTTrue = bm->CreateNode(TRUE);
- ASTFalse = bm->CreateNode(FALSE);
- ASTUndefined = bm->CreateNode(UNDEFINED);
- }
+ /****************************************************************
+ * Public Member Functions *
+ ****************************************************************/
+ Simplifier(STPMgr * bm) : _bm(bm)
+ {
+ SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
+ SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
+ SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
+ ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE);
+ ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE);
+
+ ASTTrue = bm->CreateNode(TRUE);
+ ASTFalse = bm->CreateNode(FALSE);
+ ASTUndefined = bm->CreateNode(UNDEFINED);
+ }
- ~Simplifier()
- {
- delete SimplifyMap;
- delete SimplifyNegMap;
- delete ReferenceCount;
- }
-
- /****************************************************************
- * Functions to check and update various Maps *
- ****************************************************************/
+ ~Simplifier()
+ {
+ delete SimplifyMap;
+ delete SimplifyNegMap;
+ delete ReferenceCount;
+ }
+
+ /****************************************************************
+ * Functions to check and update various Maps *
+ ****************************************************************/
- //Check the map passed to SimplifyTerm
- bool CheckMap(ASTNodeMap* VarConstMap,
- const ASTNode& key, ASTNode& output);
-
- //substitution
- bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output);
- bool CheckSubstitutionMap(const ASTNode& a);
- bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1);
+ //Check the map passed to SimplifyTerm
+ bool CheckMap(ASTNodeMap* VarConstMap,
+ const ASTNode& key, ASTNode& output);
+
+ //substitution
+ bool CheckSubstitutionMap(const ASTNode& a, ASTNode& output);
+ bool CheckSubstitutionMap(const ASTNode& a);
+ bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1);
- //functions for checking and updating simplifcation map
- 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);
- bool CheckAlwaysTrueFormMap(const ASTNode& key);
- void UpdateAlwaysTrueFormMap(const ASTNode& val);
- bool CheckMultInverseMap(const ASTNode& key, ASTNode& output);
- void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value);
+ //functions for checking and updating simplifcation map
+ 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);
+ bool CheckAlwaysTrueFormMap(const ASTNode& key);
+ void UpdateAlwaysTrueFormMap(const ASTNode& val);
+ bool CheckMultInverseMap(const ASTNode& key, ASTNode& output);
+ void UpdateMultInverseMap(const ASTNode& key, const ASTNode& value);
- //Map for solved variables
- bool CheckSolverMap(const ASTNode& a, ASTNode& output);
- bool CheckSolverMap(const ASTNode& a);
- bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1);
+ //Map for solved variables
+ bool CheckSolverMap(const ASTNode& a, ASTNode& output);
+ bool CheckSolverMap(const ASTNode& a);
+ bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1);
- void ResetSimplifyMaps(void);
+ void ResetSimplifyMaps(void);
- /****************************************************************
- * Simplification functions *
- ****************************************************************/
+ /****************************************************************
+ * Simplification functions *
+ ****************************************************************/
- ASTNode SimplifyFormula_TopLevel(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 SimplifyTerm_TopLevel(const ASTNode& b);
- ASTNode SimplifyFormula(const ASTNode& a,
- bool pushNeg,
- ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyTerm(const ASTNode& inputterm,
- ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyTerm(const ASTNode& inputterm,
+ ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a,
- bool pushNeg,
- ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyFormula_NoRemoveWrites(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
- void CheckSimplifyInvariant(const ASTNode& a,
- const ASTNode& output);
+ void CheckSimplifyInvariant(const ASTNode& a,
+ const ASTNode& output);
- void BuildReferenceCountMap(const ASTNode& b);
+ void BuildReferenceCountMap(const ASTNode& b);
- ASTNode SimplifyAtomicFormula(const ASTNode& a,
- bool pushNeg,
- ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyAtomicFormula(const ASTNode& a,
+ bool pushNeg,
+ ASTNodeMap* VarConstMap=NULL);
- ASTNode CreateSimplifiedEQ(const ASTNode& t1,
- const ASTNode& t2);
+ ASTNode CreateSimplifiedEQ(const ASTNode& t1,
+ const ASTNode& t2);
- ASTNode ITEOpt_InEqs(const ASTNode& in1,
- ASTNodeMap* VarConstMap=NULL);
+ ASTNode ITEOpt_InEqs(const ASTNode& in1,
+ ASTNodeMap* VarConstMap=NULL);
- ASTNode PullUpITE(const ASTNode& in);
+ ASTNode PullUpITE(const ASTNode& in);
- ASTNode RemoveContradictionsFromAND(const ASTNode& in);
+ ASTNode RemoveContradictionsFromAND(const ASTNode& in);
- ASTNode CreateSimplifiedTermITE(const ASTNode& t1,
- const ASTNode& t2,
- const ASTNode& t3);
+ ASTNode CreateSimplifiedTermITE(const ASTNode& t1,
+ const ASTNode& t2,
+ const ASTNode& t3);
- ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0,
- const ASTNode& in1,
- const ASTNode& in2);
+ ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0,
+ const ASTNode& in1,
+ const ASTNode& in2);
- ASTNode CreateSimplifiedINEQ(Kind k,
- const ASTNode& a0,
- const ASTNode& a1, bool pushNeg);
+ ASTNode CreateSimplifiedINEQ(Kind k,
+ const ASTNode& a0,
+ const ASTNode& a1, bool pushNeg);
- ASTNode SimplifyNotFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyNotFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyAndOrFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyAndOrFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyXorFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyXorFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyNandFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyNandFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyNorFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyNorFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyImpliesFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyImpliesFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyIffFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyIffFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyIteFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyIteFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode SimplifyForFormula(const ASTNode& a,
- bool pushNeg, ASTNodeMap* VarConstMap=NULL);
+ ASTNode SimplifyForFormula(const ASTNode& a,
+ bool pushNeg, ASTNodeMap* VarConstMap=NULL);
- ASTNode Flatten(const ASTNode& a);
+ ASTNode Flatten(const ASTNode& a);
- ASTNode FlattenOneLevel(const ASTNode& a);
+ ASTNode FlattenOneLevel(const ASTNode& a);
- ASTNode FlattenAndOr(const ASTNode& a);
+ ASTNode FlattenAndOr(const ASTNode& a);
- ASTNode CombineLikeTerms(const ASTNode& a);
+ ASTNode CombineLikeTerms(const ASTNode& a);
- ASTNode LhsMinusRhs(const ASTNode& eq);
+ ASTNode LhsMinusRhs(const ASTNode& eq);
- ASTNode DistributeMultOverPlus(const ASTNode& a,
- bool startdistribution = false);
+ ASTNode DistributeMultOverPlus(const ASTNode& a,
+ bool startdistribution = false);
- ASTNode ConvertBVSXToITE(const ASTNode& a);
+ ASTNode ConvertBVSXToITE(const ASTNode& a);
- //accepts constant term and simplifies it to a bvconst
- ASTNode BVConstEvaluator(const ASTNode& t);
+ //accepts constant term and simplifies it to a bvconst
+ ASTNode BVConstEvaluator(const ASTNode& t);
- //checks if the input constant is odd or not
- bool BVConstIsOdd(const ASTNode& c);
+ //checks if the input constant is odd or not
+ bool BVConstIsOdd(const ASTNode& c);
- //computes the multiplicatve inverse of the input
- ASTNode MultiplicativeInverse(const ASTNode& c);
+ //computes the multiplicatve inverse of the input
+ ASTNode MultiplicativeInverse(const ASTNode& c);
- //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j))
- ASTNode RemoveWrites_TopLevel(const ASTNode& term);
- ASTNode RemoveWrites(const ASTNode& term);
- ASTNode SimplifyWrites_InPlace(const ASTNode& term,
- ASTNodeMap* VarConstMap=NULL);
- ASTNode ReadOverWrite_To_ITE(const ASTNode& term,
- ASTNodeMap* VarConstMap=NULL);
+ //Replaces WRITE(Arr,i,val) with ITE(j=i, val, READ(Arr,j))
+ ASTNode RemoveWrites_TopLevel(const ASTNode& term);
+ ASTNode RemoveWrites(const ASTNode& term);
+ ASTNode SimplifyWrites_InPlace(const ASTNode& term,
+ ASTNodeMap* VarConstMap=NULL);
+ ASTNode ReadOverWrite_To_ITE(const ASTNode& term,
+ ASTNodeMap* VarConstMap=NULL);
- void printCacheStatus();
+ void printCacheStatus();
- //FIXME: Get rid of this horrible function
- const ASTNodeMap * ReadOverWriteMap()
- {
- return ReadOverWrite_NewName_Map;
- } // End of ReadOverWriteMap()
+ //FIXME: Get rid of this horrible function
+ const ASTNodeMap * ReadOverWriteMap()
+ {
+ return ReadOverWrite_NewName_Map;
+ } // End of ReadOverWriteMap()
- const ASTNodeMap * Return_SolverMap()
- {
- return SolverMap;
- } // End of SolverMap()
-
- void ClearAllTables(void)
- {
- SimplifyMap->clear();
- SimplifyNegMap->clear();
- SolverMap->clear();
- ReadOverWrite_NewName_Map->clear();
- NewName_ReadOverWrite_Map.clear();
- AlwaysTrueFormMap.clear();
- MultInverseMap.clear();
- ReferenceCount->clear();
- }
- };//end of class Simplifier
+ const ASTNodeMap * Return_SolverMap()
+ {
+ return SolverMap;
+ } // End of SolverMap()
+
+ void ClearAllTables(void)
+ {
+ SimplifyMap->clear();
+ SimplifyNegMap->clear();
+ SolverMap->clear();
+ ReadOverWrite_NewName_Map->clear();
+ NewName_ReadOverWrite_Map.clear();
+ AlwaysTrueFormMap.clear();
+ MultInverseMap.clear();
+ ReferenceCount->clear();
+ }
+ };//end of class Simplifier
}; //end of namespace
#endif
break;
}
- case BVRIGHTSHIFT:
- case BVSRSHIFT:
- case BVLEFTSHIFT:
- {
- // Barrel shifter
- const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
- const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();
-
- // Signed right shift, need to copy the sign bit.
- ASTNode toFill;
- if (BVSRSHIFT == k)
- toFill = bbarg1.back();
- else
- toFill = ASTFalse;
-
- ASTVec temp_result(bbarg1);
- // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero.
- // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about
- // 8.2 so round up to 9.
-
- const unsigned width = bbarg1.size();
- unsigned log2Width = (unsigned)log2(width) + 1;
-
-
- if (k == BVSRSHIFT || k == BVRIGHTSHIFT)
- for (unsigned int i = 0; i < log2Width; i++)
- {
- if (bbarg2[i] == ASTFalse)
- continue; // Not shifting by anything.
-
- unsigned int shift_amount = 1 << i;
-
- for (unsigned int j = 0; j < width; j++)
- {
- if (j + shift_amount >= width)
- temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
- else
- temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]);
- }
- }
- else
- for (unsigned int i = 0; i < log2Width; i++)
- {
- if (bbarg2[i] == ASTFalse)
- continue; // Not shifting by anything.
-
- int shift_amount = 1 << i;
-
- for (signed int j = width - 1; j > 0; j--)
- {
- if (j < shift_amount)
- temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
- else
- temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]);
- }
- }
-
- // If any of the remainder are true. Then the whole thing gets the fill value.
- ASTNode remainder = ASTFalse;
- for (unsigned int i = log2Width; i < width; i++)
- {
- remainder = _bm->CreateNode(OR, remainder, bbarg2[i]);
- }
-
- for (unsigned int i = 0; i < width; i++)
- {
- temp_result[i] = _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]);
- }
-
- result = _bm->CreateNode(BOOLVEC, temp_result);
- }
- break;
+ case BVRIGHTSHIFT:
+ case BVSRSHIFT:
+ case BVLEFTSHIFT:
+ {
+ // Barrel shifter
+ const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
+ const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();
+
+ // Signed right shift, need to copy the sign bit.
+ ASTNode toFill;
+ if (BVSRSHIFT == k)
+ toFill = bbarg1.back();
+ else
+ toFill = ASTFalse;
+
+ ASTVec temp_result(bbarg1);
+ // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero.
+ // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about
+ // 8.2 so round up to 9.
+
+ const unsigned width = bbarg1.size();
+ unsigned log2Width = (unsigned)log2(width) + 1;
+
+
+ if (k == BVSRSHIFT || k == BVRIGHTSHIFT)
+ for (unsigned int i = 0; i < log2Width; i++)
+ {
+ if (bbarg2[i] == ASTFalse)
+ continue; // Not shifting by anything.
+
+ unsigned int shift_amount = 1 << i;
+
+ for (unsigned int j = 0; j < width; j++)
+ {
+ if (j + shift_amount >= width)
+ temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
+ else
+ temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]);
+ }
+ }
+ else
+ for (unsigned int i = 0; i < log2Width; i++)
+ {
+ if (bbarg2[i] == ASTFalse)
+ continue; // Not shifting by anything.
+
+ int shift_amount = 1 << i;
+
+ for (signed int j = width - 1; j > 0; j--)
+ {
+ if (j < shift_amount)
+ temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]);
+ else
+ temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]);
+ }
+ }
+
+ // If any of the remainder are true. Then the whole thing gets the fill value.
+ ASTNode remainder = ASTFalse;
+ for (unsigned int i = log2Width; i < width; i++)
+ {
+ remainder = _bm->CreateNode(OR, remainder, bbarg2[i]);
+ }
+
+ for (unsigned int i = 0; i < width; i++)
+ {
+ temp_result[i] = _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]);
+ }
+
+ result = _bm->CreateNode(BOOLVEC, temp_result);
+ }
+ break;
case BVVARSHIFT:
FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term);
break;
if (result_width == arg_width)
{
//nothing to sign extend
- result = arg;
+ result = arg;
break;
}
else
{
ASTNode neglit = _bm->CreateSimpNot(*lit);
ASTNode thisbit = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglit, *rit), // TRUE if l < r
- _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglit, *rit), // false if not equal
- prevbit)); // else prevbit
+ _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglit, *rit), // false if not equal
+ prevbit)); // else prevbit
prevbit = thisbit;
}
ASTNode neglmsb = _bm->CreateSimpNot(lmsb);
ASTNode msb = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), // TRUE if l < r
- _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglmsb, rmsb), // false if not equal
- prevbit)); // else prevbit
+ _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglmsb, rmsb), // false if not equal
+ prevbit)); // else prevbit
return msb;
}
// q and r are "out" parameters. rwidth puts a bound on the
// recursion depth. Unsigned only, for now.
void BBDivMod(const ASTVec &y, const ASTVec &x,
- ASTVec &q, ASTVec &r, unsigned int rwidth);
+ ASTVec &q, ASTVec &r, unsigned int rwidth);
// Return formula for majority function of three formulas.
ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c);
//can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or
//SOLVER_UNDECIDED
bool ToSAT::CallSAT(MINISAT::Solver& SatSolver,
- const ASTNode& modified_input,
- const ASTNode& original_input)
+ const ASTNode& modified_input,
+ const ASTNode& original_input)
{
bm->GetRunTimes()->start(RunTimes::BitBlasting);
BitBlaster BB(bm);
if (smtlib_parser_flag)
{
if (true_iff_valid &&
- (input_status == TO_BE_SATISFIABLE))
+ (input_status == TO_BE_SATISFIABLE))
{
cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl;
}
else if (!true_iff_valid &&
- (input_status == TO_BE_UNSATISFIABLE))
+ (input_status == TO_BE_UNSATISFIABLE))
{
cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl;
}
switch (k)
{
case TRUE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case FALSE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case SYMBOL:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVCONST:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
default:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
}
return result;
switch (k)
{
case BVLT:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVLE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVGT:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVGE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVSLT:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVSLE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVSGT:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case BVSGE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case EQ:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
default:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
}
return result;
switch (k)
{
case ITE:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
default:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
}
return result;
switch (k)
{
case NOT:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
case NAND:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
case NOR:
- {
- result = false;
- break;
- }
+ {
+ result = false;
+ break;
+ }
case IMPLIES:
- {
- if (idx == 0)
- {
- result = false;
- }
- break;
- }
+ {
+ if (idx == 0)
+ {
+ result = false;
+ }
+ break;
+ }
default:
- {
- break;
- }
+ {
+ break;
+ }
}
return result;
switch (k)
{
case NOT:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case NAND:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case NOR:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case XOR:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case IFF:
- {
- result = true;
- break;
- }
+ {
+ result = true;
+ break;
+ }
case IMPLIES:
- {
- if (idx == 0)
- {
- result = true;
- }
- break;
- }
+ {
+ if (idx == 0)
+ {
+ result = true;
+ }
+ break;
+ }
case ITE:
- {
- if (idx == 0)
- {
- result = true;
- }
- break;
- }
+ {
+ if (idx == 0)
+ {
+ result = true;
+ }
+ break;
+ }
default:
- {
- break;
- }
+ {
+ break;
+ }
}
return result;
bool result = false;
if (x.control & (1 << idx))
- {
- result = true;
+ {
+ result = true;
}
return result;
ClauseList::const_iterator it = varphi.begin();
for (; it != varphi.end(); it++)
{
- psi->push_back(new vector<const ASTNode*> (**it));
+ psi->push_back(new vector<const ASTNode*> (**it));
}
return psi;
void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2)
{
varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end());
- delete varphi2;
+ delete varphi2;
} //End of NOCOPY_INPLACE_UNION
ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2)
ClauseList::const_iterator it1 = varphi1.begin();
for (; it1 != varphi1.end(); it1++)
{
- ClausePtr clause1 = *it1;
- ClauseList::const_iterator it2 = varphi2.begin();
- for (; it2 != varphi2.end(); it2++)
- {
- ClausePtr clause2 = *it2;
- ClausePtr clause = new vector<const ASTNode*> ();
- clause->reserve(clause1->size() + clause2->size());
- clause->insert(clause->end(), clause1->begin(), clause1->end());
- clause->insert(clause->end(), clause2->begin(), clause2->end());
- psi->push_back(clause);
- }
+ ClausePtr clause1 = *it1;
+ ClauseList::const_iterator it2 = varphi2.begin();
+ for (; it2 != varphi2.end(); it2++)
+ {
+ ClausePtr clause2 = *it2;
+ ClausePtr clause = new vector<const ASTNode*> ();
+ clause->reserve(clause1->size() + clause2->size());
+ clause->insert(clause->end(), clause1->begin(), clause1->end());
+ clause->insert(clause->end(), clause2->begin(), clause2->end());
+ psi->push_back(clause);
+ }
}
return psi;
if (info.find(varphi) == info.end())
{
- x = new CNFInfo();
- initializeCNFInfo(*x);
- info[varphi] = x;
+ x = new CNFInfo();
+ initializeCNFInfo(*x);
+ info[varphi] = x;
}
else
{
- x = info[varphi];
+ x = info[varphi];
}
//########################################
if (isPos && sharesPos(*x) == 2)
{
- return;
+ return;
}
if (!isPos && sharesNeg(*x) == 2)
{
- return;
+ return;
}
//########################################
if (isPos)
{
- incrementSharesPos(*x);
+ incrementSharesPos(*x);
}
if (!isPos)
{
- incrementSharesNeg(*x);
+ incrementSharesNeg(*x);
}
//########################################
if (isAtom(varphi))
{
- return;
+ return;
}
else if (isPred(varphi))
{
- for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
- {
- scanTerm(varphi[i]);
- }
+ for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
+ {
+ scanTerm(varphi[i]);
+ }
}
else
{
- for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
- {
- if (onChildDoPos(varphi, i))
- {
- scanFormula(varphi[i], isPos);
- }
- if (onChildDoNeg(varphi, i))
- {
- scanFormula(varphi[i], !isPos);
- }
- }
+ for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
+ {
+ if (onChildDoPos(varphi, i))
+ {
+ scanFormula(varphi[i], isPos);
+ }
+ if (onChildDoNeg(varphi, i))
+ {
+ scanFormula(varphi[i], !isPos);
+ }
+ }
}
} //End of ScanFormula()
if (info.find(varphi) == info.end())
{
- x = new CNFInfo();
- initializeCNFInfo(*x);
- info[varphi] = x;
+ x = new CNFInfo();
+ initializeCNFInfo(*x);
+ info[varphi] = x;
}
else
{
- x = info[varphi];
+ x = info[varphi];
}
//########################################
if (sharesPos(*x) == 2)
{
- return;
+ return;
}
//########################################
if (isAtom(varphi))
{
- return;
+ return;
}
else if (isITE(varphi))
{
- scanFormula(varphi[0], true);
- scanFormula(varphi[0], false);
- scanTerm(varphi[1]);
- scanTerm(varphi[2]);
+ scanFormula(varphi[0], true);
+ scanFormula(varphi[0], false);
+ scanTerm(varphi[1]);
+ scanTerm(varphi[2]);
}
else
{
- for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
- {
- scanTerm(varphi[i]);
- }
+ for (unsigned int i = 0; i < varphi.GetChildren().size(); i++)
+ {
+ scanTerm(varphi[i]);
+ }
}
}//End of scanterm()
- //########################################
- //########################################
- // main cnf conversion function
+ //########################################
+ //########################################
+ // main cnf conversion function
void CNFMgr::convertFormulaToCNF(const ASTNode& varphi, ClauseList* defs)
{
if (isTerm(*x))
{
- convertTermForCNF(varphi, defs);
- setWasVisited(*x);
- return;
+ convertTermForCNF(varphi, defs);
+ setWasVisited(*x);
+ return;
}
//########################################
if (sharesPos(*x) > 0 && !wasVisited(*x))
{
- convertFormulaToCNFPosCases(varphi, defs);
+ convertFormulaToCNFPosCases(varphi, defs);
}
if (x->clausespos != NULL && x->clausespos->size() > 1)
{
- if (doSibRenamingPos(*x) || sharesPos(*x) > 1)
- {
- doRenamingPos(varphi, defs);
- }
+ if (doSibRenamingPos(*x) || sharesPos(*x) > 1)
+ {
+ doRenamingPos(varphi, defs);
+ }
}
if (sharesNeg(*x) > 0 && !wasVisited(*x))
{
- convertFormulaToCNFNegCases(varphi, defs);
+ convertFormulaToCNFNegCases(varphi, defs);
}
if (x->clausesneg != NULL && x->clausesneg->size() > 1)
{
- if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1)
- {
- doRenamingNeg(varphi, defs);
- }
+ if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1)
+ {
+ doRenamingNeg(varphi, defs);
+ }
}
//########################################
if (x->termforcnf != NULL)
{
- return;
+ return;
}
//########################################
if (isITE(varphi))
{
- x->termforcnf = doRenameITE(varphi, defs);
- reduceMemoryFootprintPos(varphi[0]);
- reduceMemoryFootprintNeg(varphi[0]);
-
+ x->termforcnf = doRenameITE(varphi, defs);
+ reduceMemoryFootprintPos(varphi[0]);
+ reduceMemoryFootprintNeg(varphi[0]);
+
}
else if (isAtom(varphi))
{
- x->termforcnf = ASTNodeToASTNodePtr(varphi);
+ x->termforcnf = ASTNodeToASTNodePtr(varphi);
}
else
- {
- ASTVec psis;
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- for (; it != varphi.GetChildren().end(); it++)
- {
- convertTermForCNF(*it, defs);
- psis.push_back(*(info[*it]->termforcnf));
- }
-
- ASTNode psi = bm->CreateNode(varphi.GetKind(), psis);
- psi.SetValueWidth(varphi.GetValueWidth());
- psi.SetIndexWidth(varphi.GetIndexWidth());
- x->termforcnf = ASTNodeToASTNodePtr(psi);
+ {
+ ASTVec psis;
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ for (; it != varphi.GetChildren().end(); it++)
+ {
+ convertTermForCNF(*it, defs);
+ psis.push_back(*(info[*it]->termforcnf));
+ }
+
+ ASTNode psi = bm->CreateNode(varphi.GetKind(), psis);
+ psi.SetValueWidth(varphi.GetValueWidth());
+ psi.SetIndexWidth(varphi.GetIndexWidth());
+ x->termforcnf = ASTNodeToASTNodePtr(psi);
}
} //End of convertTermForCNF()
//########################################
// step 2, calc new variable
- //########################################
+ //########################################
ostringstream oss;
oss << "cnf" << "{" << varphi.GetNodeNum() << "}";
{
if (isPred(varphi))
{
- convertFormulaToCNFPosPred(varphi, defs);
- return;
+ convertFormulaToCNFPosPred(varphi, defs);
+ return;
}
Kind k = varphi.GetKind();
switch (k)
{
case FALSE:
- {
- convertFormulaToCNFPosFALSE(varphi, defs);
- break;
- }
- case TRUE:
- {
- convertFormulaToCNFPosTRUE(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosFALSE(varphi, defs);
+ break;
+ }
+ case TRUE:
+ {
+ convertFormulaToCNFPosTRUE(varphi, defs);
+ break;
+ }
case BVGETBIT:
- {
- convertFormulaToCNFPosBVGETBIT(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosBVGETBIT(varphi, defs);
+ break;
+ }
case SYMBOL:
- {
- convertFormulaToCNFPosSYMBOL(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosSYMBOL(varphi, defs);
+ break;
+ }
case NOT:
- {
- convertFormulaToCNFPosNOT(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosNOT(varphi, defs);
+ break;
+ }
case AND:
- {
- convertFormulaToCNFPosAND(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosAND(varphi, defs);
+ break;
+ }
case NAND:
- {
- convertFormulaToCNFPosNAND(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosNAND(varphi, defs);
+ break;
+ }
case OR:
- {
- convertFormulaToCNFPosOR(varphi, defs);
- break;
- }
+ {
+ convertFormulaToCNFPosOR(varphi, defs);
+ break;
+ }
case NOR:
- {
- convertFormulaToCNFPosNOR(varphi, defs);
- break;
- }
- case XOR:
- {
- convertFormulaToCNFPosXOR(varphi, defs);
- break;
- }
- case IMPLIES:
- {
- convertFormulaToCNFPosIMPLIES(varphi, defs);
- break;
- }
- case ITE:
- {
- convertFormulaToCNFPosITE(varphi, defs);
- break;
- }
- default:
- {
- fprintf(stderr, "convertFormulaToCNFPosCases: doesn't handle kind %d\n", k);
- FatalError("");
- }
+ {
+ convertFormulaToCNFPosNOR(varphi, defs);
+ break;
+ }
+ case XOR:
+ {
+ convertFormulaToCNFPosXOR(varphi, defs);
+ break;
}
+ case IMPLIES:
+ {
+ convertFormulaToCNFPosIMPLIES(varphi, defs);
+ break;
+ }
+ case ITE:
+ {
+ convertFormulaToCNFPosITE(varphi, defs);
+ break;
+ }
+ default:
+ {
+ fprintf(stderr, "convertFormulaToCNFPosCases: doesn't handle kind %d\n", k);
+ FatalError("");
+ }
+ }
} //End of convertFormulaToCNFPosCases()
void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs)
- {
+ {
+
+ if (isPred(varphi))
+ {
+ convertFormulaToCNFNegPred(varphi, defs);
+ return;
+ }
- if (isPred(varphi))
+ Kind k = varphi.GetKind();
+ switch (k)
+ {
+ case FALSE:
{
- convertFormulaToCNFNegPred(varphi, defs);
- return;
+ convertFormulaToCNFNegFALSE(varphi, defs);
+ break;
}
-
- Kind k = varphi.GetKind();
- switch (k)
+ case TRUE:
{
- case FALSE:
- {
- convertFormulaToCNFNegFALSE(varphi, defs);
- break;
- }
- case TRUE:
- {
- convertFormulaToCNFNegTRUE(varphi, defs);
- break;
- }
- case BVGETBIT:
- {
- convertFormulaToCNFNegBVGETBIT(varphi, defs);
- break;
- }
- case SYMBOL:
- {
- convertFormulaToCNFNegSYMBOL(varphi, defs);
- break;
- }
- case NOT:
- {
- convertFormulaToCNFNegNOT(varphi, defs);
- break;
- }
- case AND:
- {
- convertFormulaToCNFNegAND(varphi, defs);
- break;
- }
- case NAND:
- {
- convertFormulaToCNFNegNAND(varphi, defs);
- break;
- }
- case OR:
- {
- convertFormulaToCNFNegOR(varphi, defs);
- break;
- }
- case NOR:
- {
- convertFormulaToCNFNegNOR(varphi, defs);
- break;
- }
- case XOR:
- {
- convertFormulaToCNFNegXOR(varphi, defs);
- break;
- }
- case IMPLIES:
- {
- convertFormulaToCNFNegIMPLIES(varphi, defs);
- break;
- }
- case ITE:
- {
- convertFormulaToCNFNegITE(varphi, defs);
- break;
- }
- default:
- {
- fprintf(stderr, "convertFormulaToCNFNegCases: doesn't handle kind %d\n", k);
- FatalError("");
- }
+ convertFormulaToCNFNegTRUE(varphi, defs);
+ break;
}
- } //convertFormulaToCNFNegCases()
-
- //########################################
- //########################################
- // individual cnf conversion cases
-
- void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs)
- {
- ASTVec psis;
-
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- for (; it != varphi.GetChildren().end(); it++)
+ case BVGETBIT:
{
- convertTermForCNF(*it, defs);
- psis.push_back(*(info[*it]->termforcnf));
+ convertFormulaToCNFNegBVGETBIT(varphi, defs);
+ break;
}
-
- info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis));
- } //End of convertFormulaToCNFPosPred()
-
- void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs)
- {
- ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
- info[varphi]->clausespos = SINGLETON(dummy_false_var);
- } //End of convertFormulaToCNFPosFALSE()
-
- void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs)
- {
- ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
- info[varphi]->clausespos = SINGLETON(dummy_true_var);
- } //End of convertFormulaToCNFPosTRUE
-
- void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs)
- {
- info[varphi]->clausespos = SINGLETON(varphi);
- }//End of convertFormulaToCNFPosBVGETBIT()
-
- void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs)
- {
- info[varphi]->clausespos = SINGLETON(varphi);
- } //End of convertFormulaToCNFPosSYMBOL()
-
- void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs)
- {
- convertFormulaToCNF(varphi[0], defs);
- info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg));
- reduceMemoryFootprintNeg(varphi[0]);
- } //End of convertFormulaToCNFPosNOT()
-
- void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (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++)
+ case SYMBOL:
{
- convertFormulaToCNF(*it, defs);
- INPLACE_UNION(psi, *(info[*it]->clausespos));
- reduceMemoryFootprintPos(*it);
+ convertFormulaToCNFNegSYMBOL(varphi, defs);
+ break;
}
-
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFPosAND()
-
- void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs)
- {
- bool renamesibs = false;
- ClauseList* clauses;
- ClauseList* psi;
- ClauseList* oldpsi;
-
- //****************************************
- // (pos) NAND ~> PRODUCT NOT
- //****************************************
-
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausesneg;
- if (clauses->size() > 1)
+ case NOT:
{
- renamesibs = true;
+ convertFormulaToCNFNegNOT(varphi, defs);
+ break;
}
- psi = COPY(*clauses);
- reduceMemoryFootprintNeg(*it);
-
- for (it++; it != varphi.GetChildren().end(); it++)
+ case AND:
{
- if (renamesibs)
- {
- setDoSibRenamingNeg(*(info[*it]));
- }
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausesneg;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- oldpsi = psi;
- psi = PRODUCT(*psi, *clauses);
- reduceMemoryFootprintNeg(*it);
- DELETE(oldpsi);
+ convertFormulaToCNFNegAND(varphi, defs);
+ break;
}
-
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFPosNAND()
-
- void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs)
- {
- bool renamesibs = false;
- ClauseList* clauses;
- ClauseList* psi;
- ClauseList* oldpsi;
-
- //****************************************
- // (pos) OR ~> PRODUCT
- //****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausespos;
- if (clauses->size() > 1)
+ case NAND:
{
- renamesibs = true;
+ convertFormulaToCNFNegNAND(varphi, defs);
+ break;
}
- psi = COPY(*clauses);
- reduceMemoryFootprintPos(*it);
-
- for (it++; it != varphi.GetChildren().end(); it++)
+ case OR:
{
- if (renamesibs)
- {
- setDoSibRenamingPos(*(info[*it]));
- }
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausespos;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- oldpsi = psi;
- psi = PRODUCT(*psi, *clauses);
- reduceMemoryFootprintPos(*it);
- DELETE(oldpsi);
+ convertFormulaToCNFNegOR(varphi, defs);
+ break;
}
-
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFPosOR()
-
- void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (pos) NOR ~> UNION NOT
- //****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- ClauseList* psi = COPY(*(info[*it]->clausesneg));
- reduceMemoryFootprintNeg(*it);
- for (it++; it != varphi.GetChildren().end(); it++)
+ case NOR:
{
- convertFormulaToCNF(*it, defs);
- INPLACE_UNION(psi, *(info[*it]->clausesneg));
- reduceMemoryFootprintNeg(*it);
+ convertFormulaToCNFNegNOR(varphi, defs);
+ break;
}
-
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFPosNOR()
-
- void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1]
- //****************************************
- CNFInfo* x0 = info[varphi[0]];
- CNFInfo* x1 = info[varphi[1]];
- convertFormulaToCNF(varphi[0], defs);
- if (x0->clausesneg->size() > 1)
+ case XOR:
{
- setDoSibRenamingPos(*x1);
+ convertFormulaToCNFNegXOR(varphi, defs);
+ break;
}
- convertFormulaToCNF(varphi[1], defs);
- ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
- reduceMemoryFootprintNeg(varphi[0]);
- reduceMemoryFootprintPos(varphi[1]);
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFPosIMPLIES()
-
- void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1])
- // ; (PRODUCT [0] ; [2])
- //****************************************
- CNFInfo* x0 = info[varphi[0]];
- CNFInfo* x1 = info[varphi[1]];
- CNFInfo* x2 = info[varphi[2]];
- convertFormulaToCNF(varphi[0], defs);
- if (x0->clausesneg->size() > 1)
+ case IMPLIES:
{
- setDoSibRenamingPos(*x1);
+ convertFormulaToCNFNegIMPLIES(varphi, defs);
+ break;
}
- convertFormulaToCNF(varphi[1], defs);
- if (x0->clausespos->size() > 1)
+ case ITE:
{
- setDoSibRenamingPos(*x2);
+ convertFormulaToCNFNegITE(varphi, defs);
+ break;
}
- convertFormulaToCNF(varphi[2], defs);
- ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
- ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos));
- NOCOPY_INPLACE_UNION(psi1, psi2);
- reduceMemoryFootprintNeg(varphi[0]);
- reduceMemoryFootprintPos(varphi[1]);
- reduceMemoryFootprintPos(varphi[0]);
- reduceMemoryFootprintPos(varphi[2]);
-
- info[varphi]->clausespos = psi1;
- } //End of convertFormulaToCNFPosITE()
-
- void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs)
- {
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- for (; it != varphi.GetChildren().end(); it++)
+ default:
{
- convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+ fprintf(stderr, "convertFormulaToCNFNegCases: doesn't handle kind %d\n", k);
+ FatalError("");
}
- ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
- info[varphi]->clausespos = psi;
- ASTVec::const_iterator it2 = varphi.GetChildren().begin();
- for (; it2 != varphi.GetChildren().end(); it2++){
- reduceMemoryFootprintPos(*it2);
- reduceMemoryFootprintNeg(*it2);
}
- } //End of convertFormulaToCNFPosXOR()
+ } //convertFormulaToCNFNegCases()
- ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
- {
+ //########################################
+ //########################################
+ // individual cnf conversion cases
- bool renamesibs;
- ClauseList* psi;
- ClauseList* psi1;
- ClauseList* psi2;
+ void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTVec psis;
- if (idx == varphi.GetChildren().size() - 2)
- {
- //****************************************
- // (pos) XOR ~> UNION
- // (PRODUCT [idx] ; [idx+1])
- // ; (PRODUCT NOT [idx] ; NOT [idx+1])
- //****************************************
- renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingPos(*info[varphi[idx + 1]]);
- }
- renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingNeg(*info[varphi[idx + 1]]);
- }
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ for (; it != varphi.GetChildren().end(); it++)
+ {
+ convertTermForCNF(*it, defs);
+ psis.push_back(*(info[*it]->termforcnf));
+ }
- psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos));
- psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg));
- NOCOPY_INPLACE_UNION(psi1, psi2);
+ info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis));
+ } //End of convertFormulaToCNFPosPred()
- psi = psi1;
- }
- else
- {
- //****************************************
- // (pos) XOR ~> UNION
- // (PRODUCT [idx] ; XOR [idx+1..])
- // ; (PRODUCT NOT [idx] ; NOT XOR [idx+1..])
- //****************************************
- ClauseList* theta1;
- theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs);
- renamesibs = theta1->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingPos(*info[varphi[idx]]);
- }
- ClauseList* theta2;
- theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs);
- renamesibs = theta2->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingNeg(*info[varphi[idx]]);
- }
+ void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+ info[varphi]->clausespos = SINGLETON(dummy_false_var);
+ } //End of convertFormulaToCNFPosFALSE()
- psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1);
- psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2);
- DELETE(theta1);
- DELETE(theta2);
- NOCOPY_INPLACE_UNION(psi1, psi2);
+ void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+ info[varphi]->clausespos = SINGLETON(dummy_true_var);
+ } //End of convertFormulaToCNFPosTRUE
- psi = psi1;
- }
+ void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs)
+ {
+ info[varphi]->clausespos = SINGLETON(varphi);
+ }//End of convertFormulaToCNFPosBVGETBIT()
- return psi;
- } //End of convertFormulaToCNFPosXORAux()
+ void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs)
+ {
+ info[varphi]->clausespos = SINGLETON(varphi);
+ } //End of convertFormulaToCNFPosSYMBOL()
- void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs)
- {
+ void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs)
+ {
+ convertFormulaToCNF(varphi[0], defs);
+ info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg));
+ reduceMemoryFootprintNeg(varphi[0]);
+ } //End of convertFormulaToCNFPosNOT()
- ASTVec psis;
+ void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (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);
+ INPLACE_UNION(psi, *(info[*it]->clausespos));
+ reduceMemoryFootprintPos(*it);
+ }
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- for (; it != varphi.GetChildren().end(); it++)
- {
- convertFormulaToCNF(*it, defs);
- psis.push_back(*(info[*it]->termforcnf));
- }
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosAND()
- info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis)));
- } //End of convertFormulaToCNFNegPred()
-
- void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs)
- {
- ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
- info[varphi]->clausesneg = SINGLETON(dummy_true_var);
- } //End of convertFormulaToCNFNegFALSE()
-
- void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs)
- {
- ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
- info[varphi]->clausesneg = SINGLETON(dummy_false_var);
- } //End of convertFormulaToCNFNegTRUE()
-
- void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs)
- {
- ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi));
- info[varphi]->clausesneg = psi;
- } //End of convertFormulaToCNFNegBVGETBIT()
-
- void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs)
- {
- info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi));
- } //End of convertFormulaToCNFNegSYMBOL()
-
- void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs)
- {
- convertFormulaToCNF(varphi[0], defs);
- info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos));
- reduceMemoryFootprintPos(varphi[0]);
- } //End of convertFormulaToCNFNegNOT()
-
- void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs)
- {
- bool renamesibs = false;
- ClauseList* clauses;
- ClauseList* psi;
- ClauseList* oldpsi;
-
- //****************************************
- // (neg) AND ~> PRODUCT NOT
- //****************************************
-
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausesneg;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- psi = COPY(*clauses);
- reduceMemoryFootprintNeg(*it);
+ void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs)
+ {
+ bool renamesibs = false;
+ ClauseList* clauses;
+ ClauseList* psi;
+ ClauseList* oldpsi;
+
+ //****************************************
+ // (pos) NAND ~> PRODUCT NOT
+ //****************************************
+
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausesneg;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ psi = COPY(*clauses);
+ reduceMemoryFootprintNeg(*it);
- for (it++; it != varphi.GetChildren().end(); it++)
- {
- if (renamesibs)
- {
- setDoSibRenamingNeg(*(info[*it]));
- }
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausesneg;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- oldpsi = psi;
- psi = PRODUCT(*psi, *clauses);
- reduceMemoryFootprintNeg(*it);
- DELETE(oldpsi);
- }
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*(info[*it]));
+ }
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausesneg;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ oldpsi = psi;
+ psi = PRODUCT(*psi, *clauses);
+ reduceMemoryFootprintNeg(*it);
+ DELETE(oldpsi);
+ }
- info[varphi]->clausesneg = psi;
- } //End of convertFormulaToCNFNegAND()
-
- void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (neg) NAND ~> UNION
- //****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- ClauseList* psi = COPY(*(info[*it]->clausespos));
- reduceMemoryFootprintPos(*it);
- for (it++; it != varphi.GetChildren().end(); it++)
- {
- convertFormulaToCNF(*it, defs);
- INPLACE_UNION(psi, *(info[*it]->clausespos));
- reduceMemoryFootprintPos(*it);
- }
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosNAND()
- info[varphi]->clausespos = psi;
- } //End of convertFormulaToCNFNegNAND()
-
- void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (neg) OR ~> UNION NOT
- //****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- ClauseList* psi = COPY(*(info[*it]->clausesneg));
- reduceMemoryFootprintNeg(*it);
- for (it++; it != varphi.GetChildren().end(); it++)
- {
- convertFormulaToCNF(*it, defs);
- INPLACE_UNION(psi, *(info[*it]->clausesneg));
- reduceMemoryFootprintNeg(*it);
- }
+ void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ bool renamesibs = false;
+ ClauseList* clauses;
+ ClauseList* psi;
+ ClauseList* oldpsi;
+
+ //****************************************
+ // (pos) OR ~> PRODUCT
+ //****************************************
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausespos;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ psi = COPY(*clauses);
+ reduceMemoryFootprintPos(*it);
- info[varphi]->clausesneg = psi;
- } //End of convertFormulaToCNFNegOR()
-
- void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs)
- {
- bool renamesibs = false;
- ClauseList* clauses;
- ClauseList* psi;
- ClauseList* oldpsi;
-
- //****************************************
- // (neg) NOR ~> PRODUCT
- //****************************************
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausespos;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- psi = COPY(*clauses);
- reduceMemoryFootprintPos(*it);
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*(info[*it]));
+ }
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausespos;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ oldpsi = psi;
+ psi = PRODUCT(*psi, *clauses);
+ reduceMemoryFootprintPos(*it);
+ DELETE(oldpsi);
+ }
- for (it++; it != varphi.GetChildren().end(); it++)
- {
- if (renamesibs)
- {
- setDoSibRenamingPos(*(info[*it]));
- }
- convertFormulaToCNF(*it, defs);
- clauses = info[*it]->clausespos;
- if (clauses->size() > 1)
- {
- renamesibs = true;
- }
- oldpsi = psi;
- psi = PRODUCT(*psi, *clauses);
- reduceMemoryFootprintPos(*it);
- DELETE(oldpsi);
- }
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosOR()
- info[varphi]->clausesneg = psi;
- } //End of convertFormulaToCNFNegNOR()
-
- void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (neg) IMPLIES ~> UNION [0] ; NOT [1]
- //****************************************
- CNFInfo* x0 = info[varphi[0]];
- CNFInfo* x1 = info[varphi[1]];
- convertFormulaToCNF(varphi[0], defs);
- convertFormulaToCNF(varphi[1], defs);
- ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg));
- info[varphi]->clausesneg = psi;
- reduceMemoryFootprintPos(varphi[0]);
- reduceMemoryFootprintNeg(varphi[1]);
- } //End of convertFormulaToCNFNegIMPLIES()
-
- void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs)
- {
- //****************************************
- // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1])
- // ; (PRODUCT [0] ; NOT [2])
- //****************************************
- CNFInfo* x0 = info[varphi[0]];
- CNFInfo* x1 = info[varphi[1]];
- CNFInfo* x2 = info[varphi[2]];
- convertFormulaToCNF(varphi[0], defs);
- if (x0->clausesneg->size() > 1)
- {
- setDoSibRenamingNeg(*x1);
- }
- convertFormulaToCNF(varphi[1], defs);
- if (x0->clausespos->size() > 1)
- {
- setDoSibRenamingNeg(*x2);
- }
- convertFormulaToCNF(varphi[2], defs);
- ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg));
- ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg));
- NOCOPY_INPLACE_UNION(psi1, psi2);
- reduceMemoryFootprintNeg(varphi[0]);
- reduceMemoryFootprintNeg(varphi[1]);
- reduceMemoryFootprintPos(varphi[0]);
- reduceMemoryFootprintNeg(varphi[2]);
-
- info[varphi]->clausesneg = psi1;
- } //End of convertFormulaToCNFNegITE()
-
- void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs)
- {
- ASTVec::const_iterator it = varphi.GetChildren().begin();
- for (; it != varphi.GetChildren().end(); it++)
- {
- convertFormulaToCNF(*it, defs); // make pos and neg clause sets
- }
- ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs);
- info[varphi]->clausesneg = psi;
- ASTVec::const_iterator it2 = varphi.GetChildren().begin();
- for (; it2 != varphi.GetChildren().end(); it2++){
- reduceMemoryFootprintPos(*it2);
- reduceMemoryFootprintNeg(*it2);
- }
- } //End of convertFormulaToCNFNegXOR()
-
- ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
- {
- bool renamesibs;
- ClauseList* psi;
- ClauseList* psi1;
- ClauseList* psi2;
-
- if (idx == varphi.GetChildren().size() - 2)
- {
+ void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (pos) NOR ~> UNION NOT
+ //****************************************
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ ClauseList* psi = COPY(*(info[*it]->clausesneg));
+ reduceMemoryFootprintNeg(*it);
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs);
+ INPLACE_UNION(psi, *(info[*it]->clausesneg));
+ reduceMemoryFootprintNeg(*it);
+ }
- //****************************************
- // (neg) XOR ~> UNION
- // (PRODUCT NOT [idx] ; [idx+1])
- // ; (PRODUCT [idx] ; NOT [idx+1])
- //****************************************
- convertFormulaToCNF(varphi[idx], defs);
- renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingPos(*info[varphi[idx + 1]]);
- }
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosNOR()
- convertFormulaToCNF(varphi[idx], defs);
- renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingNeg(*info[varphi[idx + 1]]);
- }
+ void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1]
+ //****************************************
+ CNFInfo* x0 = info[varphi[0]];
+ CNFInfo* x1 = info[varphi[1]];
+ convertFormulaToCNF(varphi[0], defs);
+ if (x0->clausesneg->size() > 1)
+ {
+ setDoSibRenamingPos(*x1);
+ }
+ convertFormulaToCNF(varphi[1], defs);
+ ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
+ reduceMemoryFootprintNeg(varphi[0]);
+ reduceMemoryFootprintPos(varphi[1]);
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFPosIMPLIES()
+
+ void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1])
+ // ; (PRODUCT [0] ; [2])
+ //****************************************
+ CNFInfo* x0 = info[varphi[0]];
+ CNFInfo* x1 = info[varphi[1]];
+ CNFInfo* x2 = info[varphi[2]];
+ convertFormulaToCNF(varphi[0], defs);
+ if (x0->clausesneg->size() > 1)
+ {
+ setDoSibRenamingPos(*x1);
+ }
+ convertFormulaToCNF(varphi[1], defs);
+ if (x0->clausespos->size() > 1)
+ {
+ setDoSibRenamingPos(*x2);
+ }
+ convertFormulaToCNF(varphi[2], defs);
+ ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos));
+ ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos));
+ NOCOPY_INPLACE_UNION(psi1, psi2);
+ reduceMemoryFootprintNeg(varphi[0]);
+ reduceMemoryFootprintPos(varphi[1]);
+ reduceMemoryFootprintPos(varphi[0]);
+ reduceMemoryFootprintPos(varphi[2]);
+
+ info[varphi]->clausespos = psi1;
+ } //End of convertFormulaToCNFPosITE()
+
+ void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ for (; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+ }
+ ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs);
+ info[varphi]->clausespos = psi;
+ ASTVec::const_iterator it2 = varphi.GetChildren().begin();
+ for (; it2 != varphi.GetChildren().end(); it2++){
+ reduceMemoryFootprintPos(*it2);
+ reduceMemoryFootprintNeg(*it2);
+ }
+ } //End of convertFormulaToCNFPosXOR()
- psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos));
- psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg));
- NOCOPY_INPLACE_UNION(psi1, psi2);
+ ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
+ {
- psi = psi1;
- }
- else
- {
- //****************************************
- // (neg) XOR ~> UNION
- // (PRODUCT NOT [idx] ; XOR [idx+1..])
- // ; (PRODUCT [idx] ; NOT XOR [idx+1..])
- //****************************************
- ClauseList* theta1;
- theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs);
- renamesibs = theta1->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingNeg(*info[varphi[idx]]);
- }
- convertFormulaToCNF(varphi[idx], defs);
+ bool renamesibs;
+ ClauseList* psi;
+ ClauseList* psi1;
+ ClauseList* psi2;
- ClauseList* theta2;
- theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs);
- renamesibs = theta2->size() > 1 ? true : false;
- if (renamesibs)
- {
- setDoSibRenamingPos(*info[varphi[idx]]);
- }
+ if (idx == varphi.GetChildren().size() - 2)
+ {
+ //****************************************
+ // (pos) XOR ~> UNION
+ // (PRODUCT [idx] ; [idx+1])
+ // ; (PRODUCT NOT [idx] ; NOT [idx+1])
+ //****************************************
+ renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*info[varphi[idx + 1]]);
+ }
+ renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*info[varphi[idx + 1]]);
+ }
- psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1);
- psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2);
- DELETE(theta1);
- DELETE(theta2);
- NOCOPY_INPLACE_UNION(psi1, psi2);
+ psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausespos));
+ psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausesneg));
+ NOCOPY_INPLACE_UNION(psi1, psi2);
- psi = psi1;
- }
+ psi = psi1;
+ }
+ else
+ {
+ //****************************************
+ // (pos) XOR ~> UNION
+ // (PRODUCT [idx] ; XOR [idx+1..])
+ // ; (PRODUCT NOT [idx] ; NOT XOR [idx+1..])
+ //****************************************
+ ClauseList* theta1;
+ theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs);
+ renamesibs = theta1->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*info[varphi[idx]]);
+ }
+ ClauseList* theta2;
+ theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs);
+ renamesibs = theta2->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*info[varphi[idx]]);
+ }
+
+ psi1 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta1);
+ psi2 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta2);
+ DELETE(theta1);
+ DELETE(theta2);
+ NOCOPY_INPLACE_UNION(psi1, psi2);
+
+ psi = psi1;
+ }
+
+ return psi;
+ } //End of convertFormulaToCNFPosXORAux()
+
+ void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs)
+ {
+
+ ASTVec psis;
+
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ for (; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs);
+ psis.push_back(*(info[*it]->termforcnf));
+ }
+
+ info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis)));
+ } //End of convertFormulaToCNFNegPred()
+
+ void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+ info[varphi]->clausesneg = SINGLETON(dummy_true_var);
+ } //End of convertFormulaToCNFNegFALSE()
+
+ void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
+ info[varphi]->clausesneg = SINGLETON(dummy_false_var);
+ } //End of convertFormulaToCNFNegTRUE()
+
+ void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs)
+ {
+ ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi));
+ info[varphi]->clausesneg = psi;
+ } //End of convertFormulaToCNFNegBVGETBIT()
+
+ void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs)
+ {
+ info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi));
+ } //End of convertFormulaToCNFNegSYMBOL()
+
+ void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs)
+ {
+ convertFormulaToCNF(varphi[0], defs);
+ info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos));
+ reduceMemoryFootprintPos(varphi[0]);
+ } //End of convertFormulaToCNFNegNOT()
+
+ void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs)
+ {
+ bool renamesibs = false;
+ ClauseList* clauses;
+ ClauseList* psi;
+ ClauseList* oldpsi;
+
+ //****************************************
+ // (neg) AND ~> PRODUCT NOT
+ //****************************************
+
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausesneg;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ psi = COPY(*clauses);
+ reduceMemoryFootprintNeg(*it);
+
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*(info[*it]));
+ }
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausesneg;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ oldpsi = psi;
+ psi = PRODUCT(*psi, *clauses);
+ reduceMemoryFootprintNeg(*it);
+ DELETE(oldpsi);
+ }
+
+ info[varphi]->clausesneg = psi;
+ } //End of convertFormulaToCNFNegAND()
+
+ void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (neg) NAND ~> UNION
+ //****************************************
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ ClauseList* psi = COPY(*(info[*it]->clausespos));
+ reduceMemoryFootprintPos(*it);
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs);
+ INPLACE_UNION(psi, *(info[*it]->clausespos));
+ reduceMemoryFootprintPos(*it);
+ }
- return psi;
- } //End of convertFormulaToCNFNegXORAux()
+ info[varphi]->clausespos = psi;
+ } //End of convertFormulaToCNFNegNAND()
+
+ void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (neg) OR ~> UNION NOT
+ //****************************************
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ ClauseList* psi = COPY(*(info[*it]->clausesneg));
+ reduceMemoryFootprintNeg(*it);
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs);
+ INPLACE_UNION(psi, *(info[*it]->clausesneg));
+ reduceMemoryFootprintNeg(*it);
+ }
+
+ info[varphi]->clausesneg = psi;
+ } //End of convertFormulaToCNFNegOR()
+
+ void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ bool renamesibs = false;
+ ClauseList* clauses;
+ ClauseList* psi;
+ ClauseList* oldpsi;
+
+ //****************************************
+ // (neg) NOR ~> PRODUCT
+ //****************************************
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausespos;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ psi = COPY(*clauses);
+ reduceMemoryFootprintPos(*it);
+
+ for (it++; it != varphi.GetChildren().end(); it++)
+ {
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*(info[*it]));
+ }
+ convertFormulaToCNF(*it, defs);
+ clauses = info[*it]->clausespos;
+ if (clauses->size() > 1)
+ {
+ renamesibs = true;
+ }
+ oldpsi = psi;
+ psi = PRODUCT(*psi, *clauses);
+ reduceMemoryFootprintPos(*it);
+ DELETE(oldpsi);
+ }
+
+ info[varphi]->clausesneg = psi;
+ } //End of convertFormulaToCNFNegNOR()
+
+ void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (neg) IMPLIES ~> UNION [0] ; NOT [1]
+ //****************************************
+ CNFInfo* x0 = info[varphi[0]];
+ CNFInfo* x1 = info[varphi[1]];
+ convertFormulaToCNF(varphi[0], defs);
+ convertFormulaToCNF(varphi[1], defs);
+ ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg));
+ info[varphi]->clausesneg = psi;
+ reduceMemoryFootprintPos(varphi[0]);
+ reduceMemoryFootprintNeg(varphi[1]);
+ } //End of convertFormulaToCNFNegIMPLIES()
+
+ void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs)
+ {
+ //****************************************
+ // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1])
+ // ; (PRODUCT [0] ; NOT [2])
+ //****************************************
+ CNFInfo* x0 = info[varphi[0]];
+ CNFInfo* x1 = info[varphi[1]];
+ CNFInfo* x2 = info[varphi[2]];
+ convertFormulaToCNF(varphi[0], defs);
+ if (x0->clausesneg->size() > 1)
+ {
+ setDoSibRenamingNeg(*x1);
+ }
+ convertFormulaToCNF(varphi[1], defs);
+ if (x0->clausespos->size() > 1)
+ {
+ setDoSibRenamingNeg(*x2);
+ }
+ convertFormulaToCNF(varphi[2], defs);
+ ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg));
+ ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg));
+ NOCOPY_INPLACE_UNION(psi1, psi2);
+ reduceMemoryFootprintNeg(varphi[0]);
+ reduceMemoryFootprintNeg(varphi[1]);
+ reduceMemoryFootprintPos(varphi[0]);
+ reduceMemoryFootprintNeg(varphi[2]);
+
+ info[varphi]->clausesneg = psi1;
+ } //End of convertFormulaToCNFNegITE()
+
+ void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs)
+ {
+ ASTVec::const_iterator it = varphi.GetChildren().begin();
+ for (; it != varphi.GetChildren().end(); it++)
+ {
+ convertFormulaToCNF(*it, defs); // make pos and neg clause sets
+ }
+ ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs);
+ info[varphi]->clausesneg = psi;
+ ASTVec::const_iterator it2 = varphi.GetChildren().begin();
+ for (; it2 != varphi.GetChildren().end(); it2++){
+ reduceMemoryFootprintPos(*it2);
+ reduceMemoryFootprintNeg(*it2);
+ }
+ } //End of convertFormulaToCNFNegXOR()
+
+ ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs)
+ {
+ bool renamesibs;
+ ClauseList* psi;
+ ClauseList* psi1;
+ ClauseList* psi2;
+
+ if (idx == varphi.GetChildren().size() - 2)
+ {
+
+ //****************************************
+ // (neg) XOR ~> UNION
+ // (PRODUCT NOT [idx] ; [idx+1])
+ // ; (PRODUCT [idx] ; NOT [idx+1])
+ //****************************************
+ convertFormulaToCNF(varphi[idx], defs);
+ renamesibs = (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*info[varphi[idx + 1]]);
+ }
+
+ convertFormulaToCNF(varphi[idx], defs);
+ renamesibs = (info[varphi[idx]]->clausespos)->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*info[varphi[idx + 1]]);
+ }
+
+ psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *(info[varphi[idx + 1]]->clausespos));
+ psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *(info[varphi[idx + 1]]->clausesneg));
+ NOCOPY_INPLACE_UNION(psi1, psi2);
+
+ psi = psi1;
+ }
+ else
+ {
+ //****************************************
+ // (neg) XOR ~> UNION
+ // (PRODUCT NOT [idx] ; XOR [idx+1..])
+ // ; (PRODUCT [idx] ; NOT XOR [idx+1..])
+ //****************************************
+ ClauseList* theta1;
+ theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs);
+ renamesibs = theta1->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingNeg(*info[varphi[idx]]);
+ }
+ convertFormulaToCNF(varphi[idx], defs);
+
+ ClauseList* theta2;
+ theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs);
+ renamesibs = theta2->size() > 1 ? true : false;
+ if (renamesibs)
+ {
+ setDoSibRenamingPos(*info[varphi[idx]]);
+ }
+
+ psi1 = PRODUCT(*(info[varphi[idx]]->clausesneg), *theta1);
+ psi2 = PRODUCT(*(info[varphi[idx]]->clausespos), *theta2);
+ DELETE(theta1);
+ DELETE(theta2);
+ NOCOPY_INPLACE_UNION(psi1, psi2);
+
+ psi = psi1;
+ }
+
+ return psi;
+ } //End of convertFormulaToCNFNegXORAux()
//########################################
//########################################
// utilities for reclaiming memory.
- void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi)
- {
- CNFInfo* x = info[varphi];
- if (sharesPos(*x) == 1)
- {
- DELETE(x->clausespos);
- x->clausespos = NULL;
- if (x->clausesneg == NULL)
- {
- delete x;
- info.erase(varphi);
- }
- }
- } //End of reduceMemoryFootprintPos()
+ void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi)
+ {
+ CNFInfo* x = info[varphi];
+ if (sharesPos(*x) == 1)
+ {
+ DELETE(x->clausespos);
+ x->clausespos = NULL;
+ if (x->clausesneg == NULL)
+ {
+ delete x;
+ info.erase(varphi);
+ }
+ }
+ } //End of reduceMemoryFootprintPos()
- void CNFMgr::reduceMemoryFootprintNeg(const ASTNode& varphi)
- {
- CNFInfo* x = info[varphi];
- if (sharesNeg(*x) == 1)
- {
- DELETE(x->clausesneg);
- x->clausesneg = NULL;
- if (x->clausespos == NULL)
- {
- delete x;
- info.erase(varphi);
- }
- }
- } //End of reduceMemoryFootprintNeg()
+ void CNFMgr::reduceMemoryFootprintNeg(const ASTNode& varphi)
+ {
+ CNFInfo* x = info[varphi];
+ if (sharesNeg(*x) == 1)
+ {
+ DELETE(x->clausesneg);
+ x->clausesneg = NULL;
+ if (x->clausespos == NULL)
+ {
+ delete x;
+ info.erase(varphi);
+ }
+ }
+ } //End of reduceMemoryFootprintNeg()
//########################################
//########################################
- ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi)
- {
- ASTNode* psi;
+ ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi)
+ {
+ ASTNode* psi;
- if (store.find(varphi) != store.end())
- {
- psi = store[varphi];
- }
- else
- {
- psi = new ASTNode(varphi);
- store[varphi] = psi;
- }
+ if (store.find(varphi) != store.end())
+ {
+ psi = store[varphi];
+ }
+ else
+ {
+ psi = new ASTNode(varphi);
+ store[varphi] = psi;
+ }
- return psi;
- } //End of ASTNodeToASTNodePtr()
+ return psi;
+ } //End of ASTNodeToASTNodePtr()
//########################################
//########################################
- void CNFMgr::cleanup(const ASTNode& varphi)
- {
- delete info[varphi]->clausespos;
- CNFInfo* toDelete = info[varphi]; // get the thing to delete.
- info.erase(varphi); // remove it from the hashtable
- delete toDelete;
+ void CNFMgr::cleanup(const ASTNode& varphi)
+ {
+ delete info[varphi]->clausespos;
+ CNFInfo* toDelete = info[varphi]; // get the thing to delete.
+ info.erase(varphi); // remove it from the hashtable
+ delete toDelete;
- ASTNodeToCNFInfoMap::const_iterator it1 = info.begin();
- for (; it1 != info.end(); it1++)
- {
- CNFInfo* x = it1->second;
- if (x->clausespos != NULL)
- {
- DELETE(x->clausespos);
- }
- if (x->clausesneg != NULL)
- {
- if (!isTerm(*x))
- {
- DELETE(x->clausesneg);
- }
- }
- delete x;
- }
+ ASTNodeToCNFInfoMap::const_iterator it1 = info.begin();
+ for (; it1 != info.end(); it1++)
+ {
+ CNFInfo* x = it1->second;
+ if (x->clausespos != NULL)
+ {
+ DELETE(x->clausespos);
+ }
+ if (x->clausesneg != NULL)
+ {
+ if (!isTerm(*x))
+ {
+ DELETE(x->clausesneg);
+ }
+ }
+ delete x;
+ }
- info.clear();
- } //End of cleanup()
+ info.clear();
+ } //End of cleanup()
//########################################
//########################################
// constructor
- CNFMgr::CNFMgr(STPMgr *bmgr)
- {
- bm = bmgr;
- }
+ CNFMgr::CNFMgr(STPMgr *bmgr)
+ {
+ bm = bmgr;
+ }
- //########################################
- //########################################
- // destructor
+ //########################################
+ //########################################
+ // destructor
CNFMgr::~CNFMgr()
{
ASTNodeToASTNodePtrMap::const_iterator it1 = store.begin();
for (; it1 != store.end(); it1++)
{
- delete it1->second;
+ delete it1->second;
}
store.clear();
}
- //########################################
- //########################################
- // top-level conversion function
-
- ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi)
- {
- bm->GetRunTimes()->start(RunTimes::CNFConversion);
- scanFormula(varphi, true);
- ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
- ClauseList* defs = SINGLETON(dummy_true_var);
- convertFormulaToCNF(varphi, defs);
- ClauseList* top = info[varphi]->clausespos;
- defs->insert(defs->begin() + 1, top->begin(), top->end());
-
- cleanup(varphi);
- bm->GetRunTimes()->stop(RunTimes::CNFConversion);
- return defs;
- }//End of convertToCNF()
-
- void CNFMgr::DELETE(ClauseList* varphi)
- {
- ClauseList::const_iterator it = varphi->begin();
- for (; it != varphi->end(); it++)
- {
- delete *it;
- }
+ //########################################
+ //########################################
+ // top-level conversion function
+
+ ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi)
+ {
+ bm->GetRunTimes()->start(RunTimes::CNFConversion);
+ scanFormula(varphi, true);
+ ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*");
+ ClauseList* defs = SINGLETON(dummy_true_var);
+ convertFormulaToCNF(varphi, defs);
+ ClauseList* top = info[varphi]->clausespos;
+ defs->insert(defs->begin() + 1, top->begin(), top->end());
+
+ cleanup(varphi);
+ bm->GetRunTimes()->stop(RunTimes::CNFConversion);
+ return defs;
+ }//End of convertToCNF()
+
+ void CNFMgr::DELETE(ClauseList* varphi)
+ {
+ ClauseList::const_iterator it = varphi->begin();
+ for (; it != varphi->end(); it++)
+ {
+ delete *it;
+ }
- delete varphi;
- } //End of DELETE()
+ delete varphi;
+ } //End of DELETE()
} // end namespace BEEV
satSolverClause.capacity((*i)->size());
//now iterate through the internals of the ASTclause itself
- vector<const ASTNode*>::const_iterator j = (*i)->begin(), jend = (*i)->end();
+ vector<const ASTNode*>::const_iterator j = (*i)->begin();
+ vector<const ASTNode*>::const_iterator jend = (*i)->end();
+
//j is a disjunct in the ASTclause (*i)
for (; j != jend; j++)
{
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
return false;
}
- }
+ }
bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
//PrintActivityLevels_Of_SATVars("Before SAT:",newS);
//ChangeActivityLevels_Of_SATVars(newS);
- //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS);
- //newS.solve();
+ //PrintActivityLevels_Of_SATVars("Before SAT and after initial
+ //bias:",newS); newS.solve();
bm->GetRunTimes()->start(RunTimes::Solving);
newS.solve();
return false;
} //end of toSATandSolve()
- // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment.
- // Returns ASTTrue if true, ASTFalse if false or undefined.
+ // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying
+ // assignment. Returns ASTTrue if true, ASTFalse if false or
+ // undefined.
ASTNode ToSAT::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form)
{
MINISAT::Var satvar = _ASTNode_to_SATVar_Map[form];
// variable in ASTClause a new MINISAT::Var is created (these vars
// typedefs for ints)
typedef HASHMAP<
- ASTNode,
- MINISAT::Var,
- ASTNode::ASTNodeHasher,
- ASTNode::ASTNodeEqual> ASTtoSATMap;
+ ASTNode,
+ MINISAT::Var,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTtoSATMap;
ASTtoSATMap _ASTNode_to_SATVar_Map;
// MAP: This is a map from MINISAT::Vars to ASTNodes
//looksup a MINISAT var from the minisat-var memo-table. if none
//exists, then creates one. Treat the result as const.
MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S,
- const ASTNode& n);
+ const ASTNode& n);
// Evaluates bitblasted formula in satisfying assignment
ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form);
// Bitblasts, CNF conversion and calls toSATandSolve()
bool CallSAT(MINISAT::Solver& SatSolver,
- const ASTNode& modified_input,
- const ASTNode& original_input);
+ const ASTNode& modified_input,
+ const ASTNode& original_input);
// Converts the clause to SAT and calls SAT solver
bool toSATandSolve(MINISAT::Solver& S, ClauseList& cll);
projects / francis / stp.git / commitdiff