Lines Matching defs:clause
50 /* A conjunctive or disjunctive clause.
52 Each clause maintains an iterator that refers to the current
56 struct clause
61 /* Initialize a clause with an initial term. */
63 clause (tree t)
76 clause (clause const& c)
99 clause, remove but do not replace ITER. Returns a pair
118 the clause, no action is taken, and the current iterator
162 /* Returns true if the clause contains the term T. */
171 /* Returns an iterator to the first clause in the formula. */
178 /* Returns an iterator to the first clause in the formula. */
185 /* Returns an iterator past the last clause in the formula. */
192 /* Returns an iterator past the last clause in the formula. */
218 typedef std::list<clause>::iterator iterator;
219 typedef std::list<clause>::const_iterator const_iterator;
222 single clause. */
243 /* Insert a copy of clause into the formula. This corresponds
246 clause& branch ()
252 /* Returns the position of the current clause. */
259 /* Returns an iterator to the first clause in the formula. */
266 /* Returns an iterator to the first clause in the formula. */
273 /* Returns an iterator past the last clause in the formula. */
280 /* Returns an iterator past the last clause in the formula. */
287 /* Remove the specified clause from the formula. */
295 std::list<clause> m_clauses; /* The list of clauses. */
296 iterator m_current; /* The current clause. */
300 debug (clause& c)
302 for (clause::iterator i = c.begin(); i != c.end(); ++i)
374 is a disjunction, an additional clause is produced. When neither
523 is a conjunction, an additional clause is produced. When neither
586 replace_term (clause& c, tree t)
593 /* Create a new clause in the formula by copying the current
594 clause. In the current clause, the term at CI is replaced
595 by the first operand, and in the new clause, it is replaced
599 branch_clause (formula& f, clause& c1, tree t)
603 clause& c2 = f.branch ();
611 decompose_conjuntion (formula& f, clause& c, tree t, rules r)
622 decompose_disjunction (formula& f, clause& c, tree t, rules r)
632 decompose_atom (clause& c)
637 /* Decompose a term of clause C (in formula F) according to the
641 decompose_term (formula& f, clause& c, tree t, rules r)
658 decompose_clause (formula& f, clause& c, rules r)
665 static bool derive_proof (clause&, tree, rules);
670 derive_proof_for_both_operands (clause& c, tree t, rules r)
680 derive_proof_for_either_operand (clause& c, tree t, rules r)
687 /* Derive a proof of the atomic constraint T in clause C. */
690 derive_atomic_proof (clause& c, tree t)
698 derive_proof (clause& c, tree t, rules r)
801 each (conjunctive) clause in the decomposed LHS implies RHS. */
805 conjunctive normal form and checking that each (disjunctive) clause
Indexes created Wed Apr 29 00:23:26 UTC 2026