Fixed issue where variables added through implications were erroneous…

…ly being added to the final count
vlab-cs-ucsb · Apr 10, 2023 · 7da45e2 · 7da45e2
1 parent d1f5c0b
commit 7da45e2
Show file tree

Hide file tree

Showing 5 changed files with 102 additions and 4 deletions.
diff --git a/src/interface/Driver.cpp b/src/interface/Driver.cpp
@@ -305,20 +305,60 @@ void Driver::SetModelCounter() {
   int num_str_var = 0;
 
   for (const auto &variable_entry : getSatisfyingVariables()) {
+    // LOG(INFO) << *variable_entry.first;
     if (variable_entry.second == nullptr || symbol_table_->is_sorted_variable(variable_entry.first)) {
       continue;
     }
-    // LOG(INFO) << *variable_entry.first;
+
+
+    // LOG(INFO) << "    IS VALID";
+
     switch (variable_entry.second->getType()) {
       case Vlab::Solver::Value::Type::BINARYINT_AUTOMATON: {
         auto binary_auto = variable_entry.second->getBinaryIntAutomaton();
         auto formula = binary_auto->GetFormula();
+        bool has_actual_var = false;
+
+        std::vector<std::string> vars_to_project;
+
+        // LOG(INFO) << "VARIABLE: " << variable_entry.first;
         for (auto& el : formula->GetVariableCoefficientMap()) {
+          // LOG(INFO) << "  has " << el.first << " at track " << formula->GetVariableIndex(el.first);
           if (symbol_table_->get_variable_unsafe(el.first) != nullptr) {
             ++num_bin_var;
+            has_actual_var = true;
+          } else {
+            vars_to_project.push_back(el.first);
           }
         }
-        model_counter_.add_symbolic_counter(binary_auto->GetSymbolicCounter());
+
+        // LOG(INFO) << "FOR VARIABLE: " << variable_entry.first;
+
+        // binary_auto->inspectAuto(false,true);
+
+
+        for(auto var : vars_to_project) {
+          // LOG(INFO) << "  projecting away " << var;
+          auto tmp = binary_auto;
+          tmp = binary_auto->ProjectAwayVariable(var);
+          delete binary_auto;
+          binary_auto = tmp;
+        }
+
+        variable_entry.second->setData(binary_auto);
+        // binary_auto->inspectAuto(false,true);
+
+        // LOG(INFO) << binary_auto->Count(50);
+
+        // LOG(INFO) << " IS EMPTY ? " << binary_auto->IsEmptyLanguage();
+
+        if(has_actual_var) {
+          // LOG(INFO) << "HAS ACTUAL VAR";
+          model_counter_.add_symbolic_counter(binary_auto->GetSymbolicCounter());
+          // LOG(INFO) << "countints = " << model_counter_.CountInts(5000);
+        } else {
+          // LOG(INFO) << "NO ACTUAL VAR";
+        }
       }
         break;
       case Vlab::Solver::Value::Type::INT_CONSTANT: {

diff --git a/src/main.cpp b/src/main.cpp
@@ -300,6 +300,7 @@ int main(const int argc, const char **argv) {
         }
       } else if (not count_tuple) {
         if (int_bounds.size() == 1 and str_bounds.size() == 1 and int_bounds[0] == str_bounds[0]) {
+
           auto b = int_bounds[0];
           start = std::chrono::steady_clock::now();
           auto count = driver.Count(b, b);
@@ -308,20 +309,21 @@ int main(const int argc, const char **argv) {
           LOG(INFO) << "report bound: " << b << " count: " << count << " time: "
                     << std::chrono::duration<long double, std::milli>(count_time).count() << " ms";
         } else {
+
           for (auto b : int_bounds) {
             start = std::chrono::steady_clock::now();
             auto count = driver.CountInts(b);
             end = std::chrono::steady_clock::now();
             auto count_time = end - start;
-            LOG(INFO) << "report bound: " << b << " count: " << count << " time: "
+            LOG(INFO) << "report bound (integer): " << b << " count: " << count << " time: "
                       << std::chrono::duration<long double, std::milli>(count_time).count() << " ms";
           }
           for (auto b : str_bounds) {
             start = std::chrono::steady_clock::now();
             auto count = driver.CountStrs(b);
             end = std::chrono::steady_clock::now();
             auto count_time = end - start;
-            LOG(INFO) << "report bound: " << b << " count: " << count << " time: "
+            LOG(INFO) << "report bound (string): " << b << " count: " << count << " time: "
                       << std::chrono::duration<long double, std::milli>(count_time).count() << " ms";
           }
         }

diff --git a/src/solver/Value.cpp b/src/solver/Value.cpp
@@ -171,6 +171,10 @@ void Value::setData(Theory::StringAutomaton_ptr data) {
   string_automaton = data;
 }
 
+void Value::setData(Theory::BinaryIntAutomaton_ptr data) {
+  binaryint_automaton = data;
+}
+
 bool Value::getBoolConstant() const {
   return bool_constant;
 }

diff --git a/src/theory/BinaryIntAutomaton.cpp b/src/theory/BinaryIntAutomaton.cpp
@@ -756,6 +756,56 @@ std::map<std::string, int> BinaryIntAutomaton::GetAnAcceptingIntForEachVar() {
   return var_values;
 }
 
+BinaryIntAutomaton_ptr BinaryIntAutomaton::ProjectAwayVariable(std::string variable) {
+  if(formula_ == nullptr) {
+		LOG(FATAL) << "No Int formula!";
+	}
+
+  int track = formula_->GetVariableIndex(variable);
+  int k_track = track;
+  // LOG(INFO) << "projection away track " << track;
+
+  int num_tracks = formula_->GetNumberOfVariables();
+
+  std::vector<int> indices;
+  int *map = CreateBddVariableIndices(num_tracks);
+  for(int i = 0,k=0; i < this->num_of_bdd_variables_; i++) {
+    if(i == k_track) {
+        map[i] = num_tracks-1;
+        continue;
+    }
+    map[i] = k++;
+  }
+
+  std::vector<int> _map;
+  for(int i = 0; i < num_tracks; i++) {
+  	_map.push_back(map[i]);
+  }
+  for(int i = 0; i < 1 ; i++) {
+  	indices.push_back(k_track);
+  }
+
+  auto result_dfa = DFAProjectAway(dfa_,_map,indices);
+
+  auto result_formula = formula_->clone();
+	result_formula->RemoveVariable(variable);
+
+  BinaryIntAutomaton_ptr result_auto = new BinaryIntAutomaton(result_dfa, result_formula, is_natural_number_);
+
+
+  // auto anyint = MakeAnyInt(result_formula->clone(),is_natural_number_);
+  // auto r2 = result_auto->Intersect(anyint);
+  // delete result_auto;
+  // delete anyint;
+
+  // result_auto = r2;
+
+
+
+
+  return result_auto;
+}
+
 void BinaryIntAutomaton::decide_counting_schema(Eigen::SparseMatrix<BigInteger>& count_matrix) {
   if (is_natural_number_) {
     counter_.set_type(SymbolicCounter::Type::BINARYUNSIGNEDINT);

diff --git a/src/theory/BinaryIntAutomaton.h b/src/theory/BinaryIntAutomaton.h
@@ -84,6 +84,8 @@ class BinaryIntAutomaton: public Automaton {
 
   std::map<std::string, int> GetAnAcceptingIntForEachVar();
 
+  BinaryIntAutomaton_ptr ProjectAwayVariable(std::string);
+
   BigInteger SymbolicCount(double bound, bool count_less_than_or_equal_to_bound = false) override;
   std::map<std::string,std::vector<std::string>> GetModelsWithinBound(int num_models, int bound) override;