return lvp;
}
-/*****************************************************************
- * INLINE METHODS from various classed, declared here because of
- * dependencies on classes that are declared later.
- *****************************************************************/
-// ASTNode accessor function.
-inline Kind ASTNode::GetKind() const
-{
- //cout << "GetKind: " << _int_node_ptr;
- return _int_node_ptr->GetKind();
-}
-
-// FIXME: should be const ASTVec const?
-// Declared here because of same ordering problem as GetKind.
-inline const ASTVec &ASTNode::GetChildren() const
-{
- return _int_node_ptr->GetChildren();
-}
-
-// Access node number
-inline int ASTNode::GetNodeNum() const
-{
- return _int_node_ptr->_node_num;
-}
-
-inline unsigned int ASTNode::GetIndexWidth() const
-{
- return _int_node_ptr->_index_width;
-}
-
-inline void ASTNode::SetIndexWidth(unsigned int iw) const
-{
- _int_node_ptr->_index_width = iw;
-}
-
-inline unsigned int ASTNode::GetValueWidth() const
-{
- return _int_node_ptr->_value_width;
-}
-
-inline void ASTNode::SetValueWidth(unsigned int vw) const
-{
- _int_node_ptr->_value_width = vw;
-}
-
-//return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2
-//iff ARRAY; 3 iff UNKNOWN;
-inline types ASTNode::GetType() const
-{
- if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN
- return BOOLEAN_TYPE;
- if ((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR
- return BITVECTOR_TYPE;
- if ((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY
- return ARRAY_TYPE;
- return UNKNOWN_TYPE;
-}
-
-// Constructor; creates a new pointer, increments refcount of
-// pointed-to object.
-inline ASTNode::ASTNode(ASTInternal *in) :
- _int_node_ptr(in)
-{
- if (in)
- in->IncRef();
-}
-
-// Assignment. Increment refcount of new value, decrement refcount of
-// old value and destroy if this was the last pointer. FIXME:
-// accelerate this by creating an intnode with a ref counter instead
-// of pointing to NULL. Need a special check in CleanUp to make sure
-// the null node never gets freed.
-
-inline ASTNode& ASTNode::operator=(const ASTNode& n)
-{
- if (n._int_node_ptr)
- {
- n._int_node_ptr->IncRef();
- }
- if (_int_node_ptr)
- {
- _int_node_ptr->DecRef();
- }
- _int_node_ptr = n._int_node_ptr;
- return *this;
-}
-
-inline void ASTInternal::DecRef()
-{
- if (--_ref_count == 0)
- {
- // Delete node from unique table and kill it.
- CleanUp();
- }
-}
-
-// Destructor
-inline ASTNode::~ASTNode()
-{
- if (_int_node_ptr)
- {
- _int_node_ptr->DecRef();
- }
-}
-
-inline BeevMgr& ASTNode::GetBeevMgr() const
-{
- return _int_node_ptr->_bm;
-}
-
/***************************************************************************
* Class BeevMgr. This holds all "global" variables for the system, such as
* unique tables for the various kinds of nodes.
int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input);
- int Expand_A_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap);
+ int Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap);
ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody,
ASTNodeMap* VarConstMap);
return e;
}
}
-};
+};//end of Class CompleteCounterExample
+
+
+/*****************************************************************
+ * INLINE METHODS from various classed, declared here because of
+ * dependencies on classes that are declared later.
+ *****************************************************************/
+// ASTNode accessor function.
+inline Kind ASTNode::GetKind() const
+{
+ //cout << "GetKind: " << _int_node_ptr;
+ return _int_node_ptr->GetKind();
+}
+
+// FIXME: should be const ASTVec const?
+// Declared here because of same ordering problem as GetKind.
+inline const ASTVec &ASTNode::GetChildren() const
+{
+ return _int_node_ptr->GetChildren();
+}
+
+// Access node number
+inline int ASTNode::GetNodeNum() const
+{
+ return _int_node_ptr->_node_num;
+}
+
+inline unsigned int ASTNode::GetIndexWidth() const
+{
+ return _int_node_ptr->_index_width;
+}
+
+inline void ASTNode::SetIndexWidth(unsigned int iw) const
+{
+ _int_node_ptr->_index_width = iw;
+}
+
+inline unsigned int ASTNode::GetValueWidth() const
+{
+ return _int_node_ptr->_value_width;
+}
+
+inline void ASTNode::SetValueWidth(unsigned int vw) const
+{
+ _int_node_ptr->_value_width = vw;
+}
+
+//return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2
+//iff ARRAY; 3 iff UNKNOWN;
+inline types ASTNode::GetType() const
+{
+ if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN
+ return BOOLEAN_TYPE;
+ if ((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR
+ return BITVECTOR_TYPE;
+ if ((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY
+ return ARRAY_TYPE;
+ return UNKNOWN_TYPE;
+}
+
+// Constructor; creates a new pointer, increments refcount of
+// pointed-to object.
+inline ASTNode::ASTNode(ASTInternal *in) :
+ _int_node_ptr(in)
+{
+ if (in)
+ in->IncRef();
+}
+
+// Assignment. Increment refcount of new value, decrement refcount of
+// old value and destroy if this was the last pointer. FIXME:
+// accelerate this by creating an intnode with a ref counter instead
+// of pointing to NULL. Need a special check in CleanUp to make sure
+// the null node never gets freed.
+
+inline ASTNode& ASTNode::operator=(const ASTNode& n)
+{
+ if (n._int_node_ptr)
+ {
+ n._int_node_ptr->IncRef();
+ }
+ if (_int_node_ptr)
+ {
+ _int_node_ptr->DecRef();
+ }
+ _int_node_ptr = n._int_node_ptr;
+ return *this;
+}
+
+inline void ASTInternal::DecRef()
+{
+ if (--_ref_count == 0)
+ {
+ // Delete node from unique table and kill it.
+ CleanUp();
+ }
+}
+
+// Destructor
+inline ASTNode::~ASTNode()
+{
+ if (_int_node_ptr)
+ {
+ _int_node_ptr->DecRef();
+ }
+}
+
+inline BeevMgr& ASTNode::GetBeevMgr() const
+{
+ return _int_node_ptr->_bm;
+}
//Return the unsigned constant value of the input 'n'
inline unsigned int GetUnsignedConst(const ASTNode n)
/*
* For each 'finiteloop' in the global list 'List_Of_FiniteLoops'
*
- * Expand_A_FiniteLoop(finiteloop);
+ * Expand_FiniteLoop(finiteloop);
*
- * The 'Expand_A_FiniteLoop' function expands the 'finiteloop' in a
+ * 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
*/
}
-int BeevMgr::Expand_A_FiniteLoop(const ASTNode& finiteloop,
- ASTNodeMap* ParamToCurrentValMap) {
+int BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop,
+ ASTNodeMap* ParamToCurrentValMap) {
/*
* 'finiteloop' is the finite loop to be expanded
*
* Every finiteloop has three parts:
*
+ * 0) Parameter Name
+ *
* 1) Parameter initialization
*
* 2) Parameter limit value
*
- * 3) Formula Body (This can be a NESTED for loop)
- *
- * 4) Increment formula
- *
- * Each entry of the parameter_stack contains the following:
- *
- * 1. Current parameter name
- *
- * 2. Initial value of the parameter
- *
- * 3. Limit value of the parameter
- *
- * 4. Increment value
- *
- * If parameter_stack is empty then it means that we are at the
- * start of expanding this finite loop
+ * 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
*
* 3.2: We have SAT, and it is indeed a satisfying model
*/
- //0th element of FOR-construct stores the initial parameter value
- int paramInitValue = finiteloop[0].GetUnsignedConst();
-}
+ //Make sure that the parameter is a variable
+ ASTNode parameter = finiteloop[0];
+ int paramInit = GetUnsignedConst(finiteloop[1]);
+ int paramLimit = GetUnsignedConst(finiteloop[2]);
+ int paramIncrement = GetUnsignedConst(finiteloop[3]);
+ ASTNode formulabody = finiteloop[4];
+ int paramCurrentValue = paramInit;
+
+ //Update ParamToCurrentValMap with parameter and its current
+ //value. Here paramCurrentValue is the initial value
+ unsigned width = 32;
+ (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+
+ //Go recursively thru' all the FOR-constructs.
+ if(FOR == formulabody.GetKind()) {
+ while(paramCurrentValue < paramLimit) {
+ Expand_FiniteLoop(formulabody, ParamToCurrentValMap);
+ paramCurrentValue = paramCurrentValue + paramIncrement;
+
+ //Update ParamToCurrentValMap with parameter and its current
+ //value
+ //
+ //FIXME: Possible leak since I am not freeing the previous
+ //'value' for the same 'key'
+ (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ } //end of While
+ }
+ else {
+ //Expand the leaf level FOR-construct completely
+ for(;
+ paramCurrentValue < paramLimit;
+ paramCurrentValue = paramCurrentValue + paramIncrement) {
+ ASTNode currentformula =
+ FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap);
+
+ //Check the currentformula against the model, and add it to the
+ //SAT solver if it is false against the model
+
+ //Update ParamToCurrentValMap with parameter and its current
+ //value
+ //
+ //FIXME: Possible leak since I am not freeing the previous
+ //'value' for the same 'key'
+ (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ }
+ } //end of else
+} //end of the Expand_FiniteLoop()
ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody,
ASTNodeMap* VarToConstantMap)
* variable-to-constant map 'VarToConstantMap'
*/
return SimplifyFormula(formulabody, VarToConstantMap);
-}
+} //end of FiniteLoop_Extract_SingleFormula()
//FUNCTION: this function accepts a boolvector and returns a BVConst
projects / francis / stp.git / commitdiff