Home
last modified time | relevance | path

Searched refs:reflexivityRule (Results 1 – 25 of 29) sorted by relevance

12

/dports/math/cvc3/cvc3-2.4.1/src/theory_core/
H A Dexpr_transform.cpp84 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 Dtheory.cpp77 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 Dtheory_core.cpp479 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 Dcore_theorem_producer.cpp428 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 Dbryant.cpp606 return d_core->reflexivityRule(T); in dobryant()
/dports/math/cvc3/cvc3-2.4.1/src/theory_array/
H A Dtheory_array.cpp388 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 Dtheory.h159 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 Dcommon_proof_rules.h95 virtual Theorem reflexivityRule(const Expr& a) = 0;
/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dcnf_manager.cpp77 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 Dcommon_theorem_producer.cpp162 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 Dcommon_theorem_producer.h67 Theorem reflexivityRule(const Expr& a);
/dports/math/cvc3/cvc3-2.4.1/src/theory_records/
H A Dtheory_records.cpp67 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 Dtheory_arith3.cpp348 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 Dtheory_arith_new.cpp225 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 Dtheory_arith_old.cpp358 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 Dtheory_arith.cpp33 if (isLeaf(e)) return reflexivityRule(e); in canonRec()
H A Darith_theorem_producer.cpp611 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 Dtheory_bitvector.cpp794 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 Dbitvector_theorem_producer.cpp2350 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 Dtheory_simulate.cpp59 return reflexivityRule(e); in rewrite()
/dports/math/cvc3/cvc3-2.4.1/src/theory_uf/
H A Dtheory_uf.cpp225 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 Dtheory_datatype_lazy.cpp260 d_processQueue.push_back(reflexivityRule(e[0])); in setup()
/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_impl_base.cpp818 res = d_commonRules->reflexivityRule(e); in replaceITE()
/dports/math/cvc3/cvc3-2.4.1/src/vcl/
H A Dvcl.cpp488 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 Dtheory_quant.cpp269 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()

12