Adding sypet to repo
[Benchmarks_CSolver.git] / sypet / output / geometry / benchmark15.log
diff --git a/sypet/output/geometry/benchmark15.log b/sypet/output/geometry/benchmark15.log
new file mode 100644 (file)
index 0000000..a290b7c
--- /dev/null
@@ -0,0 +1,118 @@
+Buildfile: /scratch/satcheck/satproject/constraint_compiler/src/Benchmarks/sypet/build.xml
+
+sypet:
+     [java] ----------Options
+     [java] Verbose: false
+     [java] Timeout: 600000
+     [java] Round Robin: true
+     [java] Round Robin Iterations: 100
+     [java] Round Robin Range: 2
+     [java] Solver limit: 5
+     [java] ----------benchmarks/geometry/15/benchmark15.json
+     [java] Benchmark Id: 15
+     [java] Method name: getIntersection
+     [java] Packages: [java.awt.geom]
+     [java] Libraries: [./lib/rt7.jar]
+     [java] Source type(s): [java.awt.geom.Rectangle2D, java.awt.geom.Ellipse2D]
+     [java] Target type: java.awt.geom.Rectangle2D
+     [java] --------------------------------------------------------
+     [java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Cipher is a phantom class!
+     [java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
+     [java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.SecretKey is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
+     [java] Warning: javax.crypto.Mac is a phantom class!
+     [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+     [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+     [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+     [java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
+     [java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
+     [java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
+     [java] Warning: javax.crypto.CipherInputStream is a phantom class!
+     [java] Warning: javax.crypto.CipherOutputStream is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
+     [java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
+     [java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
+     [java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
+     [java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource is a phantom class!
+     [java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
+     [java] Warning: javax.crypto.KeyGenerator is a phantom class!
+     [java] #Classes: 50
+     [java] #Methods: 751
+     [java] Soot Time: 3547.579897
+     [java] PetriNet for path length: 1 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 2 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 3 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 4 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] PetriNet for path length: 5 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 13.853309
+     [java] Path Solving Time: 5.840024
+     [java] PetriNet for path length: 6 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 15.420463
+     [java] Path Solving Time: 31.253161
+     [java] Path Solving Time: 8.097906
+     [java] PetriNet for path length: 7 [places: 64 ; transitions: 537 ; edges: 1238]
+     [java] Path Solving Time: 14.15435
+     [java] Path Solving Time: 5.231169
+     [java] Path Solving Time: 1.760408
+     [java] Let's read clauses ...
+     [java] Let's read clauses ...
+     [java] Done with finding holes : Flag = true
+     [java] 1594753576193 Original Encoding Solving Time: 0.973717
+     [java] isSat= true ,SatuneSat= true
+     [java] 1594753576193Satune Solving Time: 31.469794
+     [java] =========Statistics (time in milliseconds)=========
+     [java] Benchmark Id: 15
+     [java] Sketch Generation Time: 99.766082
+     [java] Sketch Completion Time: 63.225662
+     [java] Compilation Time: 293.216654
+     [java] Running Test cases Time: 0.846772
+     [java] Synthesis Time: 163.83851599999997
+     [java] Total Time: 457.05517
+     [java] Number of components: 4
+     [java] Number of holes: 6
+     [java] Number of completed programs: 1
+     [java] Number of sketches: 1
+     [java] Solution:
+     [java]  java.awt.Shape sypet_var3 = sypet_arg1;
+     [java]  java.awt.geom.Path2D.Double sypet_var4 = new java.awt.geom.Path2D.Double(sypet_var3);
+     [java]  java.awt.geom.Rectangle2D sypet_var5 = sypet_var4.getBounds2D();
+     [java]  java.awt.geom.Rectangle2D sypet_var6 = sypet_var5.createIntersection(sypet_arg0);
+     [java]  return sypet_var6;
+     [java]  
+     [java] ============================
+     [java] Polarity time: 0.000036
+     [java] Preprocess time: 0.000021
+     [java] Decompose Order: 0.000017
+     [java] INFO: naive encoder is making the decision about element 0x7f792c8061a0....
+     [java] INFO: naive encoder is making the decision about element 0x7f792c806310....
+     [java] INFO: naive encoder is making the decision about element 0x7f792c805b40....
+     [java] INFO: naive encoder is making the decision about element 0x7f792c805c60....
+     [java] INFO: naive encoder is making the decision about element 0x7f792c805dd0....
+     [java] INFO: naive encoder is making the decision about element 0x7f792c806480....
+     [java] Encoding Graph Time: 0.000211
+     [java] Elapse Encode time: 0.000309
+     [java] Is problem UNSAT after encoding: 0
+     [java] #Clauses = 17      #Vars = 11
+     [java] Data is available now.
+     [java] CNF Encode time: 0.000001
+     [java] SAT Solving time: 0.031108
+     [java] Result Computed in SAT solver:     SAT
+     [java] CSOLVER solve time: 0.031429
+
+BUILD SUCCESSFUL
+Total time: 5 seconds