extended calculation of info for regexes #4656

veanes · 2020-08-21T03:52:18Z

Added new fields to the info object and implemented their calculation rules.
In particular, this fixes some earlier issues with
min-length of compl as well as min-length of difference (that was buggy).
Also updated tracing of state_graph with regex info.
Introduced the trace tag "re_info" to trace info calculation of new regex expressions.

…aph with regex info

NikolajBjorner · 2020-08-21T04:03:17Z

There are build warnings for the initialization order.

You want this list:

	                valid(true), classical(is_classical), standard(is_standard), interpreted(is_interpreted), nonbranching(is_nonbranching),
                normalized(is_normalized), monadic(is_monadic), nullable(is_nullable), singleton(is_singleton), 
                min_length(min_l), star_height(star_h) {}

To have the same order as the appearances in the declarations.
Singleton and nullable are swapped.

             ^
src/smt/smt_context_inv.cpp
src/smt/theory_bv.cpp
src/smt/theory_str_regex.cpp
In file included from ../src/ast/static_features.h:26:0,
                 from ../src/smt/asserted_formulas.h:22,
                 from ../src/smt/smt_context.h:40,
                 from ../src/smt/smt_context_inv.cpp:19:
../src/ast/seq_decl_plugin.h: In constructor ‘seq_util::rex::info::info(bool, bool, bool, bool, bool, bool, bool, lbool, unsigned int, unsigned int)’:
../src/ast/seq_decl_plugin.h:432:19: warning: ‘seq_util::rex::info::nullable’ will be initialized after [-Wreorder]
             lbool nullable;
                   ^
../src/ast/seq_decl_plugin.h:430:18: warning:   ‘bool seq_util::rex::info::singleton’ [-Wreorder]
             bool singleton;
                  ^
../src/ast/seq_decl_plugin.h:446:13: warning:   when initialized here [-Wreorder]
             info(bool is_classical, 
             ^
In file included from ../src/ast/static_features.h:26:0,
                 from ../src/smt/asserted_formulas.h:22,
                 from ../src/smt/smt_context.h:40,
                 from ../src/smt/theory_bv.cpp:19:
../src/ast/seq_decl_plugin.h: In constructor ‘seq_util::rex::info::info(bool, bool, bool, bool, bool, bool, bool, lbool, unsigned int, unsigned int)’:
../src/ast/seq_decl_plugin.h:432:19: warning: ‘seq_util::rex::info::nullable’ will be initialized after [-Wreorder]
             lbool nullable;
                   ^
../src/ast/seq_decl_plugin.h:430:18: warning:   ‘bool seq_util::rex::info::singleton’ [-Wreorder]
             bool singleton;
                  ^
../src/ast/seq_decl_plugin.h:446:13: warning:   when

NikolajBjorner · 2020-08-21T04:05:45Z

src/ast/seq_decl_plugin.h

+            /* All bounded loops have a body that is a singleton. */
+            bool monadic;
+            /* Positive Boolean combination of ranges or predicates or singleton sequences. */
+            bool singleton;


need to be in same order during initialization

NikolajBjorner · 2020-08-21T04:08:20Z

src/ast/seq_decl_plugin.cpp

+        min_length = std::min(i1.min_length, i2.min_length);
+        nullable = (i1.nullable == i2.nullable ? i1.nullable : l_undef);
+        //TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
+        return info(false, false, false, false, i1.normalized && i2.normalized, i1.monadic && i2.monadic, i1.singleton && i2.singleton, nullable, min_length, std::max(i1.star_height, i2.star_height));
    }
    return invalid_info;


Since it is possible to return invalid_info, the combiners need to be defined if one of the infos is invalid.
Currently, initialization of invalid infos leave a lot of fields uninitialized. This leads to undefined behavior.

NikolajBjorner · 2020-08-21T04:09:10Z

src/ast/seq_decl_plugin.h

+            /* 
+              Constructs an invalid info
+            */
+            info() : valid(false) {}


better to assign default initialization to all fields.
You can use the syntax

lbool nullable { l_undef };

in the declarations to indicate default initializers.

NikolajBjorner · 2020-08-21T04:10:44Z

src/ast/seq_decl_plugin.cpp

        case OP_RE_STAR:
+            i1 = get_info_rec(e->get_arg(0));
+            return info(i1.classical, i1.classical, i1.interpreted, i1.nonbranching, i1.normalized, i1.monadic, false, l_true, 0, i1.star_height + 1);


Seems cleaner if you simply update i1, such as i1.star_height++;

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner · 2020-08-21T19:19:06Z

Note the build failures

uded from ../src/ast/rewriter/arith_rewriter.h:23:0,
                 from ../src/smt/arith_eq_solver.h:20,
                 from ../src/smt/arith_eq_solver.cpp:17:
../src/ast/seq_decl_plugin.h:488:23: error: expected class-name before ‘(’ token
             info compl() const;
                       ^

and regression failure (on the win64 build)

…aph with regex info

…aration order of methods

… re-info-extension

veanes · 2020-08-21T20:50:42Z

hopefully fixed regression (forgotten return stmt)
not sure about .."expected class-name before ‘(’ toke"
I believe this was because compl() declaration order did not match definition order?
With VS neither gave any compilation errors.

… invalid_info

NikolajBjorner · 2020-08-22T02:27:54Z

src/ast/seq_decl_plugin.h

+            info opt() const;
+            info complement() const;
+            info concat(info & rhs, bool lhs_is_concat) const;
+            info disj(info& rhs) const;


info const& rhs ?

NikolajBjorner · 2020-08-22T02:28:18Z

src/ast/seq_decl_plugin.h

        };
    private:
        seq_util&    u;
        ast_manager& m;
        family_id    m_fid;
        vector<info> mutable m_infos;
        expr_ref_vector mutable m_info_pinned;
-        info invalid_info;
+        info invalid_info{ info(l_undef) };


space after info before {

NikolajBjorner · 2020-08-22T02:28:45Z

src/ast/seq_decl_plugin.h

+            /* Value is either undefined (known=l_undef) or defined and known (l_true) or defined but unknown (l_false)*/
+            lbool known{ l_undef };
+            /* No complement, no intersection, no difference, and no if-then-else is used. Reverse is allowed. */
+            bool classical{ false };


space between classical and {

NikolajBjorner · 2020-08-22T02:29:42Z

src/ast/seq_decl_plugin.cpp

        case OP_RE_UNION:
            i1 = get_info_rec(e->get_arg(0));
            i2 = get_info_rec(e->get_arg(1));
-            return info(std::min(i1.min_length, i2.min_length));
+            return i1.disj(i2);


I think this was for the better. If you are really into overloading, you can use operator| or operator|| instead of disj.

I did these updates and also updated loop info calculation, worked on the same branch but since the PR was closed, I guess I need to open a new one for these

extended calculation of info for regexes, updated tracing of state_gr…

738d091

…aph with regex info

NikolajBjorner reviewed Aug 21, 2020

View reviewed changes

veanes and others added 3 commits August 21, 2020 05:38

took care of PR comments and fixed some info calculation bugs

4879258

fix rlimit for clang-10 (Z3Prover#4658)

22b5daf

merge

080be7a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

veanes added 4 commits August 21, 2020 13:00

extended calculation of info for regexes, updated tracing of state_gr…

93bc1bc

…aph with regex info

took care of PR comments and fixed some info calculation bugs

1099c51

added missing return statements, reordered def of compl to match decl…

3fb226d

…aration order of methods

Merge branch 're-info-extension' of https://github.com/veanes/z3 into…

6b11af7

… re-info-extension

veanes added 4 commits August 21, 2020 15:59

fixed loop lower bound bug in loop info and default nullable value in…

7b478c8

… invalid_info

fixed type bug: bool to lbool

8285162

trying to remove invisible control characters

4dd9249

renamed compl method (compl is a reserved c++ keyword) to complement

1e29ba7

NikolajBjorner merged commit db65381 into Z3Prover:master Aug 22, 2020

NikolajBjorner reviewed Aug 22, 2020

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

extended calculation of info for regexes #4656

extended calculation of info for regexes #4656

veanes commented Aug 21, 2020

NikolajBjorner commented Aug 21, 2020 •

edited

Loading

NikolajBjorner Aug 21, 2020

NikolajBjorner Aug 21, 2020

NikolajBjorner Aug 21, 2020

NikolajBjorner Aug 21, 2020 •

edited

Loading

NikolajBjorner commented Aug 21, 2020

veanes commented Aug 21, 2020

NikolajBjorner Aug 22, 2020

NikolajBjorner Aug 22, 2020

NikolajBjorner Aug 22, 2020

NikolajBjorner Aug 22, 2020

veanes Aug 22, 2020

extended calculation of info for regexes #4656

extended calculation of info for regexes #4656

Conversation

veanes commented Aug 21, 2020

NikolajBjorner commented Aug 21, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner Aug 21, 2020 • edited Loading

Choose a reason for hiding this comment

NikolajBjorner commented Aug 21, 2020

veanes commented Aug 21, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NikolajBjorner commented Aug 21, 2020 •

edited

Loading

NikolajBjorner Aug 21, 2020 •

edited

Loading