fzn2z3 cannot access file

[oferst]

Trying to use fzn2z3, but it seems to get stuck on accessing some file (formula.smt2) that it seems to generate. I checked that this file indeed exists and it is not locked or used by anything else. Any idea ? (the same example\coloring.fzn works fine with fzn2optimathsat).

Here is the output:

c:\temp\fzn2omt-master>bin\fzn2z3.py examples\coloring.fzn
Traceback (most recent call last):
  File "C:\temp\fzn2omt-master\bin\fzn2z3.py", line 68, in zthree_solve
    zthree_compile(config)
  File "C:\temp\fzn2omt-master\bin\fzn2z3.py", line 190, in zthree_compile
    make_smtlib_compatible_with_zthree(config, optimathsat_config)
  File "C:\temp\fzn2omt-master\bin\fzn2z3.py", line 264, in make_smtlib_compatible_with_zthree
    shutil.copy(tmp_file_name, config.smt2)
  File "C:\Users\Ofer\AppData\Local\Programs\Python\Python38-32\lib\shutil.py", line 415, in copy
    copyfile(src, dst, follow_symlinks=follow_symlinks)
  File "C:\Users\Ofer\AppData\Local\Programs\Python\Python38-32\lib\shutil.py", line 261, in copyfile
    with open(src, 'rb') as fsrc, open(dst, 'wb') as fdst:
OSError: [Errno 22] Invalid argument: 'C:\\Users\\Ofer\\AppData\\Local\\Temp\\tmpaavd6a_r\\formula.smt2'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "C:\Users\Ofer\AppData\Local\Programs\Python\Python38-32\lib\shutil.py", line 613, in _rmtree_unsafe
    os.unlink(fullname)
PermissionError: [WinError 32] The process cannot access the file because it is being used by another process: 'C:\\Users\\Ofer\\AppData\\Local\\Temp\\tmpa
avd6a_r\\formula.smt2'

[PatrickTrentin88]

@oferst I apologize for this inconvenience, I shouldn't have tested the project on linux only. I'll take a look as soon as I can. How urgent is this?

[oferst]

Again, I wouldn’t want to impose my needs on your schedule .... Thanks, Patrick,

Ofer

[PatrickTrentin88]

Again, I wouldn’t want to impose my needs on your schedule

There is no imposition, I am asking for reference. Please provide a timeline for both issues.

[oferst]

I normally use one of the minizinc built-in engines, and I have many instances (mostly from scheduling problems) that cannot be solved by any of them. Your tool gives me hope that through the SMT route I might be able to. I am surprised and encouraged by your results that through this route MathSAT beats Gurobi. Originally I tried to model these problems directly in PBS and in SMT, but Gurobi was far better. So perhaps your new route will prove me otherwise. So I will wait patiently until it is ready even if it is in a month.

Thanks again, Ofer

[PatrickTrentin88]

@oferst I fixed the problem you submitted. Some regular expressions appears to be broken on windows due to the characters ^$, I'll fix it later today. I'll close this issue when the software will pass the unit-tests.

[oferst]

yes, a known windows problem in their folder structures. Thanks, Ofer

[PatrickTrentin88]

@oferst I have tested fzn2optimathsat.py and fzn2z3.py on windows, and they both appear to be working as intended now. I am closing this issue.

[oferst]

Please confirm that you got this one. Ofer

[PatrickTrentin88]

@oferst I get the message, but no file. You may want to try pastebin.com

[oferst]

Please change suffix to .fzn (apparently github does not agree to upload fzn): Hakbatzot.txt

[PatrickTrentin88]

@oferst delete the first line and it should work

> python bin/fzn2optimathsat.py examples/Hakbatzot.fzn
% objective: X_INTRODUCED_494_ (optimal model)
teacher_gaps_soft = 0;
unscheduled = 2;
max_teacher_hours_violations = 0;
m_timetable = array3d(1..3, 1..6, 1..8, [true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]);
----------
==========

[oferst]

Indeed it solves it. But this line is generated by mzn2fzn. Is there a way to tell it not to ? otherwise I'l need to write a script to remove such lines (can there be more than one in the fzn file of this form ?)

[PatrickTrentin88]

@oferst

Indeed it solves it. But this line is generated by mzn2fzn. Is there a way to tell it not to ? otherwise I'l need to write a script to remove such lines (can there be more than one in the fzn file of this form ?)

The FlatZinc documentation says that only non-standard predicates must be declared at the top of a FlatZinc model:

Predicates used in the model that are not standard FlatZinc must be declared at the top of a FlatZinc model, before any other lexical items. Predicate declarations take the form

<predicate-item> ::= "predicate" <identifier> "(" [ <pred-param-type> : <identifier> "," ... ] ")" ";"

source: link

However, half-reified predicates appear to be part of the standard.

Therefore, I would expect mzn2fzn to not print such predicate at the top of the generated FlatZinc file. I must get in touch with the MiniZinc team before choosing how to address this issue (see: Stackoverflow Q/A).

Can you please provide the MiniZinc file?

[PatrickTrentin88]

@oferst a MiniZinc dev confirmed that builtin half-reified predicates can be declared at the top of a model. Thus, I have updated OptiMathSAT to ignore such declarations. Please download version 1.7.1 again.

[oferst]

Dear Patrick, Is there a way to set a timeout to fzn2optimathsat or to optimathsat itself ?

-- Ofer

From: PatrickTrentin88 notifications@github.com Sent: Friday, June 5, 2020 10:22 AM To: PatrickTrentin88/fzn2omt fzn2omt@noreply.github.com Cc: Ofer Strichman ofers@technion.ac.il; Mention mention@noreply.github.com Subject: Re: [PatrickTrentin88/fzn2omt] fzn2z3 cannot access file (#7)

@ofersthttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Foferst&data=02%7C01%7Cofers%40technion.ac.il%7Cf04973e322854796993308d809211b13%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637269385974912637&sdata=2rqfs%2Fjht5%2FhB%2Bq69k9wEbKtt28Tdb3ga7OzJlPfS48%3D&reserved=0 a MiniZinc dev confirmed that builtin half-reified predicates can be declared at the top of a model. Thus, I have updated OptiMathSAT to ignore such declarations. Please download version 1.7.1 again.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHubhttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FPatrickTrentin88%2Ffzn2omt%2Fissues%2F7%23issuecomment-639305717&data=02%7C01%7Cofers%40technion.ac.il%7Cf04973e322854796993308d809211b13%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637269385974922633&sdata=rBW3xiuJKBAjGbN4uWnSJLq8DPHIqx1PSJxgxXmu0Po%3D&reserved=0, or unsubscribehttps://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FACLFDDGHXW6JLBV5ZR3JMI3RVCMIBANCNFSM4NQ7QAGQ&data=02%7C01%7Cofers%40technion.ac.il%7Cf04973e322854796993308d809211b13%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637269385974922633&sdata=CFVRyeS%2BgB0MJOpM5PfpfHFPBsuPIkAY8veuACzDXVo%3D&reserved=0.

This email is from an external mail server, be judicious when opening attachments or links

[PatrickTrentin88]

Dear Patrick, Is there a way to set a timeout to fzn2optimathsat or to optimathsat itself ?

Due to a decision beyond my control, it is only available in the restricted release or via the SMT-LIB interface. I would suggest to use an external tool (e.g. timeout) to ensure that the software terminates within a given timeout.