verifit / z3-noodler Goto Github PK

Currently, if we get contains predicate, we call both handle_contains() and handle_not_contains() functions. However, handle_not_contains can add it to m_not_contains_todo, which automatically leads to unknown result, even if negated contains does not occur in the formula. It should be checked in assign_eh whether we really got negated contains or not, and only return unknown in the negated case.

Implement the Nielsen transformation for efficient solving of quadratic equations.

The support for these predicates should be hopefully doable without major changes in the decision procedure.

These two predicates are defined in the string theory, so we should probably add support for them eventually. But they do not show up in the benchmarks. We can probably solve it similarly to disequations, but there might be some problems.

We give sat on QF_SLIA/2019-full_str_int/py-conbyte_trauc/leetcode_int-numDecodings/130.smt2 for z3-noodler-3233733-2cddb2f on release version on pikachu (and everywhere else we give unknown, so it is not possible to debug). See #133

The current rewriter of Z3 does a lot of unknown stuff for us, and some of it can be damaging for noodler. Sometimes it even brings stuff from seq theory, for example by running this

(set-logic QF_S)
(declare-fun s1 () String)
(assert (str.in_re "abbbe" (str.to_re s1)))
(check-sat)

we get (seq.nth_i s1 0) in relevant_eh() which we cannot handle right now.

For example running

(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)

(declare-fun var_x () String)
(declare-fun var_y () String)
(declare-fun var_z () String)
(declare-fun var_u () String)
(declare-fun var_w () String)

; xyx = zu ∧ ww = xa ∧ u ∈ (baba)^∗ a ∧ z ∈ a(ba)^∗
(assert (= (str.++ var_x var_y var_x) (str.++ var_z var_u)))
(assert (= (str.++ var_w var_w) (str.++ var_x "a")))
(assert (str.in_re var_u (re.++ (re.* (re.++ (str.to_re "b") (str.to_re "a") (str.to_re "b") (str.to_re "a"))) (str.to_re "a"))))
(assert (str.in_re var_z (re.++ (str.to_re "a") (re.* (re.++ (str.to_re "b") (str.to_re "a") )))))
(check-sat)
(exit)

somehow produces automata in noodles that have unreachable states, even though noodlification is called with reducing turned on.

In Slog benchmarks, there are instances using re.replace. In theory, we should be able to solve those, but we need to test that it is truth in praxis.

For example, see QF_S/2019-Jiang/slog/slog_stranger_56_sink.smt2.

So far we have util::mk_str_var_fresh and theory_str_noodler::mk_str_var_fresh with the same semantics. We should unify them.

Optimize construction of automata from regular expressions with the aim at large regexes.

As of now, we say that expr is variable when it is app that has zero parameters. However, this holds true for, for example, integer literal, boolean constants and possibly more expr constructs.

We should find out how to precisely find variables in expr tree and use this solution in our solver.

As a temporary workaround, we now test only for string variables (as per #19) which we should be able to distinguish from string literals.

Add support for efficient handling of specific predicate instances:

• str.substr "B" z z
• str.substr "" 1 z str.substr "" z z
• str.replace "A" x y
• str.replace "" x y
• str.replace "B" x ""
• str.replace "B" x "A"
• str.replace "A" x "A"
• str.substr x 1 1 == str.at x 1

Currently, it seems that handle_substr is totally broken. It somehow mixes concatenation and length constraints into some nonsense AST.

We should pay some attention to a refactoring of the main theory files (theory_str_noodler).

Add a basic support for inequalities.

We could add a basic support for to_int/from_int. Maybe start with the case that the language is finite.

Current version of z3-noodler is not compatible with the current version of mata.

So far we have a stabilization-based decision procedure, procedure for solving regular language (dis)equalities, and in the future we will have a procedure tailored for quadratic equations. We should design a dispatcher that choses a best decision procedure for an instance in final_check.

Add options to represent predicates of the form notcontains(x,y) and k = to_int(x), x = from_int(k) inside the class Formula. Modify FormulaPreprocessor to handle these predicates (and hence get rid of parameters representing variables from the conversion arguments).

Some formulae introduced in predicate/function axiomatization may be implemented inside the theory rewriter. We could better move them there to make the axiomatization simpler.

We agreed that comments explaning functions should be in header files, where we only explain what is does, and in source files we keep how it does it.

For the input slog_stranger_1828_sink.smt2, the procedure for replacing string literals by BasicTerms returns different BasicTerm for the same string literal "//". We should get the BasicTerm literal with the same name.

So far, there is no handling of difficult not contains and replaceAll predicates. We need to return unknown if some of these occurs on the input.

Implement a conversion of an inclusion graph do dot format for a better understanding how the graphs are created.

It seems there is a fishy thing in automata assignment. For some input slog_stranger_64_sink.smt2, we get in the preprocessing automata assignment containing an Mata::NFA having IntAlphabet as an alphabet. If we then call AutAssignment::update_alphabet we get an exception, since get_alphabet_symbols is not defined for IntAlphabet. I think IntAlphabet should not be used for automata in an automata assignment.

I have followed the Readme instruction, unable to Install and got the following error. please do help.

z3-noodler/src/smt/theory_str_noodler/aut_assignment.h:12:10: fatal error: 'mata/nfa/nfa.hh' file not found
#include <mata/nfa/nfa.hh>
^~~~~~~~~~~~~~~~~
1 error generated.
make[2]: *** [src/smt/CMakeFiles/smt.dir/smt_setup.cpp.o] Error 1
make[1]: *** [src/smt/CMakeFiles/smt.dir/all] Error 2
make: *** [all] Error 2

The installation guide is not complete. So-far the installation fails on catch2 things.