--- /dev/null
+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/math/2/benchmark2.json
+ [java] Benchmark Id: 2
+ [java] Method name: getInnerProduct
+ [java] Packages: [com.opengamma.analytics.math, org.apache.commons.math.linear]
+ [java] Libraries: [./lib/commons-math-2.2.jar, ./lib/og-analytics-2.17.0.jar, ./lib/commons-lang-2.6.jar]
+ [java] Source type(s): [com.opengamma.analytics.math.matrix.DoubleMatrix1D, com.opengamma.analytics.math.matrix.DoubleMatrix1D]
+ [java] Target type: double
+ [java] --------------------------------------------------------
+ [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+ [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+ [java] Warning: javax.crypto.Cipher is a phantom class!
+ [java] Warning: javax.crypto.SealedObject is a phantom class!
+ [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+ [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+ [java] Warning: javax.crypto.spec.DHParameterSpec 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.SecretKey is a phantom class!
+ [java] Warning: com.opengamma.util.ArgumentChecker is a phantom class!
+ [java] Warning: com.opengamma.util.money.Currency is a phantom class!
+ [java] Warning: com.opengamma.util.money.CurrencyAmount is a phantom class!
+ [java] Warning: com.opengamma.util.money.MultipleCurrencyAmount is a phantom class!
+ [java] Warning: it.unimi.dsi.fastutil.doubles.DoubleArrayList is a phantom class!
+ [java] Warning: org.threeten.bp.Period is a phantom class!
+ [java] Warning: org.threeten.bp.ZonedDateTime is a phantom class!
+ [java] Warning: com.opengamma.id.ExternalId is a phantom class!
+ [java] Warning: com.opengamma.OpenGammaRuntimeException is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Pair is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Pairs is a phantom class!
+ [java] Warning: org.joda.convert.ToString is a phantom class!
+ [java] Warning: org.joda.convert.FromStringFactory is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAdjuster is a phantom class!
+ [java] Warning: org.threeten.bp.LocalDate is a phantom class!
+ [java] Warning: com.opengamma.util.time.Expiry is a phantom class!
+ [java] Warning: org.joda.beans.Bean is a phantom class!
+ [java] Warning: org.joda.beans.Property is a phantom class!
+ [java] Warning: org.joda.beans.MetaProperty is a phantom class!
+ [java] Warning: org.joda.beans.MetaBean is a phantom class!
+ [java] Warning: org.joda.beans.PropertyDefinition is a phantom class!
+ [java] Warning: org.joda.beans.JodaBeanUtils is a phantom class!
+ [java] Warning: org.joda.beans.BeanDefinition is a phantom class!
+ [java] Warning: org.joda.beans.ImmutableBean is a phantom class!
+ [java] Warning: com.opengamma.util.i18n.Country is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableSet is a phantom class!
+ [java] Warning: org.joda.beans.impl.flexi.FlexiBean is a phantom class!
+ [java] Warning: org.joda.convert.FromString is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableMap is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableMap$Builder is a phantom class!
+ [java] Warning: com.opengamma.util.CompareUtils is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.ObjectsPair is a phantom class!
+ [java] Warning: org.slf4j.Logger is a phantom class!
+ [java] Warning: org.slf4j.LoggerFactory is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.DoublesPair is a phantom class!
+ [java] Warning: org.threeten.bp.chrono.ChronoZonedDateTime is a phantom class!
+ [java] Warning: com.opengamma.util.time.DateUtils is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaBean is a phantom class!
+ [java] Warning: org.joda.beans.BeanBuilder is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaProperty is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectMetaPropertyMap is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectBeanBuilder is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectFieldsBeanBuilder is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.Temporal is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAmount is a phantom class!
+ [java] Warning: com.opengamma.util.time.Tenor is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAdjusters is a phantom class!
+ [java] Warning: org.threeten.bp.Month is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.zdt.ZonedDateTimeDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.DoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Triple is a phantom class!
+ [java] Warning: com.google.common.collect.ImmutableList is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.FirstThenSecondDoublesPairComparator is a phantom class!
+ [java] Warning: com.opengamma.util.time.Tenor$BusinessDayTenor is a phantom class!
+ [java] Warning: org.threeten.bp.LocalDateTime is a phantom class!
+ [java] Warning: com.opengamma.util.ParallelArrayBinarySort is a phantom class!
+ [java] Warning: org.threeten.bp.LocalTime is a phantom class!
+ [java] Warning: org.threeten.bp.ZoneId is a phantom class!
+ [java] Warning: org.threeten.bp.chrono.ChronoLocalDate is a phantom class!
+ [java] Warning: org.threeten.bp.ZoneOffset is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.ImmutableLocalDateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.zdt.ImmutableZonedDateTimeDoubleTimeSeries is a phantom class!
+ [java] Warning: org.threeten.bp.format.DateTimeFormatter is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalField is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.JulianFields is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalAccessor is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.FirstThenSecondPairComparator is a phantom class!
+ [java] Warning: com.google.common.collect.Maps is a phantom class!
+ [java] Warning: com.opengamma.util.ClassUtils is a phantom class!
+ [java] Warning: com.opengamma.util.money.MultipleCurrencyAmountPricer is a phantom class!
+ [java] Warning: cern.jet.random.Normal is a phantom class!
+ [java] Warning: cern.jet.stat.Probability is a phantom class!
+ [java] Warning: cern.jet.random.engine.RandomEngine is a phantom class!
+ [java] Warning: cern.jet.random.engine.MersenneTwister64 is a phantom class!
+ [java] Warning: com.opengamma.lang.annotation.ExternalFunction is a phantom class!
+ [java] Warning: com.google.common.primitives.Doubles is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleMatrix1D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleFactory2D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleFactory1D is a phantom class!
+ [java] Warning: cern.colt.matrix.DoubleMatrix2D is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.Algebra is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.SingularValueDecomposition is a phantom class!
+ [java] Warning: com.google.common.collect.ArrayListMultimap is a phantom class!
+ [java] Warning: com.google.common.collect.ListMultimap is a phantom class!
+ [java] Warning: it.unimi.dsi.fastutil.ints.IntArrayList is a phantom class!
+ [java] Warning: com.google.common.collect.LinkedListMultimap is a phantom class!
+ [java] Warning: com.google.common.collect.Multimap is a phantom class!
+ [java] Warning: org.joda.beans.impl.direct.DirectBean is a phantom class!
+ [java] Warning: com.google.common.collect.Iterators is a phantom class!
+ [java] Warning: cern.jet.random.engine.MersenneTwister is a phantom class!
+ [java] Warning: com.google.common.collect.Iterables is a phantom class!
+ [java] Warning: com.google.common.collect.Sets$SetView is a phantom class!
+ [java] Warning: com.google.common.collect.Sets is a phantom class!
+ [java] Warning: org.threeten.bp.DayOfWeek is a phantom class!
+ [java] Warning: org.threeten.bp.MonthDay is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.DateDoubleTimeSeries is a phantom class!
+ [java] Warning: com.google.common.collect.Lists is a phantom class!
+ [java] Warning: org.joda.beans.PropertyStyle is a phantom class!
+ [java] Warning: cern.jet.math.Bessel is a phantom class!
+ [java] Warning: com.opengamma.util.types.ParameterizedTypeImpl is a phantom class!
+ [java] Warning: com.opengamma.util.types.VariantType is a phantom class!
+ [java] Warning: org.apache.log4j.Logger is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateToIntConverter is a phantom class!
+ [java] Warning: cern.jet.random.StudentT is a phantom class!
+ [java] Warning: com.opengamma.util.CalculationMode is a phantom class!
+ [java] Warning: com.opengamma.timeseries.TimeSeriesException is a phantom class!
+ [java] Warning: cern.colt.Arrays is a phantom class!
+ [java] Warning: cern.jet.random.ChiSquare is a phantom class!
+ [java] Warning: cern.colt.list.IntArrayList is a phantom class!
+ [java] Warning: org.testng.AssertJUnit is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.ChronoField is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.TemporalUnit is a phantom class!
+ [java] Warning: org.threeten.bp.temporal.ChronoUnit is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleEntryIterator is a phantom class!
+ [java] Warning: edu.emory.mathcs.jtransforms.fft.DoubleFFT_1D is a phantom class!
+ [java] Warning: com.opengamma.timeseries.precise.PreciseDoubleTimeSeries is a phantom class!
+ [java] Warning: com.opengamma.timeseries.date.localdate.LocalDateDoubleTimeSeriesBuilder is a phantom class!
+ [java] Warning: com.opengamma.util.tuple.Quadruple is a phantom class!
+ [java] Warning: cern.colt.matrix.linalg.EigenvalueDecomposition is a phantom class!
+ [java] Warning: cern.jet.random.Gamma is a phantom class!
+ [java] Warning: org.threeten.bp.Year is a phantom class!
+ [java] #Classes: 615
+ [java] #Methods: 5526
+ [java] Soot Time: 4124.801313
+ [java] PetriNet for path length: 1 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 2 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 3 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 4 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] PetriNet for path length: 5 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 66.424035
+ [java] Path Solving Time: 140.86225
+ [java] Path Solving Time: 16.298536
+ [java] PetriNet for path length: 6 [places: 692 ; transitions: 5020 ; edges: 13369]
+ [java] Path Solving Time: 33.371652
+ [java] Path Solving Time: 4.790186
+ [java] 1594752158452 Original Encoding Solving Time: 0.964243
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752158452Satune Solving Time: 52.485695
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752158998 Original Encoding Solving Time: 0.097413
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752158998Satune Solving Time: 0.106168
+ [java] 1594752159252 Original Encoding Solving Time: 0.090356
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752159252Satune Solving Time: 0.08234
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752159505 Original Encoding Solving Time: 0.06335
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752159505Satune Solving Time: 0.085786
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594752159759 Original Encoding Solving Time: 0.070144
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752159759Satune Solving Time: 0.093995
+ [java] Path Solving Time: 33.510787
+ [java] Path Solving Time: 6.86109
+ [java] 1594752159855 Original Encoding Solving Time: 0.376222
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752159855Satune Solving Time: 54.490417
+ [java] 1594752159932 Original Encoding Solving Time: 0.119188
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752159932Satune Solving Time: 0.077128
+ [java] 1594752159953 Original Encoding Solving Time: 0.044317
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594752159953Satune Solving Time: 0.084771
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 31.746437
+ [java] Path Solving Time: 15.868169
+ [java] Path Solving Time: 6.597604
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594752160062 Original Encoding Solving Time: 0.558066
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594752160062Satune Solving Time: 58.128972
+ [java] =========Statistics (time in milliseconds)=========
+ [java] Benchmark Id: 2
+ [java] Sketch Generation Time: 376.26029300000005
+ [java] Sketch Completion Time: 327.62210000000005
+ [java] Compilation Time: 327.512369
+ [java] Running Test cases Time: 984.874911
+ [java] Synthesis Time: 1688.7573040000002
+ [java] Total Time: 2016.2696730000002
+ [java] Number of components: 3
+ [java] Number of holes: 5
+ [java] Number of completed programs: 9
+ [java] Number of sketches: 3
+ [java] Solution:
+ [java] org.apache.commons.math.linear.RealVector sypet_var13 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.wrap(sypet_arg1);
+ [java] org.apache.commons.math.linear.RealVector sypet_var14 = com.opengamma.analytics.math.util.wrapper.CommonsMathWrapper.wrap(sypet_arg0);
+ [java] double sypet_var15 = sypet_var14.dotProduct(sypet_var13);
+ [java] return sypet_var15;
+ [java]
+ [java] ============================
+ [java] Polarity time: 0.000020
+ [java] Preprocess time: 0.000014
+ [java] Decompose Order: 0.000009
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccfc0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd130....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd460....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd5d0....
+ [java] Encoding Graph Time: 0.000138
+ [java] Elapse Encode time: 0.000200
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.052245
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.052456
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000039
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000078
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000040
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Elapse Encode time: 0.000032
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000090
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000006
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd5d0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd460....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccfc0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd130....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccea0....
+ [java] Encoding Graph Time: 0.000112
+ [java] Elapse Encode time: 0.000135
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.054337
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.054479
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000037
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.000073
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000080
+ [java] Polarity time: 0.000012
+ [java] Preprocess time: 0.000016
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccea0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140ccfc0....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd130....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd460....
+ [java] INFO: naive encoder is making the decision about element 0x7f86140cd5d0....
+ [java] Encoding Graph Time: 0.000172
+ [java] Elapse Encode time: 0.000231
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.057880
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.058120
+
+BUILD SUCCESSFUL
+Total time: 24 seconds
projects / Benchmarks_CSolver.git / blobdiff