| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/SBVTestSuite/TestSuite/Arrays/ |
| H A D | Query.hs | 49 _ <- checkSat
61 _ <- checkSat
70 _ <- checkSat
80 _ <- checkSat
84 _ <- checkSat
99 cs <- checkSat
116 cs <- checkSat
132 r1 <- checkSat
137 r2 <- checkSat
146 r1 <- checkSat
[all …]
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/SBVTestSuite/TestSuite/Queries/ |
| H A D | Sums.hs | 55 _ <- checkSat
71 _ <- checkSat
85 _ <- checkSat
101 _ <- checkSat
116 _ <- checkSat
129 _ <- checkSat
143 _ <- checkSat
157 _ <- checkSat
171 _ <- checkSat
|
| H A D | Int_Boolector.hs | 44 cs <- checkSat
53 _ <- checkSat
|
| H A D | Int_Mathsat.hs | 44 cs <- checkSat
53 _ <- checkSat
|
| H A D | Int_Yices.hs | 44 cs <- checkSat
53 _ <- checkSat
|
| H A D | Int_CVC4.hs | 46 cs <- checkSat
58 _ <- checkSat
|
| H A D | Int_Z3.hs | 46 cs <- checkSat
60 _ <- checkSat
|
| H A D | Tuples.hs | 44 _ <- checkSat
59 _ <- checkSat
|
| H A D | Strings.hs | 43 query $ do _ <- checkSat
55 query $ do _ <- checkSat
|
| H A D | BasicQuery.hs | 80 cs <- checkSat
118 _ <- checkSat
|
| H A D | Interpolants.hs | 51 query $ do _ <- checkSat
69 query $ do _ <- checkSat
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/SBVTestSuite/TestSuite/Basics/ |
| H A D | Tuple.hs | 62 query $ do _ <- checkSat
71 query $ do _ <- checkSat
81 query $ do _ <- checkSat
96 query $ do _ <- checkSat
118 _ <- checkSat
143 query $ do cs <- checkSat
|
| H A D | DynSign.hs | 32 checkSat :: ThmResult -> Assertion
33 checkSat r = assert isThm function
42 [ testCase "dynSign" $ checkSat =<< proveWith z3 prop
|
| H A D | Exceptions.hs | 38 query $ do cs <- checkSat
55 query $ do cs <- checkSat
66 show <$> checkSat
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Documentation/SBV/Examples/Queries/ |
| H A D | Concurrency.hs | 59 cs <- checkSat
79 cs <- checkSat
123 cs <- checkSat
151 cs <- checkSat
|
| /dports/math/cvc4/CVC4-1.7/test/system/ |
| H A D | reset_assertions.cpp | 40 std::cout << smt.checkSat() << std::endl; in main()
52 std::cout << smt.checkSat() << std::endl; in main()
|
| H A D | sep_log_api.cpp | 63 Result r(smt.checkSat()); in validate_exception()
183 Result r(smt.checkSat()); in validate_getters()
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/ |
| H A D | Control.hs | 29 …, CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUn…
94 , freshArray, freshArray_, checkSat, ensureSat
|
| /dports/math/cvc4/CVC4-1.7/examples/ |
| H A D | simple_vc_quant_cxx.cpp | 57 cout << "Result from CVC4 is: " << smt.checkSat() << endl; in main()
74 cout << "Result from CVC4 is: " << smtp.checkSat() << endl; in main()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_quick_check.h | 61 prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
69 prop::SatValue checkSat(unsigned long budget);
|
| H A D | bv_quick_check.cpp | 53 prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) { in checkSat() function in CVC4::theory::bv::BVQuickCheck
85 prop::SatValue BVQuickCheck::checkSat(unsigned long budget) { in checkSat() function in CVC4::theory::bv::BVQuickCheck
230 SatValue res = d_solver->checkSat(d_budget); in minimizeConflictInternal()
260 res = d_solver->checkSat(d_budget); in minimizeConflictInternal()
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Control/ |
| H A D | BaseIO.hs | 464 checkSat :: Query CheckSatResult
465 checkSat = Trans.checkSat function
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Documentation/SBV/Examples/Puzzles/ |
| H A D | HexPuzzle.hs | 98 cs <- checkSat
117 cs <- checkSat
|
| /dports/math/cvc3/cvc3-2.4.1/doc/ |
| H A D | theory_api_flow.fig | 137 4 0 0 50 0 0 14 0.0000 4 195 960 8025 1050 checkSat()\001
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_simulate.h | 59 void checkSat(bool fullEffort) { } in checkSat() function
|