Running Messy

[aleksdimovski]

Hello,

I am trying to run Messy on max2-impv.sem taken from Semgus-Benchmarks.

• I first convert sem file to jason
  $ semgus-parser --format json --mode batch --output max2-impv.json -- max2-impv.sem

• Then, try to run with Messy
  $ scala Messy-1.0-fat.jar -i max2-impv.json

obtain:
Translating max2-impv.json to an SMT file
ExternalParseException: Unexpected event supplied by external JSON parser
at semgusJava.package$.translateEvent(package.scala:117)
at semgusJava.package$.$anonfun$translate2Semgus$1(package.scala:121)
at scala.collection.immutable.List.map(List.scala:250)
at semgusJava.package$.translate2Semgus(package.scala:121)
at semgusJava.package$.JSON2Semgus(package.scala:123)
at Main$.main(Main.scala:24)
at Main.main(Main.scala)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
at scala.tools.nsc.JarRunner$.run(MainGenericRunner.scala:13)
at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
at scala.tools.nsc.JarRunner$.runJar(MainGenericRunner.scala:25)
at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:69)
at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

If I use
$ scala Messy-1.0-fat.jar -i max2-impv.sem

Translating max2-impv.sem to an SMT file
Unexpected character (;) at position 0.
at org.json.simple.parser.Yylex.yylex(Yylex.java:610)
at org.json.simple.parser.JSONParser.nextToken(JSONParser.java:269)
at org.json.simple.parser.JSONParser.parse(JSONParser.java:118)
at org.json.simple.parser.JSONParser.parse(JSONParser.java:81)
at org.json.simple.parser.JSONParser.parse(JSONParser.java:75)
at org.semgus.java.event.EventParser.parse(EventParser.java:58)
at semgusJava.package$.parseSemgusFile(package.scala:44)
at semgusJava.package$.JSON2Semgus(package.scala:123)
at Main$.main(Main.scala:24)
at Main.main(Main.scala)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
at scala.tools.nsc.JarRunner$.run(MainGenericRunner.scala:13)
at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
at scala.tools.nsc.JarRunner$.runJar(MainGenericRunner.scala:25)
at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:69)
at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

Thank you,

[kjcjohnson]

Try passing the --no-function-events flag to the parser:

$ semgus-parser --format json --mode batch --output max2-impv.json --no-function-events -- max2-impv.sem

Messy is using an older version of the Semgus-Java library (see #1), which doesn't support some features of recent semgus-parser versions. I suspect that's what's going on here.

[aleksdimovski]

Yes, this is ok ... However, once I get json file and the corresponding out.z3 file using messy, how do I run out.z3 in order to get the model if out.z3 is sat ...
E.g. let's take the example cube_4_2.sl from benchmarks/boolean/cube
$ semgus-parser --no-function-events --format json --mode batch --output cube_4_2.json -- cube_4_2.sl
$ scala Messy-1.0-fat.jar -i cube_4_2.json
I obtain out.z3 that I cannot run it with z3 ... I tired: $z3 fp.engine=spacer out.z3, $ z3 out.z3, but no model is returned ... I have z3 version 4.11.2 ...
This is the obtained out.z3 file:

(declare-datatypes () ((B ($var ($varAc1 V)) ($and ($andAc2 B) ($andAc3 B)))
(V $v0 $v1 $v2 $v3)))
(declare-var bt1 B)
(declare-var v1 Bool)
(declare-var bt2 B)
(declare-var r1 Bool)
(declare-var v2 Bool)
(declare-var vt V)
(declare-var r Bool)
(declare-var v0 Bool)
(declare-var bt B)
(declare-var result Bool)
(declare-var v3 Bool)
(declare-var r2 Bool)
(declare-var @B__agtt.SynVar1 B)
(declare-var formula B)
(declare-var @B__agtt.SynVar0 B)
(declare-var @V__agtt.SynVar0 V)
(declare-var @B__agtt.SynVar2 B)
(declare-var @V__agtt.SynVar1 V)
(declare-rel B.Sem (B Bool Bool Bool Bool Bool))
(declare-rel V.Sem (V Bool Bool Bool Bool Bool))
(declare-rel realizable ())
(declare-rel @B__agtt.Syn (B))
(declare-rel @V__agtt.Syn (V))
(rule (=> (and (= @B__agtt.SynVar0 ($var @V__agtt.SynVar1)) (@V__agtt.Syn @V__agtt.SynVar1)) (@B__agtt.Syn @B__agtt.SynVar0)))
(rule (=> (and (= @B__agtt.SynVar0 ($and @B__agtt.SynVar1 @B__agtt.SynVar2)) (@B__agtt.Syn @B__agtt.SynVar1) (@B__agtt.Syn @B__agtt.SynVar2)) (@B__agtt.Syn @B__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v2) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v3) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v0) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v1) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (and (= bt ($var (as vt V))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r Bool)) (= (as result Bool) (as r Bool))) (B.Sem (as bt B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= bt ($and (as bt1 B) (as bt2 B))) (B.Sem (as bt1 B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r1 Bool)) (B.Sem (as bt2 B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r2 Bool)) (= (as result Bool) (and (as r1 Bool) (as r2 Bool)))) (B.Sem (as bt B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v0) (= (as result Bool) (as v0 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v1) (= (as result Bool) (as v1 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v2) (= (as result Bool) (as v2 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v3) (= (as result Bool) (as v3 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (B.Sem formula false true true false true) (B.Sem formula false true false false false) (B.Sem formula true false true false false)) realizable))
(query realizable)

[kjcjohnson]

I think this is a question for Jinwoo @kjw227