| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/SBVTestSuite/TestSuite/Basics/ |
| H A D | Quantifiers.hs | 23 tests = testGroup "Basics.Quantifiers" $ concatMap mkGoal goals ++ concatMap mkPred preds
24 …where mkGoal (g, nm) = [ goldenCapturedIO ("quantified_sat" ++ "_" ++ nm) $ \rf -> void $ satWit… function
|
| /dports/math/z3/z3-z3-4.8.13/src/api/java/ |
| H A D | Goal.java | 239 super(ctx, Native.mkGoal(ctx.nCtx(), (models), in Goal()
|
| H A D | Context.java | 2780 public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs) in mkGoal() method in Context
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/java/ |
| H A D | Goal.java | 239 super(ctx, Native.mkGoal(ctx.nCtx(), (models), in Goal()
|
| H A D | Context.java | 2695 public Goal mkGoal(boolean models, boolean unsatCores, boolean proofs) in mkGoal() method in Context
|
| /dports/math/z3/z3-z3-4.8.13/examples/java/ |
| H A D | JavaExample.java | 323 Goal g4 = ctx.mkGoal(true, false, false); in modelConverterTest()
358 Goal g = ctx.mkGoal(true, false, false); in arrayExample1()
792 Goal g = ctx.mkGoal(true, false, false); in basicTests()
821 Goal g2 = ctx.mkGoal(true, true, false); in basicTests()
826 g2 = ctx.mkGoal(true, true, false); in basicTests()
832 Goal g3 = ctx.mkGoal(true, true, false); in basicTests()
1095 Goal g = ctx.mkGoal(true, false, false); in logicExample()
1118 Goal g = ctx.mkGoal(true, false, false); in parOrExample()
|
| H A D | JavaGenericExample.java | 308 Goal g4 = ctx.mkGoal(true, false, false); in modelConverterTest()
344 Goal g = ctx.mkGoal(true, false, false); in arrayExample1()
744 Goal g = ctx.mkGoal(true, false, false); in basicTests()
772 Goal g2 = ctx.mkGoal(true, true, false); in basicTests()
777 g2 = ctx.mkGoal(true, true, false); in basicTests()
783 Goal g3 = ctx.mkGoal(true, true, false); in basicTests()
887 Goal g = ctx.mkGoal(true, false, false); in logicExample()
910 Goal g = ctx.mkGoal(true, false, false); in parOrExample()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/examples/java/ |
| H A D | JavaExample.java | 323 Goal g4 = ctx.mkGoal(true, false, false); in modelConverterTest()
358 Goal g = ctx.mkGoal(true, false, false); in arrayExample1()
792 Goal g = ctx.mkGoal(true, false, false); in basicTests()
821 Goal g2 = ctx.mkGoal(true, true, false); in basicTests()
826 g2 = ctx.mkGoal(true, true, false); in basicTests()
832 Goal g3 = ctx.mkGoal(true, true, false); in basicTests()
1095 Goal g = ctx.mkGoal(true, false, false); in logicExample()
1118 Goal g = ctx.mkGoal(true, false, false); in parOrExample()
|
| H A D | JavaGenericExample.java | 308 Goal g4 = ctx.mkGoal(true, false, false);
344 Goal g = ctx.mkGoal(true, false, false);
744 Goal g = ctx.mkGoal(true, false, false);
772 Goal g2 = ctx.mkGoal(true, true, false);
777 g2 = ctx.mkGoal(true, true, false);
783 Goal g3 = ctx.mkGoal(true, true, false);
856 Goal g = ctx.mkGoal(true, false, false);
879 Goal g = ctx.mkGoal(true, false, false); in gzlog_open()
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Core/ |
| H A D | Symbolic.hs | 1796 let mkGoal nm orig = liftIO $ do origSV <- svToSV st orig function
1801 … let walk (Minimize nm v) = Minimize nm <$> mkGoal nm v
1802 … walk (Maximize nm v) = Maximize nm <$> mkGoal nm v
1803 … walk (AssertWithPenalty nm v mbP) = flip (AssertWithPenalty nm) mbP <$> mkGoal nm v
|