Home
last modified time | relevance | path

Searched refs:getTheorem (Results 1 – 14 of 14) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/search/
H A Dvariable.cpp96 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 Dcircuit.cpp54 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 Dsearch_fast.cpp850 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 Dclause.cpp142 os << "](" << c.getTheorem() in operator <<()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dvariable.h73 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 Dclause.h117 const Theorem& getTheorem() const { in getTheorem() function
H A Dexpr.h466 const Theorem& getTheorem() const;
1142 inline const Theorem& Expr::getTheorem() const { in getTheorem() function
1146 return d_expr->getTheorem(); in getTheorem()
H A Dexpr_value.h405 virtual const Theorem& getTheorem() const { in getTheorem() function
/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dminisat_types.h153 CVC3::Theorem getTheorem() const { return d_theorem; }; in getTheorem() function
H A Dminisat_derivation.cpp311 FatalAssert(!clause->getTheorem().isNull(), "createProof: leaf without clause"); in createProof()
312 proofNodes[clause->id()] = proof->registerLeaf(clause->getTheorem()); in createProof()
H A Dminisat_solver.cpp513 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 DExpr_impl.cpp257 return embed_const_ref<Theorem>(env, &expr->getTheorem());
H A DExpr.java536 public Theorem getTheorem() throws Cvc3Exception { in getTheorem() method in Expr
/dports/math/cvc3/cvc3-2.4.1/src/expr/
H A Dexpr.cpp443 os << space << "{Theorem: " << getTheorem().toString() << "}"; in printAST()