| 1075 | } |
| 1076 | |
| 1077 | double *Engine::createConstraintMatrix() |
| 1078 | { |
| 1079 | const List<Equation> &equations( _preprocessedQuery->getEquations() ); |
| 1080 | unsigned m = equations.size(); |
| 1081 | unsigned n = _preprocessedQuery->getNumberOfVariables(); |
| 1082 | |
| 1083 | // Step 1: create a constraint matrix from the equations |
| 1084 | double *constraintMatrix = new double[n * m]; |
| 1085 | if ( !constraintMatrix ) |
| 1086 | throw MarabouError( MarabouError::ALLOCATION_FAILED, "Engine::constraintMatrix" ); |
| 1087 | std::fill_n( constraintMatrix, n * m, 0.0 ); |
| 1088 | |
| 1089 | unsigned equationIndex = 0; |
| 1090 | for ( const auto &equation : equations ) |
| 1091 | { |
| 1092 | if ( equation._type != Equation::EQ ) |
| 1093 | { |
| 1094 | _exitCode = Engine::ERROR; |
| 1095 | throw MarabouError( MarabouError::NON_EQUALITY_INPUT_EQUATION_DISCOVERED ); |
| 1096 | } |
| 1097 | |
| 1098 | for ( const auto &addend : equation._addends ) |
| 1099 | constraintMatrix[equationIndex * n + addend._variable] = addend._coefficient; |
| 1100 | |
| 1101 | ++equationIndex; |
| 1102 | } |
| 1103 | |
| 1104 | return constraintMatrix; |
| 1105 | } |
| 1106 | |
| 1107 | void Engine::removeRedundantEquations( const double *constraintMatrix ) |
| 1108 | { |
nothing calls this directly
no test coverage detected