{
Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl;
Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl;
-
- //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings.
- // change this if we generalize to sequences.
- //set<Node> termSet;
- // Compute terms appearing in assertions and shared terms
- //computeRelevantTerms(termSet);
- //m->assertEqualityEngine( &d_equalityEngine, &termSet );
- if (!m->assertEqualityEngine(&d_equalityEngine))
+ std::set<Node> termSet;
+
+ // Compute terms appearing in assertions and shared terms
+ computeRelevantTerms(termSet);
+ // assert the (relevant) portion of the equality engine to the model
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
{
return false;
}
+ std::unordered_set<Node, NodeHashFunction> repSet;
NodeManager* nm = NodeManager::currentNM();
// Generate model
- std::vector< Node > nodes;
- getEquivalenceClasses( nodes );
+ // get the relevant string equivalence classes
+ for (const Node& s : termSet)
+ {
+ if (s.getType().isString())
+ {
+ Node r = getRepresentative(s);
+ repSet.insert(r);
+ }
+ }
+ std::vector<Node> nodes(repSet.begin(), repSet.end());
std::map< Node, Node > processed;
std::vector< std::vector< Node > > col;
std::vector< Node > lts;
separateByLength( nodes, col, lts );
//step 1 : get all values for known lengths
std::vector< Node > lts_values;
- std::map< unsigned, bool > values_used;
+ std::map<unsigned, Node> values_used;
+ std::vector<Node> len_splits;
for( unsigned i=0; i<col.size(); i++ ) {
Trace("strings-model") << "Checking length for {";
for( unsigned j=0; j<col[i].size(); j++ ) {
Trace("strings-model") << col[i][j];
}
Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
+ Node len_value;
if( lts[i].isConst() ) {
- lts_values.push_back( lts[i] );
- Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()),
+ len_value = lts[i];
+ }
+ else if (!lts[i].isNull())
+ {
+ // get the model value for lts[i]
+ len_value = d_valuation.getModelValue(lts[i]);
+ }
+ if (len_value.isNull())
+ {
+ lts_values.push_back(Node::null());
+ }
+ else
+ {
+ Assert(len_value.getConst<Rational>() <= Rational(String::maxSize()),
"Exceeded UINT32_MAX in string model");
- unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
- values_used[ lvalue ] = true;
- }else{
- //get value for lts[i];
- if( !lts[i].isNull() ){
- Node v = d_valuation.getModelValue(lts[i]);
- Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
- lts_values.push_back( v );
- Assert(v.getConst<Rational>() <= Rational(String::maxSize()),
- "Exceeded UINT32_MAX in string model");
- unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt();
- values_used[ lvalue ] = true;
- }else{
- //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl;
- //Assert( false );
- lts_values.push_back( Node::null() );
+ unsigned lvalue =
+ len_value.getConst<Rational>().getNumerator().toUnsignedInt();
+ std::map<unsigned, Node>::iterator itvu = values_used.find(lvalue);
+ if (itvu == values_used.end())
+ {
+ values_used[lvalue] = lts[i];
+ }
+ else
+ {
+ len_splits.push_back(lts[i].eqNode(itvu->second));
}
+ lts_values.push_back(len_value);
}
}
////step 2 : assign arbitrary values for unknown lengths?
//step 3 : assign values to equivalence classes that are pure variables
for( unsigned i=0; i<col.size(); i++ ){
std::vector< Node > pure_eq;
- Trace("strings-model") << "The equivalence classes ";
+ Trace("strings-model") << "The (" << col[i].size()
+ << ") equivalence classes ";
for (const Node& eqc : col[i])
{
Trace("strings-model") << eqc << " ";
}
Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
lts_values[i] = nm->mkConst(Rational(lvalue));
- values_used[ lvalue ] = true;
+ values_used[lvalue] = Node::null();
}
Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
for( unsigned j=0; j<pure_eq.size(); j++ ){
while (m->hasTerm(c))
{
++sel;
- Assert(!sel.isFinished());
+ if (sel.isFinished())
+ {
+ // We are in a case where model construction is impossible due to
+ // an insufficient number of constants of a given length.
+
+ // Consider an integer equivalence class E whose value is assigned
+ // n in the model. Let { S_1, ..., S_m } be the set of string
+ // equivalence classes such that len( x ) is a member of E for
+ // some member x of each class S1, ...,Sm. Since our calculus is
+ // saturated with respect to cardinality inference (see Liang
+ // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is
+ // the cardinality of our alphabet.
+
+ // Now, consider the case where there exists two integer
+ // equivalence classes E1 and E2 that are assigned n, and moreover
+ // we did not received notification from arithmetic that E1 = E2.
+ // This typically should never happen, but assume in the following
+ // that it does.
+
+ // Now, it may be the case that there are string equivalence
+ // classes { S_1, ..., S_m1 } whose lengths are in E1,
+ // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where
+ // m1 + m2 > A^n. In this case, we have insufficient strings to
+ // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this
+ // happens, we add a split on len( u1 ) = len( u2 ) for some
+ // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of
+ // integer equivalence classes that are assigned to the same value
+ // in the model.
+ AlwaysAssert(!len_splits.empty());
+ for (const Node& sl : len_splits)
+ {
+ Node spl = nm->mkNode(OR, sl, sl.negate());
+ d_out->lemma(spl);
+ }
+ return false;
+ }
c = *sel;
}
++sel;
std::vector< Node > lts;
separateByLength( d_strings_eqc, cols, lts );
+ Trace("strings-card") << "Check cardinality...." << std::endl;
for( unsigned i = 0; i<cols.size(); ++i ) {
Node lr = lts[i];
Trace("strings-card") << "Number of strings with length equal to " << lr << " is " << cols[i].size() << std::endl;
}
}
}
+ Trace("strings-card") << "...end check cardinality" << std::endl;
}
void TheoryStrings::getEquivalenceClasses( std::vector< Node >& eqcs ) {
--- /dev/null
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+(define-fun byte_2_int ((s String)) Int (ite (= (str.len s) 1) (str.code s) 256))
+
+(define-fun read_buffer16 ((s1 String) (s2 String)) Int
+ (+ (* 256 (byte_2_int s1))
+ (byte_2_int s2))
+)
+
+
+(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int
+ (+ (+ (+ (* 16777216 (byte_2_int s1) )
+ (* 65536 (byte_2_int s2) ) )
+ (* 256 (byte_2_int s3) ) )
+ (byte_2_int s4) )
+)
+
+
+(declare-const magic String)
+(declare-const p1 String)
+(declare-const p2 String)
+(declare-const p3 String)
+(declare-const size1 String)
+(declare-const size2 String)
+(declare-const size3 String)
+(declare-const size4 String)
+(declare-const off1 String)
+(declare-const off2 String)
+(declare-const off3 String)
+(declare-const off4 String)
+(assert (= magic "ABCD"))
+(assert (= 1 (str.len size1)))
+(assert (= 1 (str.len size2)))
+(assert (= 1 (str.len size3)))
+(assert (= 1 (str.len size4)))
+(assert (= 1 (str.len off1)))
+(assert (= 1 (str.len off2)))
+(assert (= 1 (str.len off3)))
+(assert (= 1 (str.len off4)))
+
+
+(declare-const p3_off Int)
+(declare-const before_p3 String)
+(assert (= before_p3 (str.++ p1 p2)))
+(assert (not (str.contains before_p3 magic)))
+(assert (= p3_off (str.len before_p3)))
+
+
+(declare-const p2_size Int)
+(declare-const p2_off Int)
+(declare-const p2_min_size Int)
+(assert (= p2_size (read_buffer32 size1 size2 size3 size4)))
+(assert (= p2_off (read_buffer32 off1 off2 off3 off4)))
+(assert (<= (+ p2_size p2_off) p3_off))
+(assert (>= p2_size p2_min_size))
+(assert (= p2_min_size 10))
+
+(check-sat)
--- /dev/null
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+(define-fun byte_2_int ((s String)) Int
+ (ite (= s "\x00") 0
+ (ite (= s "\x01") 1
+ (ite (= s "\x02") 2
+ (ite (= s "\x03") 3
+ (ite (= s "\x04") 4
+ (ite (= s "\x05") 5
+ (ite (= s "\x06") 6
+ (ite (= s "\x07") 7
+ (ite (= s "\x08") 8
+ (ite (= s "\x09") 9
+ (ite (= s "\x0A") 10
+ (ite (= s "\x0B") 11
+ (ite (= s "\x0C") 12
+ (ite (= s "\x0D") 13
+ (ite (= s "\x0E") 14
+ (ite (= s "\x0F") 15
+ (ite (= s "\x10") 16
+ (ite (= s "\x11") 17
+ (ite (= s "\x12") 18
+ (ite (= s "\x13") 19
+ (ite (= s "\x14") 20
+ (ite (= s "\x15") 21
+ (ite (= s "\x16") 22
+ (ite (= s "\x17") 23
+ (ite (= s "\x18") 24
+ (ite (= s "\x19") 25
+ (ite (= s "\x1A") 26
+ (ite (= s "\x1B") 27
+ (ite (= s "\x1C") 28
+ (ite (= s "\x1D") 29
+ (ite (= s "\x1E") 30
+ (ite (= s "\x1F") 31
+ (ite (= s "\x20") 32
+ (ite (= s "\x21") 33
+ (ite (= s "\x22") 34
+ (ite (= s "\x23") 35
+ (ite (= s "\x24") 36
+ (ite (= s "\x25") 37
+ (ite (= s "\x26") 38
+ (ite (= s "\x27") 39
+ (ite (= s "\x28") 40
+ (ite (= s "\x29") 41
+ (ite (= s "\x2A") 42
+ (ite (= s "\x2B") 43
+ (ite (= s "\x2C") 44
+ (ite (= s "\x2D") 45
+ (ite (= s "\x2E") 46
+ (ite (= s "\x2F") 47
+ (ite (= s "\x30") 48
+ (ite (= s "\x31") 49
+ (ite (= s "\x32") 50
+ (ite (= s "\x33") 51
+ (ite (= s "\x34") 52
+ (ite (= s "\x35") 53
+ (ite (= s "\x36") 54
+ (ite (= s "\x37") 55
+ (ite (= s "\x38") 56
+ (ite (= s "\x39") 57
+ (ite (= s "\x3A") 58
+ (ite (= s "\x3B") 59
+ (ite (= s "\x3C") 60
+ (ite (= s "\x3D") 61
+ (ite (= s "\x3E") 62
+ (ite (= s "\x3F") 63
+ (ite (= s "\x40") 64
+ (ite (= s "\x41") 65
+ (ite (= s "\x42") 66
+ (ite (= s "\x43") 67
+ (ite (= s "\x44") 68
+ (ite (= s "\x45") 69
+ (ite (= s "\x46") 70
+ (ite (= s "\x47") 71
+ (ite (= s "\x48") 72
+ (ite (= s "\x49") 73
+ (ite (= s "\x4A") 74
+ (ite (= s "\x4B") 75
+ (ite (= s "\x4C") 76
+ (ite (= s "\x4D") 77
+ (ite (= s "\x4E") 78
+ (ite (= s "\x4F") 79
+ (ite (= s "\x50") 80
+ (ite (= s "\x51") 81
+ (ite (= s "\x52") 82
+ (ite (= s "\x53") 83
+ (ite (= s "\x54") 84
+ (ite (= s "\x55") 85
+ (ite (= s "\x56") 86
+ (ite (= s "\x57") 87
+ (ite (= s "\x58") 88
+ (ite (= s "\x59") 89
+ (ite (= s "\x5A") 90
+ (ite (= s "\x5B") 91
+ (ite (= s "\x5C") 92
+ (ite (= s "\x5D") 93
+ (ite (= s "\x5E") 94
+ (ite (= s "\x5F") 95
+ (ite (= s "\x60") 96
+ (ite (= s "\x61") 97
+ (ite (= s "\x62") 98
+ (ite (= s "\x63") 99
+ (ite (= s "\x64") 100
+ (ite (= s "\x65") 101
+ (ite (= s "\x66") 102
+ (ite (= s "\x67") 103
+ (ite (= s "\x68") 104
+ (ite (= s "\x69") 105
+ (ite (= s "\x6A") 106
+ (ite (= s "\x6B") 107
+ (ite (= s "\x6C") 108
+ (ite (= s "\x6D") 109
+ (ite (= s "\x6E") 110
+ (ite (= s "\x6F") 111
+ (ite (= s "\x70") 112
+ (ite (= s "\x71") 113
+ (ite (= s "\x72") 114
+ (ite (= s "\x73") 115
+ (ite (= s "\x74") 116
+ (ite (= s "\x75") 117
+ (ite (= s "\x76") 118
+ (ite (= s "\x77") 119
+ (ite (= s "\x78") 120
+ (ite (= s "\x79") 121
+ (ite (= s "\x7A") 122
+ (ite (= s "\x7B") 123
+ (ite (= s "\x7C") 124
+ (ite (= s "\x7D") 125
+ (ite (= s "\x7E") 126
+ (ite (= s "\x7F") 127
+ (ite (= s "\x80") 128
+ (ite (= s "\x81") 129
+ (ite (= s "\x82") 130
+ (ite (= s "\x83") 131
+ (ite (= s "\x84") 132
+ (ite (= s "\x85") 133
+ (ite (= s "\x86") 134
+ (ite (= s "\x87") 135
+ (ite (= s "\x88") 136
+ (ite (= s "\x89") 137
+ (ite (= s "\x8A") 138
+ (ite (= s "\x8B") 139
+ (ite (= s "\x8C") 140
+ (ite (= s "\x8D") 141
+ (ite (= s "\x8E") 142
+ (ite (= s "\x8F") 143
+ (ite (= s "\x90") 144
+ (ite (= s "\x91") 145
+ (ite (= s "\x92") 146
+ (ite (= s "\x93") 147
+ (ite (= s "\x94") 148
+ (ite (= s "\x95") 149
+ (ite (= s "\x96") 150
+ (ite (= s "\x97") 151
+ (ite (= s "\x98") 152
+ (ite (= s "\x99") 153
+ (ite (= s "\x9A") 154
+ (ite (= s "\x9B") 155
+ (ite (= s "\x9C") 156
+ (ite (= s "\x9D") 157
+ (ite (= s "\x9E") 158
+ (ite (= s "\x9F") 159
+ (ite (= s "\xA0") 160
+ (ite (= s "\xA1") 161
+ (ite (= s "\xA2") 162
+ (ite (= s "\xA3") 163
+ (ite (= s "\xA4") 164
+ (ite (= s "\xA5") 165
+ (ite (= s "\xA6") 166
+ (ite (= s "\xA7") 167
+ (ite (= s "\xA8") 168
+ (ite (= s "\xA9") 169
+ (ite (= s "\xAA") 170
+ (ite (= s "\xAB") 171
+ (ite (= s "\xAC") 172
+ (ite (= s "\xAD") 173
+ (ite (= s "\xAE") 174
+ (ite (= s "\xAF") 175
+ (ite (= s "\xB0") 176
+ (ite (= s "\xB1") 177
+ (ite (= s "\xB2") 178
+ (ite (= s "\xB3") 179
+ (ite (= s "\xB4") 180
+ (ite (= s "\xB5") 181
+ (ite (= s "\xB6") 182
+ (ite (= s "\xB7") 183
+ (ite (= s "\xB8") 184
+ (ite (= s "\xB9") 185
+ (ite (= s "\xBA") 186
+ (ite (= s "\xBB") 187
+ (ite (= s "\xBC") 188
+ (ite (= s "\xBD") 189
+ (ite (= s "\xBE") 190
+ (ite (= s "\xBF") 191
+ (ite (= s "\xC0") 192
+ (ite (= s "\xC1") 193
+ (ite (= s "\xC2") 194
+ (ite (= s "\xC3") 195
+ (ite (= s "\xC4") 196
+ (ite (= s "\xC5") 197
+ (ite (= s "\xC6") 198
+ (ite (= s "\xC7") 199
+ (ite (= s "\xC8") 200
+ (ite (= s "\xC9") 201
+ (ite (= s "\xCA") 202
+ (ite (= s "\xCB") 203
+ (ite (= s "\xCC") 204
+ (ite (= s "\xCD") 205
+ (ite (= s "\xCE") 206
+ (ite (= s "\xCF") 207
+ (ite (= s "\xD0") 208
+ (ite (= s "\xD1") 209
+ (ite (= s "\xD2") 210
+ (ite (= s "\xD3") 211
+ (ite (= s "\xD4") 212
+ (ite (= s "\xD5") 213
+ (ite (= s "\xD6") 214
+ (ite (= s "\xD7") 215
+ (ite (= s "\xD8") 216
+ (ite (= s "\xD9") 217
+ (ite (= s "\xDA") 218
+ (ite (= s "\xDB") 219
+ (ite (= s "\xDC") 220
+ (ite (= s "\xDD") 221
+ (ite (= s "\xDE") 222
+ (ite (= s "\xDF") 223
+ (ite (= s "\xE0") 224
+ (ite (= s "\xE1") 225
+ (ite (= s "\xE2") 226
+ (ite (= s "\xE3") 227
+ (ite (= s "\xE4") 228
+ (ite (= s "\xE5") 229
+ (ite (= s "\xE6") 230
+ (ite (= s "\xE7") 231
+ (ite (= s "\xE8") 232
+ (ite (= s "\xE9") 233
+ (ite (= s "\xEA") 234
+ (ite (= s "\xEB") 235
+ (ite (= s "\xEC") 236
+ (ite (= s "\xED") 237
+ (ite (= s "\xEE") 238
+ (ite (= s "\xEF") 239
+ (ite (= s "\xF0") 240
+ (ite (= s "\xF1") 241
+ (ite (= s "\xF2") 242
+ (ite (= s "\xF3") 243
+ (ite (= s "\xF4") 244
+ (ite (= s "\xF5") 245
+ (ite (= s "\xF6") 246
+ (ite (= s "\xF7") 247
+ (ite (= s "\xF8") 248
+ (ite (= s "\xF9") 249
+ (ite (= s "\xFA") 250
+ (ite (= s "\xFB") 251
+ (ite (= s "\xFC") 252
+ (ite (= s "\xFD") 253
+ (ite (= s "\xFE") 254
+ (ite (= s "\xFF") 255
+ 256))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+)
+
+
+
+(define-fun read_buffer16 ((s1 String) (s2 String)) Int
+ (+ (* 256 (byte_2_int s1))
+ (byte_2_int s2))
+)
+
+
+(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int
+ (+ (+ (+ (* 16777216 (byte_2_int s1) )
+ (* 65536 (byte_2_int s2) ) )
+ (* 256 (byte_2_int s3) ) )
+ (byte_2_int s4) )
+)
+
+
+(declare-const magic String)
+(declare-const p1 String)
+(declare-const p2 String)
+(declare-const p3 String)
+(declare-const size1 String)
+(declare-const size2 String)
+(declare-const size3 String)
+(declare-const size4 String)
+(declare-const off1 String)
+(declare-const off2 String)
+(declare-const off3 String)
+(declare-const off4 String)
+(assert (= magic "ABCD"))
+(assert (= 1 (str.len size1)))
+(assert (= 1 (str.len size2)))
+(assert (= 1 (str.len size3)))
+(assert (= 1 (str.len size4)))
+(assert (= 1 (str.len off1)))
+(assert (= 1 (str.len off2)))
+(assert (= 1 (str.len off3)))
+(assert (= 1 (str.len off4)))
+
+
+(declare-const p3_off Int)
+(declare-const before_p3 String)
+(assert (= before_p3 (str.++ p1 p2)))
+(assert (not (str.contains before_p3 magic)))
+(assert (= p3_off (str.len before_p3)))
+
+
+(declare-const p2_size Int)
+(declare-const p2_off Int)
+(declare-const p2_min_size Int)
+(assert (= p2_size (read_buffer32 size1 size2 size3 size4)))
+(assert (= p2_off (read_buffer32 off1 off2 off3 off4)))
+(assert (<= (+ p2_size p2_off) p3_off))
+(assert (>= p2_size p2_min_size))
+(assert (= p2_min_size 10))
+
+(check-sat)
projects / cvc5.git / commitdiff