diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-13 18:08:49 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-13 18:08:49 -0600 |
| commit | 6f6708083a6b57243fd59ceb1a783ad65b086550 (patch) | |
| tree | a534aa3c8d1cc98ddbecf60f537d5351f57e18b0 /src/smt | |
| parent | 2e1d725478eb24433eaf0f70822550966ef53d3d (diff) | |
fix expanding def
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 52 |
1 files changed, 48 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8754dc084..ef4f01cd1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -310,7 +310,7 @@ class SmtEnginePrivate : public NodeManagerListener { * Function symbol used to implement uninterpreted undefined string * semantics. Needed to deal with partial charat/substr function. */ - //Node d_substrUndef; + Node d_ufSubstr; /** * Function symbol used to implement uninterpreted division-by-zero @@ -1555,9 +1555,53 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF node = expandBVDivByZero(node); break; - //case kind::STRING_CHARAT: - //case kind::STRING_SUBSTR: - + case kind::STRING_CHARAT: { + if(d_ufSubstr.isNull()) { + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->stringType()), + "uf substr", + NodeManager::SKOLEM_EXACT_NAME); + } + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero); + Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); + Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one); + node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + break; + } + case kind::STRING_SUBSTR: { + if(d_ufSubstr.isNull()) { + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->stringType()), + "uf substr", + NodeManager::SKOLEM_EXACT_NAME); + } + Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), + NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) ); + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero); + Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero); + Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); + Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]); + Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]); + node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf ); + break; + } case kind::DIVISION: { // partial function: division if(d_divByZero.isNull()) { |