| /dports/cad/yosys/yosys-yosys-0.12/libs/ezsat/ |
| H A D | demo_bit.cc | 23 void print_results(bool satisfiable, const std::vector<bool> &modelValues) in print_results() argument
25 if (!satisfiable) { in print_results()
49 bool satisfiable; in main() local
58 satisfiable = sat.solve(modelVars, modelValues, pos_active); in main()
59 print_results(satisfiable, modelValues); in main()
62 satisfiable = sat.solve(modelVars, modelValues, neg_active); in main()
63 print_results(satisfiable, modelValues); in main()
66 satisfiable = sat.solve(modelVars, modelValues, impossible); in main()
67 print_results(satisfiable, modelValues); in main()
|
| /dports/math/ogdf/OGDF/test/src/basic/ |
| H A D | minisat.cpp | 57 bool satisfiable = F.solve(model); in satisfiableTest() local
59 AssertThat(satisfiable, IsTrue()); in satisfiableTest()
80 bool satisfiable = F.solve(model); in nonsatisfiableTest() local
82 AssertThat(satisfiable, IsFalse()); in nonsatisfiableTest()
91 bool satisfiable = formula.solve(model); in readDIMACSTest() local
92 AssertThat(satisfiable, IsTrue()); in readDIMACSTest()
95 satisfiable = formula.solve(model); in readDIMACSTest()
96 AssertThat(satisfiable, IsFalse()); in readDIMACSTest()
|
| /dports/math/py-Pyomo/Pyomo-6.1.2/pyomo/contrib/satsolver/ |
| H A D | test_satsolver.py | 35 self.assertTrue(satisfiable(m))
43 self.assertFalse(satisfiable(m))
50 self.assertTrue(satisfiable(m))
57 self.assertFalse(satisfiable(m))
64 self.assertFalse(satisfiable(m))
73 self.assertTrue(satisfiable(m))
98 self.assertTrue(satisfiable(m))
105 self.assertFalse(satisfiable(m))
115 self.assertTrue(satisfiable(m))
129 self.assertTrue(satisfiable(m))
[all …]
|
| /dports/math/py-claripy/claripy-9.0.5405/tests/ |
| H A D | test_solver.py | 256 assert s.satisfiable()
394 assert s.satisfiable()
470 assert s.satisfiable()
472 assert not s.satisfiable()
533 assert not s.satisfiable()
554 assert s.satisfiable()
556 assert s.satisfiable()
559 assert s.satisfiable()
591 assert s.satisfiable()
597 assert s.satisfiable()
[all …]
|
| H A D | common_backend_smt_solver.py | 31 self.assertTrue(solver.satisfiable())
47 self.assertTrue(solver.satisfiable())
56 self.assertTrue(solver.satisfiable())
68 self.assertTrue(solver.satisfiable())
80 self.assertTrue(solver.satisfiable())
97 self.assertTrue(solver.satisfiable())
110 self.assertTrue(solver.satisfiable())
121 self.assertTrue(solver.satisfiable())
132 self.assertTrue(solver.satisfiable())
147 self.assertTrue(solver.satisfiable())
[all …]
|
| H A D | test_replacements.py | 22 assert sr.satisfiable()
26 assert not sr.satisfiable()
44 assert s1a.satisfiable()
45 assert not s1b.satisfiable()
61 assert s1a.satisfiable()
62 assert not s1b.satisfiable()
|
| H A D | test_regressions.py | 9 assert s.satisfiable()
13 assert not s.satisfiable(extra_constraints=[claripy.BVS('lol', 32)==0])
14 assert not s.satisfiable()
|
| H A D | test_merging.py | 89 nose.tools.assert_true(smm_1.satisfiable())
93 nose.tools.assert_true(smm_1.satisfiable())
97 nose.tools.assert_true(smm_1.satisfiable())
101 nose.tools.assert_true(smm_1.satisfiable())
108 nose.tools.assert_false(smm_1.satisfiable())
|
| /dports/math/py-sympy/sympy-1.9/doc/src/modules/ |
| H A D | logic.rst | 116 The function satisfiable will test that a given Boolean expression is satisfiable,
119 For example, the expression ``x & ~x`` is not satisfiable, since there are no
121 | y) & (x | ~y) & (~x | y)`` is satisfiable with both ``x`` and ``y`` being
124 >>> from sympy.logic.inference import satisfiable
128 >>> satisfiable(x & ~x)
130 >>> satisfiable((x | y) & (x | ~y) & (~x | y))
133 As you see, when a sentence is satisfiable, it returns a model that makes that
134 sentence ``True``. If it is not satisfiable it will return ``False``.
136 .. autofunction:: sympy.logic.inference::satisfiable
|
| /dports/math/py-Diofant/Diofant-0.13.0/docs/modules/ |
| H A D | logic.rst | 101 The function satisfiable will test that a given Boolean expression is satisfiable,
104 For example, the expression ``x & ~x`` is not satisfiable, since there are no
106 | y) & (x | ~y) & (~x | y)`` is satisfiable with both ``x`` and ``y`` being
109 >>> satisfiable(x & ~x)
111 >>> satisfiable((x | y) & (x | ~y) & (~x | y))
114 As you see, when a sentence is satisfiable, it returns a model that makes that
115 sentence ``True``. If it is not satisfiable it will return ``False``.
117 .. autofunction:: diofant.logic.inference.satisfiable
|
| /dports/math/py-Diofant/Diofant-0.13.0/diofant/tests/logic/ |
| H A D | test_inference.py | 8 satisfiable, true)
135 assert satisfiable(A & (A >> B) & ~B) is False
136 assert next(satisfiable(A & ~A, all_models=True)) is False
245 assert satisfiable(true) == {true: true}
246 assert satisfiable(false) is False
250 assert next(satisfiable(False, all_models=True)) is False
252 assert list(satisfiable(True, all_models=True)) == [{true: true}]
255 result = satisfiable(A ^ B, all_models=True)
261 assert list(satisfiable(Equivalent(A, B), all_models=True)) == \
265 for model in satisfiable(A >> B, all_models=True):
[all …]
|
| /dports/math/py-sympy/sympy-1.9/sympy/logic/tests/ |
| H A D | test_inference.py | 6 pl_true, satisfiable, valid, entails, PropKB
171 assert satisfiable(A & (A >> B) & ~B) is False
278 assert satisfiable(true) == {true: true}
279 assert satisfiable(S.true) == {true: true}
280 assert satisfiable(false) is False
281 assert satisfiable(S.false) is False
286 assert next(satisfiable(False, all_models=True)) is False
291 result = satisfiable(A ^ B, all_models=True)
297 assert list(satisfiable(Equivalent(A, B), all_models=True)) == \
301 for model in satisfiable(A >> B, all_models=True):
[all …]
|
| /dports/math/py-claripy/claripy-9.0.5405/claripy/frontends/ |
| H A D | full_frontend.py | 98 def satisfiable(self, extra_constraints=(), exact=None): member in FullFrontend
100 return self._solver_backend.satisfiable(
108 if not self.satisfiable(extra_constraints=extra_constraints):
120 if not self.satisfiable(extra_constraints=extra_constraints):
135 if not self.satisfiable(extra_constraints=extra_constraints):
155 if not self.satisfiable(extra_constraints=extra_constraints):
206 if self.satisfiable(extra_constraints=extra_constraints):
|
| /dports/math/py-sympy/sympy-1.9/sympy/logic/algorithms/ |
| H A D | pycosat_wrapper.py | 31 satisfiable = False
36 satisfiable = True
38 if not satisfiable:
|
| H A D | minisat22_wrapper.py | 32 satisfiable = False
40 satisfiable = True
41 if not satisfiable:
|
| /dports/math/py-Diofant/Diofant-0.13.0/diofant/logic/ |
| H A D | inference.py | 34 def satisfiable(expr, algorithm='dpll2', all_models=False): function
104 return not satisfiable(Not(expr))
170 if not satisfiable(result):
199 return not satisfiable(And(*formula_set))
|
| /dports/math/py-sympy/sympy-1.9/sympy/logic/ |
| H A D | inference.py | 38 def satisfiable(expr, algorithm=None, all_models=False, minimal=False): function
132 return not satisfiable(Not(expr))
203 if not satisfiable(result):
238 return not satisfiable(And(*formula_set))
|
| /dports/security/py-angr/angr-9.0.5405/tests/ |
| H A D | test_symbolic.py | 86 nose.tools.assert_true(s.satisfiable())
97 nose.tools.assert_true(sa.satisfiable())
106 nose.tools.assert_true(sv.satisfiable())
115 nose.tools.assert_true(sv.satisfiable())
139 nose.tools.assert_false(s.satisfiable())
|
| H A D | test_state.py | 152 assert m.satisfiable(extra_constraints=(m.memory.load(0x400000, 4) == 8,))
153 assert m.satisfiable(extra_constraints=(m.memory.load(0x400000, 4) == 9,))
154 assert m.satisfiable(extra_constraints=(m.memory.load(0x400000, 4) == 10,))
176 assert i, s.solver.satisfiable(extra_constraints=(culprit == i,))
178 assert not s.solver.satisfiable(extra_constraints=(culprit == 12, ))
199 assert i, s.solver.satisfiable(extra_constraints=(culprit == i,))
201 assert not s.solver.satisfiable(extra_constraints=(culprit == 12, ))
222 nose.tools.assert_false(s.solver.satisfiable())
|
| /dports/java/eclipse/eclipse.platform.releng.aggregator-R4_16/rt.equinox.p2/bundles/org.eclipse.equinox.p2.director/src/org/eclipse/equinox/internal/p2/director/ |
| H A D | messages.properties | 19 …_Unsatisfied_Dependencies=Cannot complete the install because some dependencies are not satisfiable
20 Director_Satisfied_Dependencies=Overall install request is satisfiable
21 Director_Satisfied_Change={0} request for {1} is satisfiable
22 Director_Unsatisfied_Change={0} request for {1} is NOT satisfiable
|
| /dports/www/qt5-webengine/qtwebengine-everywhere-src-5.15.2/src/3rdparty/chromium/mojo/public/cpp/system/ |
| H A D | handle_signals_state.h | 22 MojoHandleSignals satisfiable) { in HandleSignalsState()
24 satisfiable_signals = satisfiable; in HandleSignalsState()
|
| /dports/www/chromium-legacy/chromium-88.0.4324.182/mojo/public/cpp/system/ |
| H A D | handle_signals_state.h | 22 MojoHandleSignals satisfiable) { in HandleSignalsState()
24 satisfiable_signals = satisfiable; in HandleSignalsState()
|
| /dports/www/qt5-webengine/qtwebengine-everywhere-src-5.15.2/src/3rdparty/chromium/mojo/core/ |
| H A D | handle_signals_state.h | 26 MojoHandleSignals satisfiable) { in HandleSignalsState()
28 satisfiable_signals = satisfiable; in HandleSignalsState()
|
| /dports/www/chromium-legacy/chromium-88.0.4324.182/mojo/core/ |
| H A D | handle_signals_state.h | 26 MojoHandleSignals satisfiable) { in HandleSignalsState()
28 satisfiable_signals = satisfiable; in HandleSignalsState()
|
| /dports/misc/otter/otter-3.3f/examples/split/ |
| H A D | README.more | 11 zebra2.in This is the zebra puzzle with Dale Myers' rep. (satisfiable).
12 zebra4.in Like Z2, with a cleaner rep., but it takes longer (satisfiable).
|