diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-17 17:56:08 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-18 11:10:40 -0600 |
| commit | 368e2945a871e16bdf2f3a26a401b9d157240a9d (patch) | |
| tree | f5201f5c43f36b581b830ba291c80828a67ae6ad /src/smt/smt_engine.cpp | |
| parent | 0d2c0a0c5a07479cadc5ba54e5f6258f1964d1e0 (diff) | |
strings with new ideas
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 761348890..406db286f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -309,6 +309,7 @@ class SmtEnginePrivate : public NodeManagerListener { * Function symbol used to implement uninterpreted undefined string * semantics. Needed to deal with partial charat/substr function. */ + Node d_charAtUF; Node d_charAtUndef; Node d_substrUndef; @@ -440,6 +441,7 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), + d_charAtUF(), d_charAtUndef(), d_substrUndef(), d_divByZero(), @@ -1534,11 +1536,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF node = expandBVDivByZero(node); break; - case kind::STRING_CHARAT: { - if(d_charAtUndef.isNull()) { + /*case kind::STRING_CHARAT: { + if(d_charAtUF.isNull()) { std::vector< TypeNode > argTypes; argTypes.push_back(NodeManager::currentNM()->stringType()); argTypes.push_back(NodeManager::currentNM()->integerType()); + d_charAtUF = NodeManager::currentNM()->mkSkolem("charAt", + NodeManager::currentNM()->mkFunctionType( + argTypes, + NodeManager::currentNM()->stringType()), + "total charat", + NodeManager::SKOLEM_EXACT_NAME); d_charAtUndef = NodeManager::currentNM()->mkSkolem("charAt_undef", NodeManager::currentNM()->mkFunctionType( argTypes, @@ -1551,14 +1559,17 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF d_smt.d_logic.lock(); } } - TNode str = n[0], num = n[1]; + Node str = n[0]; + Node num = n[1]; + //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 1"); Node lenx = nm->mkNode(kind::STRING_LENGTH, str); Node cond = nm->mkNode(kind::GT, lenx, num); Node total = nm->mkNode(kind::STRING_CHARAT_TOTAL, str, num); Node undef = nm->mkNode(kind::APPLY_UF, d_charAtUndef, str, num); node = nm->mkNode(kind::ITE, cond, total, undef); + node = nm->mkNode(kind::APPLY_UF, d_charAtUF, n[0], n[1]); } - break; + break;*/ case kind::STRING_SUBSTR: { if(d_substrUndef.isNull()) { std::vector< TypeNode > argTypes; @@ -1577,7 +1588,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF d_smt.d_logic.lock(); } } - TNode str = n[0]; + Node str = n[0]; + //Assert(str.getType() == NodeManager::currentNM()->stringType(), "String Type Check 2"); Node lenx = nm->mkNode(kind::STRING_LENGTH, str); Node num = nm->mkNode(kind::PLUS, n[1], n[2]); Node cond = nm->mkNode(kind::GEQ, lenx, num); |