| /dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
| H A D | arith_proof_rules.h | 219 const Theorem& isIntx)=0;
232 const Theorem& isIntx)=0;
295 const Theorem& isIntx) = 0;
299 virtual Theorem IsIntegerElim(const Theorem& isIntx) = 0;
395 const Theorem& isIntx,
|
| H A D | arith_theorem_producer.h | 254 const Theorem& isIntx);
260 const Theorem& isIntx);
284 Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
286 Theorem IsIntegerElim(const Theorem& isIntx);
287 Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
|
| H A D | arith_theorem_producer_old.h | 253 const Theorem& isIntx);
259 const Theorem& isIntx);
284 Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
285 Theorem IsIntegerElim(const Theorem& isIntx);
287 Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
|
| H A D | arith_theorem_producer3.h | 253 const Theorem& isIntx);
259 const Theorem& isIntx);
283 Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
284 Theorem IsIntegerElim(const Theorem& isIntx);
286 Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
|
| H A D | arith_theorem_producer3.cpp | 1270 CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0][1], in intEqIrrational()
1274 +isIntx.getExpr().toString()); in intEqIrrational()
1639 const Theorem& isIntx) { in darkGrayShadow2ab() argument
1695 thms.push_back(isIntx); in darkGrayShadow2ab()
1717 pfs.push_back(isIntx.getProof()); in darkGrayShadow2ab()
1730 const Theorem& isIntx) { in darkGrayShadow2ba() argument
1786 thms.push_back(isIntx); in darkGrayShadow2ba()
2096 const Theorem& isIntx) { in intVarEqnConst() argument
2482 Expr expr = isIntx.getExpr(); in IsIntegerElim()
2490 Assumptions a(isIntx); in IsIntegerElim()
[all …]
|
| H A D | arith_theorem_producer.cpp | 1283 CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0][1], in intEqIrrational()
1287 +isIntx.getExpr().toString()); in intEqIrrational()
1682 const Theorem& isIntx) { in darkGrayShadow2ab() argument
1738 thms.push_back(isIntx); in darkGrayShadow2ab()
1760 pfs.push_back(isIntx.getProof()); in darkGrayShadow2ab()
1773 const Theorem& isIntx) { in darkGrayShadow2ba() argument
1829 thms.push_back(isIntx); in darkGrayShadow2ba()
2139 const Theorem& isIntx) { in intVarEqnConst() argument
2507 Expr expr = isIntx.getExpr(); in IsIntegerElim()
2515 Assumptions a(isIntx); in IsIntegerElim()
[all …]
|
| H A D | arith_theorem_producer_old.cpp | 1342 …CHECK_SOUND(isIntPred(isIntx.getExpr()) && isIntx.getExpr()[0] == expr[0], "intEqIrrational invari… in intEqIrrational()
1837 const Theorem& isIntx) { in darkGrayShadow2ab() argument
1895 thms.push_back(isIntx); in darkGrayShadow2ab()
1917 pfs.push_back(isIntx.getProof()); in darkGrayShadow2ab()
1930 const Theorem& isIntx) { in darkGrayShadow2ba() argument
1989 thms.push_back(isIntx); in darkGrayShadow2ba()
1998 pfs.push_back(isIntx.getProof()); in darkGrayShadow2ba()
2298 const Theorem& isIntx) { in intVarEqnConst() argument
2684 Expr expr = isIntx.getExpr(); in IsIntegerElim()
2692 Assumptions a(isIntx); in IsIntegerElim()
[all …]
|
| H A D | theory_arith3.cpp | 565 Theorem isIntx(isIntegerThm(left[1])); in doSolve() local
566 DebugAssert(!isIntx.isNull(), "left = "+left.toString()); in doSolve()
567 return iffMP(res, d_rules->intEqIrrational(res.getExpr(), isIntx)); in doSolve()
780 Theorem isIntx(isIntegerThm(x)); in processSimpleIntEq() local
781 DebugAssert(!isIntx.isNull(), "right = "+right.toString() in processSimpleIntEq()
783 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx))); in processSimpleIntEq()
1459 Theorem isIntx(isIntegerThm(x)); in normalizeProjectIneqs() local
1462 bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull()); in normalizeProjectIneqs()
1494 isIntAlpha, isIntBeta, isIntx); in normalizeProjectIneqs()
1497 isIntAlpha, isIntBeta, isIntx); in normalizeProjectIneqs()
|
| H A D | theory_arith_new.cpp | 525 Theorem isIntx(isIntegerThm(x)); in processSimpleIntEq() local
526 DebugAssert(!isIntx.isNull(), "right = "+right.toString()); in processSimpleIntEq()
527 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx))); in processSimpleIntEq()
535 Theorem isIntx(isIntegerThm(x)); in processSimpleIntEq() local
536 DebugAssert(!isIntx.isNull(), "right = "+right.toString() in processSimpleIntEq()
538 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx))); in processSimpleIntEq()
|
| H A D | theory_arith_old.cpp | 760 Theorem isIntx(isIntegerThm(x)); in processSimpleIntEq() local
761 DebugAssert(!isIntx.isNull(), "right = "+right.toString() in processSimpleIntEq()
763 Theorem res(iffMP(eqn, d_rules->intVarEqnConst(eqn.getExpr(), isIntx))); in processSimpleIntEq()
1832 Theorem isIntx(isIntegerThm(x)); in normalizeProjectIneqs() local
1835 bool isInt = !(isIntx.isNull() || isIntBeta.isNull() || isIntAlpha.isNull()); in normalizeProjectIneqs()
1867 isIntAlpha, isIntBeta, isIntx); in normalizeProjectIneqs()
1870 isIntAlpha, isIntBeta, isIntx); in normalizeProjectIneqs()
|
| /dports/java/openjdk8/jdk8u-jdk8u312-b07.1/hotspot/agent/src/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 173 public boolean isIntx() { in isIntx() method in VM.Flag
179 Assert.that(isIntx(), "not a intx flag!"); in getIntx()
198 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk8-jre/jdk8u-jdk8u312-b07.1/hotspot/agent/src/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 173 public boolean isIntx() { in isIntx() method in VM.Flag
179 Assert.that(isIntx(), "not a intx flag!"); in getIntx()
198 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk11/jdk11u-jdk-11.0.13-8-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 201 public boolean isIntx() { in isIntx() method in VM.Flag
207 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
241 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk11-jre/jdk11u-jdk-11.0.13-8-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 201 public boolean isIntx() { in isIntx() method in VM.Flag
207 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
241 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk12/openjdk-jdk12u-jdk-12.0.2-10-4/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 201 public boolean isIntx() { in isIntx() method in VM.Flag
207 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
241 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk13/jdk13u-jdk-13.0.10-1-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 245 public boolean isIntx() { in isIntx() method in VM.Flag
251 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
329 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk15/jdk15u-jdk-15.0.6-1-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 245 public boolean isIntx() { in isIntx() method in VM.Flag
251 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
329 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk16/jdk16u-jdk-16.0.2-7-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 247 public boolean isIntx() { in isIntx() method in VM.Flag
253 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
331 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk17/jdk17u-jdk-17.0.1-12-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 245 public boolean isIntx() { in isIntx() method in VM.Flag
251 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
329 } else if (isIntx()) { in getValue()
|
| /dports/java/openjdk14/jdk14u-jdk-14.0.2-12-1/src/jdk.hotspot.agent/share/classes/sun/jvm/hotspot/runtime/ |
| H A D | VM.java | 244 public boolean isIntx() { in isIntx() method in VM.Flag
250 Assert.that(isIntx(), "not an intx flag!"); in getIntx()
328 } else if (isIntx()) { in getValue()
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_quant/ |
| H A D | theory_quant.cpp | 3731 bool isIntx(const Expr& e, const Rational& x){ in isIntx() function
3745 if(isIntx(e[i][0], -1)){ in getLeft()
3779 if(isIntx(e[i][0], -1)){ in getRight()
3799 if(isIntx(const_expr,0)){ in getRight()
4495 if(isIntx(vl,0)){ in newTopMatchNoSig()
4499 else if(isIntx(vr,0)) { in newTopMatchNoSig()
4802 if(isIntx(vl,0)){ in newTopMatchSig()
4806 else if(isIntx(vr,0)) { in newTopMatchSig()
|