Home
last modified time | relevance | path

Searched refs:ASTFalse (Results 1 – 25 of 33) sorted by relevance

12

/dports/math/stp/stp-2.3.3/lib/Simplifier/
H A Dconsteval.cpp47 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 DSimplifier.cpp316 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 DUseITEContext.cpp79 return ASTFalse; in visit()
139 ASTFalse = bm->ASTFalse; in UseITEContext()
H A DPropagateEqualities.cpp177 bool updated = searchXOR(a[0], ASTFalse); in propagate()
324 if (ASTFalse == aaa) in propagate()
325 return ASTFalse; in propagate()
H A DBVSolver.cpp76 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 DFindPureLiterals.cpp76 simplifier->UpdateSubstitutionMap(n, stpMgr->ASTFalse); in topLevel()
/dports/math/stp/stp-2.3.3/include/stp/Simplifier/
H A DPropagateEqualities.h51 const ASTNode ASTTrue, ASTFalse; variable
63 : ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse), in PropagateEqualities()
H A DBVSolver.h70 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable
135 ASTFalse = _bm->CreateNode(FALSE); in BVSolver()
H A DSubstitutionMap.h47 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable
94 ASTFalse = bm->CreateNode(FALSE); in SubstitutionMap()
H A DUseITEContext.h49 ASTNode ASTTrue, ASTFalse; variable
H A DSimplifier.h46 ASTNode ASTTrue, ASTFalse, ASTUndefined;
95 ASTFalse = bm->CreateNode(FALSE); in Simplifier()
H A DAlwaysTrue.h99 return stpMgr->ASTFalse; in visit()
/dports/math/stp/stp-2.3.3/include/stp/ToSat/ASTNode/
H A DBBNodeManagerASTNode.h42 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 DSimplifyingNodeFactory.h75 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 DSimplifyingNodeFactory.cpp93 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 DNodeFactory.cpp138 return bm.ASTFalse; in getFalse()
/dports/math/stp/stp-2.3.3/include/stp/ToSat/
H A DToSATBase.h36 ASTNode ASTTrue, ASTFalse, ASTUndefined;
49 ASTFalse = bm->CreateNode(FALSE); in ToSATBase()
/dports/math/stp/stp-2.3.3/include/stp/AbsRefineCounterExample/
H A DArrayTransformer.h78 ASTNode ASTTrue, ASTFalse, ASTUndefined; variable
125 ASTFalse = bm->CreateNode(FALSE); in ArrayTransformer()
H A DAbsRefine_CounterExample.h40 ASTNode ASTTrue, ASTFalse, ASTUndefined;
89 ASTFalse = bm->CreateNode(FALSE); in AbsRefine_CounterExample()
/dports/math/stp/stp-2.3.3/lib/AbsRefineCounterExample/
H A DCounterExample.cpp89 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 DArrayTransformer.cpp448 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 Dconstantbitprop.cpp90 n = mgr->ASTFalse; in main()
/dports/math/stp/stp-2.3.3/lib/STPManager/
H A DSTP.cpp128 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 DSTPManager.h85 ASTNode ASTFalse, ASTTrue, ASTUndefined; variable
226 ASTFalse = CreateNode(FALSE); in STPMgr()
/dports/math/stp/stp-2.3.3/lib/ToSat/AIG/
H A DToSATAIG.cpp49 if (input == ASTFalse) in CallSAT()

12