From 3fabfdb1e6817f2c668cca4d9570ed51988bf2e8 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 24 Jan 2012 04:26:37 +0000 Subject: [PATCH] Improvement. Add the ability to set a soft timeout via the c_interface. You specify the number of milliseconds that you want STP to run for. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1520 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 41 +++-- src/STPManager/STPManager.h | 7 +- .../CounterExample.cpp | 3 + src/c_interface/c_interface.cpp | 28 ++- src/c_interface/c_interface.h | 9 +- src/main/Globals.h | 3 +- src/sat/MinisatCore.cpp | 4 +- src/sat/MinisatCore.h | 2 +- src/sat/MinisatCore_prop.cpp | 4 +- src/sat/MinisatCore_prop.h | 2 +- src/sat/SimplifyingMinisat.cpp | 4 +- src/sat/SimplifyingMinisat.h | 2 +- src/sat/core/Solver.cc | 4 +- src/sat/core/Solver.h | 4 +- src/sat/core_prop/Solver_prop.cc | 4 +- src/sat/core_prop/Solver_prop.h | 4 +- src/sat/simp/SimpSolver.cc | 3 +- src/sat/simp/SimpSolver.h | 2 +- tests/c-api-tests/Makefile | 4 + tests/c-api-tests/example.smt | 166 ++++++++++++++++++ tests/c-api-tests/timeout.c | 24 +++ 21 files changed, 286 insertions(+), 38 deletions(-) create mode 100644 tests/c-api-tests/example.smt create mode 100644 tests/c-api-tests/timeout.c diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 47d29ec..088e4ea 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -54,13 +54,13 @@ namespace BEEV { SATSolver *newS; if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER) - newS = new SimplifyingMinisat(); + newS = new SimplifyingMinisat(bm->soft_timeout_expired); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::CRYPTOMINISAT_SOLVER) newS = new CryptoMinisat(); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER) - newS = new MinisatCore(); + newS = new MinisatCore(bm->soft_timeout_expired); else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) - newS = new MinisatCore_prop(); + newS = new MinisatCore_prop(bm->soft_timeout_expired); @@ -208,8 +208,8 @@ namespace BEEV { cerr << "Difficulty Initially:" << difficulty.score(original_input) << endl; // A heap object so I can easily control its lifetime. - BVSolver* bvSolver = new BVSolver(bm, simp); - PropagateEqualities * pe = new PropagateEqualities(simp,bm->defaultNodeFactory,bm); + std::auto_ptr bvSolver(new BVSolver(bm, simp)); + std::auto_ptr pe (new PropagateEqualities(simp,bm->defaultNodeFactory,bm)); ASTNode simplified_solved_InputToSAT = original_input; @@ -234,7 +234,7 @@ namespace BEEV { assert(!arrayops); // Run size reducing just once. - simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe); + simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get()); unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); @@ -242,7 +242,7 @@ namespace BEEV { // Currently we discards all the state each time sizeReducing is called, // so it's expensive to call. if ((!arrayops && initial_difficulty_score < 1000000) || bm->UserFlags.isSet("preserving-fixedpoint", "0")) - simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score); + simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get(), initial_difficulty_score); if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1"))) { @@ -253,7 +253,7 @@ namespace BEEV { cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl; // So we can delete the object and release all the hash-buckets storage. - Revert_to* revert = new Revert_to(); + auto_ptr revert(new Revert_to()); if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1"))) { @@ -275,6 +275,9 @@ namespace BEEV { { inputToSAT = simplified_solved_InputToSAT; + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; + if (bm->UserFlags.optimize_flag) { simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer); @@ -343,6 +346,9 @@ namespace BEEV { } } + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; + // Simplify using Ite context if (bm->UserFlags.optimize_flag && bm->UserFlags.isSet("ite-context", "0")) { @@ -459,7 +465,7 @@ namespace BEEV { // it to put back in all the bad simplifications. bm->UserFlags.optimize_flag = false; } - delete revert; + revert.reset(NULL); simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT); bm->ASTNodeStats("after transformation: ", simplified_solved_InputToSAT); @@ -480,10 +486,9 @@ namespace BEEV { bm->ClearAllTables(); // Deleting it clears out all the buckets associated with hashmaps etc. too. - delete bvSolver; - bvSolver = NULL; - delete pe; - pe = NULL; + bvSolver.reset(NULL); + pe.reset(NULL); + if (bm->UserFlags.stats_flag) simp->printCacheStatus(); @@ -512,10 +517,20 @@ namespace BEEV { ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ; + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; + // If it doesn't contain array operations, use ABC's CNF generation. res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, original_input, satBase, maybeRefinement); + if (bm->soft_timeout_expired) + { + if (toSATAIG.cbIsDestructed()) + cleaner.release(); + + return SOLVER_TIMEOUT; + } if (SOLVER_UNDECIDED != res) { // If the aig converter knows that it is never going to be called again, diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 03576ce..a329728 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -76,13 +76,15 @@ namespace BEEV uint8_t last_iteration; - public: + public: HashingNodeFactory* hashingNodeFactory; NodeFactory *defaultNodeFactory; //frequently used nodes ASTNode ASTFalse, ASTTrue, ASTUndefined; + volatile bool soft_timeout_expired; + // No nodes should already have the iteration number that is returned from here. // This never returns zero. uint8_t getNextIteration() @@ -215,7 +217,8 @@ namespace BEEV UserFlags(), _symbol_count(0), CNFFileNameCounter(0), - last_iteration(0) + last_iteration(0), + soft_timeout_expired(false) { _max_node_num = 0; diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index f3a21da..9f59e0f 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -919,6 +919,9 @@ namespace BEEV bool sat = tosat->CallSAT(SatSolver, modified_input, refinement); + if (bm->soft_timeout_expired) + return SOLVER_TIMEOUT; + if (!sat) { //PrintOutput(true); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 0d282d8..aaba6b2 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -410,6 +410,10 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) { b->AddAssert(*a, absrefine_bucket_num); } +void soft_time_out(int ignored) +{ + BEEV::ParserBM->soft_timeout_expired = true; +} //! Check validity of e in the current context. e must be a FORMULA // @@ -424,11 +428,23 @@ void vc_assertFormula(VC vc, Expr e, int absrefine_bucket_num) { * the starting context. If the result is false, then the resulting * context is a context in which e is false. e must have Boolean * type. */ -int vc_query(VC vc, Expr e) { +int vc_query(VC vc, Expr e, int timeout_ms) { nodestar a = (nodestar)e; stpstar stp = ((stpstar)vc); bmstar b = (bmstar)(stp->bm); + assert(!BEEV::ParserBM->soft_timeout_expired); + if (timeout_ms != -1) + { + itimerval timeout; + signal(SIGVTALRM, soft_time_out); + timeout.it_interval.tv_usec = 0; + timeout.it_interval.tv_sec = 0; + timeout.it_value.tv_usec = 1000 * (timeout_ms % 1000); + timeout.it_value.tv_sec = timeout_ms / 1000; + setitimer(ITIMER_VIRTUAL, &timeout, NULL); + } + if(!BEEV::is_Form_kind(a->GetKind())) { BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a); @@ -456,6 +472,14 @@ int vc_query(VC vc, Expr e) { { output = stp->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a); } + + if (timeout_ms !=-1) + { + // Reset the timer. + setitimer(ITIMER_VIRTUAL, NULL, NULL); + BEEV::ParserBM->soft_timeout_expired = false; + } + return output; } //end of vc_query @@ -1567,7 +1591,7 @@ Expr vc_parseExpr(VC vc, const char* infile) { BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0]; BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1]; - //BEEV::GlobalSTP->TopLevelSTP(asserts, query); + node oo = b->CreateNode(BEEV::NOT,query); node o = b->CreateNode(BEEV::AND,asserts,oo); diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index b4f57b3..5b64ef5 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -210,7 +210,14 @@ extern "C" { //if returned 1 then input is VALID // //if returned 2 then ERROR - int vc_query(VC vc, Expr e); + + // NB. The timeout is a soft timeout, use the -g flag for a hard timeout that + // will abort automatically. The soft timeout is checked sometimes in the code, + // and if the time has passed, then "timeout" will be returned. It's only checked + // sometimes though, so the actual timeout may be larger. Cryptominisat doesn't check + // the timeout yet.. + int vc_query(VC vc, Expr e, int timeout_ms= -1); + //! Return the counterexample after a failed query. Expr vc_getCounterExample(VC vc, Expr e); diff --git a/src/main/Globals.h b/src/main/Globals.h index efc3143..b79628a 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -58,7 +58,8 @@ namespace BEEV { SOLVER_INVALID=0, SOLVER_VALID=1, - SOLVER_UNDECIDED=2, + SOLVER_UNDECIDED=2, + SOLVER_TIMEOUT=3, SOLVER_ERROR=-100, SOLVER_UNSATISFIABLE = 1, SOLVER_SATISFIABLE = 0 diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp index c655fa2..581bf2f 100644 --- a/src/sat/MinisatCore.cpp +++ b/src/sat/MinisatCore.cpp @@ -7,9 +7,9 @@ namespace BEEV { template - MinisatCore::MinisatCore() + MinisatCore::MinisatCore(volatile bool& interrupt) { - s = new T(); + s = new T(interrupt); }; template diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h index 0f4d02e..6259305 100644 --- a/src/sat/MinisatCore.h +++ b/src/sat/MinisatCore.h @@ -19,7 +19,7 @@ namespace BEEV T * s; public: - MinisatCore(); + MinisatCore(volatile bool& interrupt); ~MinisatCore(); diff --git a/src/sat/MinisatCore_prop.cpp b/src/sat/MinisatCore_prop.cpp index 4dacfb7..6eec650 100644 --- a/src/sat/MinisatCore_prop.cpp +++ b/src/sat/MinisatCore_prop.cpp @@ -6,9 +6,9 @@ namespace BEEV { template - MinisatCore_prop::MinisatCore_prop() + MinisatCore_prop::MinisatCore_prop(volatile bool& timeout) { - s = new T(); + s = new T(timeout); }; template diff --git a/src/sat/MinisatCore_prop.h b/src/sat/MinisatCore_prop.h index 5dc3688..c9e2d2b 100644 --- a/src/sat/MinisatCore_prop.h +++ b/src/sat/MinisatCore_prop.h @@ -19,7 +19,7 @@ namespace BEEV T * s; public: - MinisatCore_prop(); + MinisatCore_prop(volatile bool& timeout); ~MinisatCore_prop(); diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp index 3794445..ac9e31d 100644 --- a/src/sat/SimplifyingMinisat.cpp +++ b/src/sat/SimplifyingMinisat.cpp @@ -4,9 +4,9 @@ namespace BEEV { - SimplifyingMinisat::SimplifyingMinisat() + SimplifyingMinisat::SimplifyingMinisat(volatile bool& timeout) { - s = new Minisat::SimpSolver(); + s = new Minisat::SimpSolver(timeout); } SimplifyingMinisat::~SimplifyingMinisat() diff --git a/src/sat/SimplifyingMinisat.h b/src/sat/SimplifyingMinisat.h index 7c746e5..7311432 100644 --- a/src/sat/SimplifyingMinisat.h +++ b/src/sat/SimplifyingMinisat.h @@ -19,7 +19,7 @@ namespace BEEV public: - SimplifyingMinisat(); + SimplifyingMinisat(volatile bool& timeout); ~SimplifyingMinisat(); bool diff --git a/src/sat/core/Solver.cc b/src/sat/core/Solver.cc index 63d7969..6c8ad78 100644 --- a/src/sat/core/Solver.cc +++ b/src/sat/core/Solver.cc @@ -48,7 +48,7 @@ static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction o // Constructor/Destructor: -Solver::Solver() : +Solver::Solver(volatile bool& interrupt) : // Parameters (user settable): // @@ -95,7 +95,7 @@ Solver::Solver() : // , conflict_budget (-1) , propagation_budget (-1) - , asynch_interrupt (false) + , asynch_interrupt (interrupt) {} diff --git a/src/sat/core/Solver.h b/src/sat/core/Solver.h index 8e5445c..af16887 100644 --- a/src/sat/core/Solver.h +++ b/src/sat/core/Solver.h @@ -38,7 +38,7 @@ public: // Constructor/Destructor: // - Solver(); + Solver(volatile bool& interrupt); virtual ~Solver(); // Problem specification: @@ -208,7 +208,7 @@ protected: // int64_t conflict_budget; // -1 means no budget. int64_t propagation_budget; // -1 means no budget. - bool asynch_interrupt; + volatile bool& asynch_interrupt; // Main internal methods: // diff --git a/src/sat/core_prop/Solver_prop.cc b/src/sat/core_prop/Solver_prop.cc index bd10986..6a89472 100644 --- a/src/sat/core_prop/Solver_prop.cc +++ b/src/sat/core_prop/Solver_prop.cc @@ -56,7 +56,7 @@ static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction o //================================================================================================= // Constructor/Destructor: -Solver_prop::Solver_prop() : +Solver_prop::Solver_prop(volatile bool& timeout) : // Parameters (user settable): // @@ -111,7 +111,7 @@ Solver_prop::Solver_prop() : // , conflict_budget (-1) , propagation_budget (-1) - , asynch_interrupt (false) + , asynch_interrupt (timeout) {} diff --git a/src/sat/core_prop/Solver_prop.h b/src/sat/core_prop/Solver_prop.h index a465932..5fab638 100644 --- a/src/sat/core_prop/Solver_prop.h +++ b/src/sat/core_prop/Solver_prop.h @@ -313,7 +313,7 @@ private: public: // Constructor/Destructor: // - Solver_prop(); + Solver_prop(volatile bool& timeout); virtual ~Solver_prop(); // Problem specification: @@ -484,7 +484,7 @@ protected: // int64_t conflict_budget; // -1 means no budget. int64_t propagation_budget; // -1 means no budget. - bool asynch_interrupt; + volatile bool& asynch_interrupt; // Main internal methods: // diff --git a/src/sat/simp/SimpSolver.cc b/src/sat/simp/SimpSolver.cc index f77897f..b91a8f1 100644 --- a/src/sat/simp/SimpSolver.cc +++ b/src/sat/simp/SimpSolver.cc @@ -43,7 +43,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of // Constructor/Destructor: -SimpSolver::SimpSolver() : +SimpSolver::SimpSolver(volatile bool& interrupt) : + Solver(interrupt), grow (opt_grow) , clause_lim (opt_clause_lim) , subsumption_lim (opt_subsumption_lim) diff --git a/src/sat/simp/SimpSolver.h b/src/sat/simp/SimpSolver.h index f820fa5..f5beffa 100644 --- a/src/sat/simp/SimpSolver.h +++ b/src/sat/simp/SimpSolver.h @@ -34,7 +34,7 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(); + SimpSolver(volatile bool& interrupt); ~SimpSolver(); // Problem specification: diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 11df111..0c4e097 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -123,5 +123,9 @@ 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 2 g++ $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS) $(VALGRIND) ./a28.out +29: + g++ $(CXXFLAGS) timeout.c -o a29.out $(LIBS) + ./a29.out + clean: rm -rf *~ *.out *.dSYM diff --git a/tests/c-api-tests/example.smt b/tests/c-api-tests/example.smt new file mode 100644 index 0000000..3eb72d2 --- /dev/null +++ b/tests/c-api-tests/example.smt @@ -0,0 +1,166 @@ +(benchmark icbrtorinvalidvc.smt +:source { +Integer cube root algorithm icbrt(x), where x is an unsigned 32 bit integer. +From the book "Hacker's delight" by Henry S. Warren, Jr., page 212 +We use "or" instead of "add" to increment values inside the loop. + +We try to show the invalid verification condition: +y^3 == x or (y^3 < x and (y+1)^3 > x) holds, where y is the result. + +Contributed by Robert Brummayer (robert.brummayer@gmail.com) +} +:status sat +:category { crafted } +:logic QF_BV +:extrafuns ((x BitVec[32])) +:formula +(let (?e2 bv30[5]) +(let (?e3 bv0[32]) +(let (?e4 bv1[32]) +(let (?e5 bv2[32]) +(let (?e6 bv3[32]) +(let (?e7 bv3[5]) +(let (?e8 (bvmul ?e3 ?e5)) +(let (?e9 (bvor ?e8 ?e4)) +(let (?e10 (bvmul ?e8 ?e6)) +(let (?e11 (bvmul ?e10 ?e9)) +(let (?e12 (bvor ?e11 ?e4)) +(let (?e13 (bvshl ?e12 (zero_extend[27] ?e2))) +(let (?e14 (bvsub ?e2 ?e7)) +(let (?e15 (ite (bvuge x ?e13) bv1[1] bv0[1])) +(let (?e16 (bvsub x ?e13)) +(let (?e17 (ite (= bv1[1] ?e15) ?e16 x)) +(let (?e18 (bvor ?e8 ?e4)) +(let (?e19 (ite (= bv1[1] ?e15) ?e18 ?e8)) +(let (?e20 (bvmul ?e19 ?e5)) +(let (?e21 (bvor ?e20 ?e4)) +(let (?e22 (bvmul ?e20 ?e6)) +(let (?e23 (bvmul ?e22 ?e21)) +(let (?e24 (bvor ?e23 ?e4)) +(let (?e25 (bvshl ?e24 (zero_extend[27] ?e14))) +(let (?e26 (bvsub ?e14 ?e7)) +(let (?e27 (ite (bvuge ?e17 ?e25) bv1[1] bv0[1])) +(let (?e28 (bvsub ?e17 ?e25)) +(let (?e29 (ite (= bv1[1] ?e27) ?e28 ?e17)) +(let (?e30 (bvor ?e20 ?e4)) +(let (?e31 (ite (= bv1[1] ?e27) ?e30 ?e20)) +(let (?e32 (bvmul ?e31 ?e5)) +(let (?e33 (bvor ?e32 ?e4)) +(let (?e34 (bvmul ?e32 ?e6)) +(let (?e35 (bvmul ?e34 ?e33)) +(let (?e36 (bvor ?e35 ?e4)) +(let (?e37 (bvshl ?e36 (zero_extend[27] ?e26))) +(let (?e38 (bvsub ?e26 ?e7)) +(let (?e39 (ite (bvuge ?e29 ?e37) bv1[1] bv0[1])) +(let (?e40 (bvsub ?e29 ?e37)) +(let (?e41 (ite (= bv1[1] ?e39) ?e40 ?e29)) +(let (?e42 (bvor ?e32 ?e4)) +(let (?e43 (ite (= bv1[1] ?e39) ?e42 ?e32)) +(let (?e44 (bvmul ?e43 ?e5)) +(let (?e45 (bvor ?e44 ?e4)) +(let (?e46 (bvmul ?e44 ?e6)) +(let (?e47 (bvmul ?e46 ?e45)) +(let (?e48 (bvor ?e47 ?e4)) +(let (?e49 (bvshl ?e48 (zero_extend[27] ?e38))) +(let (?e50 (bvsub ?e38 ?e7)) +(let (?e51 (ite (bvuge ?e41 ?e49) bv1[1] bv0[1])) +(let (?e52 (bvsub ?e41 ?e49)) +(let (?e53 (ite (= bv1[1] ?e51) ?e52 ?e41)) +(let (?e54 (bvor ?e44 ?e4)) +(let (?e55 (ite (= bv1[1] ?e51) ?e54 ?e44)) +(let (?e56 (bvmul ?e55 ?e5)) +(let (?e57 (bvor ?e56 ?e4)) +(let (?e58 (bvmul ?e56 ?e6)) +(let (?e59 (bvmul ?e58 ?e57)) +(let (?e60 (bvor ?e59 ?e4)) +(let (?e61 (bvshl ?e60 (zero_extend[27] ?e50))) +(let (?e62 (bvsub ?e50 ?e7)) +(let (?e63 (ite (bvuge ?e53 ?e61) bv1[1] bv0[1])) +(let (?e64 (bvsub ?e53 ?e61)) +(let (?e65 (ite (= bv1[1] ?e63) ?e64 ?e53)) +(let (?e66 (bvor ?e56 ?e4)) +(let (?e67 (ite (= bv1[1] ?e63) ?e66 ?e56)) +(let (?e68 (bvmul ?e67 ?e5)) +(let (?e69 (bvor ?e68 ?e4)) +(let (?e70 (bvmul ?e68 ?e6)) +(let (?e71 (bvmul ?e70 ?e69)) +(let (?e72 (bvor ?e71 ?e4)) +(let (?e73 (bvshl ?e72 (zero_extend[27] ?e62))) +(let (?e74 (bvsub ?e62 ?e7)) +(let (?e75 (ite (bvuge ?e65 ?e73) bv1[1] bv0[1])) +(let (?e76 (bvsub ?e65 ?e73)) +(let (?e77 (ite (= bv1[1] ?e75) ?e76 ?e65)) +(let (?e78 (bvor ?e68 ?e4)) +(let (?e79 (ite (= bv1[1] ?e75) ?e78 ?e68)) +(let (?e80 (bvmul ?e79 ?e5)) +(let (?e81 (bvor ?e80 ?e4)) +(let (?e82 (bvmul ?e80 ?e6)) +(let (?e83 (bvmul ?e82 ?e81)) +(let (?e84 (bvor ?e83 ?e4)) +(let (?e85 (bvshl ?e84 (zero_extend[27] ?e74))) +(let (?e86 (bvsub ?e74 ?e7)) +(let (?e87 (ite (bvuge ?e77 ?e85) bv1[1] bv0[1])) +(let (?e88 (bvsub ?e77 ?e85)) +(let (?e89 (ite (= bv1[1] ?e87) ?e88 ?e77)) +(let (?e90 (bvor ?e80 ?e4)) +(let (?e91 (ite (= bv1[1] ?e87) ?e90 ?e80)) +(let (?e92 (bvmul ?e91 ?e5)) +(let (?e93 (bvor ?e92 ?e4)) +(let (?e94 (bvmul ?e92 ?e6)) +(let (?e95 (bvmul ?e94 ?e93)) +(let (?e96 (bvor ?e95 ?e4)) +(let (?e97 (bvshl ?e96 (zero_extend[27] ?e86))) +(let (?e98 (bvsub ?e86 ?e7)) +(let (?e99 (ite (bvuge ?e89 ?e97) bv1[1] bv0[1])) +(let (?e100 (bvsub ?e89 ?e97)) +(let (?e101 (ite (= bv1[1] ?e99) ?e100 ?e89)) +(let (?e102 (bvor ?e92 ?e4)) +(let (?e103 (ite (= bv1[1] ?e99) ?e102 ?e92)) +(let (?e104 (bvmul ?e103 ?e5)) +(let (?e105 (bvor ?e104 ?e4)) +(let (?e106 (bvmul ?e104 ?e6)) +(let (?e107 (bvmul ?e106 ?e105)) +(let (?e108 (bvor ?e107 ?e4)) +(let (?e109 (bvshl ?e108 (zero_extend[27] ?e98))) +(let (?e110 (bvsub ?e98 ?e7)) +(let (?e111 (ite (bvuge ?e101 ?e109) bv1[1] bv0[1])) +(let (?e112 (bvsub ?e101 ?e109)) +(let (?e113 (ite (= bv1[1] ?e111) ?e112 ?e101)) +(let (?e114 (bvor ?e104 ?e4)) +(let (?e115 (ite (= bv1[1] ?e111) ?e114 ?e104)) +(let (?e116 (bvmul ?e115 ?e5)) +(let (?e117 (bvor ?e116 ?e4)) +(let (?e118 (bvmul ?e116 ?e6)) +(let (?e119 (bvmul ?e118 ?e117)) +(let (?e120 (bvor ?e119 ?e4)) +(let (?e121 (bvshl ?e120 (zero_extend[27] ?e110))) +(let (?e122 (bvsub ?e110 ?e7)) +(let (?e123 (ite (bvuge ?e113 ?e121) bv1[1] bv0[1])) +(let (?e124 (bvsub ?e113 ?e121)) +(let (?e125 (ite (= bv1[1] ?e123) ?e124 ?e113)) +(let (?e126 (bvor ?e116 ?e4)) +(let (?e127 (ite (= bv1[1] ?e123) ?e126 ?e116)) +(let (?e128 (bvmul ?e127 ?e5)) +(let (?e129 (bvor ?e128 ?e4)) +(let (?e130 (bvmul ?e128 ?e6)) +(let (?e131 (bvmul ?e130 ?e129)) +(let (?e132 (bvor ?e131 ?e4)) +(let (?e133 (bvshl ?e132 (zero_extend[27] ?e122))) +(let (?e134 (bvsub ?e122 ?e7)) +(let (?e135 (ite (bvuge ?e125 ?e133) bv1[1] bv0[1])) +(let (?e136 (bvsub ?e125 ?e133)) +(let (?e137 (ite (= bv1[1] ?e135) ?e136 ?e125)) +(let (?e138 (bvor ?e128 ?e4)) +(let (?e139 (ite (= bv1[1] ?e135) ?e138 ?e128)) +(let (?e140 (bvmul ?e139 ?e139)) +(let (?e141 (bvmul ?e140 ?e139)) +(let (?e142 (ite (= x ?e141) bv1[1] bv0[1])) +(let (?e143 (bvadd ?e139 bv1[32])) +(let (?e144 (bvmul ?e143 ?e143)) +(let (?e145 (bvmul ?e144 ?e143)) +(let (?e146 (ite (bvult ?e141 x) bv1[1] bv0[1])) +(let (?e147 (ite (bvugt ?e145 x) bv1[1] bv0[1])) +(let (?e148 (bvand ?e146 ?e147)) +(let (?e149 (bvor ?e142 ?e148)) +(not (= (bvnot ?e149) bv0[1])) +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/tests/c-api-tests/timeout.c b/tests/c-api-tests/timeout.c new file mode 100644 index 0000000..54a73c1 --- /dev/null +++ b/tests/c-api-tests/timeout.c @@ -0,0 +1,24 @@ +//g++ -I$(HOME)/stp/c_interface print.c -L$(HOME)/stp/lib -lstp -o hex + +#include +#include "c_interface.h" +#include +#include + +int main() { + VC vc = vc_createValidityChecker(); + vc_setFlags(vc,'m'); + + srand(time(NULL)); + Expr c = vc_parseExpr(vc,"./example.smt"); + + for (int i=0; i < 10; i++) + { + int time = rand() % 7000; + std::cout << "Timeout : " << time << " : result " ; + std::cout << vc_query(vc,vc_falseExpr(vc),time) << std::endl; + } + vc_DeleteExpr(c); + vc_Destroy(vc); +} + -- 2.47.3