Merge pull request #156 from VeriFIT/model_gen2

Model generation fixing

README.md

@@ -15,7 +15,7 @@ For a brief overview of the architecture, see [SMT-COMP'24 Z3-Noodler descriptio
 
 ### Dependencies
 
-1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.3`.
+1) The [Mata](https://github.com/VeriFIT/mata/) library for efficient handling of finite automata. Minimum required version of `mata` is `v1.6.6`.
     ```shell
     git clone 'https://github.com/VeriFIT/mata.git'
     cd mata
@@ -47,16 +47,16 @@ make test-noodler
 ```
 
 ### Running Z3-Noodler
-To run Z3-Noodler, select Z3-Noodler as Z3's string solver when executing Z3.
+To run Z3-Noodler, use:
 ```shell
 cd build/
-./z3 smt.string_solver=noodler <instance_file.smt2> 
+./z3 <instance_file.smt2> 
 ```
 
-If you want to get a model for sat instances, you need to enable producing models (otherwise the resulting models are not usable).
+If you want to get a model for sat instances (using `get-model` or `get-value`), you need to enable model generation:
 ```shell
 cd build/
-./z3 smt.string_solver=noodler smt.str.produce_models=true <instance_file.smt2> 
+./z3 model=true <instance_file.smt2> 
 ```
 However, model generation is highly experimental, the models might be invalid or they cannot be computed (yet).
 

src/cmd_context/basic_cmds.cpp

@@ -114,7 +114,7 @@ class get_model_cmd : public cmd {
         if (ctx.ignore_check())
             return;
         if (!ctx.is_model_available(m) || !ctx.get_check_sat_result())
-            throw cmd_exception("model is not available");
+            throw cmd_exception("model is not available, did you forget to enable model generation with ''model=true'?");
         if (m_index > 0 && ctx.get_opt()) {
             ctx.get_opt()->get_box_model(m, m_index);
         }
@@ -129,7 +129,7 @@ class get_model_cmd : public cmd {
 ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
     model_ref m;
     if (!ctx.is_model_available(m) || ctx.get_check_sat_result() == 0)
-        throw cmd_exception("model is not available");
+        throw cmd_exception("model is not available, did you forget to enable model generation with 'model=true'?");
     ctx.regular_stream() << "(";
     dictionary<macro_decls> const & macros = ctx.get_macros();
     bool first = true;

src/params/context_params.cpp

@@ -175,7 +175,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
 
 void context_params::collect_solver_param_descrs(param_descrs & d) {
     d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
-    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
+    d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "false");
     d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
 }
 

src/params/context_params.h

@@ -37,7 +37,7 @@ class context_params {
     bool             m_debug_ref_count { false };
     bool             m_trace { false };
     bool             m_well_sorted_check { false };
-    bool             m_model { true };
+    bool             m_model { false };
     bool             m_model_validate { false };
     bool             m_dump_models { false };
     bool             m_unsat_core { false };

src/parsers/smt2/smt2parser.cpp

@@ -2685,7 +2685,7 @@ namespace smt2 {
                 return;
             }
             if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == nullptr)
-                throw cmd_exception("model is not available");
+                throw cmd_exception("model is not available, did you forget to enable model generation with 'model=true'?");
             if (index != 0) {
                 m_ctx.get_opt()->get_box_model(md, index);
             }

src/smt/params/smt_params_helper.pyg

@@ -113,7 +113,7 @@ def_module_params(module_name='smt',
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
                           ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'),
-                          ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver), \'empty\' (a no-op solver that forces an answer unknown if strings were used), \'none\' (no solver)'),
+                          ('string_solver', SYMBOL, 'noodler', 'solver for string/sequence theories. options are: \'noodler\' (Z3-Noodler string solver), \'z3str3\', \'seq\' (Z3 default solver), \'auto\' (use static features to choose best solver), \'empty\' (a no-op solver that forces an answer unknown if strings were used), \'none\' (no solver)'),
                           ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
                           ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
@@ -138,7 +138,6 @@ def_module_params(module_name='smt',
                           ('str.preprocess_red', BOOL, False, 'use automata reduction eagerly in the preprocessing (Z3-Noodler only)'),
                           ('str.try_nielsen', BOOL, True, 'use Nielsen reduction for quadratic formulas (Z3-Noodler only)'),
                           ('str.underapprox_length', UINT, 5, 'maximum length of digit words used in underapproximating from_int/to_int conversions (Z3-Noodler only)'),
-                          ('str.produce_models', BOOL, False, 'generate models (Z3-Noodler only)'),
                           ('str.ca_constr', BOOL, False, 'use counter automata for solving extended string constraints (Z3-Noodler only)'),
                           ('str.try_length_proc', BOOL, False, 'use length-based decision procedure (Z3-Noodler only)'),
                           ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'),

src/smt/params/theory_str_noodler_params.cpp

@@ -1,6 +1,7 @@
 
 #include "smt/params/theory_str_noodler_params.h"
 #include "smt/params/smt_params_helper.hpp"
+#include "util/gparams.h"
 
 void theory_str_noodler_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
@@ -10,8 +11,8 @@ void theory_str_noodler_params::updt_params(params_ref const & _p) {
     m_try_nielsen = p.str_try_nielsen();
     m_try_length_proc = p.str_try_length_proc();
     m_underapprox_length = p.str_underapprox_length();
-    m_produce_models = p.str_produce_models();
     m_ca_constr = p.str_ca_constr();
+    m_produce_models = gparams::get_ref().get_bool("model", false);
 }
 
 #define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;

src/smt/theory_str_noodler/aut_assignment.cpp

@@ -1,5 +1,6 @@
 #include "aut_assignment.h"
 #include "util.h"
+#include "regex.h"
 
 namespace smt::noodler {
     LenNode AutAssignment::get_lengths(const BasicTerm& var) const {
@@ -188,4 +189,42 @@ namespace smt::noodler {
         aut.tarjan_scc_discover(callback);
         return flat;
     }
+
+    void AutAssignment::add_symbol_from_dummy(mata::Symbol sym) {
+        if(alphabet.contains(sym)) { return; }
+        bool is_there_some_dummy = false;
+        for (auto& [var, nfa] : *this) {
+            for (mata::nfa::State state = 0; state < nfa->num_of_states(); ++state) {
+                const mata::nfa::StatePost& delta_from_state = nfa->delta[state];
+                if (!delta_from_state.empty() && delta_from_state.back().symbol == util::get_dummy_symbol()) { // dummy symbol should be largest (we do not have epsilons), so should be at the back
+                    is_there_some_dummy = true;
+                    nfa->delta.add(state, sym, nfa->delta[state].back().targets);
+                }
+            }
+        }
+        if (is_there_some_dummy) {
+            alphabet.insert(sym);
+        }
+    }
+
+    void AutAssignment::replace_dummy_with_new_symbol() {
+        mata::Symbol new_symbol = regex::Alphabet(alphabet).get_unused_symbol();
+        bool is_there_some_dummy = false;
+        for (auto& [var, nfa] : *this) {
+            for (mata::nfa::State state = 0; state < nfa->num_of_states(); ++state) {
+                if (!nfa->delta[state].empty()) { // if there is some transition from state
+                    mata::nfa::StatePost& delta_from_state = nfa->delta.mutable_state_post(state); // then we can for sure get mutable transitions from state without side effect
+                    if (delta_from_state.back().symbol == util::get_dummy_symbol()) { // dummy symbol should be largest (we do not have epsilons), so should be at the back
+                        is_there_some_dummy = true;
+                        mata::nfa::StateSet targets = delta_from_state.back().targets;
+                        delta_from_state.pop_back();
+                        nfa->delta.add(state, new_symbol, targets);
+                    }
+                }
+            }
+        }
+        if (is_there_some_dummy) {
+            alphabet.insert(new_symbol);
+        }
+    }
 }

src/smt/theory_str_noodler/aut_assignment.h

@@ -194,6 +194,12 @@ namespace smt::noodler {
             }
         }
 
+        /// @brief Add symbol @p s to alphabet and removes it from dummy symbol (i.e. adds transitions trough @p s in all automata if there is transition trough dummy symbol)
+        void add_symbol_from_dummy(mata::Symbol s);
+
+        /// @brief Replace dummy symbol in all automata by a new symbol
+        void replace_dummy_with_new_symbol();
+
         /**
          * @brief Is language complement of a finite language?
          *