fixed DFASAT for new flexfringe version, now merges states once the sat solver returns a solution, solution is maxed at 5000 chars, this should be fixed at some point to be arbitrary length, also predict with json is fixed, uses json now for printing (please let me know if there are problem)

Author: sicco

source/main.cpp

@@ -163,6 +163,8 @@ void run() {
         eval->initialize_after_adding_traces(merger);
         LOG_S(INFO) << "Satsolver mode selected, starting run";
 
+        if(SAT_RUN_GREEDY) greedy_run(merger);
+
         run_dfasat(merger, SAT_SOLVER, -1);
 
         print_current_automaton(merger, OUTPUT_FILE, ".final");
@@ -375,6 +377,9 @@ int main(int argc, char *argv[]){
     app.add_option("--satfinalred", TARGET_REJECTING, "Make all transitions from red states without any occurrences force to have 0 occurrences (similar to targeting a rejecting sink), (setting 0 or 1) before sending the problem to the SAT solver; default=0. Advice: the same as finalred but for the SAT solver. Setting it to 1 greatly improves solving speed.");
     app.add_option("--symmetry", SYMMETRY_BREAKING, "Add symmetry breaking predicates to the SAT encoding (setting 0 or 1), based on Ulyantsev et al. BFS symmetry breaking; default=1. Advice: in our experience this only improves solving speed.");
     app.add_option("--forcing", FORCING, "Add predicates to the SAT encoding that force transitions in the learned DFA to be used by input examples (setting 0 or 1); default=0. Advice: leads to non-complete models. When the data is sparse, this should be set to 1. It does make the instance larger and can have a negative effect on the solving time.");
+    app.add_option("--satgreedy", SAT_RUN_GREEDY, "Run the greedy process before starting the SAT solver, default=0.");
+    app.add_option("--aptabound", APTA_SIZE_BOUND, "Lower bound on the APTA (entire data tree) size. When reached by greedy, no more merges will be performed. Default=0.");
+    app.add_option("--dfabound", DFA_SIZE_BOUND, "Upper bound on the Automaton (only red states) size. When reached by greedy, no more merges will be performed. Default=0.");
 
     app.add_option("--printblue", PRINT_BLUE, "Print blue states in the .dot file? Default 1 (true).");
     app.add_option("--printwhite", PRINT_WHITE, "Print white states in the .dot file? These are typically sinks states, i.e., states that have not been considered for merging. Default 0 (false).");

source/parameters.cpp

@@ -123,5 +123,7 @@ int DIFF_SIZE = 1000;
 int DIFF_MAX_LENGTH = 50;
 double DIFF_MIN = -100.0;
 
-
+int DFA_SIZE_BOUND = -1;
+int APTA_SIZE_BOUND = -1;
+bool SAT_RUN_GREEDY = false;
 

source/parameters.h

@@ -138,4 +138,9 @@ extern int IDENTICAL_KTAIL;
 
 extern bool STAR_FREE;
 extern bool SINK_TYPE;
+
+extern int DFA_SIZE_BOUND;
+extern int APTA_SIZE_BOUND;
+extern bool SAT_RUN_GREEDY;
+
 #endif

source/state_merger.cpp

@@ -923,7 +923,14 @@ refinement_set* state_merger::get_possible_refinements(){
     if(!found_non_sink && !MERGE_SINKS){
         return result;
     }
-    
+
+    if(DFA_SIZE_BOUND != -1 && get_num_red_states() >= DFA_SIZE_BOUND){
+        return result;
+    }
+    if(APTA_SIZE_BOUND != -1 && get_final_apta_size() <= APTA_SIZE_BOUND){
+        return result;
+    }
+
     for(auto it = blue_its.begin(); it != blue_its.end(); ++it){
         apta_node* blue = *it;
         bool found = false;
@@ -972,9 +979,10 @@ refinement_set* state_merger::get_possible_refinements(){
             return result;
         }
 
-        if(!found || EXTEND_SINKS || !blue->is_sink())
+        if(!found || EXTEND_SINKS || !blue->is_sink()){
             result->insert(mem_store::create_extend_refinement(this, blue));
-        
+        }
+
         if(MERGE_MOST_VISITED) break;
     }
     return result;