Error in Installing

[AnkitMU]

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

[Adda0]

Hello. From the error message, it seems that you do not have the automata library Mata installed properly. You should have Mata installed in /usr/local/include/mata. Can you verify that you have Mata installed in this or similar location where the system looks for libraries? Furthermore, which OS do you use?

[AnkitMU]

I'm using Mac OS (m1) 14.3.

[Adda0]

Thank you. And what about the installation of Mata? Does (non-empty) mata folder exist in your include directories searched by the system?

[AnkitMU]

suppose im running these command in my Download.

git clone 'https://github.com/VeriFIT/mata.git' cd mata make release make install

I got mata/include/mata/utils and there are file inside utils folder im getting error on make install step at 64%

[Adda0]

First of, instead of make install, one should run sudo make install to install Mata properly. We seem to miss the sudo command in our installation instructions. Not sure whether system would pick Mata up when using only make install.

Second, post the error you are getting, please. There might be some inconsistencies between Linux and MacOS causing the build to crash on different compiler versions etc., even though we have several people developing Mata on MacOS sucessfully.

[AnkitMU]

After running the following command step 1: git clone 'https://github.com/VeriFIT/z3-noodler.git' step 2: mkdir z3-noodler/build step 3: cd z3-noodler/build step 4: cmake -DCMAKE_BUILD_TYPE=Release .. step 5: make

This is the exact error that im facing while installing step 5

[ 66%] Building CXX object src/smt/CMakeFiles/smt.dir/smt_setup.cpp.o In file included from /Users/ankitjha/Downloads/OCl/z3-noodler/src/smt/smt_setup.cpp:41: In file included from /Users/ankitjha/Downloads/OCl/z3-noodler/src/smt/theory_str_noodler/theory_str_noodler.h:34: In file included from /Users/ankitjha/Downloads/OCl/z3-noodler/src/smt/theory_str_noodler/decision_procedure.h:11: /Users/ankitjha/Downloads/OCl/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

[Adda0]

Thank you. This error indicates your system cannot find Mata installed in your library paths. Did you try reinstalling Mata with make release, followed by sudo make install, as advised above?

[AnkitMU]

step 1 : cd mata step 2 :make release (I got following after executing step2 ) cmake -B build -S . -DCMAKE_BUILD_TYPE=Release -- Default C++ compiler: /Library/Developer/CommandLineTools/usr/bin/c++ -- Could NOT find Doxygen (missing: DOXYGEN_EXECUTABLE) CMake Warning at CMakeLists.txt:45 (message): Doxygen not found. Documentation will not be built

-- Configuring done (0.4s) -- Generating done (0.1s) -- Build files have been written to: /Users/ankitjha/Downloads/OCl/mata/build cmake --build build --parallel -j 6 [ 1%] Built target simlib [ 8%] Built target re2 [ 57%] Built target cudd [ 67%] Built target libmata [ 68%] Built target example03-lang-empty [ 69%] Built target example06-mintermization [ 70%] Built target example05-parsing [ 71%] Built target example01-simple [ 73%] Built target example04-complement [ 74%] Built target example02-determinize [ 76%] Built target bench-bool-comb-cox-diff [ 78%] Built target bench-email-filter [ 79%] Built target bench-bool-comb-cox-inter [ 81%] Built target bench-bool-comb-intersect [ 82%] Built target bench-automata-inclusion [ 83%] Built target binary-operations [ 85%] Built target test-unary-op [ 86%] Built target reduce_epsilon [ 88%] Built target nfa-operations [ 90%] Built target unary-operations [100%] Built target tests step 4: sudo make install /Library/Developer/CommandLineTools/usr/bin/make -C build install [ 49%] Built target cudd [ 56%] Built target re2 [ 57%] Built target simlib [ 67%] Built target libmata [ 68%] Built target example01-simple [ 69%] Built target example02-determinize [ 70%] Built target example03-lang-empty [ 72%] Built target example04-complement [ 73%] Built target example05-parsing [ 74%] Built target example06-mintermization [ 84%] Built target tests [ 85%] Built target bench-automata-inclusion [ 87%] Built target bench-bool-comb-cox-diff [ 88%] Built target bench-bool-comb-cox-inter [ 90%] Built target bench-bool-comb-intersect [ 92%] Built target bench-email-filter [ 93%] Built target binary-operations [ 95%] Built target nfa-operations [ 96%] Built target reduce_epsilon [ 98%] Built target test-unary-op [100%] Built target unary-operations Install the project... -- Install configuration: "Release" -- Installing: /usr/local/lib/libmata.a -- Up-to-date: /usr/local/include -- Up-to-date: /usr/local/include/mata -- Up-to-date: /usr/local/include/mata/nfa -- Up-to-date: /usr/local/include/mata/nfa/delta.hh -- Up-to-date: /usr/local/include/mata/nfa/builder.hh -- Up-to-date: /usr/local/include/mata/nfa/nfa.hh -- Up-to-date: /usr/local/include/mata/nfa/strings.hh -- Up-to-date: /usr/local/include/mata/nfa/plumbing.hh -- Up-to-date: /usr/local/include/mata/nfa/algorithms.hh -- Up-to-date: /usr/local/include/mata/nfa/types.hh -- Up-to-date: /usr/local/include/mata/alphabet.hh -- Up-to-date: /usr/local/include/mata/utils -- Up-to-date: /usr/local/include/mata/utils/closed-set.hh -- Up-to-date: /usr/local/include/mata/utils/sparse-set.hh -- Up-to-date: /usr/local/include/mata/utils/utils.hh -- Up-to-date: /usr/local/include/mata/utils/synchronized-iterator.hh -- Up-to-date: /usr/local/include/mata/utils/ord-vector.hh -- Up-to-date: /usr/local/include/mata/parser -- Up-to-date: /usr/local/include/mata/parser/parser.hh -- Up-to-date: /usr/local/include/mata/parser/re2parser.hh -- Up-to-date: /usr/local/include/mata/parser/inter-aut.hh -- Up-to-date: /usr/local/include/mata/parser/mintermization.hh -- Up-to-date: /usr/local/include -- Up-to-date: /usr/local/include/mata -- Up-to-date: /usr/local/include/mata/cudd -- Up-to-date: /usr/local/include/mata/cudd/cuddObj.hh -- Up-to-date: /usr/local/include/mata/cudd/cudd.h -- Up-to-date: /usr/local/include -- Up-to-date: /usr/local/include/mata -- Up-to-date: /usr/local/include/mata/simlib -- Up-to-date: /usr/local/include/mata/simlib/util -- Up-to-date: /usr/local/include/mata/simlib/util/simlib.hh -- Up-to-date: /usr/local/include/mata/simlib/util/splitting_relation.hh -- Up-to-date: /usr/local/include/mata/simlib/util/smart_set.hh -- Up-to-date: /usr/local/include/mata/simlib/util/shared_list.hh -- Up-to-date: /usr/local/include/mata/simlib/util/shared_counter.hh -- Up-to-date: /usr/local/include/mata/simlib/util/caching_allocator.hh -- Up-to-date: /usr/local/include/mata/simlib/util/two_way_dict.hh -- Up-to-date: /usr/local/include/mata/simlib/util/transl_weak.hh -- Up-to-date: /usr/local/include/mata/simlib/util/abstract_transl.hh -- Up-to-date: /usr/local/include/mata/simlib/util/binary_relation.hh -- Up-to-date: /usr/local/include/mata/simlib/util/convert.hh -- Up-to-date: /usr/local/include/mata/simlib/explicit_lts.hh

After this step when I try to install z3-Noodler it gives me same error.

[Adda0]

Thank you. That is the correct installation process. Then, I am not sure why your system cannot detect the library. Can you verify that your system checks /usr/local/include for libraries? As we can see,

 -- Up-to-date: /usr/local/include/mata/nfa/nfa.hh

mata/nfa/nfa.hh is in the correct location.

[Adda0]

Additionally, if your system does not include usr/local/include in your paths, try running the command from an answer on SO on a similar topic. It might solve the issue.

[AnkitMU]

Thanks, This worked for me , but Im facing a problem while running a .smt2 file .

(declare-fun first_name (Int) String) (declare-fun last_name (Int) String) (declare-fun email (Int) String) (declare-fun Address (Int) String) (declare-fun Account_number (Int) Int) (define-fun Person ((o Int)) Bool true )

(assert (forall ((o Int)) (=> (Person o) (and (> (str.len (first_name o)) 5) (str.in.re (first_name o) (re.* (re.range "a" "z"))) ) )) )

(assert (forall ((o Int)) (=> (Person o) (and (> (str.len (last_name o)) 5) (str.in.re (last_name o) (re.* (re.union (re.range "A" "Z") (re.range "a" "z")))) ) )) )

(assert (forall ((o Int)) (=> (Person o) (not (= (first_name o) (last_name o))) )) )

(assert (forall ((o Int)) (=> (Person o) (= (email o) (str.++ (first_name o) "." (last_name o) "@mu.ie")) )) )

(assert (forall ((o Int)) (=> (Person o) (str.suffixof "mu.ie" (email o)) )) )

(assert (forall ((o Int)) (=> (Person o) (and (> (str.len (Address o)) 14) (str.in.re (Address o) (re.* (re.union (re.range "A" "Z") (re.range "a" "z")))) ) )) )

(assert (forall ((o Int)) (=> (Person o) (and (<= (Account_number o) 9999999999) (>= (Account_number o) 1000000000) ) )) )

(assert (exists ((o Int)) (Person o)))

(check-sat) (get-value ((first_name 1)(last_name 1)(email 1)(Address 1)(Account_number 1)))

this is my file the Im trying to run for noodler

for z3 it is giving me the sat value as well as model. as ./z3 file.smt2 sat (((first_name 1) "hkckhs") ((last_name 1) "pKpPsK") ((email 1) "hkckhs.pKpPsK@mu.ie") ((Address 1) "DPPHbPKKPppkKCS") ((Account_number 1) 1000000000))

But, when im trying to run for noodler it is not giving me any sat value , so there is no model. ./z3 smt.string_solver="noodler" file.smt2 unknown (error "line 70 column 78: model is not available")

[Adda0]

Noodler currently does not support providing models for the results. We plan to implement model extraction at some point, but as of now, there is no support.

Second, Noodler supports at this point in time only quantifier-free theory of strings (so no universal quantifiers) and we do not support user-defined functions such as (declare-fun first_name (Int) String), i.e. you can only have string constants.

[AnkitMU]

Thanks for the information

[Adda0]

Unless you have other questions, I would close this issue as resolved. If you need any help or have any more questions, feel free to open another issue or create a new discussion. Have a great day.