24 static Var
mkVar(
int id) { Var v; v.
id = id;
return v; }
25 static Lit
mkLit(
int id) { Lit l; l.
id = id;
return l; }
41 {
return mkVar(varIndex); }
50 {
return mkLit((var.
id << 1)+phase); }
52 {
return mkVar(lit.id >> 1); }
54 {
return lit.id & 1; }
62 for (
unsigned i=0; i< _solver->
clauses().size(); ++i)
67 for (
unsigned i= clause.
id + 1; i< _solver->clauses().size(); ++i)
Clause GetClause(int clauseIndex)
void RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie)
void(* _assignment_hook)(void *, Var, int)
vector< CClause > & clauses(void)
bool SetRandSeed(int seed)
SatSolver::SATStatus Continue()
void set_mem_limit(int s)
void RegisterDecisionHook(int(*f)(void *, bool *), void *cookie)
int GetNumDeletedLiterals()
int GetNumDeletedClauses()
void set_time_limit(float t)
CVariable & variable(int idx)
SatSolver::SATStatus Satisfiable(bool allowNewClauses)
void * _assignment_hook_cookie
Clause GetNextClause(Clause clause)
static Clause mkClause(int id)
void enable_cls_deletion(bool allow)
int & num_deleted_literals()
void GetClauseLits(SatSolver::Clause clause, std::vector< Lit > *lits)
ClauseIdx add_clause(vector< long > &lits, bool addConflicts=true)
bool SetMemLimit(int mem_limit)
void set_random_seed(int seed)
int GetPhaseFromLit(Lit lit)
void RegisterDLevelHook(void(*f)(void *, int), void *cookie)
Var GetVarFromLit(Lit lit)
Var AddVariables(int nvars)
bool SetBudget(int budget)
void RegisterDLevelHook(void(*f)(void *, int), void *cookie)
void * _decision_hook_cookie
void RegisterDeductionHook(void(*f)(void *), void *cookie)
void RegisterAssignmentHook(void(*f)(void *, Var, int), void *cookie)
int add_variables(int new_vars)
void RegisterDeductionHook(void(*f)(void *), void *cookie)
void RegisterAssignmentHook(void(*f)(void *, int, int), void *cookie)
int GetVarAssignment(Var var)
Lit(* _decision_hook)(void *, bool *)
bool SetRandomness(int n)
void set_randomness(int n)
Clause AddClause(std::vector< Lit > &lits)
static void TranslateAssignmentHook(void *cookie, int var, int value)
bool EnableClauseDeletion()
Lit MakeLit(Var var, int phase)
CClause & clause(ClauseIdx idx)
static int TranslateDecisionHook(void *cookie, bool *done)
bool DisableClauseDeletion()
int & num_deleted_clauses()