Home
last modified time | relevance | path

Searched refs:getExpr (Results 1 – 25 of 1915) sorted by relevance

12345678910>>...77

/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dsearch_theorem_producer.cpp138 Expr c(a_proves_c.getExpr()); in caseSplit()
229 os << i->getExpr() << ",\n"; in conflictClause()
233 os << i->getExpr() << ",\n"; in conflictClause()
251 Expr neg(i->getExpr().negate()); in conflictClause()
288 if(!thm.getExpr().isFalse()) in conflictClause()
304 if(!v.getExpr().isVar()) { in conflictClause()
306 subst[v.getExpr()] = label.getExpr(); in conflictClause()
390 exprs.push_back(i->getExpr()); in cutRule()
514 Expr e(clause.getExpr()); in unitProp()
1111 Expr e(clause.getExpr()); in conflictRule()
[all …]
H A Dsearch_impl_base.cpp382 Expr thetaExpr = theta.getExpr(); in enqueueCNFrec()
394 thetaExpr = theta.getExpr(); in enqueueCNFrec()
404 +theta.getExpr().toString()); in enqueueCNFrec()
411 thetaExpr = theta.getExpr(); in enqueueCNFrec()
492 DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2, in enqueueCNFrec()
494 +thm.getExpr().toString()); in enqueueCNFrec()
511 thm.getExpr(), ")"); in enqueueCNFrec()
543 d_cnfVars[var.getExpr()] = true; in enqueueCNFrec()
602 DebugAssert(thm.getExpr().isAnd() && thm.getExpr().arity()==2, in applyCNFRules()
604 +thm.getExpr().toString()); in applyCNFRules()
[all …]
H A Dsearch_fast.cpp291 simp.getExpr().toString(), ""); in split()
688 DebugAssert(c.watched(k).getExpr() == (!l).getExpr(), in bcp()
760 const Expr& e = thm.getExpr(); in bcp()
902 +inv.getExpr().toString()); in propagate()
931 +thm.getExpr().toString()); in unitPropagation()
976 if(thm.getExpr().isOr()) in fixConflict()
1034 thm.getExpr(), ") {"); in enqueueFact()
1099 return t1.getExpr() == t2.getExpr(); in TheoremEq()
1450 const Expr& e(thm.getExpr()); in addNonLiteralFact()
1549 +l.getExpr().toString()); in addLiteralFact()
[all …]
H A Dvariable.cpp68 Variable::getExpr() const { in getExpr() function in CVC3::Variable
71 return d_val->getExpr(); in getExpr()
184 IF_DEBUG(Expr e(thm.getExpr());) in deriveThmRec()
185 DebugAssert(e == getExpr() in deriveThmRec()
186 || (e.isNot() && e[0] == getExpr()), in deriveThmRec()
283 : c[idx].getExpr());) in setValue()
284 DebugAssert((val > 0 && l == getExpr()) in setValue()
285 || (val < 0 && l.isNot() && l[0] == getExpr()), in setValue()
288 + "):\n expr = " + getExpr().toString() in setValue()
310 Expr e(thm.getExpr()); in setValue()
[all …]
/dports/math/cvc4/CVC4-1.7/src/expr/
H A Darray_store_all.cpp58 d_expr(new Expr(other.getExpr())) {} in ArrayStoreAll()
63 (*d_expr) = other.getExpr(); in operator =()
69 const Expr& ArrayStoreAll::getExpr() const { return *d_expr; } in getExpr() function in CVC4::ArrayStoreAll
73 return getType() == asa.getType() && getExpr() == asa.getExpr(); in operator ==()
84 (getType() == asa.getType() && getExpr() < asa.getExpr()); in operator <()
90 (getType() == asa.getType() && getExpr() <= asa.getExpr()); in operator <=()
104 return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() in operator <<()
109 return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); in operator ()()
/dports/devel/blitz/blitz-1.0.2/blitz/array/
H A Dnewet-macros.h53 return result(blitz::asExpr<T1>::getExpr(d1.unwrap())); \
73 return result(blitz::asExpr<T1>::getExpr(d1.unwrap()), \
74 blitz::asExpr<T2>::getExpr(d2.unwrap())); \
178 return result(blitz::asExpr<T1>::getExpr(d1.unwrap()), \
179 blitz::asExpr<T2>::getExpr(d2.unwrap()), \
180 blitz::asExpr<T3>::getExpr(d3.unwrap()), \
181 blitz::asExpr<T4>::getExpr(d4.unwrap())); \
402 blitz::asExpr<T1>::getExpr(d1.unwrap()), \
403 blitz::asExpr<T2>::getExpr(d2.unwrap()), \
404 blitz::asExpr<T2>::getExpr(d3.unwrap()), \
[all …]
H A Dasexpr.cc46 _bz_typename asExpr<T>::T_expr asExpr<T>::getExpr(const T& x) in getExpr() function in blitz::asExpr
52 asExpr<_bz_ArrayExpr<T> >::getExpr(const T_expr& x) in getExpr() function in blitz::asExpr
58 asExpr<Array<T,N> >::getExpr(const Array<T,N>& x) in getExpr() function in blitz::asExpr
64 asExpr<TinyVector<T,N> >::getExpr(const TinyVector<T,N>& x) in getExpr() function in blitz::asExpr
70 asExpr<TinyMatrix<T,Nr, Nc> >::getExpr(const TinyMatrix<T,Nr,Nc>& x) in getExpr() function in blitz::asExpr
76 asExpr<IndexPlaceholder<N> >::getExpr(const T_expr& x) in getExpr() function in blitz::asExpr
81 asExpr<LeviCivita>::getExpr(T_expr x) in getExpr() function in blitz::asExpr
86 asExpr<Range>::getExpr(T_expr x) in getExpr() function in blitz::asExpr
/dports/devel/wasi-libcxx/llvm-project-13.0.1.src/llvm/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target)
83 Kind = getTargetFixup(MO.getExpr());
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
97 if (MO.getExpr()->getKind() == MCExpr::Target)
98 Kind = getTargetFixup(MO.getExpr());
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
111 if (MO.getExpr()->getKind() == MCExpr::Target)
112 Kind = getTargetFixup(MO.getExpr());
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
125 if (MO.getExpr()->getKind() == MCExpr::Target)
[all …]
/dports/graphics/llvm-mesa/llvm-13.0.1.src/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target) in getBranchSymbolOpValue()
83 Kind = getTargetFixup(MO.getExpr()); in getBranchSymbolOpValue()
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getBranchSymbolOpValue()
97 if (MO.getExpr()->getKind() == MCExpr::Target) in getConstpoolSymbolOpValue()
98 Kind = getTargetFixup(MO.getExpr()); in getConstpoolSymbolOpValue()
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getConstpoolSymbolOpValue()
111 if (MO.getExpr()->getKind() == MCExpr::Target) in getCallSymbolOpValue()
112 Kind = getTargetFixup(MO.getExpr()); in getCallSymbolOpValue()
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getCallSymbolOpValue()
125 if (MO.getExpr()->getKind() == MCExpr::Target) in getBareSymbolOpValue()
[all …]
/dports/lang/rust/rustc-1.58.1-src/src/llvm-project/llvm/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target) in getBranchSymbolOpValue()
83 Kind = getTargetFixup(MO.getExpr()); in getBranchSymbolOpValue()
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getBranchSymbolOpValue()
97 if (MO.getExpr()->getKind() == MCExpr::Target) in getConstpoolSymbolOpValue()
98 Kind = getTargetFixup(MO.getExpr()); in getConstpoolSymbolOpValue()
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getConstpoolSymbolOpValue()
111 if (MO.getExpr()->getKind() == MCExpr::Target) in getCallSymbolOpValue()
112 Kind = getTargetFixup(MO.getExpr()); in getCallSymbolOpValue()
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getCallSymbolOpValue()
125 if (MO.getExpr()->getKind() == MCExpr::Target) in getBareSymbolOpValue()
[all …]
/dports/devel/llvm-devel/llvm-project-f05c95f10fc1d8171071735af8ad3a9e87633120/llvm/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target) in getBranchSymbolOpValue()
83 Kind = getTargetFixup(MO.getExpr()); in getBranchSymbolOpValue()
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getBranchSymbolOpValue()
97 if (MO.getExpr()->getKind() == MCExpr::Target) in getConstpoolSymbolOpValue()
98 Kind = getTargetFixup(MO.getExpr()); in getConstpoolSymbolOpValue()
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getConstpoolSymbolOpValue()
111 if (MO.getExpr()->getKind() == MCExpr::Target) in getCallSymbolOpValue()
112 Kind = getTargetFixup(MO.getExpr()); in getCallSymbolOpValue()
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getCallSymbolOpValue()
125 if (MO.getExpr()->getKind() == MCExpr::Target) in getBareSymbolOpValue()
[all …]
/dports/devel/wasi-compiler-rt13/llvm-project-13.0.1.src/llvm/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target) in getBranchSymbolOpValue()
83 Kind = getTargetFixup(MO.getExpr()); in getBranchSymbolOpValue()
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getBranchSymbolOpValue()
97 if (MO.getExpr()->getKind() == MCExpr::Target) in getConstpoolSymbolOpValue()
98 Kind = getTargetFixup(MO.getExpr()); in getConstpoolSymbolOpValue()
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getConstpoolSymbolOpValue()
111 if (MO.getExpr()->getKind() == MCExpr::Target) in getCallSymbolOpValue()
112 Kind = getTargetFixup(MO.getExpr()); in getCallSymbolOpValue()
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc())); in getCallSymbolOpValue()
125 if (MO.getExpr()->getKind() == MCExpr::Target) in getBareSymbolOpValue()
[all …]
/dports/devel/llvm13/llvm-project-13.0.1.src/llvm/lib/Target/CSKY/MCTargetDesc/
H A DCSKYMCCodeEmitter.h82 if (MO.getExpr()->getKind() == MCExpr::Target)
83 Kind = getTargetFixup(MO.getExpr());
85 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
97 if (MO.getExpr()->getKind() == MCExpr::Target)
98 Kind = getTargetFixup(MO.getExpr());
100 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
111 if (MO.getExpr()->getKind() == MCExpr::Target)
112 Kind = getTargetFixup(MO.getExpr());
114 Fixups.push_back(MCFixup::create(0, MO.getExpr(), Kind, MI.getLoc()));
125 if (MO.getExpr()->getKind() == MCExpr::Target)
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/theorem/
H A Dcommon_theorem_producer.cpp71 args.push_back(phi.getExpr()); in queryTCC()
72 args.push_back(D_phi.getExpr()); in queryTCC()
138 args.push_back(phi.getExpr()); in implIntro3()
142 args.push_back(i->getExpr()); in implIntro3()
210 args.push_back(t.getExpr()); in symmetryRule()
400 + i->getExpr().toString() in substitutivityRule()
565 CHECK_SOUND(!e.getExpr() == not_e.getExpr(), in contradictionRule()
657 CHECK_SOUND(not_not_e.getExpr().isNot() && not_not_e.getExpr()[0].isNot(), in notNotElim()
759 kids.push_back(i->getExpr()); in andIntro()
913 Expr e(not_e.getExpr()[0]); in notToIff()
[all …]
H A Dtheorem_producer.cpp114 kids.push_back(pf.getExpr()); in newPf()
147 kids.push_back(i->getExpr()); in newPf()
180 kids.push_back(i->getExpr()); in newPf()
194 kids.push_back(i->getExpr()); in newPf()
205 kids.push_back(i->getExpr()); in newPf()
216 kids.push_back(pf.getExpr()); in newPf()
229 kids.push_back(i->getExpr()); in newPf()
236 Expr v(label.getExpr()); in newPf()
248 Expr v(label.getExpr()); in newPf()
263 const Expr& v = labels[i].getExpr(); in newPf()
[all …]
H A Dtheorem.cpp68 const Expr& e1 = t1.getExpr(); in compare()
79 else return compare(t1.getExpr(), e2); in compare()
230 Expr Theorem::getExpr() const { in getExpr() function in CVC3::Theorem
237 else return thm()->getExpr(); in getExpr()
264 assumptions.insert(getExpr()); in getAssumptionsRec()
292 Expr e = getExpr(); in GetSatAssumptionsRec()
326 assumptions.insert(getExpr()); in getAssumptionsAndCongRec()
337 hyp.push_back(!thm.getExpr()); in getAssumptionsAndCongRec()
340 const Expr& e = getExpr(); in getAssumptionsAndCongRec()
483 return getExpr().isAbsLiteral(); in isAbsLiteral()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/theory_arith/
H A Dtheory_arith_new.cpp77 const Expr& e = thm.getExpr(); in isIntegerDerive()
283 Expr e(thm.getExpr()); in canonPred()
333 const Expr& e = thm.getExpr(); in doSolve()
618 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2, in processSimpleIntEq()
623 if(newRes.getExpr() != result.getExpr()) result = newRes; in processSimpleIntEq()
657 DebugAssert(result.getExpr().isAnd() && result.getExpr().arity() == 2, in processIntEq()
705 thm.getExpr(), ""); in solvedForm()
793 +eq.getExpr().toString()); in substAndCanonize()
833 const Expr& e = thm.getExpr(); in addToBuffer()
1798 +thm.getExpr().toString()); in update()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtype.h52 const Expr& getExpr() const { return d_expr; } in getExpr() function
80 std::string toString() const { return getExpr().toString(); } in toString()
84 { return t1.getExpr() == t2.getExpr(); }
87 { return t1.getExpr() != t2.getExpr(); }
91 return os << t.getExpr();
H A Dproof.h46 Expr getExpr() const { return d_proof; } // Extract the expr handle in getExpr() function
58 return os << "Proof(" << pf.getExpr() << ")";
62 return pf1.getExpr() == pf2.getExpr();
/dports/java/jaxen/jaxen-1.0-FCS/src/java/main/org/jaxen/expr/
H A DDefaultPredicate.java79 public Expr getExpr() in getExpr() method in DefaultPredicate
91 return "[" + getExpr().getText() + "]"; in getText()
96 return "[(DefaultPredicate): " + getExpr() + "]"; in toString()
101 setExpr( getExpr().simplify() ); in simplify()
106 return getExpr().evaluate( context ); in evaluate()
H A DDefaultUnaryExpr.java80 public Expr getExpr() in getExpr() method in DefaultUnaryExpr
87 return "[(DefaultUnaryExpr): " + getExpr() + "]"; in toString()
92 return "-(" + getExpr().getText() + ")"; in getText()
104 Number number = NumberFunction.evaluate( getExpr().evaluate( context ), in evaluate()
/dports/math/cvc3/cvc3-2.4.1/src/theory_records/
H A Drecords_theorem_producer.cpp160 Expr e = neqThrm.getExpr(); in expandNeq()
164 Expr e0 = e[0].getType().getExpr() , e1 = e[1].getType().getExpr(); in expandNeq()
182 "equation types mismatch \n" + neqThrm.getExpr().toString()); in expandNeq()
207 Expr lhs(eqThrm.getLHS()), e0 = lhs.getType().getExpr(); in expandEq()
208 Expr rhs(eqThrm.getRHS()), e1 = rhs.getType().getExpr(); in expandEq()
213 + eqThrm.getExpr().toString()); in expandEq()
215 "equation types mismatch \n" + eqThrm.getExpr().toString()); in expandEq()
227 "equation types mismatch \n" + eqThrm.getExpr().toString()); in expandEq()
247 eqThrm.getExpr(), eqThrm.getProof()); in expandEq()
258 const vector<Expr>& fields = getFields(tp.getExpr()); in expandRecord()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dcnf_theorem_producer.cpp62 if (!thm.getExpr().isFalse()) { in getSmartClauses()
63 TempVec.push_back(thm.getExpr()); in getSmartClauses()
67 if (thm.getExpr() == assumptions[i].getExpr()) { in getSmartClauses()
74 TempVec.push_back(assumptions[i].getExpr().negate()); in getSmartClauses()
136 if (!thm.getExpr().isFalse()) in learnedClauses()
137 assumptions.push_back(thm.getExpr()); in learnedClauses()
316 pf = newPf("cnf_add_unit", thm.getExpr(), thm.getProof() ); in CNFAddUnit()
318 return newTheorem(thm.getExpr(), thm.getAssumptionsRef(), pf); in CNFAddUnit()
326 pf = newPf("cnf_convert", e, thm.getExpr(), thm.getProof() ); in CNFConvert()
328 DebugAssert(thm.getExpr().isOr(),"convert is not or exprs"); in CNFConvert()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/theory_datatype/
H A Dtheory_datatype.cpp118 ExprMap<unsigned>& c = d_datatypes[t.getExpr()]; in initializeLabels()
204 const Expr& expr = e.getExpr(); in assertFact()
480 Expr funType = cons.getType().getExpr(); in finiteTypeInfo()
569 Expr op = e.getOp().getExpr(); in computeType()
572 if (t.getExpr().getKind() == DATATYPE) { in computeType()
1169 d_getConstantStack[t.getExpr()] = true; in getConstant()
1178 d_getConstantStack.erase(t.getExpr()); in getConstant()
1194 d_getConstantStack.erase(t.getExpr()); in getConstant()
1210 d_getConstantStack.erase(t.getExpr()); in getConstant()
1222 d_getConstantStack.erase(t.getExpr()); in getConstant()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dtheory_bitvector.cpp171 DebugAssert(notE.getExpr().isNot() && (notE.getExpr())[0].isEq(), in bitBlastDisEqn()
175 const Expr& e = (notE.getExpr())[0]; in bitBlastDisEqn()
1625 res.getExpr(), " }"); in rewriteBV()
1863 const Expr& expr = e.getExpr(); in assertFact()
2368 Expr e = thm.getExpr(); in simplifyPendingEq()
2412 Expr e = thm.getExpr(); in generalBitBlast()
2558 if (!thm.getExpr().isTrue()) { in comparebv()
2821 Expr e = t.getExpr(); in solve()
3332 switch(tp.getExpr().getOpKind()) { in computeModelTerm()
3384 switch(tp.getExpr().getOpKind()) { in computeModel()
[all …]

12345678910>>...77