Home
last modified time | relevance | path

Searched refs:newPol (Results 1 – 15 of 15) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dquant_util.cpp128 …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 Dquant_epr.cpp74 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 Dquant_util.h207 …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 Drelevant_domain.cpp176 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 Dfun_def_process.cpp169 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 Dquantifiers_rewriter.cpp592 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 Dinst_propagator.cpp435 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 Dquant_conflict_find.cpp150 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 Dsep_skolem_emp.cpp72 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 DROIRC.lsp735 ((#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 Dsygus_pbe.cpp136 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 Dreclos.spad728 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 Dtrigger.cpp476 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 Dtheory_sep.cpp935 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 Dwsolve3247 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);