/dports/math/cvc3/cvc3-2.4.1/src/theory_core/ |
H A D | expr_transform.cpp | 84 Theorem res = d_commonRules->reflexivityRule(e); in preprocess() 128 if(e.isTerm()) return d_commonRules->reflexivityRule(e); in pushNegation() 151 Theorem res(d_core->reflexivityRule((neg)? !e : e)); in pushNegationRec() 193 res = d_commonRules->reflexivityRule(!e); in pushNegationRec() 216 res = d_commonRules->reflexivityRule(e); in pushNegationRec() 275 res = d_commonRules->reflexivityRule(e); in pushNegation1() 290 return d_commonRules->reflexivityRule(e); in newPP() 312 thm = d_commonRules->reflexivityRule(e); in specialSimplify() 337 Theorem res = d_commonRules->reflexivityRule(e); in newPPrec() 455 Theorem res = d_commonRules->reflexivityRule(e); in substitute() [all …]
|
H A D | theory.cpp | 77 return reflexivityRule(e); in simplifyOp() 312 if (!e.hasFind()) return reflexivityRule(e); in find() 353 return reflexivityRule(e); in findReduce() 454 return reflexivityRule(e); in updateHelper() 464 Theorem thm = reflexivityRule(e); in setupCC() 514 if (rep.isNull()) return reflexivityRule(e); in rewriteCC() 931 return reflexivityRule(e); in rewriteIte()
|
H A D | theory_core.cpp | 479 return reflexivityRule(e); in rewriteCore() 584 return reflexivityRule(e); in rewriteLitCore() 859 Theorem thm = reflexivityRule(e); in callTheoryPreprocess() 977 thm = reflexivityRule(e); in rewrite() 988 else thm = reflexivityRule(e); in rewrite() 1054 else thm = reflexivityRule(e); in rewrite() 1062 else thm = reflexivityRule(e); in rewrite() 1083 thm = reflexivityRule(e); in rewrite() 1404 return reflexivityRule(e); in simplifyOp() 4302 t.setFind(reflexivityRule(t)); in setupTerm() [all …]
|
H A D | core_theorem_producer.cpp | 428 if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e); in IffToIte() 444 if(e[0] == e[1]) return d_core->getCommonRules()->reflexivityRule(e); in ImpToIte()
|
H A D | bryant.cpp | 606 return d_core->reflexivityRule(T); in dobryant()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_array/ |
H A D | theory_array.cpp | 388 return reflexivityRule(e); in rewrite() 418 return reflexivityRule(e); in rewrite() 429 return reflexivityRule(e); in rewrite() 432 return reflexivityRule(e); in rewrite() 447 return reflexivityRule(e); in rewrite() 470 return reflexivityRule(e); in rewrite() 474 return reflexivityRule(e); in rewrite() 478 return reflexivityRule(e); in rewrite() 483 return reflexivityRule(e); in rewrite() 486 return reflexivityRule(e); in rewrite() [all …]
|
/dports/math/cvc3/cvc3-2.4.1/src/include/ |
H A D | theory.h | 159 virtual Theorem rewrite(const Expr& e) { return reflexivityRule(e); } in rewrite() 164 virtual Theorem theoryPreprocess(const Expr& e) { return reflexivityRule(e); } in theoryPreprocess() 365 virtual Theorem rewriteAtomic(const Expr& e) { return reflexivityRule(e); } in rewriteAtomic() 673 Theorem reflexivityRule(const Expr& a) in reflexivityRule() function 674 { return d_commonRules->reflexivityRule(a); } in reflexivityRule()
|
H A D | common_proof_rules.h | 95 virtual Theorem reflexivityRule(const Expr& a) = 0;
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | cnf_manager.cpp | 77 if (e.isAtomic()) return d_commonRules->reflexivityRule(e); in replaceITErec() 121 else thm = d_commonRules->reflexivityRule(e); in replaceITErec() 142 ret = d_commonRules->reflexivityRule(ine); in concreteThm() 377 if (e0thm.isNull()) e0thm = d_commonRules->reflexivityRule(e[0]); in translateExprRec() 379 if (e1thm.isNull()) e1thm = d_commonRules->reflexivityRule(e[1]); in translateExprRec() 381 if (e2thm.isNull()) e2thm = d_commonRules->reflexivityRule(e[2]); in translateExprRec()
|
/dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
H A D | common_theorem_producer.cpp | 162 Theorem CommonTheoremProducer::reflexivityRule(const Expr& a) { in reflexivityRule() function in CommonTheoremProducer 201 if(a1 == a2) return reflexivityRule(a1); in symmetryRule() 228 if(a1 == a2) return reflexivityRule(a1_eq_a2); in rewriteUsingSymmetry() 269 if(a1 == a3) return reflexivityRule(a1); in transitivityRule() 385 return reflexivityRule(d_tm->getEM()->newLeafExpr(op)); in substitutivityRule() 409 if(e1 == e2) return reflexivityRule(e1); in substitutivityRule() 445 return substitutivityRule(e, thms[0], reflexivityRule(e[1])); in substitutivityRule() 448 return substitutivityRule(e, reflexivityRule(e[0]), thms[0]); in substitutivityRule() 979 return reflexivityRule(e); in rewriteIff() 1282 return iffTrueElim(reflexivityRule(d_em->trueExpr())); in trueTheorem()
|
H A D | common_theorem_producer.h | 67 Theorem reflexivityRule(const Expr& a);
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_records/ |
H A D | theory_records.cpp | 67 res = reflexivityRule(e); in rewriteAux() 79 res = reflexivityRule(e); in rewriteAux() 188 rw = reflexivityRule(e); in rewrite() 200 rw = reflexivityRule(e); in rewrite() 207 rw = reflexivityRule(e); in rewrite() 215 rw = reflexivityRule(e); in rewrite()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/ |
H A D | theory_arith3.cpp | 348 result = reflexivityRule(e); in canon() 351 result = reflexivityRule(e); in canon() 1026 res = reflexivityRule(t); in substAndCanonize() 2008 e.setFind(reflexivityRule(e)); in setupRec() 2395 thm = reflexivityRule(e); in rewrite() 2405 thm = reflexivityRule(e); in rewrite() 2411 thm = reflexivityRule(e); in rewrite() 2437 thm = reflexivityRule(e); in rewrite() 2444 thm = reflexivityRule(e); in rewrite() 2450 thm = reflexivityRule(e); in rewrite() [all …]
|
H A D | theory_arith_new.cpp | 225 else result = reflexivityRule(e); in canon() 233 result = reflexivityRule(e); in canon() 741 Theorem res(reflexivityRule(t)); in substAndCanonize() 753 Theorem res(reflexivityRule(t)); in substAndCanonize() 775 res = reflexivityRule(t); in substAndCanonize() 1259 e.setFind(reflexivityRule(e)); in setupRec() 1260 e.setEqNext(reflexivityRule(e)); in setupRec() 1526 thm = reflexivityRule(e); in normalize() 1594 thm = reflexivityRule(e); in rewrite() 1716 else thm = reflexivityRule(e); in rewrite() [all …]
|
H A D | theory_arith_old.cpp | 358 result = reflexivityRule(e); in canon() 362 result = reflexivityRule(e); in canon() 1005 res = reflexivityRule(t); in substAndCanonize() 2465 e.setFind(reflexivityRule(e)); in setupRec() 3111 thm = reflexivityRule(e); in rewrite() 3122 thm = reflexivityRule(e); in rewrite() 3128 thm = reflexivityRule(e); in rewrite() 3248 thm = reflexivityRule(e); in rewrite() 3255 thm = reflexivityRule(e); in rewrite() 3261 thm = reflexivityRule(e); in rewrite() [all …]
|
H A D | theory_arith.cpp | 33 if (isLeaf(e)) return reflexivityRule(e); in canonRec()
|
H A D | arith_theorem_producer.cpp | 611 return d_theoryArith->reflexivityRule (e); in canonMultMtermMterm() 627 return d_theoryArith->reflexivityRule(e); in canonMultMtermMterm() 974 if (d_theoryArith->isLeaf(e)) return d_theoryArith->reflexivityRule (rat(1)*e); in canonMultOne()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
H A D | theory_bitvector.cpp | 794 res = reflexivityRule(e); in pushNegationRec() 829 thm0 = reflexivityRule(e); in simplifyOp() 854 thm0 = reflexivityRule(e); in simplifyOp() 876 return reflexivityRule(e); in simplifyOp() 972 res = reflexivityRule(e); in rewriteBV() 1206 res = reflexivityRule(e); in rewriteBV() 1219 res = reflexivityRule(e); in rewriteBV() 1483 res = reflexivityRule(e); in rewriteBV() 1615 res = reflexivityRule(e); in rewriteBV() 2497 return reflexivityRule( e ); in generalBitBlast() [all …]
|
H A D | bitvector_theorem_producer.cpp | 2350 return d_theoryBitvector->reflexivityRule(e); in bvplusZeroConcatRule() 2935 return d_theoryBitvector->reflexivityRule(e); in bitwiseConcat() 4261 return d_theoryBitvector->reflexivityRule(e); in extractBVPlus() 4362 return d_theoryBitvector->reflexivityRule(e); in MarkNonSolvableEq() 4714 if (idx == -1) return d_theoryBitvector->reflexivityRule(e); in liftConcatBVMult() 4949 return d_theoryBitvector->reflexivityRule(e); in liftConcatBVPlus() 4959 return d_theoryBitvector->reflexivityRule(e); in liftConcatBVPlus() 4973 if (nonconst) return d_theoryBitvector->reflexivityRule(e); in liftConcatBVPlus() 4980 if (nonzero) return d_theoryBitvector->reflexivityRule(e); in liftConcatBVPlus() 4991 return d_theoryBitvector->reflexivityRule(e); in liftConcatBVPlus()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_simulate/ |
H A D | theory_simulate.cpp | 59 return reflexivityRule(e); in rewrite()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_uf/ |
H A D | theory_uf.cpp | 225 if (e.getType().isBool()) return reflexivityRule(e); in rewrite() 231 return reflexivityRule(e); in rewrite() 548 assignValue(reflexivityRule(e)); in computeModel()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_datatype/ |
H A D | theory_datatype_lazy.cpp | 260 d_processQueue.push_back(reflexivityRule(e[0])); in setup()
|
/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | search_impl_base.cpp | 818 res = d_commonRules->reflexivityRule(e); in replaceITE()
|
/dports/math/cvc3/cvc3-2.4.1/src/vcl/ |
H A D | vcl.cpp | 488 falseExpr().setFind(d_theoryCore->reflexivityRule(falseExpr())); in init() 489 trueExpr().setFind(d_theoryCore->reflexivityRule(trueExpr())); in init()
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_quant/ |
H A D | theory_quant.cpp | 269 return reflexivityRule(e); in rewrite() 2348 return reflexivityRule(e); in theoryPreprocess() 2353 return reflexivityRule(e); in theoryPreprocess() 2378 return reflexivityRule(e); in theoryPreprocess() 2392 return reflexivityRule(e); in theoryPreprocess()
|