From: vijay_ganesh Date: Thu, 3 Sep 2009 17:38:12 +0000 (+0000) Subject: lots of small useful edits. Has some untested FOR-construct code as well X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e35129d4329bb07d55754f7cb00cdb9c075ed830;p=francis%2Fstp.git lots of small useful edits. Has some untested FOR-construct code as well git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@172 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/README b/README index 4463d6e..ab02b5c 100644 --- a/README +++ b/README @@ -38,3 +38,12 @@ PAPERS ----- http://sites.google.com/site/stpfastprover +REGRESSIONS +----------- + +Assumes you have downloaded the testcases + +make regressall +make regress_smt +make regress_c_api +make regressbigarray \ No newline at end of file diff --git a/src/AST/AST.h b/src/AST/AST.h index dc315ca..9e568b0 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -904,115 +904,6 @@ inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0) 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. @@ -1382,7 +1273,7 @@ public: 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); @@ -1792,7 +1683,117 @@ public: 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) diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 8615ece..bb9be9c 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -1429,9 +1429,9 @@ int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, /* * 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 @@ -1445,34 +1445,26 @@ int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, */ } -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 * @@ -1505,9 +1497,53 @@ int BeevMgr::Expand_A_FiniteLoop(const ASTNode& finiteloop, * 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) @@ -1517,7 +1553,7 @@ ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody, * variable-to-constant map 'VarToConstantMap' */ return SimplifyFormula(formulabody, VarToConstantMap); -} +} //end of FiniteLoop_Extract_SingleFormula() //FUNCTION: this function accepts a boolvector and returns a BVConst diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h index a6c7d90..19829e9 100644 --- a/src/AST/printer/printers.h +++ b/src/AST/printer/printers.h @@ -16,6 +16,7 @@ ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0); + } #endif /* PRINTERS_H_ */ diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 3d48dfd..e5dbbca 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -1324,7 +1324,7 @@ unsigned long long int getBVUnsignedLongLong(Expr e) { nodestar a = (nodestar)e; if(BEEV::BVCONST != a->GetKind()) - BEEV::FatalError("getBVUnsigned: Attempting to extract int value"\ + BEEV::FatalError("getBVUnsigned: Attempting to extract int value"\ "from a NON-constant BITVECTOR: ",*a); unsigned* bv = a->GetBVConst();