| 196 | } |
| 197 | |
| 198 | int VnnLibParser::parseAssert( int index, const Vector<String> &tokens, InputQuery &inputQuery ) |
| 199 | { |
| 200 | ASSERT( tokens[index] == "(" ); |
| 201 | ++index; |
| 202 | |
| 203 | const String &op = tokens[index]; |
| 204 | if ( op == "<=" || op == ">=" || op == "and" ) |
| 205 | { |
| 206 | List<Equation> equations; |
| 207 | index = parseCondition( index, tokens, equations ); |
| 208 | for ( const auto &eq : equations ) |
| 209 | { |
| 210 | if ( eq._addends.size() == 1 ) |
| 211 | { |
| 212 | const Equation::Addend &addend = eq._addends.front(); |
| 213 | if ( addend._coefficient < 0 ) |
| 214 | { |
| 215 | inputQuery.setLowerBound( addend._variable, eq._scalar / addend._coefficient ); |
| 216 | } |
| 217 | else if ( addend._coefficient > 0 ) |
| 218 | { |
| 219 | inputQuery.setUpperBound( addend._variable, eq._scalar / addend._coefficient ); |
| 220 | } |
| 221 | else if ( eq._scalar < 0 ) |
| 222 | { |
| 223 | throw InputParserError( |
| 224 | InputParserError::UNEXPECTED_INPUT, |
| 225 | Stringf( "Illegal vnnlib constraint: 0 < %f", eq._scalar ).ascii() ); |
| 226 | } |
| 227 | else |
| 228 | { |
| 229 | continue; |
| 230 | } |
| 231 | } |
| 232 | else |
| 233 | { |
| 234 | inputQuery.addEquation( eq ); |
| 235 | } |
| 236 | } |
| 237 | } |
| 238 | else if ( op == "or" ) |
| 239 | { |
| 240 | List<PiecewiseLinearCaseSplit> disjunctList; |
| 241 | ++index; |
| 242 | while ( tokens[index] != ")" ) |
| 243 | { |
| 244 | List<Equation> equations; |
| 245 | index = parseCondition( index + 1, tokens, equations ); |
| 246 | |
| 247 | PiecewiseLinearCaseSplit split; |
| 248 | for ( const auto &eq : equations ) |
| 249 | { |
| 250 | if ( eq._addends.size() == 1 ) |
| 251 | { |
| 252 | // Add bounds as tightenings |
| 253 | unsigned var = eq._addends.front()._variable; |
| 254 | double coeff = eq._addends.front()._coefficient; |
| 255 | if ( coeff == 0 ) |
nothing calls this directly
no test coverage detected