Home
last modified time | relevance | path

Searched refs:toMinisatClause (Results 1 – 5 of 5) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/prop/minisat/
H A Dminisat.cpp89 void MinisatSatSolver::toMinisatClause(SatClause& clause, in toMinisatClause() function in CVC4::prop::MinisatSatSolver
146 toMinisatClause(clause, minisat_clause); in addClause()
H A Dminisat.h40 static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/
H A Dbvminisat.cpp63 toMinisatClause(clause, minisat_clause); in addClause()
220 void BVMinisatSatSolver::toMinisatClause(SatClause& clause, in toMinisatClause() function in CVC4::prop::BVMinisatSatSolver
H A Dbvminisat.h112 static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/
H A DSolver.cc252 MinisatSatSolver::toMinisatClause(explanation_cl, explanation); in reason()
1017 MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); in propagateTheory()
1033 MinisatSatSolver::toMinisatClause(explanation_cl, explanation); in propagateTheory()