| /dports/lang/solidity/solidity_0.8.11/libyul/optimiser/ |
| H A D | SMTSolver.cpp | 87 m_solver->addAssertion(0 <= var && var <= smtutil::Expression(_maxValue)); in newRestrictedVariable()
138 m_solver->addAssertion(_value == multiplier * smtutil::Expression(bigint(1) << 256) + rest); in wrap()
156 m_solver->addAssertion( in encodeVariableDeclaration()
|
| H A D | ReasoningBasedSimplifier.cpp | 67 m_solver->addAssertion(condition == constantValue(0)); in operator ()()
79 m_solver->addAssertion(condition != constantValue(0)); in operator ()()
94 m_solver->addAssertion(condition != constantValue(0)); in operator ()()
|
| /dports/lang/solidity/solidity_0.8.11/libsolidity/formal/ |
| H A D | CHC.cpp | 213 m_context.addAssertion(errorFlag().currentValue() == 0); in endVisit()
618 m_context.addAssertion(slicePred); in endVisit()
735 m_context.addAssertion(predicate(_funCall)); in internalFunctionCall()
743 m_context.addAssertion(errorFlag().currentValue() == 0); in internalFunctionCall()
823 m_context.addAssertion(nondetCall); in externalFunctionCall()
834 m_context.addAssertion(errorFlag().currentValue() == 0); in externalFunctionCall()
862 m_context.addAssertion(pred && txConstraints); in externalFunctionCallToTrustedCode()
865 m_context.addAssertion(originalTx == state().tx()); in externalFunctionCallToTrustedCode()
873 m_context.addAssertion(errorFlag().currentValue() == 0); in externalFunctionCallToTrustedCode()
1210 m_context.addAssertion(summaryCall(_function)); in defineExternalFunctionInterface()
[all …]
|
| H A D | SMTEncoder.cpp | 892 m_context.addAssertion(symbArray->length() == arraySize); in visitObjectCreation()
1268 m_context.addAssertion(k.currentValue() == 0); in bytesToFixedBytesAssertions()
1624 m_context.addAssertion(oldLength >= 0); in arrayPush()
1642 m_context.addAssertion(symbArray->elements() == store); in arrayPush()
1670 m_context.addAssertion(symbArray->length() == newLength); in arrayPop()
1813 m_context.addAssertion(k.currentValue() >= symbMin); in arithmeticOperation()
1814 m_context.addAssertion(k.currentValue() <= symbMax); in arithmeticOperation()
1991 m_context.addAssertion(((d * _right) + r) == _left); in divModWithSlacks()
1993 m_context.addAssertion( in divModWithSlacks()
2484 m_context.addAssertion(expr(_e) == _value); in defineExpr()
[all …]
|
| H A D | BMC.cpp | 192 m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function)); in visit()
362 m_context.addAssertion(expr(*_node.condition())); in visit()
393 m_context.addAssertion(clauseId >= 0 && clauseId < clauses.size()); in visit()
916 m_interface->addAssertion(_condition); in checkCondition()
1010 m_interface->addAssertion(_constraints && _value); in checkBooleanNotConstant()
1015 m_interface->addAssertion(_constraints && !_value); in checkBooleanNotConstant()
1096 m_context.addAssertion(smtutil::Expression::ite( in assignment()
|
| H A D | SymbolicVariables.cpp | 382 m_context.addAssertion(member(memberName) == newMember); in assignMember()
398 m_context.addAssertion(_memberValues[i] == member(structMembers[i]->name())); in assignAllMembers()
|
| H A D | SymbolicState.cpp | 70 m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args)); in assignMember()
127 m_context.addAssertion(m_state.value() == newState); in transfer()
|
| /dports/www/zend-framework/ZendFramework-2.4.13/library/Zend/Permissions/Acl/Assertion/ |
| H A D | AssertionAggregate.php | 41 public function addAssertion($assertion) function in Zend\\Permissions\\Acl\\Assertion\\AssertionAggregate
51 $this->addAssertion($assertion);
|
| /dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
| H A D | bv_quick_check.cpp | 93 bool BVQuickCheck::addAssertion(TNode assertion) { in addAssertion() function in CVC4::theory::bv::BVQuickCheck
221 bool ok = d_solver->addAssertion(conflict[i]); in minimizeConflictInternal()
251 bool ok = d_solver->addAssertion(conflict[i]); in minimizeConflictInternal()
281 bool ok = d_solver->addAssertion(new_conflict[i]); in minimizeConflictInternal()
|
| H A D | bv_quick_check.h | 78 bool addAssertion(TNode assumption);
|
| /dports/lang/solidity/solidity_0.8.11/libsmtutil/ |
| H A D | SMTPortfolio.cpp | 80 void SMTPortfolio::addAssertion(Expression const& _expr) in addAssertion() function in SMTPortfolio
83 s->addAssertion(_expr); in addAssertion()
|
| H A D | CVC4Interface.h | 55 void addAssertion(Expression const& _expr) override;
|
| H A D | SMTPortfolio.h | 59 void addAssertion(Expression const& _expr) override;
|
| H A D | Z3Interface.h | 45 void addAssertion(Expression const& _expr) override;
|
| H A D | SMTLib2Interface.h | 57 void addAssertion(Expression const& _expr) override;
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | dpllt_minisat.h | 91 virtual void addAssertion(const CNF_Formula& cnf);
|
| H A D | dpllt.h | 141 virtual void addAssertion(const CNF_Formula& cnf) = 0;
|
| H A D | dpllt_basic.h | 79 void addAssertion(const CNF_Formula& cnf);
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | theory_engine.cpp | 169 proofStep.addAssertion(lemma[i]); in registerLemmaRecipe()
177 proofStep.addAssertion(lemma); in registerLemmaRecipe()
1455 proofStep.addAssertion(literal); in propagate()
1621 proofStep.addAssertion(node); in getExplanationAndRecipe()
1640 proofStep.addAssertion(flat[i].negate()); in getExplanationAndRecipe()
1648 proofStep.addAssertion(explanation.negate()); in getExplanationAndRecipe()
1679 proofStep.addAssertion(node); in getExplanationAndRecipe()
1897 proofStep.addAssertion(conflict[i].negate()); in conflict()
1900 proofStep.addAssertion(conflict.negate()); in conflict()
2119 proofStep.addAssertion(flat[k].negate()); in getExplanation()
[all …]
|
| /dports/security/shibboleth-sp/shibboleth-sp-3.3.0/shibsp/impl/ |
| H A D | StoredSession.h | 124 void addAssertion(opensaml::Assertion* assertion);
|
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | lemma_proof.h | 37 void addAssertion(const Node& assertion);
|
| /dports/converters/wkhtmltopdf/qt-5db36ec/src/xmlpatterns/schema/ |
| H A D | qxsdcomplextype_p.h | 375 void addAssertion(const XsdAssertion::Ptr &assertion);
|
| H A D | qxsdcomplextype.cpp | 216 void XsdComplexType::addAssertion(const XsdAssertion::Ptr &assertion) in addAssertion() function in XsdComplexType
|
| /dports/textproc/qt5-xmlpatterns/kde-qtxmlpatterns-5.15.2p2/src/xmlpatterns/schema/ |
| H A D | qxsdcomplextype_p.h | 371 void addAssertion(const XsdAssertion::Ptr &assertion);
|
| H A D | qxsdcomplextype.cpp | 214 void XsdComplexType::addAssertion(const XsdAssertion::Ptr &assertion) in addAssertion() function in XsdComplexType
|