From b71d497db9db3b37f83aeb86f0ac198200494aa0 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 10 Nov 2011 11:57:35 +0000 Subject: [PATCH] Improvement. Add the ability to set SAT solvers via the command line. Thanks to Stephan Falke. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1408 e59a4935-1847-0410-ae03-e826735625c1 --- src/c_interface/c_interface.cpp | 15 ++++++++--- src/c_interface/c_interface.h | 6 ++++- tests/c-api-tests/Makefile | 9 +++++-- tests/c-api-tests/f.cvc | 45 +++++++++++++++++++++++++++++++++ tests/c-api-tests/stp-test3.c | 32 +++++++++++++++++++++++ 5 files changed, 100 insertions(+), 7 deletions(-) create mode 100644 tests/c-api-tests/f.cvc create mode 100644 tests/c-api-tests/stp-test3.c diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 62ff877..849f131 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -141,16 +141,23 @@ void vc_setFlags(VC vc, char c, int param_value) { } void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value) { - switch (f) { + bmstar b = (bmstar)(((stpstar)vc)->bm); + switch (f) { case EXPRDELETE: cinterface_exprdelete_on_flag = param_value != 0; break; + case MS: + b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::MINISAT_SOLVER; + break; + case SMS: + b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER; + break; case CMS2: - { - bmstar b = (bmstar)(((stpstar)vc)->bm); b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::CRYPTOMINISAT_SOLVER; break; - } + case MSP: + b->UserFlags.solver_to_use = BEEV::UserDefinedFlags::MINISAT_PROPAGATORS; + break; default: BEEV::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized flag\n"); break; diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index 19b4a2d..a8fd947 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -58,7 +58,11 @@ extern "C" { the time that vc_Destroy is called, vc_Destroy will automatically delete them. */ EXPRDELETE, - CMS2 + MS, + SMS, + CMS2, + MSP + }; void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value); diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index d42f897..e18e2b5 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -14,7 +14,7 @@ else endif -all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 +all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 rm -rf *.out 0: @@ -105,8 +105,13 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 ./a24.out 25: - g++ $(CXXFLAGS) -o a26.out \ + g++ $(CXXFLAGS) -o a25.out \ ../../lib/libstp.a stp-bool.c ../../lib/libstp.a + ./a25.out + +26: + g++ $(CXXFLAGS) -o a26.out \ + ../../lib/libstp.a stp-test3.c ../../lib/libstp.a ./a26.out clean: diff --git a/tests/c-api-tests/f.cvc b/tests/c-api-tests/f.cvc new file mode 100644 index 0000000..85c743a --- /dev/null +++ b/tests/c-api-tests/f.cvc @@ -0,0 +1,45 @@ +%% Regression level = 0 +%% Result = InValid +%% Runtime = 1 +%% Language = presentation + +x0 : BITVECTOR(64); +x1 : BITVECTOR(64); +x2 : BITVECTOR(64); +x3 : BITVECTOR(64); +x4 : BITVECTOR(64); +x5 : BITVECTOR(64); +x6 : BITVECTOR(64); +x7 : BITVECTOR(64); +x8 : BITVECTOR(64); +x9 : BITVECTOR(64); +x10 : BITVECTOR(64); +x11 : BITVECTOR(64); +x12 : BITVECTOR(64); +x13 : BITVECTOR(64); +x14 : BITVECTOR(64); +x15 : BITVECTOR(64); +x16 : BITVECTOR(64); +x17 : BITVECTOR(64); +x18 : BITVECTOR(64); +x19 : BITVECTOR(64); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c6a), BVMULT(64,x1, 0hex0000000000000685), BVMULT(64,x2, 0hex000000000000078c), BVMULT(64,x3, 0hex00000000000005d5), BVMULT(64,x4, 0hex0000000000000809), BVMULT(64,x5, 0hex000000000000042f), BVMULT(64,x6, 0hex0000000000000d11), BVMULT(64,x7, 0hex0000000000000e32), BVMULT(64,x8, 0hex00000000000004e3), BVMULT(64,x9, 0hex0000000000000848), BVMULT(64,x10, 0hex000000000000020f), BVMULT(64,x11, 0hex00000000000005b1), BVMULT(64,x12, 0hex0000000000000f41), BVMULT(64,x13, 0hex0000000000000a8a), BVMULT(64,x14, 0hex0000000000000967), BVMULT(64,x15, 0hex0000000000000f34), BVMULT(64,x16, 0hex0000000000000eb4), BVMULT(64,x17, 0hex00000000000008a6), BVMULT(64,x18, 0hex0000000000000614), BVMULT(64,x19, 0hex00000000000005da),0hex0000000000000000) = 0hex0000000000000e43); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000264), BVMULT(64,x1, 0hex0000000000000480), BVMULT(64,x2, 0hex0000000000000ebd), BVMULT(64,x3, 0hex0000000000000118), BVMULT(64,x4, 0hex0000000000000f75), BVMULT(64,x5, 0hex00000000000002e0), BVMULT(64,x6, 0hex0000000000000ec4), BVMULT(64,x7, 0hex0000000000000691), BVMULT(64,x8, 0hex0000000000000725), BVMULT(64,x9, 0hex0000000000000836), BVMULT(64,x10, 0hex00000000000005d7), BVMULT(64,x11, 0hex0000000000000ad0), BVMULT(64,x12, 0hex0000000000000489), BVMULT(64,x13, 0hex000000000000036b), BVMULT(64,x14, 0hex000000000000029f), BVMULT(64,x15, 0hex0000000000000864), BVMULT(64,x16, 0hex0000000000000ada), BVMULT(64,x17, 0hex000000000000032a), BVMULT(64,x18, 0hex000000000000020a), BVMULT(64,x19, 0hex0000000000000ebb),0hex0000000000000000) = 0hex00000000000006e4); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000004a8), BVMULT(64,x1, 0hex00000000000001ee), BVMULT(64,x2, 0hex0000000000000cf6), BVMULT(64,x3, 0hex00000000000009b4), BVMULT(64,x4, 0hex0000000000000136), BVMULT(64,x5, 0hex0000000000000cb9), BVMULT(64,x6, 0hex0000000000000648), BVMULT(64,x7, 0hex0000000000000149), BVMULT(64,x8, 0hex000000000000014f), BVMULT(64,x9, 0hex00000000000004d0), BVMULT(64,x10, 0hex0000000000000dde), BVMULT(64,x11, 0hex0000000000000e7f), BVMULT(64,x12, 0hex00000000000005c9), BVMULT(64,x13, 0hex00000000000004f9), BVMULT(64,x14, 0hex0000000000000c4f), BVMULT(64,x15, 0hex00000000000001c0), BVMULT(64,x16, 0hex0000000000000116), BVMULT(64,x17, 0hex0000000000000a6f), BVMULT(64,x18, 0hex0000000000000e8f), BVMULT(64,x19, 0hex0000000000000222),0hex0000000000000000) = 0hex0000000000000aaf); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000d88), BVMULT(64,x1, 0hex0000000000000bc1), BVMULT(64,x2, 0hex0000000000000446), BVMULT(64,x3, 0hex0000000000000c96), BVMULT(64,x4, 0hex0000000000000655), BVMULT(64,x5, 0hex0000000000000800), BVMULT(64,x6, 0hex0000000000000d7d), BVMULT(64,x7, 0hex0000000000000b6a), BVMULT(64,x8, 0hex0000000000000650), BVMULT(64,x9, 0hex0000000000000990), BVMULT(64,x10, 0hex0000000000000028), BVMULT(64,x11, 0hex0000000000000a23), BVMULT(64,x12, 0hex0000000000000c62), BVMULT(64,x13, 0hex0000000000000ddc), BVMULT(64,x14, 0hex0000000000000bef), BVMULT(64,x15, 0hex000000000000050c), BVMULT(64,x16, 0hex0000000000000061), BVMULT(64,x17, 0hex0000000000000577), BVMULT(64,x18, 0hex0000000000000357), BVMULT(64,x19, 0hex0000000000000790),0hex0000000000000000) = 0hex0000000000000dfb); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex000000000000000b), BVMULT(64,x1, 0hex0000000000000427), BVMULT(64,x2, 0hex0000000000000d0a), BVMULT(64,x3, 0hex0000000000000c8a), BVMULT(64,x4, 0hex0000000000000446), BVMULT(64,x5, 0hex0000000000000464), BVMULT(64,x6, 0hex00000000000004d9), BVMULT(64,x7, 0hex0000000000000038), BVMULT(64,x8, 0hex0000000000000f7c), BVMULT(64,x9, 0hex0000000000000e3c), BVMULT(64,x10, 0hex00000000000007db), BVMULT(64,x11, 0hex0000000000000631), BVMULT(64,x12, 0hex000000000000011b), BVMULT(64,x13, 0hex00000000000006c7), BVMULT(64,x14, 0hex0000000000000976), BVMULT(64,x15, 0hex000000000000099f), BVMULT(64,x16, 0hex0000000000000c24), BVMULT(64,x17, 0hex00000000000001e9), BVMULT(64,x18, 0hex0000000000000872), BVMULT(64,x19, 0hex0000000000000f72),0hex0000000000000000) = 0hex00000000000009e4); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000d8d), BVMULT(64,x1, 0hex0000000000000c8d), BVMULT(64,x2, 0hex0000000000000aa3), BVMULT(64,x3, 0hex00000000000000ec), BVMULT(64,x4, 0hex00000000000005bf), BVMULT(64,x5, 0hex00000000000004a6), BVMULT(64,x6, 0hex0000000000000b3d), BVMULT(64,x7, 0hex0000000000000bdf), BVMULT(64,x8, 0hex00000000000006cd), BVMULT(64,x9, 0hex000000000000058b), BVMULT(64,x10, 0hex000000000000047b), BVMULT(64,x11, 0hex0000000000000bd3), BVMULT(64,x12, 0hex000000000000055f), BVMULT(64,x13, 0hex00000000000006f9), BVMULT(64,x14, 0hex0000000000000853), BVMULT(64,x15, 0hex000000000000092b), BVMULT(64,x16, 0hex0000000000000cc9), BVMULT(64,x17, 0hex00000000000002a0), BVMULT(64,x18, 0hex0000000000000b3c), BVMULT(64,x19, 0hex0000000000000e83),0hex0000000000000000) = 0hex0000000000000b94); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000acc), BVMULT(64,x1, 0hex000000000000011c), BVMULT(64,x2, 0hex0000000000000b65), BVMULT(64,x3, 0hex0000000000000857), BVMULT(64,x4, 0hex000000000000074a), BVMULT(64,x5, 0hex0000000000000061), BVMULT(64,x6, 0hex0000000000000625), BVMULT(64,x7, 0hex000000000000026b), BVMULT(64,x8, 0hex00000000000008ff), BVMULT(64,x9, 0hex0000000000000269), BVMULT(64,x10, 0hex0000000000000d9b), BVMULT(64,x11, 0hex00000000000001bb), BVMULT(64,x12, 0hex00000000000004c3), BVMULT(64,x13, 0hex0000000000000e33), BVMULT(64,x14, 0hex0000000000000bd5), BVMULT(64,x15, 0hex000000000000096b), BVMULT(64,x16, 0hex00000000000004ea), BVMULT(64,x17, 0hex0000000000000d61), BVMULT(64,x18, 0hex00000000000007dd), BVMULT(64,x19, 0hex00000000000004d0),0hex0000000000000000) = 0hex0000000000000146); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c17), BVMULT(64,x1, 0hex0000000000000aa1), BVMULT(64,x2, 0hex0000000000000a81), BVMULT(64,x3, 0hex0000000000000c53), BVMULT(64,x4, 0hex00000000000004eb), BVMULT(64,x5, 0hex00000000000006ed), BVMULT(64,x6, 0hex00000000000004d8), BVMULT(64,x7, 0hex000000000000003f), BVMULT(64,x8, 0hex0000000000000632), BVMULT(64,x9, 0hex000000000000056c), BVMULT(64,x10, 0hex00000000000003c3), BVMULT(64,x11, 0hex000000000000020e), BVMULT(64,x12, 0hex0000000000000a26), BVMULT(64,x13, 0hex0000000000000690), BVMULT(64,x14, 0hex00000000000001ae), BVMULT(64,x15, 0hex000000000000023e), BVMULT(64,x16, 0hex00000000000008b0), BVMULT(64,x17, 0hex000000000000094c), BVMULT(64,x18, 0hex00000000000003e0), BVMULT(64,x19, 0hex00000000000006d0),0hex0000000000000000) = 0hex00000000000000ce); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000009d7), BVMULT(64,x1, 0hex000000000000095b), BVMULT(64,x2, 0hex0000000000000cb0), BVMULT(64,x3, 0hex0000000000000c43), BVMULT(64,x4, 0hex00000000000003e1), BVMULT(64,x5, 0hex00000000000001e1), BVMULT(64,x6, 0hex0000000000000a6e), BVMULT(64,x7, 0hex00000000000002d7), BVMULT(64,x8, 0hex0000000000000808), BVMULT(64,x9, 0hex000000000000028a), BVMULT(64,x10, 0hex0000000000000806), BVMULT(64,x11, 0hex0000000000000c80), BVMULT(64,x12, 0hex00000000000006a0), BVMULT(64,x13, 0hex0000000000000e8a), BVMULT(64,x14, 0hex0000000000000b6e), BVMULT(64,x15, 0hex0000000000000ee4), BVMULT(64,x16, 0hex00000000000002d3), BVMULT(64,x17, 0hex000000000000092b), BVMULT(64,x18, 0hex00000000000002d7), BVMULT(64,x19, 0hex00000000000006ee),0hex0000000000000000) = 0hex0000000000000abd); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000047), BVMULT(64,x1, 0hex0000000000000371), BVMULT(64,x2, 0hex00000000000002dd), BVMULT(64,x3, 0hex000000000000032e), BVMULT(64,x4, 0hex0000000000000bf7), BVMULT(64,x5, 0hex0000000000000e77), BVMULT(64,x6, 0hex000000000000029c), BVMULT(64,x7, 0hex0000000000000880), BVMULT(64,x8, 0hex0000000000000bab), BVMULT(64,x9, 0hex0000000000000678), BVMULT(64,x10, 0hex000000000000090d), BVMULT(64,x11, 0hex0000000000000bc0), BVMULT(64,x12, 0hex000000000000075e), BVMULT(64,x13, 0hex000000000000095b), BVMULT(64,x14, 0hex00000000000005dd), BVMULT(64,x15, 0hex00000000000001d0), BVMULT(64,x16, 0hex0000000000000c91), BVMULT(64,x17, 0hex00000000000007db), BVMULT(64,x18, 0hex0000000000000778), BVMULT(64,x19, 0hex000000000000040c),0hex0000000000000000) = 0hex00000000000009da); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000009c2), BVMULT(64,x1, 0hex00000000000002c4), BVMULT(64,x2, 0hex000000000000021e), BVMULT(64,x3, 0hex0000000000000139), BVMULT(64,x4, 0hex0000000000000142), BVMULT(64,x5, 0hex0000000000000cf3), BVMULT(64,x6, 0hex0000000000000072), BVMULT(64,x7, 0hex00000000000000a0), BVMULT(64,x8, 0hex000000000000009a), BVMULT(64,x9, 0hex00000000000004b5), BVMULT(64,x10, 0hex00000000000000bb), BVMULT(64,x11, 0hex0000000000000eb3), BVMULT(64,x12, 0hex00000000000005ae), BVMULT(64,x13, 0hex0000000000000d0c), BVMULT(64,x14, 0hex0000000000000976), BVMULT(64,x15, 0hex0000000000000cbc), BVMULT(64,x16, 0hex00000000000008e9), BVMULT(64,x17, 0hex00000000000004e6), BVMULT(64,x18, 0hex0000000000000466), BVMULT(64,x19, 0hex0000000000000c8c),0hex0000000000000000) = 0hex0000000000000417); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000c4c), BVMULT(64,x1, 0hex0000000000000c29), BVMULT(64,x2, 0hex0000000000000f49), BVMULT(64,x3, 0hex000000000000036b), BVMULT(64,x4, 0hex0000000000000570), BVMULT(64,x5, 0hex000000000000017f), BVMULT(64,x6, 0hex0000000000000d91), BVMULT(64,x7, 0hex0000000000000e37), BVMULT(64,x8, 0hex0000000000000197), BVMULT(64,x9, 0hex0000000000000665), BVMULT(64,x10, 0hex0000000000000f1b), BVMULT(64,x11, 0hex00000000000009f3), BVMULT(64,x12, 0hex0000000000000efd), BVMULT(64,x13, 0hex00000000000000d3), BVMULT(64,x14, 0hex0000000000000a9f), BVMULT(64,x15, 0hex00000000000007c2), BVMULT(64,x16, 0hex0000000000000a84), BVMULT(64,x17, 0hex000000000000097a), BVMULT(64,x18, 0hex000000000000014b), BVMULT(64,x19, 0hex00000000000004f8),0hex0000000000000000) = 0hex00000000000009b3); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000004bf), BVMULT(64,x1, 0hex0000000000000e2f), BVMULT(64,x2, 0hex0000000000000add), BVMULT(64,x3, 0hex0000000000000119), BVMULT(64,x4, 0hex0000000000000eb1), BVMULT(64,x5, 0hex00000000000000b2), BVMULT(64,x6, 0hex0000000000000622), BVMULT(64,x7, 0hex0000000000000c0f), BVMULT(64,x8, 0hex0000000000000ed5), BVMULT(64,x9, 0hex0000000000000559), BVMULT(64,x10, 0hex0000000000000722), BVMULT(64,x11, 0hex000000000000011d), BVMULT(64,x12, 0hex000000000000098f), BVMULT(64,x13, 0hex0000000000000a54), BVMULT(64,x14, 0hex000000000000077d), BVMULT(64,x15, 0hex0000000000000132), BVMULT(64,x16, 0hex000000000000017b), BVMULT(64,x17, 0hex00000000000001af), BVMULT(64,x18, 0hex0000000000000505), BVMULT(64,x19, 0hex0000000000000aa1),0hex0000000000000000) = 0hex0000000000000548); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000445), BVMULT(64,x1, 0hex0000000000000f69), BVMULT(64,x2, 0hex0000000000000e0b), BVMULT(64,x3, 0hex000000000000058b), BVMULT(64,x4, 0hex00000000000008fc), BVMULT(64,x5, 0hex0000000000000b15), BVMULT(64,x6, 0hex0000000000000a23), BVMULT(64,x7, 0hex0000000000000aed), BVMULT(64,x8, 0hex0000000000000ec9), BVMULT(64,x9, 0hex0000000000000b28), BVMULT(64,x10, 0hex00000000000005e3), BVMULT(64,x11, 0hex0000000000000104), BVMULT(64,x12, 0hex00000000000007ed), BVMULT(64,x13, 0hex000000000000014c), BVMULT(64,x14, 0hex0000000000000ed0), BVMULT(64,x15, 0hex0000000000000d85), BVMULT(64,x16, 0hex0000000000000c63), BVMULT(64,x17, 0hex0000000000000ae6), BVMULT(64,x18, 0hex0000000000000a43), BVMULT(64,x19, 0hex00000000000004aa),0hex0000000000000000) = 0hex00000000000008fc); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000008de), BVMULT(64,x1, 0hex0000000000000ee5), BVMULT(64,x2, 0hex0000000000000e00), BVMULT(64,x3, 0hex0000000000000aee), BVMULT(64,x4, 0hex0000000000000a5b), BVMULT(64,x5, 0hex0000000000000eee), BVMULT(64,x6, 0hex0000000000000770), BVMULT(64,x7, 0hex00000000000006e5), BVMULT(64,x8, 0hex000000000000014e), BVMULT(64,x9, 0hex0000000000000286), BVMULT(64,x10, 0hex00000000000009a1), BVMULT(64,x11, 0hex0000000000000624), BVMULT(64,x12, 0hex000000000000081d), BVMULT(64,x13, 0hex00000000000000bf), BVMULT(64,x14, 0hex0000000000000428), BVMULT(64,x15, 0hex0000000000000a8a), BVMULT(64,x16, 0hex0000000000000e38), BVMULT(64,x17, 0hex0000000000000a47), BVMULT(64,x18, 0hex00000000000003b4), BVMULT(64,x19, 0hex0000000000000af0),0hex0000000000000000) = 0hex00000000000009ee); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000000e7), BVMULT(64,x1, 0hex0000000000000e3d), BVMULT(64,x2, 0hex000000000000033d), BVMULT(64,x3, 0hex000000000000053a), BVMULT(64,x4, 0hex0000000000000cff), BVMULT(64,x5, 0hex0000000000000322), BVMULT(64,x6, 0hex0000000000000534), BVMULT(64,x7, 0hex00000000000006b3), BVMULT(64,x8, 0hex0000000000000ab4), BVMULT(64,x9, 0hex000000000000058a), BVMULT(64,x10, 0hex0000000000000154), BVMULT(64,x11, 0hex0000000000000b9d), BVMULT(64,x12, 0hex0000000000000d5b), BVMULT(64,x13, 0hex0000000000000a5b), BVMULT(64,x14, 0hex000000000000091b), BVMULT(64,x15, 0hex0000000000000f18), BVMULT(64,x16, 0hex00000000000000a5), BVMULT(64,x17, 0hex0000000000000976), BVMULT(64,x18, 0hex0000000000000b9c), BVMULT(64,x19, 0hex0000000000000585),0hex0000000000000000) = 0hex0000000000000f2a); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex0000000000000ce6), BVMULT(64,x1, 0hex0000000000000c5f), BVMULT(64,x2, 0hex0000000000000b69), BVMULT(64,x3, 0hex0000000000000a54), BVMULT(64,x4, 0hex0000000000000610), BVMULT(64,x5, 0hex00000000000001a4), BVMULT(64,x6, 0hex00000000000006fd), BVMULT(64,x7, 0hex0000000000000e03), BVMULT(64,x8, 0hex0000000000000891), BVMULT(64,x9, 0hex0000000000000766), BVMULT(64,x10, 0hex0000000000000a0c), BVMULT(64,x11, 0hex0000000000000a03), BVMULT(64,x12, 0hex0000000000000e94), BVMULT(64,x13, 0hex0000000000000c12), BVMULT(64,x14, 0hex0000000000000b61), BVMULT(64,x15, 0hex0000000000000302), BVMULT(64,x16, 0hex0000000000000f4d), BVMULT(64,x17, 0hex00000000000005d8), BVMULT(64,x18, 0hex000000000000009f), BVMULT(64,x19, 0hex0000000000000b40),0hex0000000000000000) = 0hex0000000000000623); +ASSERT (BVPLUS(64,BVMULT(64,x0, 0hex00000000000005b8), BVMULT(64,x1, 0hex00000000000004b5), BVMULT(64,x2, 0hex000000000000036b), BVMULT(64,x3, 0hex00000000000002f7), BVMULT(64,x4, 0hex0000000000000f3c), BVMULT(64,x5, 0hex0000000000000388), BVMULT(64,x6, 0hex0000000000000ca4), BVMULT(64,x7, 0hex00000000000009c7), BVMULT(64,x8, 0hex0000000000000d63), BVMULT(64,x9, 0hex000000000000034c), BVMULT(64,x10, 0hex0000000000000b33), BVMULT(64,x11, 0hex0000000000000ddc), BVMULT(64,x12, 0hex000000000000029f), BVMULT(64,x13, 0hex0000000000000513), BVMULT(64,x14, 0hex0000000000000650), BVMULT(64,x15, 0hex00000000000004ef), BVMULT(64,x16, 0hex000000000000084b), BVMULT(64,x17, 0hex0000000000000b65), BVMULT(64,x18, 0hex0000000000000a8b), BVMULT(64,x19, 0hex0000000000000df0),0hex0000000000000000) = 0hex0000000000000ef5); + +QUERY FALSE; diff --git a/tests/c-api-tests/stp-test3.c b/tests/c-api-tests/stp-test3.c new file mode 100644 index 0000000..6b1bc32 --- /dev/null +++ b/tests/c-api-tests/stp-test3.c @@ -0,0 +1,32 @@ +#include +#include "c_interface.h" + + +void go (enum ifaceflag_t f) +{ + VC vc; + + + vc = vc_createValidityChecker (); + vc_setInterfaceFlags(vc, f, 0); + //vc_setFlags(vc,'s',0); + + vc_parseExpr(vc, "f.cvc"); + + Expr a = vc_varExpr(vc, "a", vc_bvType(vc, 8)); + Expr ct_0 = vc_bvConstExprFromInt(vc, 8, 0); + + Expr a_eq_0 = vc_eqExpr(vc, a, ct_0); + + int query = vc_query(vc, a_eq_0); + vc_Destroy (vc); +} + + +int main () +{ + go(SMS); + go(MS); + go(CMS2); + go(MSP); +} -- 2.47.3