Searched refs:getTheorem (Results 1 – 14 of 14) sorted by relevance
/dports/math/cvc3/cvc3-2.4.1/src/search/ |
H A D | variable.cpp | 96 Variable::getTheorem() const { in getTheorem() function in CVC3::Variable 99 return d_val->getTheorem(); in getTheorem() 166 if(!getTheorem().isNull()) return getTheorem(); in deriveThmRec() 180 thm = d_val->d_vm->getRules()->unitProp(thms, c.getTheorem(), idx); in deriveThmRec() 182 thm = d_val->d_vm->getRules()->conflictRule(thms, c.getTheorem()); in deriveThmRec() 280 if(!getTheorem().isNull()) d_thm->set(Theorem(), scope); in setValue() 341 if(!v.getTheorem().isNull()) in operator <<() 342 os << "; " << v.getTheorem(); in operator <<()
|
H A D | circuit.cpp | 54 const Theorem& t0 = d_lits[0].getTheorem(); in propagate() 55 const Theorem& t1 = d_lits[1].getTheorem(); in propagate() 56 const Theorem& t2 = d_lits[2].getTheorem(); in propagate() 57 const Theorem& t3 = d_lits[3].getTheorem(); in propagate()
|
H A D | search_fast.cpp | 850 thms.push_back(c[i].getTheorem()); in propagate() 851 d_conflictTheorem = d_rules->conflictRule(thms,c.getTheorem()); in propagate() 920 thms.push_back(c[i].getTheorem()); in unitPropagation() 925 Theorem thm(d_rules->unitProp(thms,c.getTheorem(),idx)); in unitPropagation() 975 Theorem thm = i->getTheorem(); in fixConflict() 1655 thm = simplify(((Clause)d_clauses[i]).getTheorem()); in checkValidMain()
|
H A D | clause.cpp | 142 os << "](" << c.getTheorem() in operator <<()
|
/dports/math/cvc3/cvc3-2.4.1/src/include/ |
H A D | variable.h | 73 const Theorem& getTheorem() const; 159 const Theorem& getTheorem() const { return d_var.getTheorem(); } in getTheorem() function 275 const Theorem& getTheorem() const { in getTheorem() function
|
H A D | clause.h | 117 const Theorem& getTheorem() const { in getTheorem() function
|
H A D | expr.h | 466 const Theorem& getTheorem() const; 1142 inline const Theorem& Expr::getTheorem() const { in getTheorem() function 1146 return d_expr->getTheorem(); in getTheorem()
|
H A D | expr_value.h | 405 virtual const Theorem& getTheorem() const { in getTheorem() function
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | minisat_types.h | 153 CVC3::Theorem getTheorem() const { return d_theorem; }; in getTheorem() function
|
H A D | minisat_derivation.cpp | 311 FatalAssert(!clause->getTheorem().isNull(), "createProof: leaf without clause"); in createProof() 312 proofNodes[clause->id()] = proof->registerLeaf(clause->getTheorem()); in createProof()
|
H A D | minisat_solver.cpp | 513 addClause(literals, clause.getTheorem(), clause.id()); in addClause() 515 addClause(literals, clause.getTheorem(), nextClauseID()); in addClause()
|
/dports/math/cvc3/cvc3-2.4.1/java/src/cvc3/ |
H A D | Expr_impl.cpp | 257 return embed_const_ref<Theorem>(env, &expr->getTheorem());
|
H A D | Expr.java | 536 public Theorem getTheorem() throws Cvc3Exception { in getTheorem() method in Expr
|
/dports/math/cvc3/cvc3-2.4.1/src/expr/ |
H A D | expr.cpp | 443 os << space << "{Theorem: " << getTheorem().toString() << "}"; in printAST()
|