From 1d1d38591244a5ed0e1871aa4277dc4f0840fd7a Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 11 Aug 2009 21:36:15 +0000 Subject: [PATCH] git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@111 e59a4935-1847-0410-ae03-e826735625c1 --- .../4-alpha-helices-2-rungs-more-bits.cvc | 329 ---------- .../4-alpha-helices-3-rungs-32bits.cvc | 379 ----------- tests/bio-tests/4-alpha-helices-3-rungs.cvc | 618 +++++++++--------- 3 files changed, 312 insertions(+), 1014 deletions(-) delete mode 100644 tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc delete mode 100644 tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc diff --git a/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc b/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc deleted file mode 100644 index cc437a4..0000000 --- a/tests/bio-tests/4-alpha-helices-2-rungs-more-bits.cvc +++ /dev/null @@ -1,329 +0,0 @@ -% 4 alpha helices. Each helix with 6 amino acid (residues), and 4 -% faces (two inner and two outer). Each face has 1 or 2 residues -% The problem is encoded with two bit bit-vector variable per face. - - -alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4); -alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32); -alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(32); - - -alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4); -alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32); -alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(32); - - -alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4); -alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32); -alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(32); - - -alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4); -alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32); -alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(32); - - -coil_12, coil_23, coil34 : BITVECTOR(16); -coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32); -coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(32); - -contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32); -contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32); -contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32); -contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32); - -outer_energy : BITVECTOR(32); -inner_energy : BITVECTOR(32); -bits32_one : BITVECTOR(32); -bits32_two : BITVECTOR(32); - -ASSERT (bits32_one = 0hex00000001); -ASSERT (bits32_two = 0hex00000002); - -aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(32); -ASSERT (aminoacid_energies[0hex00000000] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000001] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000002] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000003] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000004] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000005] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000006] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000007] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000008] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000009] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000A] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000000B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000C] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000000D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000010] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000011] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000012] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000013] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000014] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000015] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000016] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000017] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000018] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000019] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001A] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000001B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001D] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000001E] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000001F] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000020] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000021] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000022] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000023] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000024] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000025] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000026] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000027] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000028] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000029] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000002A] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000002B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000002C] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000002D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000002E] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000002F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000030] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000031] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000032] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000033] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000034] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000035] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000036] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000037] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000038] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000039] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000003A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003B] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000003C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003E] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000003F] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000040] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000041] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000042] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000043] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000044] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000045] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000046] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000047] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000048] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000049] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000004A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004B] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000004C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004D] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000004E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004F] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000050] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000051] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000052] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000053] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000054] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000055] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000056] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000057] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000058] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000059] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000005A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005B] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000005C] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000005D] = 0hex00000111); -ASSERT (aminoacid_energies[0hex0000005E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000060] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000061] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000062] = 0hex00000111); -ASSERT (aminoacid_energies[0hex00000063] = 0hex00000111); - -ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2); -%ASSERT (alpha1_inner1 = 0hex0); -ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2); - -ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2); -ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2); - -ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2); -ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2); - -ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2); -ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2); - -ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2) = 0hex6); -ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2) = 0hex6); -ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2) = 0hex6); -ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2) = 0hex6); - - -ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1); -ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1); -ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2); -ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1); - -ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1); -ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1); -ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2); -ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1); - -ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1); -ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1); -ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2); -ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1); - - -ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1); -ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1); -ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2); -ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1); - - -ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]); -ASSERT (alpha1_inner1 = 0hex2 => - alpha1_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index])); - - -ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer1_index])); -ASSERT (alpha1_outer1 = 0hex2 => - alpha1_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], - aminoacid_energies[alpha1_outer1_index]))); - - -ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]); -ASSERT (alpha1_inner2 = 0hex2 => - alpha1_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index])); - - -ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer2_index])); -ASSERT (alpha1_outer2 = 0hex2 => - alpha1_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], - aminoacid_energies[alpha1_outer2_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]); -ASSERT (alpha2_inner1 = 0hex2 => - alpha2_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index])); - - -ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer1_index])); -ASSERT (alpha2_outer1 = 0hex2 => - alpha2_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index]))); - - -ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]); -ASSERT (alpha2_inner2 = 0hex2 => - alpha2_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index])); - - -ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer2_index])); -ASSERT (alpha2_outer2 = 0hex2 => - alpha2_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]); -ASSERT (alpha3_inner1 = 0hex2 => - alpha3_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index])); - - -ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer1_index])); -ASSERT (alpha3_outer1 = 0hex2 => - alpha3_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], - aminoacid_energies[alpha3_outer1_index]))); - -ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]); -ASSERT (alpha3_inner2 = 0hex2 => - alpha3_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)], - aminoacid_energies[alpha3_inner2_index])); - - -ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer2_index])); -ASSERT (alpha3_outer2 = 0hex2 => - alpha3_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], - aminoacid_energies[alpha3_outer2_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]); -ASSERT (alpha4_inner1 = 0hex2 => - alpha4_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index])); - - -ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer1_index])); -ASSERT (alpha4_outer1 = 0hex2 => - alpha4_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)], - aminoacid_energies[alpha4_outer1_index]))); - - -ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]); -ASSERT (alpha4_inner2 = 0hex2 => - alpha4_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index])); - - -ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer2_index])); -ASSERT (alpha4_outer2 = 0hex2 => - alpha4_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], - aminoacid_energies[alpha4_outer2_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (contact_energy12_zero = BVMULT(32, alpha1_inner1_energy, alpha2_inner1_energy)); -ASSERT (contact_energy12_one = BVMULT(32, alpha1_inner2_energy, alpha2_inner2_energy)); - - - -ASSERT (contact_energy23_zero = BVMULT(32, alpha2_inner1_energy, alpha3_inner1_energy)); -ASSERT (contact_energy23_one = BVMULT(32, alpha2_inner2_energy, alpha3_inner2_energy)); - - - -ASSERT (contact_energy34_zero = BVMULT(32, alpha3_inner1_energy, alpha4_inner1_energy)); -ASSERT (contact_energy34_one = BVMULT(32, alpha3_inner2_energy, alpha4_inner2_energy)); - - -ASSERT (contact_energy41_zero = BVMULT(32, alpha4_inner1_energy, alpha1_inner1_energy)); -ASSERT (contact_energy41_one = BVMULT(32, alpha4_inner2_energy, alpha1_inner2_energy)); - - -ASSERT (outer_energy = BVPLUS(32, alpha1_outer1_energy, alpha1_outer2_energy, - alpha2_outer1_energy, alpha2_outer2_energy, - alpha3_outer1_energy, alpha3_outer2_energy, - alpha4_outer1_energy, alpha4_outer2_energy)); - - -ASSERT (inner_energy = BVPLUS(32, contact_energy12_zero, contact_energy12_one, - contact_energy23_zero, contact_energy23_one, - contact_energy34_zero, contact_energy34_one, - contact_energy41_zero, contact_energy41_one)); - - -% final query -ASSERT (BVGE(BVMULT(64,0hex00000000@outer_energy,0hex00000000@inner_energy), - 0hex1111111111111110)); -QUERY FALSE; \ No newline at end of file diff --git a/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc b/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc deleted file mode 100644 index e134ad6..0000000 --- a/tests/bio-tests/4-alpha-helices-3-rungs-32bits.cvc +++ /dev/null @@ -1,379 +0,0 @@ -% 4 alpha helices. Each helix with 6 amino acid (residues), and 4 -% faces (two inner and two outer). Each face has 1 or 2 residues -% The problem is encoded with two bit bit-vector variable per face. - - -alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4); -alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32); -alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(32); - - -alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4); -alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32); -alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(32); - - -alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4); -alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32); -alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(32); - - -alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4); -alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32); -alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(32); - - -coil_12, coil_23, coil34 : BITVECTOR(16); -coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32); -coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(32); - -contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32); -contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32); -contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32); -contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32); - -outer_energy : BITVECTOR(32); -inner_energy : BITVECTOR(32); -bits32_one : BITVECTOR(32); -bits32_two : BITVECTOR(32); - -ASSERT (bits32_one = 0hex00000001); -ASSERT (bits32_two = 0hex00000002); - -aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(32); -ASSERT (aminoacid_energies[0hex00000000] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000001] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000002] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000003] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000004] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000005] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000006] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000007] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000008] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000009] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000A] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000000B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000C] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000000D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000000F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000010] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000011] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000012] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000013] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000014] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000015] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000016] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000017] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000018] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000019] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001A] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000001B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000001F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000020] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000021] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000022] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000023] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000024] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000025] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000026] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000027] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000028] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000029] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000002A] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000002B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000002C] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000002D] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000002E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000002F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000030] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000031] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000032] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000033] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000034] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000035] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000036] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000037] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000038] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000039] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003B] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000003C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003D] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000003E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000003F] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000040] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000041] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000042] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000043] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000044] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000045] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000046] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000047] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000048] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000049] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000004A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004B] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004D] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000004F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000050] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000051] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000052] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000053] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000054] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000055] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000056] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000057] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000058] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000059] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005A] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005B] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000005C] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005D] = 0hex00000000); -ASSERT (aminoacid_energies[0hex0000005E] = 0hex00011111); -ASSERT (aminoacid_energies[0hex0000005F] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000060] = 0hex00000000); -ASSERT (aminoacid_energies[0hex00000061] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000062] = 0hex00011111); -ASSERT (aminoacid_energies[0hex00000063] = 0hex00000000); - -%ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2); -ASSERT (alpha1_inner1 = 0hex2); -ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2); -ASSERT (alpha1_inner3 = 0hex1 OR alpha1_inner3 = 0hex2); -ASSERT (alpha1_outer3 = 0hex1 OR alpha1_outer3 = 0hex2); - -ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2); -ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2); -ASSERT (alpha2_inner3 = 0hex1 OR alpha2_inner3 = 0hex2); -ASSERT (alpha2_outer3 = 0hex1 OR alpha2_outer3 = 0hex2); - -ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2); -ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2); -ASSERT (alpha3_inner3 = 0hex1 OR alpha3_inner3 = 0hex2); -ASSERT (alpha3_outer3 = 0hex1 OR alpha3_outer3 = 0hex2); - -ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2); -ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2); -ASSERT (alpha4_inner3 = 0hex1 OR alpha4_inner3 = 0hex2); -ASSERT (alpha4_outer3 = 0hex1 OR alpha4_outer3 = 0hex2); - - -ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3) = 0hex9); - - -ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1); -ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1); -ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2); -ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1); -ASSERT (alpha1_inner3 = 0hex1 => alpha1_outer3 = 0hex2); -ASSERT (alpha1_inner3 = 0hex2 => alpha1_outer3 = 0hex1); - -ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1); -ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1); -ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2); -ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1); -ASSERT (alpha2_inner3 = 0hex1 => alpha2_outer3 = 0hex2); -ASSERT (alpha2_inner3 = 0hex2 => alpha2_outer3 = 0hex1); - -ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1); -ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1); -ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2); -ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1); -ASSERT (alpha3_inner3 = 0hex1 => alpha3_outer3 = 0hex2); -ASSERT (alpha3_inner3 = 0hex2 => alpha3_outer3 = 0hex1); - - -ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1); -ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1); -ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2); -ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1); -ASSERT (alpha4_inner3 = 0hex1 => alpha4_outer3 = 0hex2); -ASSERT (alpha4_inner3 = 0hex2 => alpha4_outer3 = 0hex1); - - -ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000000)]); -ASSERT (alpha1_inner1 = 0hex2 => - alpha1_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index])); - - -ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer1_index])); -ASSERT (alpha1_outer1 = 0hex2 => - alpha1_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], aminoacid_energies[alpha1_outer1_index]))); - - -ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000000)]); -ASSERT (alpha1_inner2 = 0hex2 => - alpha1_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index])); - - -ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer2_index])); -ASSERT (alpha1_outer2 = 0hex2 => - alpha1_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], aminoacid_energies[alpha1_outer2_index]))); - -ASSERT (alpha1_inner3 = 0hex1 => alpha1_inner3_energy = aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000000)]); -ASSERT (alpha1_inner3 = 0hex2 => - alpha1_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000001)],aminoacid_energies[alpha1_inner3_index])); - - -ASSERT (alpha1_outer3 = 0hex1 => alpha1_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha1_outer3_index])); -ASSERT (alpha1_outer3 = 0hex2 => - alpha1_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha1_outer3_index,0hex00000001)], aminoacid_energies[alpha1_outer3_index]))); - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000000)]); -ASSERT (alpha2_inner1 = 0hex2 => - alpha2_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index])); - - -ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer1_index])); -ASSERT (alpha2_outer1 = 0hex2 => - alpha2_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index]))); - - -ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000000)]); -ASSERT (alpha2_inner2 = 0hex2 => - alpha2_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index])); - - -ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer2_index])); -ASSERT (alpha2_outer2 = 0hex2 => - alpha2_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index]))); - - -ASSERT (alpha2_inner3 = 0hex1 => alpha2_inner3_energy = aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000000)]); -ASSERT (alpha2_inner3 = 0hex2 => - alpha2_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000001)],aminoacid_energies[alpha2_inner3_index])); - - -ASSERT (alpha2_outer3 = 0hex1 => alpha2_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha2_outer3_index])); -ASSERT (alpha2_outer3 = 0hex2 => - alpha2_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha2_outer3_index,0hex00000001)], aminoacid_energies[alpha2_outer3_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000000)]); -ASSERT (alpha3_inner1 = 0hex2 => - alpha3_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index])); - - -ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer1_index])); -ASSERT (alpha3_outer1 = 0hex2 => - alpha3_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], aminoacid_energies[alpha3_outer1_index]))); - -ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000000)]); -ASSERT (alpha3_inner2 = 0hex2 => - alpha3_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)],aminoacid_energies[alpha3_inner2_index])); - - -ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer2_index])); -ASSERT (alpha3_outer2 = 0hex2 => - alpha3_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], aminoacid_energies[alpha3_outer2_index]))); - - -ASSERT (alpha3_inner3 = 0hex1 => alpha3_inner3_energy = aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000000)]); -ASSERT (alpha3_inner3 = 0hex2 => - alpha3_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000001)],aminoacid_energies[alpha3_inner3_index])); - - -ASSERT (alpha3_outer3 = 0hex1 => alpha3_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha3_outer3_index])); -ASSERT (alpha3_outer3 = 0hex2 => - alpha3_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha3_outer3_index,0hex00000001)], aminoacid_energies[alpha3_outer3_index]))); - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000000)]); -ASSERT (alpha4_inner1 = 0hex2 => - alpha4_inner1_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index])); - - -ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer1_index])); -ASSERT (alpha4_outer1 = 0hex2 => - alpha4_outer1_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)], aminoacid_energies[alpha4_outer1_index]))); - - -ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000000)]); -ASSERT (alpha4_inner2 = 0hex2 => - alpha4_inner2_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index])); - - -ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer2_index])); -ASSERT (alpha4_outer2 = 0hex2 => - alpha4_outer2_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], aminoacid_energies[alpha4_outer2_index]))); - - -ASSERT (alpha4_inner3 = 0hex1 => alpha4_inner3_energy = aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000000)]); -ASSERT (alpha4_inner3 = 0hex2 => - alpha4_inner3_energy = BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000001)],aminoacid_energies[alpha4_inner3_index])); - - -ASSERT (alpha4_outer3 = 0hex1 => alpha4_outer3_energy = BVSUB(32,bits32_one,aminoacid_energies[alpha4_outer3_index])); -ASSERT (alpha4_outer3 = 0hex2 => - alpha4_outer3_energy = BVSUB(32,bits32_two,BVPLUS(32,aminoacid_energies[BVSUB(32,alpha4_outer3_index,0hex00000001)], aminoacid_energies[alpha4_outer3_index]))); - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -ASSERT (contact_energy12_zero = BVPLUS(32, alpha1_inner1_energy, alpha2_inner1_energy)); -ASSERT (contact_energy12_one = BVPLUS(32, alpha1_inner2_energy, alpha2_inner2_energy)); -ASSERT (contact_energy12_two = BVPLUS(32, alpha1_inner3_energy, alpha2_inner3_energy)); - - -ASSERT (contact_energy23_zero = BVPLUS(32, alpha2_inner1_energy, alpha3_inner1_energy)); -ASSERT (contact_energy23_one = BVPLUS(32, alpha2_inner2_energy, alpha3_inner2_energy)); -ASSERT (contact_energy23_two = BVPLUS(32, alpha2_inner3_energy, alpha3_inner3_energy)); - - -ASSERT (contact_energy34_zero = BVPLUS(32, alpha3_inner1_energy, alpha4_inner1_energy)); -ASSERT (contact_energy34_one = BVPLUS(32, alpha3_inner2_energy, alpha4_inner2_energy)); -ASSERT (contact_energy34_two = BVPLUS(32, alpha3_inner3_energy, alpha4_inner3_energy)); - -ASSERT (contact_energy41_zero = BVPLUS(32, alpha4_inner1_energy, alpha1_inner1_energy)); -ASSERT (contact_energy41_one = BVPLUS(32, alpha4_inner2_energy, alpha1_inner2_energy)); -ASSERT (contact_energy41_two = BVPLUS(32, alpha4_inner3_energy, alpha1_inner3_energy)); - -ASSERT (outer_energy = BVPLUS(32, alpha1_outer1_energy, alpha1_outer2_energy, alpha1_outer3_energy, - alpha2_outer1_energy, alpha2_outer2_energy, alpha2_outer3_energy, - alpha3_outer1_energy, alpha3_outer2_energy, alpha3_outer3_energy, - alpha4_outer1_energy, alpha4_outer2_energy, alpha4_outer3_energy)); - - -ASSERT (inner_energy = BVPLUS(32, contact_energy12_zero, contact_energy12_one, contact_energy12_two, - contact_energy23_zero, contact_energy23_one, contact_energy23_two, - contact_energy34_zero, contact_energy34_one, contact_energy34_two, - contact_energy41_zero, contact_energy41_one, contact_energy41_two)); - - -% final query -ASSERT (BVGE(BVPLUS(64,0hex00000000@outer_energy,0hex00000000@inner_energy), 0hex0000000000000001)); -QUERY FALSE; \ No newline at end of file diff --git a/tests/bio-tests/4-alpha-helices-3-rungs.cvc b/tests/bio-tests/4-alpha-helices-3-rungs.cvc index f407ddb..e1fc120 100644 --- a/tests/bio-tests/4-alpha-helices-3-rungs.cvc +++ b/tests/bio-tests/4-alpha-helices-3-rungs.cvc @@ -3,380 +3,386 @@ % The problem is encoded with two bit bit-vector variable per face. -alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3 : BITVECTOR(4); -alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(32); -alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(64); - - -alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3 : BITVECTOR(4); -alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(32); -alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(64); - - -alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3 : BITVECTOR(4); -alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(32); -alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(64); - - -alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3 : BITVECTOR(4); -alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(32); -alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(64); - - -coil_12, coil_23, coil34 : BITVECTOR(16); -coil_12_index, coil_23_index, coil_34_index : BITVECTOR(32); -coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(64); - -contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(64); -contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(64); -contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(64); -contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(64); - -outer_energy : BITVECTOR(64); -inner_energy : BITVECTOR(64); -bits64_one : BITVECTOR(64); -bits64_two : BITVECTOR(64); - -ASSERT (bits64_one = 0hex0000000000000001); -ASSERT (bits64_two = 0hex0000000000000002); - -aminoacid_energies : ARRAY BITVECTOR(32) OF BITVECTOR(64); -ASSERT (aminoacid_energies[0hex00000000] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000001] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000002] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000003] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000004] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000005] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000006] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000007] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000008] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000009] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000000F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000010] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000011] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000012] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000013] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000014] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000015] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000016] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000017] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000018] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000019] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000001F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000020] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000021] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000022] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000023] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000024] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000025] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000026] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000027] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000028] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000029] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000002F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000030] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000031] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000032] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000033] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000034] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000035] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000036] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000037] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000038] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000039] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000003F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000040] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000041] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000042] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000043] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000044] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000045] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000046] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000047] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000048] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000049] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000004F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000050] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000051] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000052] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000053] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000054] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000055] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000056] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000057] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000058] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000059] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005A] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005B] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005C] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005D] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005E] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex0000005F] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000060] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000061] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000062] = 0hex0000000000000000); -ASSERT (aminoacid_energies[0hex00000063] = 0hex0000000000000000); - -ASSERT (alpha1_inner1 = 0hex1 OR alpha1_inner1 = 0hex2); -ASSERT (alpha1_outer1 = 0hex1 OR alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner2 = 0hex1 OR alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer2 = 0hex1 OR alpha1_outer2 = 0hex2); -ASSERT (alpha1_inner3 = 0hex1 OR alpha1_inner3 = 0hex2); -ASSERT (alpha1_outer3 = 0hex1 OR alpha1_outer3 = 0hex2); - -ASSERT (alpha2_inner1 = 0hex1 OR alpha2_inner1 = 0hex2); -ASSERT (alpha2_outer1 = 0hex1 OR alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner2 = 0hex1 OR alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer2 = 0hex1 OR alpha2_outer2 = 0hex2); -ASSERT (alpha2_inner3 = 0hex1 OR alpha2_inner3 = 0hex2); -ASSERT (alpha2_outer3 = 0hex1 OR alpha2_outer3 = 0hex2); - -ASSERT (alpha3_inner1 = 0hex1 OR alpha3_inner1 = 0hex2); -ASSERT (alpha3_outer1 = 0hex1 OR alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner2 = 0hex1 OR alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer2 = 0hex1 OR alpha3_outer2 = 0hex2); -ASSERT (alpha3_inner3 = 0hex1 OR alpha3_inner3 = 0hex2); -ASSERT (alpha3_outer3 = 0hex1 OR alpha3_outer3 = 0hex2); - -ASSERT (alpha4_inner1 = 0hex1 OR alpha4_inner1 = 0hex2); -ASSERT (alpha4_outer1 = 0hex1 OR alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner2 = 0hex1 OR alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer2 = 0hex1 OR alpha4_outer2 = 0hex2); -ASSERT (alpha4_inner3 = 0hex1 OR alpha4_inner3 = 0hex2); -ASSERT (alpha4_outer3 = 0hex1 OR alpha4_outer3 = 0hex2); - - -ASSERT (BVPLUS(4, alpha1_inner1, alpha1_outer1, alpha1_inner2, alpha1_outer2, alpha1_inner3, alpha1_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha2_inner1, alpha2_outer1, alpha2_inner2, alpha2_outer2, alpha2_inner3, alpha2_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha3_inner1, alpha3_outer1, alpha3_inner2, alpha3_outer2, alpha3_inner3, alpha3_outer3) = 0hex9); -ASSERT (BVPLUS(4, alpha4_inner1, alpha4_outer1, alpha4_inner2, alpha4_outer2, alpha4_inner3, alpha4_outer3) = 0hex9); - - -ASSERT (alpha1_inner1 = 0hex1 => alpha1_outer1 = 0hex2); -ASSERT (alpha1_inner1 = 0hex2 => alpha1_outer1 = 0hex1); -ASSERT (alpha1_outer1 = 0hex1 => alpha1_inner2 = 0hex2); -ASSERT (alpha1_outer1 = 0hex2 => alpha1_inner2 = 0hex1); -ASSERT (alpha1_inner2 = 0hex1 => alpha1_outer2 = 0hex2); -ASSERT (alpha1_inner2 = 0hex2 => alpha1_outer2 = 0hex1); -ASSERT (alpha1_inner3 = 0hex1 => alpha1_outer3 = 0hex2); -ASSERT (alpha1_inner3 = 0hex2 => alpha1_outer3 = 0hex1); - -ASSERT (alpha2_inner1 = 0hex1 => alpha2_outer1 = 0hex2); -ASSERT (alpha2_inner1 = 0hex2 => alpha2_outer1 = 0hex1); -ASSERT (alpha2_outer1 = 0hex1 => alpha2_inner2 = 0hex2); -ASSERT (alpha2_outer1 = 0hex2 => alpha2_inner2 = 0hex1); -ASSERT (alpha2_inner2 = 0hex1 => alpha2_outer2 = 0hex2); -ASSERT (alpha2_inner2 = 0hex2 => alpha2_outer2 = 0hex1); -ASSERT (alpha2_inner3 = 0hex1 => alpha2_outer3 = 0hex2); -ASSERT (alpha2_inner3 = 0hex2 => alpha2_outer3 = 0hex1); - -ASSERT (alpha3_inner1 = 0hex1 => alpha3_outer1 = 0hex2); -ASSERT (alpha3_inner1 = 0hex2 => alpha3_outer1 = 0hex1); -ASSERT (alpha3_outer1 = 0hex1 => alpha3_inner2 = 0hex2); -ASSERT (alpha3_outer1 = 0hex2 => alpha3_inner2 = 0hex1); -ASSERT (alpha3_inner2 = 0hex1 => alpha3_outer2 = 0hex2); -ASSERT (alpha3_inner2 = 0hex2 => alpha3_outer2 = 0hex1); -ASSERT (alpha3_inner3 = 0hex1 => alpha3_outer3 = 0hex2); -ASSERT (alpha3_inner3 = 0hex2 => alpha3_outer3 = 0hex1); - - -ASSERT (alpha4_inner1 = 0hex1 => alpha4_outer1 = 0hex2); -ASSERT (alpha4_inner1 = 0hex2 => alpha4_outer1 = 0hex1); -ASSERT (alpha4_outer1 = 0hex1 => alpha4_inner2 = 0hex2); -ASSERT (alpha4_outer1 = 0hex2 => alpha4_inner2 = 0hex1); -ASSERT (alpha4_inner2 = 0hex1 => alpha4_outer2 = 0hex2); -ASSERT (alpha4_inner2 = 0hex2 => alpha4_outer2 = 0hex1); -ASSERT (alpha4_inner3 = 0hex1 => alpha4_outer3 = 0hex2); -ASSERT (alpha4_inner3 = 0hex2 => alpha4_outer3 = 0hex1); +%%% ALPHA1 Helix variables +alpha1_inner1_length, alpha1_outer1_length, alpha1_inner2_length, alpha1_outer2_length, alpha1_inner3_length, alpha1_outer3_length : BITVECTOR(4); +alpha1_inner1_index, alpha1_outer1_index, alpha1_inner2_index, alpha1_outer2_index, alpha1_inner3_index, alpha1_outer3_index : BITVECTOR(16); +alpha1_inner1_energy, alpha1_outer1_energy, alpha1_inner2_energy, alpha1_outer2_energy, alpha1_inner3_energy, alpha1_outer3_energy : BITVECTOR(20); + + +%%% ALPHA2 Helix variables +alpha2_inner1_length, alpha2_outer1_length, alpha2_inner2_length, alpha2_outer2_length, alpha2_inner3_length, alpha2_outer3_length : BITVECTOR(4); +alpha2_inner1_index, alpha2_outer1_index, alpha2_inner2_index, alpha2_outer2_index, alpha2_inner3_index, alpha2_outer3_index : BITVECTOR(16); +alpha2_inner1_energy, alpha2_outer1_energy, alpha2_inner2_energy, alpha2_outer2_energy, alpha2_inner3_energy, alpha2_outer3_energy : BITVECTOR(20); + + +%%% ALPHA3 Helix variables +alpha3_inner1_length, alpha3_outer1_length, alpha3_inner2_length, alpha3_outer2_length, alpha3_inner3_length, alpha3_outer3_length : BITVECTOR(4); +alpha3_inner1_index, alpha3_outer1_index, alpha3_inner2_index, alpha3_outer2_index, alpha3_inner3_index, alpha3_outer3_index : BITVECTOR(16); +alpha3_inner1_energy, alpha3_outer1_energy, alpha3_inner2_energy, alpha3_outer2_energy, alpha3_inner3_energy, alpha3_outer3_energy : BITVECTOR(20); + + +%%% ALPHA4 Helix variables +alpha4_inner1_length, alpha4_outer1_length, alpha4_inner2_length, alpha4_outer2_length, alpha4_inner3_length, alpha4_outer3_length : BITVECTOR(4); +alpha4_inner1_index, alpha4_outer1_index, alpha4_inner2_index, alpha4_outer2_index, alpha4_inner3_index, alpha4_outer3_index : BITVECTOR(16); +alpha4_inner1_energy, alpha4_outer1_energy, alpha4_inner2_energy, alpha4_outer2_energy, alpha4_inner3_energy, alpha4_outer3_energy : BITVECTOR(20); + + +coil_12_length, coil_23_length, coil34_length : BITVECTOR(8); +coil_12_index, coil_23_index, coil_34_index : BITVECTOR(16); +coil_12_energy, coil_23_energy, coil_34_energy : BITVECTOR(20); + +contact_energy12_zero, contact_energy12_one, contact_energy12_two : BITVECTOR(32); +contact_energy23_zero, contact_energy23_one, contact_energy23_two : BITVECTOR(32); +contact_energy34_zero, contact_energy34_one, contact_energy34_two : BITVECTOR(32); +contact_energy41_zero, contact_energy41_one, contact_energy41_two : BITVECTOR(32); + +outer_energy : BITVECTOR(32); +inner_energy : BITVECTOR(32); +bits20_one : BITVECTOR(20); +bits20_two : BITVECTOR(20); + +ASSERT (bits20_one = 0hex00001); +ASSERT (bits20_two = 0hex00002); + + +%%%%%%%%%%%%%% START OF AMINO ACID ENERGY ARRAY %%%%%%%%%%%%% + +aminoacid_energies : ARRAY BITVECTOR(12) OF BITVECTOR(20); +ASSERT (aminoacid_energies[0hex000] = 0hex01111); +ASSERT (aminoacid_energies[0hex001] = 0hex01111); +ASSERT (aminoacid_energies[0hex002] = 0hex00011); +ASSERT (aminoacid_energies[0hex003] = 0hex01111); +ASSERT (aminoacid_energies[0hex004] = 0hex00011); +ASSERT (aminoacid_energies[0hex005] = 0hex01111); +ASSERT (aminoacid_energies[0hex006] = 0hex00011); +ASSERT (aminoacid_energies[0hex007] = 0hex01111); +ASSERT (aminoacid_energies[0hex008] = 0hex00011); +ASSERT (aminoacid_energies[0hex009] = 0hex01111); +ASSERT (aminoacid_energies[0hex00A] = 0hex00011); +ASSERT (aminoacid_energies[0hex00B] = 0hex01111); +ASSERT (aminoacid_energies[0hex00C] = 0hex00011); +ASSERT (aminoacid_energies[0hex00D] = 0hex01111); +ASSERT (aminoacid_energies[0hex00E] = 0hex01111); +ASSERT (aminoacid_energies[0hex00F] = 0hex01111); +ASSERT (aminoacid_energies[0hex010] = 0hex01111); +ASSERT (aminoacid_energies[0hex011] = 0hex00011); +ASSERT (aminoacid_energies[0hex012] = 0hex01111); +ASSERT (aminoacid_energies[0hex013] = 0hex01111); +ASSERT (aminoacid_energies[0hex014] = 0hex00011); +ASSERT (aminoacid_energies[0hex015] = 0hex01111); +ASSERT (aminoacid_energies[0hex016] = 0hex00011); +ASSERT (aminoacid_energies[0hex017] = 0hex01111); +ASSERT (aminoacid_energies[0hex018] = 0hex00011); +ASSERT (aminoacid_energies[0hex019] = 0hex01111); +ASSERT (aminoacid_energies[0hex01A] = 0hex00011); +ASSERT (aminoacid_energies[0hex01B] = 0hex01111); +ASSERT (aminoacid_energies[0hex01C] = 0hex01111); +ASSERT (aminoacid_energies[0hex01D] = 0hex01111); +ASSERT (aminoacid_energies[0hex01E] = 0hex01111); +ASSERT (aminoacid_energies[0hex01F] = 0hex01111); +ASSERT (aminoacid_energies[0hex020] = 0hex01111); +ASSERT (aminoacid_energies[0hex021] = 0hex00011); +ASSERT (aminoacid_energies[0hex022] = 0hex01111); +ASSERT (aminoacid_energies[0hex023] = 0hex00011); +ASSERT (aminoacid_energies[0hex024] = 0hex01111); +ASSERT (aminoacid_energies[0hex025] = 0hex00011); +ASSERT (aminoacid_energies[0hex026] = 0hex01111); +ASSERT (aminoacid_energies[0hex027] = 0hex00011); +ASSERT (aminoacid_energies[0hex028] = 0hex01111); +ASSERT (aminoacid_energies[0hex029] = 0hex01111); +ASSERT (aminoacid_energies[0hex02A] = 0hex00011); +ASSERT (aminoacid_energies[0hex02B] = 0hex01111); +ASSERT (aminoacid_energies[0hex02C] = 0hex00011); +ASSERT (aminoacid_energies[0hex02D] = 0hex00011); +ASSERT (aminoacid_energies[0hex02E] = 0hex01111); +ASSERT (aminoacid_energies[0hex02F] = 0hex01111); +ASSERT (aminoacid_energies[0hex030] = 0hex00011); +ASSERT (aminoacid_energies[0hex031] = 0hex01111); +ASSERT (aminoacid_energies[0hex032] = 0hex00011); +ASSERT (aminoacid_energies[0hex033] = 0hex01111); +ASSERT (aminoacid_energies[0hex034] = 0hex00011); +ASSERT (aminoacid_energies[0hex035] = 0hex01111); +ASSERT (aminoacid_energies[0hex036] = 0hex00011); +ASSERT (aminoacid_energies[0hex037] = 0hex01111); +ASSERT (aminoacid_energies[0hex038] = 0hex00011); +ASSERT (aminoacid_energies[0hex039] = 0hex01111); +ASSERT (aminoacid_energies[0hex03A] = 0hex01111); +ASSERT (aminoacid_energies[0hex03B] = 0hex00011); +ASSERT (aminoacid_energies[0hex03C] = 0hex01111); +ASSERT (aminoacid_energies[0hex03D] = 0hex00011); +ASSERT (aminoacid_energies[0hex03E] = 0hex01111); +ASSERT (aminoacid_energies[0hex03F] = 0hex00011); +ASSERT (aminoacid_energies[0hex040] = 0hex01111); +ASSERT (aminoacid_energies[0hex041] = 0hex00011); +ASSERT (aminoacid_energies[0hex042] = 0hex01111); +ASSERT (aminoacid_energies[0hex043] = 0hex00011); +ASSERT (aminoacid_energies[0hex044] = 0hex01111); +ASSERT (aminoacid_energies[0hex045] = 0hex00011); +ASSERT (aminoacid_energies[0hex046] = 0hex01111); +ASSERT (aminoacid_energies[0hex047] = 0hex00011); +ASSERT (aminoacid_energies[0hex048] = 0hex01111); +ASSERT (aminoacid_energies[0hex049] = 0hex00011); +ASSERT (aminoacid_energies[0hex04A] = 0hex01111); +ASSERT (aminoacid_energies[0hex04B] = 0hex01111); +ASSERT (aminoacid_energies[0hex04C] = 0hex01111); +ASSERT (aminoacid_energies[0hex04D] = 0hex01111); +ASSERT (aminoacid_energies[0hex04E] = 0hex01111); +ASSERT (aminoacid_energies[0hex04F] = 0hex01111); +ASSERT (aminoacid_energies[0hex050] = 0hex01111); +ASSERT (aminoacid_energies[0hex051] = 0hex00011); +ASSERT (aminoacid_energies[0hex052] = 0hex01111); +ASSERT (aminoacid_energies[0hex053] = 0hex00011); +ASSERT (aminoacid_energies[0hex054] = 0hex01111); +ASSERT (aminoacid_energies[0hex055] = 0hex00011); +ASSERT (aminoacid_energies[0hex056] = 0hex01111); +ASSERT (aminoacid_energies[0hex057] = 0hex00011); +ASSERT (aminoacid_energies[0hex058] = 0hex01111); +ASSERT (aminoacid_energies[0hex059] = 0hex01111); +ASSERT (aminoacid_energies[0hex05A] = 0hex01111); +ASSERT (aminoacid_energies[0hex05B] = 0hex00011); +ASSERT (aminoacid_energies[0hex05C] = 0hex01111); +ASSERT (aminoacid_energies[0hex05D] = 0hex00011); +ASSERT (aminoacid_energies[0hex05E] = 0hex01111); +ASSERT (aminoacid_energies[0hex05F] = 0hex01111); +ASSERT (aminoacid_energies[0hex060] = 0hex00011); +ASSERT (aminoacid_energies[0hex061] = 0hex01111); +ASSERT (aminoacid_energies[0hex062] = 0hex01111); +ASSERT (aminoacid_energies[0hex063] = 0hex00000); + +%%%%%%%%%%%%%% END OF AMINO ACID ENERGY ARRAY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF RUNG LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%% + +ASSERT (alpha1_inner1_length = 0hex1 OR alpha1_inner1_length = 0hex2); +ASSERT (alpha1_outer1_length = 0hex1 OR alpha1_outer1_length = 0hex2); +ASSERT (alpha1_inner2_length = 0hex1 OR alpha1_inner2_length = 0hex2); +ASSERT (alpha1_outer2_length = 0hex1 OR alpha1_outer2_length = 0hex2); +ASSERT (alpha1_inner3_length = 0hex1 OR alpha1_inner3_length = 0hex2); +ASSERT (alpha1_outer3_length = 0hex1 OR alpha1_outer3_length = 0hex2); + +ASSERT (alpha2_inner1_length = 0hex1 OR alpha2_inner1_length = 0hex2); +ASSERT (alpha2_outer1_length = 0hex1 OR alpha2_outer1_length = 0hex2); +ASSERT (alpha2_inner2_length = 0hex1 OR alpha2_inner2_length = 0hex2); +ASSERT (alpha2_outer2_length = 0hex1 OR alpha2_outer2_length = 0hex2); +ASSERT (alpha2_inner3_length = 0hex1 OR alpha2_inner3_length = 0hex2); +ASSERT (alpha2_outer3_length = 0hex1 OR alpha2_outer3_length = 0hex2); + +ASSERT (alpha3_inner1_length = 0hex1 OR alpha3_inner1_length = 0hex2); +ASSERT (alpha3_outer1_length = 0hex1 OR alpha3_outer1_length = 0hex2); +ASSERT (alpha3_inner2_length = 0hex1 OR alpha3_inner2_length = 0hex2); +ASSERT (alpha3_outer2_length = 0hex1 OR alpha3_outer2_length = 0hex2); +ASSERT (alpha3_inner3_length = 0hex1 OR alpha3_inner3_length = 0hex2); +ASSERT (alpha3_outer3_length = 0hex1 OR alpha3_outer3_length = 0hex2); + +ASSERT (alpha4_inner1_length = 0hex1 OR alpha4_inner1_length = 0hex2); +ASSERT (alpha4_outer1_length = 0hex1 OR alpha4_outer1_length = 0hex2); +ASSERT (alpha4_inner2_length = 0hex1 OR alpha4_inner2_length = 0hex2); +ASSERT (alpha4_outer2_length = 0hex1 OR alpha4_outer2_length = 0hex2); +ASSERT (alpha4_inner3_length = 0hex1 OR alpha4_inner3_length = 0hex2); +ASSERT (alpha4_outer3_length = 0hex1 OR alpha4_outer3_length = 0hex2); + + +ASSERT (BVPLUS(4, alpha1_inner1_length, alpha1_outer1_length, alpha1_inner2_length, + alpha1_outer2_length, alpha1_inner3_length, alpha1_outer3_length) = 0hex9); +ASSERT (BVPLUS(4, alpha2_inner1_length, alpha2_outer1_length, alpha2_inner2_length, + alpha2_outer2_length, alpha2_inner3_length, alpha2_outer3_length) = 0hex9); +ASSERT (BVPLUS(4, alpha3_inner1_length, alpha3_outer1_length, alpha3_inner2_length, + alpha3_outer2_length, alpha3_inner3_length, alpha3_outer3_length) = 0hex9); +ASSERT (BVPLUS(4, alpha4_inner1_length, alpha4_outer1_length, alpha4_inner2_length, + alpha4_outer2_length, alpha4_inner3_length, alpha4_outer3_length) = 0hex9); -ASSERT (alpha1_inner1 = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]); -ASSERT (alpha1_inner1 = 0hex2 => - alpha1_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner1_index,0hex00000001)],aminoacid_energies[alpha1_inner1_index])); +ASSERT (BVPLUS(4, alpha1_inner1_length, alpha1_outer1_length) = 0hex3); +ASSERT (BVPLUS(4, alpha1_inner2_length, alpha1_outer2_length) = 0hex3); +ASSERT (BVPLUS(4, alpha1_inner3_length, alpha1_outer3_length) = 0hex3); +ASSERT (BVPLUS(4, alpha2_inner1_length, alpha2_outer1_length) = 0hex3); +ASSERT (BVPLUS(4, alpha2_inner2_length, alpha2_outer2_length) = 0hex3); +ASSERT (BVPLUS(4, alpha2_inner3_length, alpha2_outer3_length) = 0hex3); -ASSERT (alpha1_outer1 = 0hex1 => alpha1_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer1_index])); -ASSERT (alpha1_outer1 = 0hex2 => - alpha1_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer1_index,0hex00000001)], aminoacid_energies[alpha1_outer1_index]))); +ASSERT (BVPLUS(4, alpha3_inner1_length, alpha3_outer1_length) = 0hex3); +ASSERT (BVPLUS(4, alpha3_inner2_length, alpha3_outer2_length) = 0hex3); +ASSERT (BVPLUS(4, alpha3_inner3_length, alpha3_outer3_length) = 0hex3); +ASSERT (BVPLUS(4, alpha4_inner1_length, alpha4_outer1_length) = 0hex3); +ASSERT (BVPLUS(4, alpha4_inner2_length, alpha4_outer2_length) = 0hex3); +ASSERT (BVPLUS(4, alpha4_inner3_length, alpha4_outer3_length) = 0hex3); -ASSERT (alpha1_inner2 = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]); -ASSERT (alpha1_inner2 = 0hex2 => - alpha1_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner2_index,0hex00000001)],aminoacid_energies[alpha1_inner2_index])); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF RUNG LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF COIL LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha1_outer2 = 0hex1 => alpha1_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer2_index])); -ASSERT (alpha1_outer2 = 0hex2 => - alpha1_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer2_index,0hex00000001)], aminoacid_energies[alpha1_outer2_index]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF COIL LENGTH CONSTRAINTS %%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha1_inner3 = 0hex1 => alpha1_inner3_energy = aminoacid_energies[alpha1_inner3_index]); -ASSERT (alpha1_inner3 = 0hex2 => - alpha1_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_inner3_index,0hex00000001)],aminoacid_energies[alpha1_inner3_index])); -ASSERT (alpha1_outer3 = 0hex1 => alpha1_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha1_outer3_index])); -ASSERT (alpha1_outer3 = 0hex2 => - alpha1_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha1_outer3_index,0hex00000001)], aminoacid_energies[alpha1_outer3_index]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF CHAINING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%ASSERT (BVLE(0hex -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF CHAINING %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha2_inner1 = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]); -ASSERT (alpha2_inner1 = 0hex2 => - alpha2_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner1_index,0hex00000001)],aminoacid_energies[alpha2_inner1_index])); +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha2_outer1 = 0hex1 => alpha2_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer1_index])); -ASSERT (alpha2_outer1 = 0hex2 => - alpha2_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer1_index,0hex00000001)], aminoacid_energies[alpha2_outer1_index]))); +ASSERT (alpha1_inner1_length = 0hex1 => alpha1_inner1_energy = aminoacid_energies[alpha1_inner1_index]); +ASSERT (alpha1_inner1_length = 0hex2 => alpha1_inner1_energy = BVPLUS(20,aminoacid_energies[alpha1_inner1_index], + aminoacid_energies[BVSUB(12,alpha1_inner1_index,0hex001)])); +ASSERT (alpha1_outer1_length = 0hex1 => alpha1_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer1_index])); +ASSERT (alpha1_outer1_length = 0hex2 => alpha1_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha1_outer1_index], + aminoacid_energies[BVSUB(12,alpha1_outer1_index,0hex001)]))); -ASSERT (alpha2_inner2 = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]); -ASSERT (alpha2_inner2 = 0hex2 => - alpha2_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner2_index,0hex00000001)],aminoacid_energies[alpha2_inner2_index])); +ASSERT (alpha1_inner2_length = 0hex1 => alpha1_inner2_energy = aminoacid_energies[alpha1_inner2_index]); +ASSERT (alpha1_inner2_length = 0hex2 => alpha1_inner2_energy = BVPLUS(20,aminoacid_energies[alpha1_inner2_index], + aminoacid_energies[BVSUB(12,alpha1_inner2_index,0hex001)])); -ASSERT (alpha2_outer2 = 0hex1 => alpha2_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer2_index])); -ASSERT (alpha2_outer2 = 0hex2 => - alpha2_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer2_index,0hex00000001)], aminoacid_energies[alpha2_outer2_index]))); +ASSERT (alpha1_outer2_length = 0hex1 => alpha1_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer2_index])); +ASSERT (alpha1_outer2_length = 0hex2 => alpha1_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha1_outer2_index], + aminoacid_energies[BVSUB(12,alpha1_outer2_index,0hex001)],))); -ASSERT (alpha2_inner3 = 0hex1 => alpha2_inner3_energy = aminoacid_energies[alpha2_inner3_index]); -ASSERT (alpha2_inner3 = 0hex2 => - alpha2_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_inner3_index,0hex00000001)],aminoacid_energies[alpha2_inner3_index])); +ASSERT (alpha1_inner3_length = 0hex1 => alpha1_inner3_energy = aminoacid_energies[alpha1_inner3_index]); +ASSERT (alpha1_inner3_length = 0hex2 => alpha1_inner3_energy = BVPLUS(20,aminoacid_energies[alpha1_inner3_index], + aminoacid_energies[BVSUB(12,alpha1_inner3_index,0hex001)])); -ASSERT (alpha2_outer3 = 0hex1 => alpha2_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha2_outer3_index])); -ASSERT (alpha2_outer3 = 0hex2 => - alpha2_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha2_outer3_index,0hex00000001)], aminoacid_energies[alpha2_outer3_index]))); +ASSERT (alpha1_outer3_length = 0hex1 => alpha1_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha1_outer3_index])); +ASSERT (alpha1_outer3_length = 0hex2 => alpha1_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha1_outer3_index], + aminoacid_energies[BVSUB(12,alpha1_outer3_index,0hex001)]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha3_inner1 = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]); -ASSERT (alpha3_inner1 = 0hex2 => - alpha3_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner1_index,0hex00000001)],aminoacid_energies[alpha3_inner1_index])); +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +ASSERT (alpha2_inner1_length = 0hex1 => alpha2_inner1_energy = aminoacid_energies[alpha2_inner1_index]); +ASSERT (alpha2_inner1_length = 0hex2 => alpha2_inner1_energy = BVPLUS(20,aminoacid_energies[alpha2_inner1_index], + aminoacid_energies[BVSUB(12,alpha2_inner1_index,0hex001)])); -ASSERT (alpha3_outer1 = 0hex1 => alpha3_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer1_index])); -ASSERT (alpha3_outer1 = 0hex2 => - alpha3_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer1_index,0hex00000001)], aminoacid_energies[alpha3_outer1_index]))); +ASSERT (alpha2_outer1_length = 0hex1 => alpha2_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer1_index])); +ASSERT (alpha2_outer1_length = 0hex2 => alpha2_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha2_outer1_index], + aminoacid_energies[BVSUB(12,alpha2_outer1_index,0hex001)]))); -% ASSERT (alpha3_outer1 = 0hex2 => -% alpha3_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,0hex0, 0hex0))); +ASSERT (alpha2_inner2_length = 0hex1 => alpha2_inner2_energy = aminoacid_energies[alpha2_inner2_index]); +ASSERT (alpha2_inner2_length = 0hex2 => alpha2_inner2_energy = BVPLUS(20,aminoacid_energies[alpha2_inner2_index], + aminoacid_energies[BVSUB(12,alpha2_inner2_index,0hex001)])); -ASSERT (alpha3_inner2 = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]); -ASSERT (alpha3_inner2 = 0hex2 => - alpha3_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner2_index,0hex00000001)],aminoacid_energies[alpha3_inner2_index])); +ASSERT (alpha2_outer2_length = 0hex1 => alpha2_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer2_index])); +ASSERT (alpha2_outer2_length = 0hex2 => alpha2_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha2_outer2_index], + aminoacid_energies[BVSUB(12,alpha2_outer2_index,0hex001)],))); -ASSERT (alpha3_outer2 = 0hex1 => alpha3_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer2_index])); -ASSERT (alpha3_outer2 = 0hex2 => - alpha3_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer2_index,0hex00000001)], aminoacid_energies[alpha3_outer2_index]))); +ASSERT (alpha2_inner3_length = 0hex1 => alpha2_inner3_energy = aminoacid_energies[alpha2_inner3_index]); +ASSERT (alpha2_inner3_length = 0hex2 => alpha2_inner3_energy = BVPLUS(20,aminoacid_energies[alpha2_inner3_index], + aminoacid_energies[BVSUB(12,alpha2_inner3_index,0hex001)])); -ASSERT (alpha3_inner3 = 0hex1 => alpha3_inner3_energy = aminoacid_energies[alpha3_inner3_index]); -ASSERT (alpha3_inner3 = 0hex2 => - alpha3_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_inner3_index,0hex00000001)],aminoacid_energies[alpha3_inner3_index])); +ASSERT (alpha2_outer3_length = 0hex1 => alpha2_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha2_outer3_index])); +ASSERT (alpha2_outer3_length = 0hex2 => alpha2_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha2_outer3_index], + aminoacid_energies[BVSUB(12,alpha2_outer3_index,0hex001)]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha3_outer3 = 0hex1 => alpha3_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha3_outer3_index])); -ASSERT (alpha3_outer3 = 0hex2 => - alpha3_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha3_outer3_index,0hex00000001)], aminoacid_energies[alpha3_outer3_index]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +ASSERT (alpha3_inner1_length = 0hex1 => alpha3_inner1_energy = aminoacid_energies[alpha3_inner1_index]); +ASSERT (alpha3_inner1_length = 0hex2 => alpha3_inner1_energy = BVPLUS(20,aminoacid_energies[alpha3_inner1_index], + aminoacid_energies[BVSUB(12,alpha3_inner1_index,0hex001)])); -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +ASSERT (alpha3_outer1_length = 0hex1 => alpha3_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer1_index])); +ASSERT (alpha3_outer1_length = 0hex2 => alpha3_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha3_outer1_index], + aminoacid_energies[BVSUB(12,alpha3_outer1_index,0hex001)]))); -ASSERT (alpha4_inner1 = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]); -ASSERT (alpha4_inner1 = 0hex2 => - alpha4_inner1_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner1_index,0hex00000001)],aminoacid_energies[alpha4_inner1_index])); +ASSERT (alpha3_inner2_length = 0hex1 => alpha3_inner2_energy = aminoacid_energies[alpha3_inner2_index]); +ASSERT (alpha3_inner2_length = 0hex2 => alpha3_inner2_energy = BVPLUS(20,aminoacid_energies[alpha3_inner2_index], + aminoacid_energies[BVSUB(12,alpha3_inner2_index,0hex001)])); -ASSERT (alpha4_outer1 = 0hex1 => alpha4_outer1_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer1_index])); -ASSERT (alpha4_outer1 = 0hex2 => - alpha4_outer1_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer1_index,0hex00000001)], aminoacid_energies[alpha4_outer1_index]))); +ASSERT (alpha3_outer2_length = 0hex1 => alpha3_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer2_index])); +ASSERT (alpha3_outer2_length = 0hex2 => alpha3_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha3_outer2_index], + aminoacid_energies[BVSUB(12,alpha3_outer2_index,0hex001)],))); -ASSERT (alpha4_inner2 = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]); -ASSERT (alpha4_inner2 = 0hex2 => - alpha4_inner2_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner2_index,0hex00000001)],aminoacid_energies[alpha4_inner2_index])); +ASSERT (alpha3_inner3_length = 0hex1 => alpha3_inner3_energy = aminoacid_energies[alpha3_inner3_index]); +ASSERT (alpha3_inner3_length = 0hex2 => alpha3_inner3_energy = BVPLUS(20,aminoacid_energies[alpha3_inner3_index], + aminoacid_energies[BVSUB(12,alpha3_inner3_index,0hex001)])); -ASSERT (alpha4_outer2 = 0hex1 => alpha4_outer2_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer2_index])); -ASSERT (alpha4_outer2 = 0hex2 => - alpha4_outer2_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer2_index,0hex00000001)], aminoacid_energies[alpha4_outer2_index]))); +ASSERT (alpha3_outer3_length = 0hex1 => alpha3_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha3_outer3_index])); +ASSERT (alpha3_outer3_length = 0hex2 => alpha3_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha3_outer3_index], + aminoacid_energies[BVSUB(12,alpha3_outer3_index,0hex001)]))); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha4_inner3 = 0hex1 => alpha4_inner3_energy = aminoacid_energies[alpha4_inner3_index]); -ASSERT (alpha4_inner3 = 0hex2 => - alpha4_inner3_energy = BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_inner3_index,0hex00000001)],aminoacid_energies[alpha4_inner3_index])); +%%%%%%%%%%%%%%%%%%%%%%%%%% START OF ENERGY COMPUTATION ALPHA4 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (alpha4_outer3 = 0hex1 => alpha4_outer3_energy = BVSUB(64,bits64_one,aminoacid_energies[alpha4_outer3_index])); -ASSERT (alpha4_outer3 = 0hex2 => - alpha4_outer3_energy = BVSUB(64,bits64_two,BVPLUS(64,aminoacid_energies[BVSUB(32,alpha4_outer3_index,0hex00000001)], aminoacid_energies[alpha4_outer3_index]))); +ASSERT (alpha4_inner1_length = 0hex1 => alpha4_inner1_energy = aminoacid_energies[alpha4_inner1_index]); +ASSERT (alpha4_inner1_length = 0hex2 => alpha4_inner1_energy = BVPLUS(20,aminoacid_energies[alpha4_inner1_index], + aminoacid_energies[BVSUB(12,alpha4_inner1_index,0hex001)])); +ASSERT (alpha4_outer1_length = 0hex1 => alpha4_outer1_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer1_index])); +ASSERT (alpha4_outer1_length = 0hex2 => alpha4_outer1_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha4_outer1_index], + aminoacid_energies[BVSUB(12,alpha4_outer1_index,0hex001)]))); -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (contact_energy12_zero = BVPLUS(64, alpha1_inner1_energy, alpha2_inner1_energy)); -ASSERT (contact_energy12_one = BVPLUS(64, alpha1_inner2_energy, alpha2_inner2_energy)); -ASSERT (contact_energy12_two = BVPLUS(64, alpha1_inner3_energy, alpha2_inner3_energy)); +ASSERT (alpha4_inner2_length = 0hex1 => alpha4_inner2_energy = aminoacid_energies[alpha4_inner2_index]); +ASSERT (alpha4_inner2_length = 0hex2 => alpha4_inner2_energy = BVPLUS(20,aminoacid_energies[alpha4_inner2_index], + aminoacid_energies[BVSUB(12,alpha4_inner2_index,0hex001)])); -ASSERT (contact_energy23_zero = BVPLUS(64, alpha2_inner1_energy, alpha3_inner1_energy)); -ASSERT (contact_energy23_one = BVPLUS(64, alpha2_inner2_energy, alpha3_inner2_energy)); -ASSERT (contact_energy23_two = BVPLUS(64, alpha2_inner3_energy, alpha3_inner3_energy)); +ASSERT (alpha4_outer2_length = 0hex1 => alpha4_outer2_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer2_index])); +ASSERT (alpha4_outer2_length = 0hex2 => alpha4_outer2_energy = BVSUB(20,bits20_two,BVPLUS(20,aminoacid_energies[alpha4_outer2_index], + aminoacid_energies[BVSUB(12,alpha4_outer2_index,0hex001)],))); +ASSERT (alpha4_inner3_length = 0hex1 => alpha4_inner3_energy = aminoacid_energies[alpha4_inner3_index]); +ASSERT (alpha4_inner3_length = 0hex2 => alpha4_inner3_energy = BVPLUS(20,aminoacid_energies[alpha4_inner3_index], + aminoacid_energies[BVSUB(12,alpha4_inner3_index,0hex001)])); -ASSERT (contact_energy34_zero = BVPLUS(64, alpha3_inner1_energy, alpha4_inner1_energy)); -ASSERT (contact_energy34_one = BVPLUS(64, alpha3_inner2_energy, alpha4_inner2_energy)); -ASSERT (contact_energy34_two = BVPLUS(64, alpha3_inner3_energy, alpha4_inner3_energy)); -ASSERT (contact_energy41_zero = BVPLUS(64, alpha4_inner1_energy, alpha1_inner1_energy)); -ASSERT (contact_energy41_one = BVPLUS(64, alpha4_inner2_energy, alpha1_inner2_energy)); -ASSERT (contact_energy41_two = BVPLUS(64, alpha4_inner3_energy, alpha1_inner3_energy)); +ASSERT (alpha4_outer3_length = 0hex1 => alpha4_outer3_energy = BVSUB(20,bits20_one,aminoacid_energies[alpha4_outer3_index])); +ASSERT (alpha4_outer3_length = 0hex2 => alpha4_outer3_energy = BVSUB(20,bits20_two, BVPLUS(20,aminoacid_energies[alpha4_outer3_index], + aminoacid_energies[BVSUB(12,alpha4_outer3_index,0hex001)]))); -ASSERT (outer_energy = BVPLUS(64, alpha1_outer1_energy, alpha1_outer2_energy, alpha1_outer3_energy, - alpha2_outer1_energy, alpha2_outer2_energy, alpha2_outer3_energy, - alpha3_outer1_energy, alpha3_outer2_energy, alpha3_outer3_energy, - alpha4_outer1_energy, alpha4_outer2_energy, alpha4_outer3_energy)); +%%%%%%%%%%%%%%%%%%%%%%%%%% END OF ENERGY COMPUTATION ALPHA4 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -ASSERT (inner_energy = BVPLUS(64, contact_energy12_zero, contact_energy12_one, contact_energy12_two, +ASSERT (contact_energy12_zero = BVPLUS(32, 0hex000@alpha1_inner1_energy, 0hex000@alpha2_inner1_energy)); +ASSERT (contact_energy12_one = BVPLUS(32, 0hex000@alpha1_inner2_energy, 0hex000@alpha2_inner2_energy)); +ASSERT (contact_energy12_two = BVPLUS(32, 0hex000@alpha1_inner3_energy, 0hex000@alpha2_inner3_energy)); + + +ASSERT (contact_energy23_zero = BVPLUS(32, 0hex000@alpha2_inner1_energy, 0hex000@alpha3_inner1_energy)); +ASSERT (contact_energy23_one = BVPLUS(32, 0hex000@alpha2_inner2_energy, 0hex000@alpha3_inner2_energy)); +ASSERT (contact_energy23_two = BVPLUS(32, 0hex000@alpha2_inner3_energy, 0hex000@alpha3_inner3_energy)); + + +ASSERT (contact_energy34_zero = BVPLUS(32, 0hex000@alpha3_inner1_energy, 0hex000@alpha4_inner1_energy)); +ASSERT (contact_energy34_one = BVPLUS(32, 0hex000@alpha3_inner2_energy, 0hex000@alpha4_inner2_energy)); +ASSERT (contact_energy34_two = BVPLUS(32, 0hex000@alpha3_inner3_energy, 0hex000@alpha4_inner3_energy)); + +ASSERT (contact_energy41_zero = BVPLUS(32, 0hex000@alpha4_inner1_energy, 0hex000@alpha1_inner1_energy)); +ASSERT (contact_energy41_one = BVPLUS(32, 0hex000@alpha4_inner2_energy, 0hex000@alpha1_inner2_energy)); +ASSERT (contact_energy41_two = BVPLUS(32, 0hex000@alpha4_inner3_energy, 0hex000@alpha1_inner3_energy)); + +ASSERT (outer_energy = BVPLUS(32, 0hex000@alpha1_outer1_energy, 0hex000@alpha1_outer2_energy, 0hex000@alpha1_outer3_energy, + 0hex000@alpha2_outer1_energy, 0hex000@alpha2_outer2_energy, 0hex000@alpha2_outer3_energy, + 0hex000@alpha3_outer1_energy, 0hex000@alpha3_outer2_energy, 0hex000@alpha3_outer3_energy, + 0hex000@alpha4_outer1_energy, 0hex000@alpha4_outer2_energy, 0hex000@alpha4_outer3_energy)); + + +ASSERT (inner_energy = BVPLUS(32, contact_energy12_zero, contact_energy12_one, contact_energy12_two, contact_energy23_zero, contact_energy23_one, contact_energy23_two, contact_energy34_zero, contact_energy34_one, contact_energy34_two, contact_energy41_zero, contact_energy41_one, contact_energy41_two)); % final query -ASSERT (BVGE(BVPLUS(64,outer_energy,inner_energy), 0hex1111111111111110)); +ASSERT (BVGE(BVMULT(64,0hex00000000@outer_energy,0hex00000000@inner_energy), 0hex0011111111111110)); QUERY FALSE; \ No newline at end of file -- 2.47.3