epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

Help with compilation #60

Closed greninja closed 6 years ago

greninja commented 6 years ago

a) I have 1) sbt - 0.13.2 2) scala - 2.10.3 3) Z3 - 4.4.1 ...on my machine. I am aware these are outdated versions but its for a specific project.

Now, I followed the steps mentioned here. But the JAR file it generated was - 'sbl_2.10-0.1-SNAPSHOT.jar'. It does not match with the pattern mentioned in the para.

b) Also, running simple "import z3.model._" in scala interpreter gives the following error : <console>:7: error: not found: value z3

Can anyone help?

romac commented 6 years ago

What happens if you run sbt +test?

greninja commented 6 years ago

The directory structure of the project (actually it is one of Ali Sinan's project that I am trying to run) is :

.
├── build.sbt
├── lib
│   ├── linux
│   │   └── scalaz3-unix-64b-2.1.jar
│   └── mac
│       └── scalaz3-osx-64b-2.1.jar
├── LICENSE
├── programs
│   ├── current-program -> VPC1.scala
│   ├── Sensors.scala
│   ├── VPC1.scala
│   ├── VPC2.scala
│   ├── VPC3.scala
│   └── VPC4.scala
├── README.md
├── scripts
│   ├── set-program-and-spec
│   ├── synthesize-sensors
│   └── synthesize-vpc1
├── specifications
│   ├── current-specification -> vpc
│   ├── sensors
│   ├── vpc
│   ├── vpc-384
│   └── vpc-pruned
└── src
    └── main
        └── scala
            └── elegans
                ├── BooleanStatelessSemantics.scala
                ├── CEGIS.scala
                ├── Cells.scala
                ├── Constraints.scala
                ├── Experiments.scala
                ├── Graphs.scala
                ├── Interpreter.scala
                ├── Invariants.scala
                ├── Main.scala
                ├── Model.scala -> ../../../../programs/current-program
                ├── package.scala
                ├── RunningMethods.scala
                ├── Schedules.scala
                ├── Semantics.scala
                ├── Serialization.scala
                ├── Settings.scala
                ├── StatefulSemantics.scala
                ├── Statistics.scala
                ├── Stopwatch.scala
                ├── Summaries.scala
                ├── TimerSemantics.scala
                ├── TraceSummarization.scala
                ├── Trees.scala
                └── Visualizer.scala

Running sbt +test gives me this:

[info] Set current project to sbl (in build file:/home/shadab/Downloads/sbl/)
[info] Setting version to 2.10.3
[info] Set current project to sbl (in build file:/home/shadab/Downloads/sbl/)
[info] Updating {file:/home/shadab/Downloads/sbl/}sbl...
[info] Resolving org.fusesource.jansi#jansi;1.4 ...
[info] Done updating.
[info] Compiling 24 Scala sources to /home/shadab/Downloads/sbl/target/scala-2.10/classes...
[warn] /home/shadab/Downloads/sbl/src/main/scala/elegans/TimerSemantics.scala:198: match may not be exhaustive.
[warn] It would fail on the following input: Some((x: elegans.LogicSolution forSome x not in elegans.TimerSolution))
[warn]       sol.get(id) match {
[warn]              ^
[warn] there were 36 deprecation warning(s); re-run with -deprecation for details
[warn] there were 16 feature warning(s); re-run with -feature for details
[warn] three warnings found
java.lang.NoSuchMethodError: scala.Predef$.ArrowAssoc(Ljava/lang/Object;)Ljava/lang/Object;
    at org.scalatest.tools.FriendlyParamsTranslator$.<init>(FriendlyParamsTranslator.scala:23)
    at org.scalatest.tools.FriendlyParamsTranslator$.<clinit>(FriendlyParamsTranslator.scala)
    at org.scalatest.tools.Framework.runner(Framework.scala:1024)
    at sbt.Defaults$$anonfun$createTestRunners$1.apply(Defaults.scala:488)
    at sbt.Defaults$$anonfun$createTestRunners$1.apply(Defaults.scala:483)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
    at scala.collection.immutable.Map$Map1.foreach(Map.scala:109)
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:244)
    at scala.collection.AbstractTraversable.map(Traversable.scala:105)
    at sbt.Defaults$.createTestRunners(Defaults.scala:483)
    at sbt.Defaults$.allTestGroupsTask(Defaults.scala:498)
    at sbt.Defaults$$anonfun$testTasks$4.apply(Defaults.scala:364)
    at sbt.Defaults$$anonfun$testTasks$4.apply(Defaults.scala:364)
    at scala.Function8$$anonfun$tupled$1.apply(Function8.scala:35)
    at scala.Function8$$anonfun$tupled$1.apply(Function8.scala:34)
    at scala.Function1$$anonfun$compose$1.apply(Function1.scala:47)
    at sbt.$tilde$greater$$anonfun$$u2219$1.apply(TypeFunctions.scala:42)
    at sbt.std.Transform$$anon$4.work(System.scala:64)
    at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:237)
    at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:237)
    at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:18)
    at sbt.Execute.work(Execute.scala:244)
    at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:237)
    at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:237)
    at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:160)
    at sbt.CompletionService$$anon$2.call(CompletionService.scala:30)
    at java.util.concurrent.FutureTask.run(FutureTask.java:266)
    at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
    at java.util.concurrent.FutureTask.run(FutureTask.java:266)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
    at java.lang.Thread.run(Thread.java:748)
[error] (test:executeTests) java.lang.NoSuchMethodError: scala.Predef$.ArrowAssoc(Ljava/lang/Object;)Ljava/lang/Object;
[error] Total time: 25 s, completed May 3, 2018 11:08:37 AM
greninja commented 6 years ago

To provide you with more details :

1) running sbt compile from the root directory of the project runs fine:

shadab@hp:~/Downloads/sbl$ sbt compile
OpenJDK 64-Bit Server VM warning: ignoring option MaxPermSize=256m; support was removed in 8.0
[info] Set current project to sbl (in build file:/home/shadab/Downloads/sbl/)
[success] Total time: 1 s, completed May 3, 2018 11:40:36 AM

2) sbt run is what throws error :

shadab@hp:~/Downloads/sbl$ sbt run
OpenJDK 64-Bit Server VM warning: ignoring option MaxPermSize=256m; support was removed in 8.0
[info] Set current project to sbl (in build file:/home/shadab/Downloads/sbl/)
[info] Running elegans.Main 
Loading scalaz3
[ERROR] Sanity check for symbolic run: FAILED
[ERROR] sanity check fails
java.lang.RuntimeException: Nonzero exit code returned from runner: 1
    at scala.sys.package$.error(package.scala:27)
[trace] Stack trace suppressed: run last compile:run for the full output.
[error] (compile:run) Nonzero exit code returned from runner: 1
[error] Total time: 3 s, completed May 3, 2018 11:42:01 AM

If you can help me with this, it'd be great

koksal commented 6 years ago

Shadab,

I see from your other posts that you ended up successfully running ScalaZ3 within your desired context. Since your problem was not relevant to this project, I think this issue can be closed.

ali