/dports/math/stp/stp-2.3.3/lib/Simplifier/ |
H A D | consteval.cpp | 47 ASTNode& ASTFalse = _bm->ASTFalse; in NonMemberBVConstEvaluator() local 106 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 597 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 605 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 615 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 677 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 681 return ASTFalse; in NonMemberBVConstEvaluator() 692 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() 702 ASTNode o = ASTFalse; in NonMemberBVConstEvaluator() 756 OutputNode = ASTFalse; in NonMemberBVConstEvaluator() [all …]
|
H A D | Simplifier.cpp | 316 return ASTFalse; in SimplifyFormula() 621 output = pushNeg ? (ASTFalse == output) ? ASTTrue : ASTFalse : output; in CreateSimplifiedINEQ() 857 output = ASTFalse; in ITEOpt_InEqs() 934 return ASTFalse; in CreateSimplifiedEQ() 950 return ASTFalse; in CreateSimplifiedEQ() 1018 return ASTFalse; in CreateSimplifiedEQ() 1080 if (t0 == ASTFalse) in CreateSimplifiedTermITE() 1111 if (t0 == ASTFalse) in CreateSimplifiedFormulaITE() 1146 isAnd ? (pushNeg ? ASTTrue : ASTFalse) : (pushNeg ? ASTFalse : ASTTrue); in SimplifyAndOrFormula() 1404 if (ASTFalse == c0) in SimplifyImpliesFormula() [all …]
|
H A D | UseITEContext.cpp | 79 return ASTFalse; in visit() 139 ASTFalse = bm->ASTFalse; in UseITEContext()
|
H A D | PropagateEqualities.cpp | 177 bool updated = searchXOR(a[0], ASTFalse); in propagate() 324 if (ASTFalse == aaa) in propagate() 325 return ASTFalse; in propagate()
|
H A D | BVSolver.cpp | 76 if (key == ASTTrue || key == ASTFalse) in CheckAlreadySolvedMap() 564 if (ASTFalse == aaa) in TopLevelBVSolve() 567 return ASTFalse; // shortcut. It's unsatisfiable. in TopLevelBVSolve() 688 return ASTFalse; in CheckEvenEqn()
|
H A D | FindPureLiterals.cpp | 76 simplifier->UpdateSubstitutionMap(n, stpMgr->ASTFalse); in topLevel()
|
/dports/math/stp/stp-2.3.3/include/stp/Simplifier/ |
H A D | PropagateEqualities.h | 51 const ASTNode ASTTrue, ASTFalse; variable 63 : ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse), in PropagateEqualities()
|
H A D | BVSolver.h | 70 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable 135 ASTFalse = _bm->CreateNode(FALSE); in BVSolver()
|
H A D | SubstitutionMap.h | 47 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable 94 ASTFalse = bm->CreateNode(FALSE); in SubstitutionMap()
|
H A D | UseITEContext.h | 49 ASTNode ASTTrue, ASTFalse; variable
|
H A D | Simplifier.h | 46 ASTNode ASTTrue, ASTFalse, ASTUndefined; 95 ASTFalse = bm->CreateNode(FALSE); in Simplifier()
|
H A D | AlwaysTrue.h | 99 return stpMgr->ASTFalse; in visit()
|
/dports/math/stp/stp-2.3.3/include/stp/ToSat/ASTNode/ |
H A D | BBNodeManagerASTNode.h | 42 ASTNode ASTTrue, ASTFalse; variable 54 ASTFalse = stpMgr->CreateNode(FALSE); in BBNodeManagerASTNode() 61 ASTNode getFalse() { return ASTFalse; } in getFalse()
|
/dports/math/stp/stp-2.3.3/include/stp/AST/NodeFactory/ |
H A D | SimplifyingNodeFactory.h | 75 ASTFalse(bm_.ASTFalse), ASTUndefined(bm_.ASTUndefined){}; in SimplifyingNodeFactory() 83 const ASTNode& ASTFalse; variable
|
/dports/math/stp/stp-2.3.3/lib/AST/NodeFactory/ |
H A D | SimplifyingNodeFactory.cpp | 93 return ASTFalse; in create_gt_node() 99 return ASTFalse; in create_gt_node() 105 return ASTFalse; in create_gt_node() 110 return ASTFalse; in create_gt_node() 148 return ASTFalse; in create_gt_node() 318 return ASTFalse; in CreateSimpleNot() 346 return ASTFalse; in CreateSimpleNot() 488 return ASTFalse; in CreateSimpleEQ() 504 return ASTFalse; in CreateSimpleEQ() 675 return ASTFalse; in CreateSimpleEQ() [all …]
|
H A D | NodeFactory.cpp | 138 return bm.ASTFalse; in getFalse()
|
/dports/math/stp/stp-2.3.3/include/stp/ToSat/ |
H A D | ToSATBase.h | 36 ASTNode ASTTrue, ASTFalse, ASTUndefined; 49 ASTFalse = bm->CreateNode(FALSE); in ToSATBase()
|
/dports/math/stp/stp-2.3.3/include/stp/AbsRefineCounterExample/ |
H A D | ArrayTransformer.h | 78 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable 125 ASTFalse = bm->CreateNode(FALSE); in ArrayTransformer()
|
H A D | AbsRefine_CounterExample.h | 40 ASTNode ASTTrue, ASTFalse, ASTUndefined; 89 ASTFalse = bm->CreateNode(FALSE); in AbsRefine_CounterExample()
|
/dports/math/stp/stp-2.3.3/lib/AbsRefineCounterExample/ |
H A D | CounterExample.cpp | 89 CounterExampleMap[symbol] = ASTFalse; in ConstructCounterExample() 256 else if (ASTFalse == condcompute) in TermToConstTermUsingModel() 319 else if (ASTFalse == condcompute) in TermToConstTermUsingModel() 446 if (ASTTrue == res || ASTFalse == res) in ComputeFormulaUsingModel() 485 output = ASTFalse; in ComputeFormulaUsingModel() 544 else if (ASTFalse == t0) in ComputeFormulaUsingModel() 592 if (ASTFalse == ComputeFormulaUsingModel(*it)) in CheckCounterExample() 1051 if (!(ASTTrue == orig_result || ASTFalse == orig_result)) in CallSAT_ResultCheck()
|
H A D | ArrayTransformer.cpp | 448 else if (ASTFalse == cond) in TransformTerm() 588 if (ASTFalse == cond) in TransformArrayRead() 736 else if (ASTFalse == cond) in TransformArrayRead()
|
/dports/math/stp/stp-2.3.3/tools/stp_constantbitprop/ |
H A D | constantbitprop.cpp | 90 n = mgr->ASTFalse; in main()
|
/dports/math/stp/stp-2.3.3/lib/STPManager/ |
H A D | STP.cpp | 128 if (query != bm->ASTFalse) in TopLevelSTP() 430 inputToSat = bm->ASTFalse; in TopLevelSTPAux() 590 inputToSat = bm->ASTFalse; in TopLevelSTPAux()
|
/dports/math/stp/stp-2.3.3/include/stp/STPManager/ |
H A D | STPManager.h | 85 ASTNode ASTFalse, ASTTrue, ASTUndefined; variable 226 ASTFalse = CreateNode(FALSE); in STPMgr()
|
/dports/math/stp/stp-2.3.3/lib/ToSat/AIG/ |
H A D | ToSATAIG.cpp | 49 if (input == ASTFalse) in CallSAT()
|