Lines Matching refs:Variable
78 const Variable v = var(lit); in addClause()
93 llvm::DenseSet<Variable> trueVars;
94 llvm::DenseSet<Variable> falseVars;
99 CNFFormula::CNFFormula(Variable LargestVar) in CNFFormula()
117 llvm::DenseMap<Variable, Atom> &Atomics) { in buildCNF() argument
125 llvm::DenseMap<const Formula *, Variable> FormulaToVar; in buildCNF()
127 Variable NextVar = 1; in buildCNF()
133 Variable Var = NextVar; in buildCNF()
171 const Variable Var = GetVar(F); in buildCNF()
184 const Variable LHS = GetVar(F->operands()[0]); in buildCNF()
185 const Variable RHS = GetVar(F->operands()[1]); in buildCNF()
204 const Variable LHS = GetVar(F->operands()[0]); in buildCNF()
205 const Variable RHS = GetVar(F->operands()[1]); in buildCNF()
224 const Variable Operand = GetVar(F->operands()[0]); in buildCNF()
234 const Variable LHS = GetVar(F->operands()[0]); in buildCNF()
235 const Variable RHS = GetVar(F->operands()[1]); in buildCNF()
247 const Variable LHS = GetVar(F->operands()[0]); in buildCNF()
248 const Variable RHS = GetVar(F->operands()[1]); in buildCNF()