diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-28 17:17:51 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-01-28 17:17:51 -0600 |
commit | 6b2b7c90c9dccb596181fcf399a8830b05db5408 (patch) | |
tree | 3034713b827e678746c8e51c4c4379ac56323839 /src/smt | |
parent | d3822db24e15e255766866a47e6ffa0d8d91911b (diff) |
merge internal and user of charat & substr into one
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 71 |
1 files changed, 3 insertions, 68 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c77c05423..8754dc084 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -310,9 +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_charAtUF; - Node d_charAtUndef; - Node d_substrUndef; + //Node d_substrUndef; /** * Function symbol used to implement uninterpreted division-by-zero @@ -442,9 +440,6 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), - d_charAtUF(), - d_charAtUndef(), - d_substrUndef(), d_divByZero(), d_intDivByZero(), d_modZero(), @@ -1560,68 +1555,8 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF node = expandBVDivByZero(node); break; - /*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, - NodeManager::currentNM()->stringType()), - "partial charat undef", - NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - 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;*/ - case kind::STRING_SUBSTR: { - if(d_substrUndef.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - argTypes.push_back(NodeManager::currentNM()->integerType()); - d_substrUndef = NodeManager::currentNM()->mkSkolem("substr_undef", - NodeManager::currentNM()->mkFunctionType( - argTypes, - NodeManager::currentNM()->stringType()), - "partial substring undef", - NodeManager::SKOLEM_EXACT_NAME); - if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_UF); - d_smt.d_logic.lock(); - } - } - 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); - Node total = nm->mkNode(kind::STRING_SUBSTR_TOTAL, str, n[1], n[2]); - Node undef = nm->mkNode(kind::APPLY_UF, d_substrUndef, str, n[1], n[2]); - node = nm->mkNode(kind::ITE, cond, total, undef); - } - break; + //case kind::STRING_CHARAT: + //case kind::STRING_SUBSTR: case kind::DIVISION: { // partial function: division |