mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove tests
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner
parent
f920644892
commit
fd0c86ec7d
3380
tests/chat1.smt2
3380
tests/chat1.smt2
File diff suppressed because it is too large
Load diff
3382
tests/chat_pb.smt2
3382
tests/chat_pb.smt2
File diff suppressed because it is too large
Load diff
3380
tests/chat_sls.smt2
3380
tests/chat_sls.smt2
File diff suppressed because it is too large
Load diff
|
|
@ -1,443 +0,0 @@
|
|||
(set-option :smt.relevancy 0)
|
||||
(set-option :smt.pb.conflict_frequency 10000)
|
||||
(set-option :opt.pb.compile_equality true)
|
||||
(set-option :smt.pb.enable_simplex true)
|
||||
; declare an integer variable for each mini-pathlet's multiplicity
|
||||
(declare-const A0_2_3_10 Int)
|
||||
(declare-const A0_2_3_5_4_7_9 Int)
|
||||
(declare-const A0_2_3_5_4_8_9 Int)
|
||||
(declare-const A0_1_3_10 Int)
|
||||
(declare-const A0_1_3_5_4_7_9 Int)
|
||||
(declare-const A0_1_3_5_4_8_9 Int)
|
||||
(declare-const A1_3_10 Int)
|
||||
(declare-const A1_3_5_4_7_9 Int)
|
||||
(declare-const A1_3_5_4_8_9 Int)
|
||||
(declare-const A2_3_10 Int)
|
||||
(declare-const A2_3_5_4_7_9 Int)
|
||||
(declare-const A2_3_5_4_8_9 Int)
|
||||
(declare-const A3_10 Int)
|
||||
(declare-const A3_5_4_7_9_12_13 Int)
|
||||
(declare-const A3_5_4_7_9_11_13 Int)
|
||||
(declare-const A3_5_4_8_9_12_13 Int)
|
||||
(declare-const A3_5_4_8_9_11_13 Int)
|
||||
(declare-const A4_7_9_12_13 Int)
|
||||
(declare-const A4_7_9_11_13 Int)
|
||||
(declare-const A4_8_9_12_13 Int)
|
||||
(declare-const A4_8_9_11_13 Int)
|
||||
(declare-const A5_4_7_9_12_13 Int)
|
||||
(declare-const A5_4_7_9_11_13 Int)
|
||||
(declare-const A5_4_8_9_12_13 Int)
|
||||
(declare-const A5_4_8_9_11_13 Int)
|
||||
(declare-const A6_21_10 Int)
|
||||
(declare-const A6_4_7_9_12_13 Int)
|
||||
(declare-const A6_4_7_9_11_13 Int)
|
||||
(declare-const A6_4_8_9_12_13 Int)
|
||||
(declare-const A6_4_8_9_11_13 Int)
|
||||
(declare-const A7_9_12_13 Int)
|
||||
(declare-const A7_9_11_13 Int)
|
||||
(declare-const A8_9_12_13 Int)
|
||||
(declare-const A8_9_11_13 Int)
|
||||
(declare-const A9_12_13_15_17_18 Int)
|
||||
(declare-const A9_12_13_15_17_16_19 Int)
|
||||
(declare-const A9_12_13_14_17_18 Int)
|
||||
(declare-const A9_12_13_14_17_16_19 Int)
|
||||
(declare-const A9_11_13_15_17_18 Int)
|
||||
(declare-const A9_11_13_15_17_16_19 Int)
|
||||
(declare-const A9_11_13_14_17_18 Int)
|
||||
(declare-const A9_11_13_14_17_16_19 Int)
|
||||
(declare-const A11_13_15_17_18_19 Int)
|
||||
(declare-const A11_13_15_17_16_19 Int)
|
||||
(declare-const A11_13_14_17_18_19 Int)
|
||||
(declare-const A11_13_14_17_16_19 Int)
|
||||
(declare-const A12_13_15_17_18_19 Int)
|
||||
(declare-const A12_13_15_17_16_19 Int)
|
||||
(declare-const A12_13_14_17_18_19 Int)
|
||||
(declare-const A12_13_14_17_16_19 Int)
|
||||
(declare-const A13_15_17_18_19 Int)
|
||||
(declare-const A13_15_17_16_19 Int)
|
||||
(declare-const A13_14_17_18_19 Int)
|
||||
(declare-const A13_14_17_16_19 Int)
|
||||
(declare-const A20_6_21_10 Int)
|
||||
(declare-const A20_6_4_7_9_12 Int)
|
||||
(declare-const A20_6_4_7_9_11 Int)
|
||||
(declare-const A20_6_4_8_9_12 Int)
|
||||
(declare-const A20_6_4_8_9_11 Int)
|
||||
(declare-const A21_10 Int)
|
||||
; positive mult for each minipathlet
|
||||
(assert (<= 0 A0_2_3_10))
|
||||
(assert (<= A0_2_3_10 4))
|
||||
(assert (<= 0 A0_2_3_5_4_7_9))
|
||||
(assert (<= A0_2_3_5_4_7_9 4))
|
||||
(assert (<= 0 A0_2_3_5_4_8_9))
|
||||
(assert (<= A0_2_3_5_4_8_9 4))
|
||||
(assert (<= 0 A0_1_3_10))
|
||||
(assert (<= A0_1_3_10 4))
|
||||
(assert (<= 0 A0_1_3_5_4_7_9))
|
||||
(assert (<= A0_1_3_5_4_7_9 4))
|
||||
(assert (<= 0 A0_1_3_5_4_8_9))
|
||||
(assert (<= A0_1_3_5_4_8_9 4))
|
||||
(assert (<= 0 A1_3_10))
|
||||
(assert (<= A1_3_10 4))
|
||||
(assert (<= 0 A1_3_5_4_7_9))
|
||||
(assert (<= A1_3_5_4_7_9 4))
|
||||
(assert (<= 0 A1_3_5_4_8_9))
|
||||
(assert (<= A1_3_5_4_8_9 4))
|
||||
(assert (<= 0 A2_3_10))
|
||||
(assert (<= A2_3_10 4))
|
||||
(assert (<= 0 A2_3_5_4_7_9))
|
||||
(assert (<= A2_3_5_4_7_9 4))
|
||||
(assert (<= 0 A2_3_5_4_8_9))
|
||||
(assert (<= A2_3_5_4_8_9 4))
|
||||
(assert (<= 0 A3_10))
|
||||
(assert (<= A3_10 4))
|
||||
(assert (<= 0 A3_5_4_7_9_12_13))
|
||||
(assert (<= A3_5_4_7_9_12_13 4))
|
||||
(assert (<= 0 A3_5_4_7_9_11_13))
|
||||
(assert (<= A3_5_4_7_9_11_13 4))
|
||||
(assert (<= 0 A3_5_4_8_9_12_13))
|
||||
(assert (<= A3_5_4_8_9_12_13 4))
|
||||
(assert (<= 0 A3_5_4_8_9_11_13))
|
||||
(assert (<= A3_5_4_8_9_11_13 4))
|
||||
(assert (<= 0 A4_7_9_12_13))
|
||||
(assert (<= A4_7_9_12_13 4))
|
||||
(assert (<= 0 A4_7_9_11_13))
|
||||
(assert (<= A4_7_9_11_13 4))
|
||||
(assert (<= 0 A4_8_9_12_13))
|
||||
(assert (<= A4_8_9_12_13 4))
|
||||
(assert (<= 0 A4_8_9_11_13))
|
||||
(assert (<= A4_8_9_11_13 4))
|
||||
(assert (<= 0 A5_4_7_9_12_13))
|
||||
(assert (<= A5_4_7_9_12_13 4))
|
||||
(assert (<= 0 A5_4_7_9_11_13))
|
||||
(assert (<= A5_4_7_9_11_13 4))
|
||||
(assert (<= 0 A5_4_8_9_12_13))
|
||||
(assert (<= A5_4_8_9_12_13 4))
|
||||
(assert (<= 0 A5_4_8_9_11_13))
|
||||
(assert (<= A5_4_8_9_11_13 4))
|
||||
(assert (<= 0 A6_21_10))
|
||||
(assert (<= A6_21_10 4))
|
||||
(assert (<= 0 A6_4_7_9_12_13))
|
||||
(assert (<= A6_4_7_9_12_13 4))
|
||||
(assert (<= 0 A6_4_7_9_11_13))
|
||||
(assert (<= A6_4_7_9_11_13 4))
|
||||
(assert (<= 0 A6_4_8_9_12_13))
|
||||
(assert (<= A6_4_8_9_12_13 4))
|
||||
(assert (<= 0 A6_4_8_9_11_13))
|
||||
(assert (<= A6_4_8_9_11_13 4))
|
||||
(assert (<= 0 A7_9_12_13))
|
||||
(assert (<= A7_9_12_13 4))
|
||||
(assert (<= 0 A7_9_11_13))
|
||||
(assert (<= A7_9_11_13 4))
|
||||
(assert (<= 0 A8_9_12_13))
|
||||
(assert (<= A8_9_12_13 4))
|
||||
(assert (<= 0 A8_9_11_13))
|
||||
(assert (<= A8_9_11_13 4))
|
||||
(assert (<= 0 A9_12_13_15_17_18))
|
||||
(assert (<= A9_12_13_15_17_18 4))
|
||||
(assert (<= 0 A9_12_13_15_17_16_19))
|
||||
(assert (<= A9_12_13_15_17_16_19 4))
|
||||
(assert (<= 0 A9_12_13_14_17_18))
|
||||
(assert (<= A9_12_13_14_17_18 4))
|
||||
(assert (<= 0 A9_12_13_14_17_16_19))
|
||||
(assert (<= A9_12_13_14_17_16_19 4))
|
||||
(assert (<= 0 A9_11_13_15_17_18))
|
||||
(assert (<= A9_11_13_15_17_18 4))
|
||||
(assert (<= 0 A9_11_13_15_17_16_19))
|
||||
(assert (<= A9_11_13_15_17_16_19 4))
|
||||
(assert (<= 0 A9_11_13_14_17_18))
|
||||
(assert (<= A9_11_13_14_17_18 4))
|
||||
(assert (<= 0 A9_11_13_14_17_16_19))
|
||||
(assert (<= A9_11_13_14_17_16_19 4))
|
||||
(assert (<= 0 A11_13_15_17_18_19))
|
||||
(assert (<= A11_13_15_17_18_19 4))
|
||||
(assert (<= 0 A11_13_15_17_16_19))
|
||||
(assert (<= A11_13_15_17_16_19 4))
|
||||
(assert (<= 0 A11_13_14_17_18_19))
|
||||
(assert (<= A11_13_14_17_18_19 4))
|
||||
(assert (<= 0 A11_13_14_17_16_19))
|
||||
(assert (<= A11_13_14_17_16_19 4))
|
||||
(assert (<= 0 A12_13_15_17_18_19))
|
||||
(assert (<= A12_13_15_17_18_19 4))
|
||||
(assert (<= 0 A12_13_15_17_16_19))
|
||||
(assert (<= A12_13_15_17_16_19 4))
|
||||
(assert (<= 0 A12_13_14_17_18_19))
|
||||
(assert (<= A12_13_14_17_18_19 4))
|
||||
(assert (<= 0 A12_13_14_17_16_19))
|
||||
(assert (<= A12_13_14_17_16_19 4))
|
||||
(assert (<= 0 A13_15_17_18_19))
|
||||
(assert (<= A13_15_17_18_19 4))
|
||||
(assert (<= 0 A13_15_17_16_19))
|
||||
(assert (<= A13_15_17_16_19 4))
|
||||
(assert (<= 0 A13_14_17_18_19))
|
||||
(assert (<= A13_14_17_18_19 4))
|
||||
(assert (<= 0 A13_14_17_16_19))
|
||||
(assert (<= A13_14_17_16_19 4))
|
||||
(assert (<= 0 A20_6_21_10))
|
||||
(assert (<= A20_6_21_10 4))
|
||||
(assert (<= 0 A20_6_4_7_9_12))
|
||||
(assert (<= A20_6_4_7_9_12 4))
|
||||
(assert (<= 0 A20_6_4_7_9_11))
|
||||
(assert (<= A20_6_4_7_9_11 4))
|
||||
(assert (<= 0 A20_6_4_8_9_12))
|
||||
(assert (<= A20_6_4_8_9_12 4))
|
||||
(assert (<= 0 A20_6_4_8_9_11))
|
||||
(assert (<= A20_6_4_8_9_11 4))
|
||||
(assert (<= 0 A21_10))
|
||||
(assert (<= A21_10 4))
|
||||
; range of multiplicities for each contig-pair
|
||||
; contigs 0 1, #pairs 7, dist 8.36
|
||||
(assert (and (<= 0 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) (<= (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.852312) ; p=0001405
|
||||
(assert-soft (= 1 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 0.852312) ; p=0140504
|
||||
(assert-soft (= 2 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 1.408176) ; p=0039068
|
||||
(assert-soft (= 3 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.838611) ; p=0001450
|
||||
(assert-soft (= 4 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.627113) ; p=0000024
|
||||
; contigs 1 3, #pairs 5, dist 1.07
|
||||
(assert (and (<= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) (<= (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 4.168291) ; p=0000068
|
||||
(assert-soft (= 1 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 2.168291) ; p=0006787
|
||||
(assert-soft (= 2 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.195873) ; p=0063698
|
||||
(assert-soft (= 3 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 0.848149) ; p=0141857
|
||||
(assert-soft (= 4 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 0.756187) ; p=0175313
|
||||
; contigs 2 3, #pairs 4, dist 1.07
|
||||
(assert (and (<= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) (<= (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 3.535379) ; p=0000291
|
||||
(assert-soft (= 1 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.535379) ; p=0029149
|
||||
(assert-soft (= 2 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.874154) ; p=0133612
|
||||
(assert-soft (= 3 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.712685) ; p=0193783
|
||||
(assert-soft (= 4 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.755826) ; p=0175458
|
||||
; contigs 3 4, #pairs 3, dist 2.77
|
||||
(assert (and (<= 0 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) (<= (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 5.564238) ; p=0000003
|
||||
(assert-soft (= 1 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 3.564238) ; p=0000273
|
||||
(assert-soft (= 2 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 2.714464) ; p=0001930
|
||||
(assert-soft (= 3 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 2.239507) ; p=0005761
|
||||
(assert-soft (= 4 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.918007) ; p=0012078
|
||||
; contigs 4 9, #pairs 2, dist 1.24
|
||||
(assert (and (<= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) (<= (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 4.280499) ; p=0000052
|
||||
(assert-soft (= 1 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 2.280499) ; p=0005242
|
||||
(assert-soft (= 2 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.725376) ; p=0018820
|
||||
(assert-soft (= 3 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.420131) ; p=0038007
|
||||
(assert-soft (= 4 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.217191) ; p=0060647
|
||||
; contigs 5 9, #pairs 1, dist 1.46
|
||||
(assert (and (<= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) (<= (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 6.000000) ; p=0000001
|
||||
(assert-soft (= 1 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 4.000000) ; p=0000100
|
||||
(assert-soft (= 2 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 6.000000) ; p=0000001
|
||||
(assert-soft (= 3 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 8.000000) ; p=0000000
|
||||
(assert-soft (= 4 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.0000000) ; p=0000000
|
||||
; contigs 6 9, #pairs 0, dist 2.79
|
||||
(assert (and (<= 0 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) (<= (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
|
||||
(assert-soft (= 1 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
|
||||
(assert-soft (= 2 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
|
||||
(assert-soft (= 3 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
|
||||
(assert-soft (= 4 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
|
||||
; contigs 7 9, #pairs 4, dist 1.08
|
||||
(assert (and (<= 0 (+ A7_9_12_13 A7_9_11_13)) (<= (+ A7_9_12_13 A7_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A7_9_12_13 A7_9_11_13)) :dweight 4.830293) ; p=0000015
|
||||
(assert-soft (= 1 (+ A7_9_12_13 A7_9_11_13)) :dweight 2.830293) ; p=0001478
|
||||
(assert-soft (= 2 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.839248) ; p=0014479
|
||||
(assert-soft (= 3 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.347958) ; p=0044879
|
||||
(assert-soft (= 4 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.061278) ; p=0086840
|
||||
; contigs 8 9, #pairs 2, dist 1.10
|
||||
(assert (and (<= 0 (+ A8_9_12_13 A8_9_11_13)) (<= (+ A8_9_12_13 A8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.085052) ; p=0000822
|
||||
(assert-soft (= 1 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.085052) ; p=0082214
|
||||
(assert-soft (= 2 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.712306) ; p=0193952
|
||||
(assert-soft (= 3 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.589437) ; p=0257373
|
||||
(assert-soft (= 4 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.568873) ; p=0269853
|
||||
; contigs 9 12, #pairs 1, dist 1.77
|
||||
(assert (and (<= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) (<= (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 2.518279) ; p=0003032
|
||||
(assert-soft (= 1 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.518279) ; p=0303195
|
||||
(assert-soft (= 2 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.434295) ; p=0367879
|
||||
(assert-soft (= 3 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.475249) ; p=0334773
|
||||
(assert-soft (= 4 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.567356) ; p=0270797
|
||||
; contigs 11 13, #pairs 2, dist 1.00
|
||||
(assert (and (<= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) (<= (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 2.755831) ; p=0001755
|
||||
(assert-soft (= 1 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.755831) ; p=0175456
|
||||
(assert-soft (= 2 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.568471) ; p=0270103
|
||||
(assert-soft (= 3 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.630988) ; p=0233890
|
||||
(assert-soft (= 4 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.795810) ; p=0160026
|
||||
; contigs 12 13, #pairs 2, dist 1.01
|
||||
(assert (and (<= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) (<= (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.662349) ; p=0002176
|
||||
(assert-soft (= 1 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.662349) ; p=0217596
|
||||
(assert-soft (= 2 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.583662) ; p=0260818
|
||||
(assert-soft (= 3 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.754853) ; p=0175852
|
||||
(assert-soft (= 4 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.028349) ; p=0093681
|
||||
; contigs 13 15, #pairs 1, dist 2.58
|
||||
(assert (and (<= 0 (+ A13_15_17_18_19 A13_15_17_16_19)) (<= (+ A13_15_17_18_19 A13_15_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 2.434616) ; p=0003676
|
||||
(assert-soft (= 1 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.434616) ; p=0367607
|
||||
(assert-soft (= 2 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.584809) ; p=0260130
|
||||
(assert-soft (= 3 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.859941) ; p=0138057
|
||||
(assert-soft (= 4 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 1.186226) ; p=0065129
|
||||
; contigs 20 6, #pairs 7, dist 1.085
|
||||
(assert (and (<= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) (<= (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11) 4)))
|
||||
(assert-soft (= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.850723) ; p=0001410
|
||||
(assert-soft (= 1 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 0.850723) ; p=0141019
|
||||
(assert-soft (= 2 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.181023) ; p=0006591
|
||||
(assert-soft (= 3 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 4.385894) ; p=0000041
|
||||
(assert-soft (= 4 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 6.948833) ; p=0000000
|
||||
; contigs 21 10, #pairs 1, dist 1.2
|
||||
(assert (and (<= 0 (+ A21_10)) (<= (+ A21_10) 4)))
|
||||
(assert-soft (= 0 (+ A21_10)) :dweight 2.629839) ; p=0002345
|
||||
(assert-soft (= 1 (+ A21_10)) :dweight 0.629839) ; p=0234510
|
||||
(assert-soft (= 2 (+ A21_10)) :dweight 0.469677) ; p=0339096
|
||||
(assert-soft (= 3 (+ A21_10)) :dweight 0.434455) ; p=0367744
|
||||
(assert-soft (= 4 (+ A21_10)) :dweight 0.450384) ; p=0354499
|
||||
; range of multiplicities for each contig
|
||||
; contig 0, length 931, #reads 41, min 0, max 4
|
||||
(assert (and (<= 0 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) (<= (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.060041) ; p=0000087
|
||||
(assert-soft (= 1 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.060041) ; p=0008709
|
||||
(assert-soft (= 2 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 1.3620829) ; p=0000000
|
||||
(assert-soft (= 3 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 3.0304105) ; p=0000000
|
||||
(assert-soft (= 4 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.9084634) ; p=0000000
|
||||
; contig 1, length 195, #reads 16, min 0, max 4
|
||||
(assert (and (<= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) (<= (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 5.312217) ; p=0000005
|
||||
(assert-soft (= 1 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 3.312217) ; p=0000487
|
||||
(assert-soft (= 2 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.202826) ; p=0062686
|
||||
(assert-soft (= 3 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.092455) ; p=0080825
|
||||
(assert-soft (= 4 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.800524) ; p=0015830
|
||||
; contig 2, length 198, #reads 21, min 0, max 4
|
||||
(assert (and (<= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) (<= (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9) 4)))
|
||||
(assert-soft (= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 7.526226) ; p=0000000
|
||||
(assert-soft (= 1 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 5.526226) ; p=0000003
|
||||
(assert-soft (= 2 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.998081) ; p=0010044
|
||||
(assert-soft (= 3 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.093650) ; p=0080603
|
||||
(assert-soft (= 4 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.263422) ; p=0054523
|
||||
; contig 3, length 347, #reads 56, min 0, max 4
|
||||
(assert (and (<= 0 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) (<= (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.6034953) ; p=0000000
|
||||
(assert-soft (= 1 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.4034953) ; p=0000000
|
||||
(assert-soft (= 2 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 4.261782) ; p=0000055
|
||||
(assert-soft (= 3 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.485181) ; p=0032720
|
||||
(assert-soft (= 4 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.573120) ; p=0026723
|
||||
; contig 4, length 113, #reads 8, min 0, max 4
|
||||
(assert (and (<= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) (<= (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 7.744934) ; p=0000000
|
||||
(assert-soft (= 1 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 5.744934) ; p=0000002
|
||||
(assert-soft (= 2 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 3.682280) ; p=0000208
|
||||
(assert-soft (= 3 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 2.619135) ; p=0002404
|
||||
(assert-soft (= 4 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.965211) ; p=0010834
|
||||
; contig 5, length 101, #reads 2, min 0, max 4
|
||||
(assert (and (<= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) (<= (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 4.686648) ; p=0000021
|
||||
(assert-soft (= 1 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 2.686648) ; p=0002058
|
||||
(assert-soft (= 2 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 2.113387) ; p=0007702
|
||||
(assert-soft (= 3 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.790003) ; p=0016218
|
||||
(assert-soft (= 4 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.568925) ; p=0026982
|
||||
; contig 6, length 223, #reads 24, min 0, max 4
|
||||
(assert (and (<= 0 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) (<= (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 7.515357) ; p=0000000
|
||||
(assert-soft (= 1 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 5.515357) ; p=0000003
|
||||
(assert-soft (= 2 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.804093) ; p=0015700
|
||||
(assert-soft (= 3 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.091359) ; p=0081029
|
||||
(assert-soft (= 4 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.606284) ; p=0024758
|
||||
; contig 7, length 191, #reads 9, min 0, max 4
|
||||
(assert (and (<= 0 (+ A7_9_12_13 A7_9_11_13)) (<= (+ A7_9_12_13 A7_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A7_9_12_13 A7_9_11_13)) :dweight 3.169161) ; p=0000677
|
||||
(assert-soft (= 1 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.169161) ; p=0067739
|
||||
(assert-soft (= 2 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.051784) ; p=0088760
|
||||
(assert-soft (= 3 (+ A7_9_12_13 A7_9_11_13)) :dweight 2.058857) ; p=0008733
|
||||
(assert-soft (= 4 (+ A7_9_12_13 A7_9_11_13)) :dweight 3.526301) ; p=0000298
|
||||
; contig 8, length 200, #reads 12, min 0, max 4
|
||||
(assert (and (<= 0 (+ A8_9_12_13 A8_9_11_13)) (<= (+ A8_9_12_13 A8_9_11_13) 4)))
|
||||
(assert-soft (= 0 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.724714) ; p=0000188
|
||||
(assert-soft (= 1 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.724714) ; p=0018849
|
||||
(assert-soft (= 2 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.963436) ; p=0108784
|
||||
(assert-soft (= 3 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.701424) ; p=0019887
|
||||
(assert-soft (= 4 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.053242) ; p=0000885
|
||||
; contig 9, length 269, #reads 32, min 0, max 4
|
||||
(assert (and (<= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) (<= (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 8.757585) ; p=0000000
|
||||
(assert-soft (= 1 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 6.757585) ; p=0000000
|
||||
(assert-soft (= 2 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 1.962827) ; p=0010894
|
||||
(assert-soft (= 3 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 1.166108) ; p=0068217
|
||||
(assert-soft (= 4 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 2.006269) ; p=0009857
|
||||
; contig 11, length 170, #reads 7, min 0, max 4
|
||||
(assert (and (<= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) (<= (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 3.066473) ; p=0000858
|
||||
(assert-soft (= 1 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 1.066473) ; p=0085808
|
||||
(assert-soft (= 2 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.946381) ; p=0113141
|
||||
(assert-soft (= 3 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 1.700861) ; p=0019913
|
||||
(assert-soft (= 4 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 2.813408) ; p=0001537
|
||||
; contig 12, length 198, #reads 15, min 0, max 4
|
||||
(assert (and (<= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) (<= (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 4.784554) ; p=0000016
|
||||
(assert-soft (= 1 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.784554) ; p=0001642
|
||||
(assert-soft (= 2 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.062589) ; p=0086579
|
||||
(assert-soft (= 3 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.214705) ; p=0060995
|
||||
(assert-soft (= 4 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.134110) ; p=0007343
|
||||
; contig 13, length 349, #reads 28, min 0, max 4
|
||||
(assert (and (<= 0 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) (<= (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19) 4)))
|
||||
(assert-soft (= 0 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 4.577071) ; p=0000026
|
||||
(assert-soft (= 1 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 2.577071) ; p=0002648
|
||||
(assert-soft (= 2 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 1.290338) ; p=0051246
|
||||
(assert-soft (= 3 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 3.501889) ; p=0000315
|
||||
(assert-soft (= 4 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 7.145711) ; p=0000000
|
||||
; contig 20, length 1151, #reads 32, min 0, max 4
|
||||
(assert (and (<= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) (<= (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11) 4)))
|
||||
(assert-soft (= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 8.689981) ; p=0000000
|
||||
(assert-soft (= 1 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 6.689981) ; p=0000000
|
||||
(assert-soft (= 2 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.7295778) ; p=0000000
|
||||
(assert-soft (= 3 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 5.1899615) ; p=0000000
|
||||
(assert-soft (= 4 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 7.8140332) ; p=0000000
|
||||
; contig 21, length 107, #reads 4, min 0, max 4
|
||||
(assert (and (<= 0 (+ A21_10)) (<= (+ A21_10) 4)))
|
||||
(assert-soft (= 0 (+ A21_10)) :dweight 5.154038) ; p=0000007
|
||||
(assert-soft (= 1 (+ A21_10)) :dweight 3.154038) ; p=0000701
|
||||
(assert-soft (= 2 (+ A21_10)) :dweight 2.122711) ; p=0007539
|
||||
(assert-soft (= 3 (+ A21_10)) :dweight 1.591139) ; p=0025637
|
||||
(assert-soft (= 4 (+ A21_10)) :dweight 1.264177) ; p=0054428
|
||||
; consistency of minipathlet multiplicities
|
||||
(assert (= (+ A9_12_13_15_17_18) (+ A12_13_15_17_18_19)))
|
||||
(assert (= (+ A5_4_7_9_11_13 A6_4_7_9_11_13) (+ A4_7_9_11_13)))
|
||||
(assert (= (+ A0_2_3_5_4_8_9) (+ A2_3_5_4_8_9)))
|
||||
(assert (= (+ A1_3_5_4_8_9 A2_3_5_4_8_9) (+ A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)))
|
||||
(assert (= (+ A9_11_13_14_17_16_19) (+ A11_13_14_17_16_19)))
|
||||
(assert (= (+ A11_13_14_17_16_19 A12_13_14_17_16_19) (+ A13_14_17_16_19)))
|
||||
(assert (= (+ A20_6_21_10) (+ A6_21_10)))
|
||||
(assert (= (+ A11_13_14_17_18_19 A12_13_14_17_18_19) (+ A13_14_17_18_19)))
|
||||
(assert (= (+ A0_1_3_5_4_7_9) (+ A1_3_5_4_7_9)))
|
||||
(assert (= (+ A9_12_13_14_17_18) (+ A12_13_14_17_18_19)))
|
||||
(assert (= (+ A1_3_10 A2_3_10) (+ A3_10)))
|
||||
(assert (= (+ A11_13_15_17_18_19 A12_13_15_17_18_19) (+ A13_15_17_18_19)))
|
||||
(assert (= (+ A11_13_15_17_16_19 A12_13_15_17_16_19) (+ A13_15_17_16_19)))
|
||||
(assert (= (+ A9_12_13_14_17_16_19) (+ A12_13_14_17_16_19)))
|
||||
(assert (= (+ A7_9_11_13 A8_9_11_13) (+ A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)))
|
||||
(assert (= (+ A0_2_3_5_4_7_9) (+ A2_3_5_4_7_9)))
|
||||
(assert (= (+ A4_8_9_11_13) (+ A8_9_11_13)))
|
||||
(assert (= (+ A0_1_3_10) (+ A1_3_10)))
|
||||
(assert (= (+ A20_6_4_8_9_12) (+ A6_4_8_9_12_13)))
|
||||
(assert (= (+ A3_5_4_8_9_11_13) (+ A5_4_8_9_11_13)))
|
||||
(assert (= (+ A0_1_3_5_4_8_9) (+ A1_3_5_4_8_9)))
|
||||
(assert (= (+ A5_4_8_9_11_13 A6_4_8_9_11_13) (+ A4_8_9_11_13)))
|
||||
(assert (= (+ A20_6_4_7_9_12) (+ A6_4_7_9_12_13)))
|
||||
(assert (= (+ A20_6_4_7_9_11) (+ A6_4_7_9_11_13)))
|
||||
(assert (= (+ A3_5_4_8_9_12_13) (+ A5_4_8_9_12_13)))
|
||||
(assert (= (+ A4_7_9_12_13) (+ A7_9_12_13)))
|
||||
(assert (= (+ A9_12_13_15_17_16_19) (+ A12_13_15_17_16_19)))
|
||||
(assert (= (+ A9_11_13_15_17_16_19) (+ A11_13_15_17_16_19)))
|
||||
(assert (= (+ A1_3_5_4_7_9 A2_3_5_4_7_9) (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13)))
|
||||
(assert (= (+ A3_5_4_7_9_12_13) (+ A5_4_7_9_12_13)))
|
||||
(assert (= (+ A7_9_12_13 A8_9_12_13) (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)))
|
||||
(assert (= (+ A0_2_3_10) (+ A2_3_10)))
|
||||
(assert (= (+ A9_11_13_14_17_18) (+ A11_13_14_17_18_19)))
|
||||
(assert (= (+ A4_8_9_12_13) (+ A8_9_12_13)))
|
||||
(assert (= (+ A5_4_7_9_12_13 A6_4_7_9_12_13) (+ A4_7_9_12_13)))
|
||||
(assert (= (+ A9_11_13_15_17_18) (+ A11_13_15_17_18_19)))
|
||||
(assert (= (+ A6_21_10) (+ A21_10)))
|
||||
(assert (= (+ A20_6_4_8_9_11) (+ A6_4_8_9_11_13)))
|
||||
(assert (= (+ A3_5_4_7_9_11_13) (+ A5_4_7_9_11_13)))
|
||||
(assert (= (+ A5_4_8_9_12_13 A6_4_8_9_12_13) (+ A4_8_9_12_13)))
|
||||
(assert (= (+ A4_7_9_11_13) (+ A7_9_11_13)))
|
||||
(optimize :print_statistics true
|
||||
:wmaxsat_engine sls
|
||||
:maxsat_engine weighted_maxsat)
|
||||
5844
tests/sls1.smt2
5844
tests/sls1.smt2
File diff suppressed because it is too large
Load diff
5842
tests/wmax1.smt2
5842
tests/wmax1.smt2
File diff suppressed because it is too large
Load diff
Loading…
Reference in a new issue