Distinguish between validated and valid in AssumptionChecker and AssumptionMaker

src/storm-pars/analysis/AssumptionChecker.cpp

@@ -147,19 +147,40 @@ namespace storm {
 
                     if (state1succ1->getColumn() == state2succ1->getColumn() && state1succ2->getColumn() == state2succ2->getColumn()) {
                         result = validateAssumptionFunction(lattice, state1succ1, state1succ2, state2succ1, state2succ2);
+
                         if (!result) {
                             result = validateAssumptionSMTSolver(lattice, state1succ1, state1succ2, state2succ1, state2succ2);
                         }
+
+                        validatedAssumptions.insert(assumption);
+                        if (result) {
+                            validAssumptions.insert(assumption);
+                        }
                     }
                 } else {
-                    result = validateAssumptionSMTSolver(lattice, assumption);
-                }
-            }
+                    bool subset = true;
+                    auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
+                    auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
 
-            if (result) {
-                validatedAssumptions.insert(assumption);
-            } else {
-                STORM_LOG_DEBUG("Could not validate: " << *assumption << std::endl);
+                    if (row1.getNumberOfEntries() > row2.getNumberOfEntries()) {
+                        std::swap(row1, row2);
+                    }
+                    for (auto itr1 = row1.begin(); subset && itr1 != row1.end(); ++itr1) {
+                        bool found = false;
+                        for (auto itr2 = row2.begin(); !found && itr2 != row2.end(); ++itr2) {
+                            found = itr1->getColumn() == itr2->getColumn();
+                        }
+                        subset &= found;
+                    }
+
+                    if (subset) {
+                        result = validateAssumptionSMTSolver(lattice, assumption);
+                        validatedAssumptions.insert(assumption);
+                        if (result) {
+                            validAssumptions.insert(assumption);
+                        }
+                    }
+                }
             }
             return result;
         }
@@ -256,30 +277,6 @@ namespace storm {
             auto row1 = matrix.getRow(std::stoi(assumption->getFirstOperand()->asVariableExpression().getVariableName()));
             auto row2 = matrix.getRow(std::stoi(assumption->getSecondOperand()->asVariableExpression().getVariableName()));
 
-            if (row1.getNumberOfEntries() <= row2.getNumberOfEntries()) {
-                for (auto itr1 = row1.begin(); result && itr1 != row1.end(); ++itr1) {
-                    bool found = false;
-                    for (auto itr2 = row2.begin(); !found && itr2 != row2.end(); ++itr2) {
-                        found = itr1->getColumn() == itr2->getColumn();
-                    }
-
-                    if (!found) {
-                        result = false;
-                    }
-                }
-            } else {
-                for (auto itr1 = row2.begin(); result && itr1 != row2.end(); ++itr1) {
-                    bool found = false;
-                    for (auto itr2 = row1.begin(); !found && itr2 != row1.end(); ++itr2) {
-                        found = itr1->getColumn() == itr2->getColumn();
-                    }
-
-                    if (!found) {
-                        result = false;
-                    }
-                }
-            }
-
             if (result) {
                 storm::solver::Z3SmtSolver s(*manager);
                 if (row1.getNumberOfEntries() >= row2.getNumberOfEntries()) {
@@ -356,6 +353,12 @@ namespace storm {
             return find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end();
         }
 
+        template <typename ValueType>
+        bool AssumptionChecker<ValueType>::valid(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption) {
+            assert(find(validatedAssumptions.begin(), validatedAssumptions.end(), assumption) != validatedAssumptions.end());
+            return find(validAssumptions.begin(), validAssumptions.end(), assumption) != validAssumptions.end();
+        }
+
         template class AssumptionChecker<storm::RationalFunction>;
     }
 }

src/storm-pars/analysis/AssumptionChecker.h

@@ -59,7 +59,8 @@ namespace storm {
              * @return true if the assumption has been validated and holds, false otherwise
              */
             bool validated(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
-            
+            bool valid(std::shared_ptr<storm::expressions::BinaryRelationExpression> assumption);
+
         private:
             std::shared_ptr<storm::logic::Formula const> formula;
 
@@ -69,6 +70,8 @@ namespace storm {
 
             std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> validatedAssumptions;
 
+            std::set<std::shared_ptr<storm::expressions::BinaryRelationExpression>> validAssumptions;
+
             bool validateAssumptionFunction(storm::analysis::Lattice* lattice,
                     typename storm::storage::SparseMatrix<ValueType>::iterator state1succ1,
                     typename storm::storage::SparseMatrix<ValueType>::iterator state1succ2,

src/storm-pars/analysis/AssumptionMaker.cpp

@@ -55,6 +55,7 @@ namespace storm {
             std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> criticalTriple = this->latticeExtender->extendLattice(lattice, assumptions.back());
 
             if (validate && assumptionChecker->validated(assumptions.back())) {
+                assert (assumptionChecker->valid(assumptions.back()));
                 assumptions.pop_back();
             }
 
@@ -91,9 +92,17 @@ namespace storm {
             if (assumptionChecker->checkOnSamples(assumption)) {
                 if (validate) {
                     assumptionChecker->validateAssumption(assumption, lattice);
+                    if (!assumptionChecker->validated(assumption) || assumptionChecker->valid(assumption)) {
+                        assumptions.push_back(
+                                std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
+                        result = (runRecursive(lattice, assumptions));
+                    }
+                } else {
+                    assumptions.push_back(std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
+                    result = (runRecursive(lattice, assumptions));
                 }
-                assumptions.push_back(std::shared_ptr<storm::expressions::BinaryRelationExpression>(assumption));
-                result = (runRecursive(lattice, assumptions));
+
+
             } else {
                 delete lattice;
             }
@@ -101,8 +110,6 @@ namespace storm {
             return result;
         }
 
-
-
         template class AssumptionMaker<storm::RationalFunction>;
     }
 }