/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | quant_util.cpp | 128 …tPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { in getPolarity() argument 131 newPol = pol; in getPolarity() 134 newPol = child==0 ? !pol : pol; in getPolarity() 137 newPol = !pol; in getPolarity() 140 newPol = pol; in getPolarity() 143 newPol = pol; in getPolarity() 146 newPol = pol; in getPolarity() 153 newPol = pol; in getEntailPolarity() 156 newPol = child==0 ? !pol : pol; in getEntailPolarity() 159 newPol = !pol; in getEntailPolarity() [all …]
|
H A D | quant_epr.cpp | 74 bool newPol; in registerNode() local 75 QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol); in registerNode() 76 registerNode(n[i], visited, beneathQuant, newHasPol, newPol); in registerNode()
|
H A D | quant_util.h | 207 …static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ); 208 … void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
|
H A D | relevant_domain.cpp | 176 bool newPol; in computeRelevantDomain() local 177 QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); in computeRelevantDomain() 178 computeRelevantDomain( q, n[i], newHasPol, newPol ); in computeRelevantDomain()
|
H A D | fun_def_process.cpp | 169 bool newPol; in simplifyFormula() local 170 QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); in simplifyFormula() 173 … c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, false, visited, visited_cons ); in simplifyFormula()
|
H A D | quantifiers_rewriter.cpp | 592 bool newPol; in computeProcessTerms2() local 593 QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); in computeProcessTerms2() 594 …Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, ne… in computeProcessTerms2() 1284 bool newPol; in getVarElimIneq() local 1285 QuantPhaseReq::getPolarity(ecur, j, hasPol, pol, newHasPol, newPol); in getVarElimIneq() 1287 evisit_pol.push_back(newHasPol ? (newPol ? 1 : -1) : 0); in getVarElimIneq() 1399 bool newPol; in computePrenex() local 1400 QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); in computePrenex() 1402 Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); in computePrenex()
|
H A D | inst_propagator.cpp | 435 bool newHasPol, newPol; in evaluateTermExp() local 436 QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol ); in evaluateTermExp() 440 … Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out, props ); in evaluateTermExp()
|
H A D | quant_conflict_find.cpp | 150 bool newPol = pol; in getPropagateVars() local 162 QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol ); in getPropagateVars() 217 bool newPol; in registerNode() local 218 QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); in registerNode() 222 registerNode( n[i], newHasPol, newPol, beneathQuant ); in registerNode()
|
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
H A D | sep_skolem_emp.cpp | 72 bool newPol, newHasPol; in preSkolemEmp() local 73 QuantPhaseReq::getPolarity(n, i, true, pol, newHasPol, newPol); in preSkolemEmp() 77 nc = preSkolemEmp(n[i], newPol, visited); in preSkolemEmp()
|
/dports/math/fricas/fricas-1.3.7/pre-generated/src/algebra/ |
H A D | ROIRC.lsp | 735 ((#2=#:G585 NIL) (|newPol| (|ThePolDom|)) 759 (LETT |newPol| 775 (SPADCALL |newPol| |c| 778 |newPol| (QREFELT $ 88)) 807 (#2=#:G595 NIL) (|c| (|TheField|)) (|newPol| (|ThePolDom|))) 843 (LETT |newPol| 855 ((EQL (SPADCALL |newPol| (QREFELT $ 12)) 1) 861 (SPADCALL |newPol| (QREFELT $ 17)) 863 (SPADCALL |newPol| 0 (QREFELT $ 16)) 891 (SPADCALL |newPol| |c| [all …]
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
H A D | sygus_pbe.cpp | 136 bool newPol; in collectExamples() local 137 QuantPhaseReq::getEntailPolarity(n, i, hasPol, pol, newHasPol, newPol); in collectExamples() 138 if (!collectExamples(n[i], visited, newHasPol, newPol)) in collectExamples()
|
/dports/math/fricas/fricas-1.3.7/src/algebra/ |
H A D | reclos.spad | 728 newPol := (rootChar.defPol exquo toTest)::P 729 ((1$ThePolDom - inv(newPol.c)*newPol) exquo toTest)::P 746 newPol := (rootChar.defPol exquo (d.generator))::P 747 degree(newPol) = 1 => 748 c := - inv(leadingCoefficient(newPol)) * coefficient(newPol, 0) 752 ((1$ThePolDom - inv(newPol.(c))*newPol) exquo toTest)::P 753 d := extendedEuclidean(newPol, toTest)
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
H A D | trigger.cpp | 476 bool newHasPol, newPol; in collectPatTerms2() local 478 QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); in collectPatTerms2() 480 …collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, … in collectPatTerms2()
|
/dports/math/cvc4/CVC4-1.7/src/theory/sep/ |
H A D | theory_sep.cpp | 935 bool newHasPol, newPol; in processAssertion() local 936 QuantPhaseReq::getEntailPolarity( n, i, hasPol, pol, newHasPol, newPol ); in processAssertion() 937 int newIndex = newHasPol ? ( newPol ? 1 : -1 ) : 0; in processAssertion() 938 …int ccard = processAssertion( n[i], visited, references, references_strict, newPol, newHasPol, new… in processAssertion()
|
/dports/math/maxima/maxima-5.43.2/share/algebra/charsets/ |
H A D | wsolve | 3247 local rt,newasc,asc,pol,hPol,hVar,hDeg,rem,newPol,tempList,varList,len; 3264 newPol:=rem*notzerolist[len]; 3265 tempList:=[newasc,newPol]; 3266 varList:=HigherOrdVars(newPol,mvl,len,ord,pord);
|