/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | local_theory_ext.h | 50 Node bvl,
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/dvfsf/ |
H A D | dvfsfqe.red | 139 % <FUNCTION> ::= [dvfsf_qesubcq]([bvl],[theo],[f],[v],<GUARD>,<POINT>) 182 procedure dvfsf_qesubcq(bvl,theo,f,v,c,u); 213 procedure dvfsf_transform(v, f, vl, an, theo, ans, bvl); 216 procedure dvfsf_trygauss(f,vl,theo,ans,bvl);
|
/dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
H A D | sygus_inference.cpp | 261 Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); in solveSygus() local 262 body = nm->mkNode(EXISTS, bvl, body.negate()); in solveSygus()
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/acfsf/ |
H A D | acfsfmisc.red | 150 procedure acfsf_getineq(f,bvl); 152 % is a formula; [bvl] is a list of variables. Returns the list of 154 % variables in [bvl]. 161 null intersection(bvl, kernels acfsf_arg2l atf) then
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/cl/ |
H A D | clmisc.red | 590 begin scalar w,q,vl,qblkl,bvl,v; 596 bvl := v . bvl; 607 return {qblkl,f,bvl} 627 begin scalar fvl,bvl,vl; 628 fvl . bvl := rl_varl f; 634 begin scalar w,fvl,bvl,vl,ql,sl,eqs,res; 635 fvl . bvl := rl_varl f; 638 repeat w := mkid(w,'!#) until not memq(w,fvl) and not memq(w,bvl);
|
/dports/math/spot/spot-2.10.2/spot/twaalgos/ |
H A D | powerset.cc | 66 bool operator()(const bitvect* bvl, const bitvect* bvr) const in operator ()() 68 return *bvl == *bvr; in operator ()()
|
/dports/math/py-spot/spot-2.10.2/spot/twaalgos/ |
H A D | powerset.cc | 66 bool operator()(const bitvect* bvl, const bitvect* bvr) const in operator ()() 68 return *bvl == *bvr; in operator ()()
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/ofsf/ |
H A D | ofsfic.red | 465 scalar q,ql,varll,bvl,svf,result,w,ww,k,rvl,jl,f2,offset,offset2; 514 {ql, varll, f, bvl} := cl_split f; 515 {ql, varll, q, rvl, jl, theo, svf} := cl_qe1!-iterate(ql, varll, f, nil, bvl); 575 w . theo := ofsfic!*cl_qevar(ce_f coe, ce_vl coe, ce_ans coe, theo, ans, bvl); 676 …l_qevar(f: QfFormula, vl: KernelL, an: Answer, theo: Theory, ans: Boolean, bvl: KernelL): DottedPa… 686 status . w := ofsfic!*cl_process!-candvl(f,vl,an,theo,ans,bvl,candvl); 724 …ww := cl_esetvectsubst(f, ic_currentfvect rlqeicdata!*, v, elimset, lto_delq(v, vl), an, ans, bvl); 786 w := apply(a, bvl . nil . sf . v . u); 789 w := apply(a, bvl . nil . sf . v . u2); 833 begin scalar a,d,u,elimres,junct,bvl,w; [all …]
|
H A D | ofsfdecdeg.red | 163 procedure ofsf_transform(v, f, vl, an, theo, ans, bvl); 188 return {nf, vl, an, theo, ans, bvl}
|
H A D | ofsfmisc.red | 208 procedure ofsf_getineq(f,bvl); 210 % hand side is always zero; [bvl] is a list of variables. Returns 212 % variables from [bvl]. 219 null intersection(bvl, kernels ofsf_arg2l atf) then
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/pasf/ |
H A D | pasfqe.red | 465 begin scalar res,tf,bvl,sf,w; 473 bvl := elimpt_bvl elimpt; 474 for each bv in bvl do << 481 res := answ_new(tf,for each bv in bvl collect car bv, 1063 procedure pasf_rep1(f,x,pos,bvl); 1079 res := append(pasf_rep1(arg,x,nil,bvl),res); 1087 return {repr_atfbnew(f,x,nil,bvl)} 1090 procedure pasf_ses(f,x,pos,bvl); 1104 tmp := pasf_ses(arg,x,append(pos,{n}),bvl); 1119 res := append(pasf_ses(arg,x,append(pos,{n}),bvl),res); [all …]
|
H A D | pasfmisc.red | 1082 procedure repr_atfbnew(atf,x,pos,bvl); 1085 % variable; [pos] is the position inside the formula; [bvl] is the list of 1094 for each v in bvl do << 1115 begin scalar bvl,pos,btl; 1122 bvl := (rl_b f . rl_var f) . bvl; 1127 return {f,pos,bvl,btl} 1157 procedure elimpt_new(pos,guard,nom,den,bvl,unif); 1161 % [den] represents the denominator of the testpoint [nom]/[den]; [bvl] is a 1165 {pos,guard,nom,den,bvl,unif};
|
/dports/math/reduce/Reduce-svn5758-src/packages/redlog/ibalp/ |
H A D | ibalp.red | 784 procedure ibalp_transform(v, f, vl, an, theo, ans, bvl); 790 procedure ibalp_trygauss(f,v,theo,ans,bvl); 796 procedure ibalp_specelim(f,vl,theo,ans,bvl); 798 % list of variables; [theo] is a theory; [ans] is Bool; [bvl] is 885 % there is $p(bvl,theo,f,v,l_{i1},...,l_{im})$ called for 898 procedure ibalp_qesub(bvl,theo,f,v,bconst);
|
/dports/multimedia/v4l_compat/linux-5.13-rc2/include/linux/ |
H A D | blkdev.h | 874 #define rq_for_each_segment(bvl, _rq, _iter) \ argument 876 bio_for_each_segment(bvl, _iter.bio, _iter.iter) 878 #define rq_for_each_bvec(bvl, _rq, _iter) \ argument 880 bio_for_each_bvec(bvl, _iter.bio, _iter.iter)
|
/dports/multimedia/libv4l/linux-5.13-rc2/include/linux/ |
H A D | blkdev.h | 874 #define rq_for_each_segment(bvl, _rq, _iter) \ argument 876 bio_for_each_segment(bvl, _iter.bio, _iter.iter) 878 #define rq_for_each_bvec(bvl, _rq, _iter) \ argument 880 bio_for_each_bvec(bvl, _iter.bio, _iter.iter)
|
/dports/multimedia/v4l-utils/linux-5.13-rc2/include/linux/ |
H A D | blkdev.h | 874 #define rq_for_each_segment(bvl, _rq, _iter) \ argument 876 bio_for_each_segment(bvl, _iter.bio, _iter.iter) 878 #define rq_for_each_bvec(bvl, _rq, _iter) \ argument 880 bio_for_each_bvec(bvl, _iter.bio, _iter.iter)
|
/dports/math/cvc4/CVC4-1.7/src/parser/tptp/ |
H A D | Tptp.g | 158 std::vector<Expr> bvl = PARSER_STATE->getFreeVar(); 159 if(!bvl.empty()) { 160 expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr); 369 Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r); 370 body = MK_EXPR(CVC4::kind::EXISTS, bvl, body);
|
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
H A D | synth_conjecture.cpp | 1186 Node bvl = Node::fromExpr(dt.getSygusVarList()); in getSynthSolutions() local 1187 if (!bvl.isNull()) in getSynthSolutions() 1189 bsol = nm->mkNode(LAMBDA, bvl, bsol); in getSynthSolutions()
|
H A D | cegis_unif.cpp | 454 Node bvl; in mkLiteral() local 464 bvl, in mkLiteral()
|
/dports/math/reduce/Reduce-svn5758-src/csl/cslbase/ |
H A D | fns2.cpp | 674 { LispObject bvl = car(cdr(b)); in Lsymbol_set_definition() local 676 while (consp(bvl)) nargs++, bvl = cdr(bvl); in Lsymbol_set_definition() 692 { LispObject bvl = car(cdr(b)); in Lsymbol_set_definition() local 694 while (consp(bvl)) nargs++, bvl = cdr(bvl); in Lsymbol_set_definition()
|
/dports/science/InsightToolkit/ITK-5.0.1/Modules/ThirdParty/GDCM/src/gdcm/Source/MediaStorageAndFileFormat/ |
H A D | gdcmRLECodec.cxx | 326 unsigned long bvl = bv->GetLength(); in Code() local 327 unsigned long image_len = bvl / dims[2]; in Code()
|
/dports/math/cvc4/CVC4-1.7/src/parser/smt2/ |
H A D | Smt2.g | 837 Expr bvl; 840 bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars); 1492 Expr head, body, expr, expr2, bvl; 1507 bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); 1523 args.push_back(bvl); 1548 bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); 1574 args.push_back(bvl); 1816 Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); 1818 args.push_back(bvl); 2206 Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); [all …]
|
/dports/devel/gdcm/gdcm-3.0.10/Source/MediaStorageAndFileFormat/ |
H A D | gdcmRLECodec.cxx | 326 unsigned long bvl = bv->GetLength(); in Code() local 327 unsigned long image_len = bvl / dims[2]; in Code()
|
/dports/lang/abcl/abcl-src-1.8.0/src/org/armedbear/lisp/ |
H A D | restart.lisp | 245 (bvl (nth 3 datum))
|
/dports/math/reduce/Reduce-svn5758-src/csl/embedded/ |
H A D | fns2.c | 1254 { Lisp_Object bvl = qcar(qcdr(b)); in Lsymbol_set_definition() local 1256 while (consp(bvl)) nargs++, bvl = qcdr(bvl); in Lsymbol_set_definition() 1273 { Lisp_Object bvl = qcar(qcdr(b)); in Lsymbol_set_definition() local 1275 while (consp(bvl)) nargs++, bvl = qcdr(bvl); in Lsymbol_set_definition()
|