not-contains: implement not-contains > LIA reduction

src/smt/theory_str_noodler/ca_str_constr.h

@@ -26,58 +26,64 @@ namespace smt::noodler::ca {
     using AutMatrix = std::vector<std::vector<mata::nfa::Nfa>>;
 
     /**
-     * @brief Class representing copies of automata for each variable. 
-     * X axis = variables 
+     * @brief Class representing copies of automata for each variable.
+     * X axis = variables
      * Y axis = copy
      */
     class DiseqAutMatrix {
-    
+
     private:
         AutMatrix aut_matrix {};
         // order of variables
         std::vector<BasicTerm> var_order {};
         // starting state of each automaton
-        std::vector<size_t> offsets {};
+        std::vector<size_t> var_aut_init_states_in_copy {};
+
+        size_t number_of_states_in_row;
 
     protected:
         void create_aut_matrix(const Predicate& diseq, const AutAssignment& aut_ass);
 
         /**
          * @brief Recompute offsets.
          */
-        void recompute_offset();
+        void recompute_var_aut_init_state_positions();
 
         /**
          * @brief Get offset in the Big unified NFA (i.e., starting state of the particular NFA [ @p copy, @p var ] in the Big NFA)
-         * 
+         *
          * @param copy Copy index
          * @param var Variable index
          * @return size_t Smallest/starting state
          */
-        size_t get_offset(size_t copy, size_t var) const {
-            return this->offsets[copy*this->var_order.size() + var];
-        } 
+        size_t get_var_aut_init_state_pos(size_t copy, size_t var) const {
+            return this->var_aut_init_states_in_copy[copy*this->var_order.size() + var];
+        }
 
-    public: 
-        DiseqAutMatrix(const Predicate& diseq, const AutAssignment& aut_ass) : aut_matrix(), var_order(), offsets() {
+    public:
+        DiseqAutMatrix(const Predicate& diseq, const AutAssignment& aut_ass) : aut_matrix(), var_order(), var_aut_init_states_in_copy() {
             create_aut_matrix(diseq, aut_ass);
         }
 
         /**
          * @brief Get state in unified automaton (where all automata in matrix are unioned).
-         * 
+         *
          * @param copy Index of the copy
          * @param var Index of the variable (index in @p var_order)
          * @param state State of the particular automaton at [ @p copy, @p var ]
          * @return mata::nfa::State State in the big NFA
          */
         mata::nfa::State get_union_state(size_t copy, size_t var, mata::nfa::State state) const {
-            return get_offset(copy, var) + state;
+            return get_var_aut_init_state_pos(copy, var) + state;
+        }
+
+        std::vector<size_t>& get_var_init_states_pos_in_copies() {
+            return this->var_aut_init_states_in_copy;
         }
 
         /**
          * @brief Unify all particular automata into a single NFA.
-         * 
+         *
          * @return mata::nfa::Nfa Big NFA
          */
         mata::nfa::Nfa union_matrix() const;
@@ -89,13 +95,21 @@ namespace smt::noodler::ca {
         void set_aut(size_t copy, size_t var, const mata::nfa::Nfa& aut, bool recomp_offset = false) {
             this->aut_matrix[copy][var] = aut;
             if(recomp_offset) {
-                recompute_offset();
+                recompute_var_aut_init_state_positions();
             }
         }
 
+        const std::vector<mata::nfa::Nfa>& get_matrix_row(size_t row_idx) const {
+            return this->aut_matrix[row_idx];
+        }
+
         const mata::nfa::Nfa& get_aut(size_t copy, size_t var) const {
             return this->aut_matrix[copy][var];
         }
+
+        size_t get_number_of_states_in_row() const {
+            return number_of_states_in_row;
+        }
     };
 
     /**
@@ -110,22 +124,22 @@ namespace smt::noodler::ca {
         ca::CounterAlphabet alph {};
 
     public:
-        TagDiseqGen(const Predicate& diseq, const AutAssignment& aut_ass) : aut_matrix(diseq, aut_ass), 
+        TagDiseqGen(const Predicate& diseq, const AutAssignment& aut_ass) : aut_matrix(diseq, aut_ass),
             aut_ass(aut_ass), diseq(diseq), alph() { }
 
     protected:
         /**
-         * @brief Replace symbols in a particular variable automaton. Replace original symbols with 
-         * the AtomicSymbols of the form <L,x> ...
-         * 
+         * @brief Replace symbols in the variable automaton in the matrix cell given by @p copy
+         *        and @p var with symbols of the form AtomicSymbols of the form <L,x>...
+         *
          * @param copy Copy identifying particular variable automaton
          * @param var Variable of the automaton
          */
         void replace_symbols(char copy, size_t var);
 
         /**
-         * @brief Add connections between copies. 
-         * 
+         * @brief Add connections between copies.
+         *
          * @param copy_start Starting copy (transitions source)
          * @param var Variable
          * @param aut_union Union automaton contains all copies in a single automaton.
@@ -135,7 +149,7 @@ namespace smt::noodler::ca {
     public:
         /**
          * @brief Construct tagged automaton for a single disequation.
-         * 
+         *
          * @return ca::CA Tagged automaton.
          */
         ca::TagAut construct_tag_aut();
@@ -144,23 +158,38 @@ namespace smt::noodler::ca {
             return this->aut_matrix;
         }
 
+
+        const Predicate& get_underlying_predicate() const {
+            return this->diseq;
+        };
+
     };
 
     /**
-     * @brief Get LIA formula for disequations. The LIA formula describes all length 
-     * models of the diseqation. 
-     * 
-     * TODO: So-far it supports only one disequation. 
-     * 
+     * @brief Get LIA formula for disequations. The LIA formula describes all length
+     * models of the diseqation.
+     *
+     * TODO: So-far it supports only one disequation.
+     *
      * @param diseqs Disequations
      * @param autass Automata assignmnent after stabilization
      * @return LenNode LIA formula describing lengths of string models
      */
     LenNode get_lia_for_disequations(const Formula& diseqs, const AutAssignment& autass);
 
+    /**
+     * @brief Construct a LIA formula that is true iff the RHS of the given @p not_contains is longer
+     *        than its LHS given a model of @p parikh_image
+     *
+     * @param not_contains A not-contains predicate whose RHS should be longer than its LHS
+     * @param autass Automata assignmnent after stabilization
+     * @return LenNode LIA formula that is true iff the RHS of the given not_contains is longer than its LHS
+    */
+    LenNode make_lia_rhs_longer_than_lhs(const Predicate& not_contains, const DiseqAutMatrix& automaton_matrix, const parikh::ParikhImage& parikh_image);
+
     /**
      * @brief Get LIA formula for not contains. So-far it performs only simple checks.
-     * 
+     *
      * @param not_conts Not contains
      * @param autass Automata assignmnent after stabilization
      * @return std::pair<LenNode, LenNodePrecision> LIA formula describing lengths of string models together with the precision.