115 virtual Clause
AddClause(std::vector<Lit>& lits)=0;
127 virtual Clause
GetClause(
int clauseIndex)=0;
138 virtual void GetClauseLits(Clause clause, std::vector<Lit>* lits)=0;
167 virtual void Reset()=0;
virtual bool SetBudget(int budget)
virtual int GetVarAssignment(Var var)=0
virtual bool SetRandomness(int n)
virtual Lit MakeLit(Var var, int phase)=0
virtual Clause GetNextClause(Clause clause)=0
virtual Var GetVarFromLit(Lit lit)=0
virtual int NumVariables()=0
virtual Clause GetClause(int clauseIndex)=0
virtual void RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie)=0
virtual Var AddVariables(int nvars)=0
virtual bool SetRandSeed(int seed)
virtual bool DisableClauseDeletion()
virtual bool DeleteClause(Clause clause)
virtual SATStatus Satisfiable(bool allowNewClauses=false)=0
virtual int GetNumLiterals()
virtual void GetClauseLits(Clause clause, std::vector< Lit > *lits)=0
virtual SATStatus Continue()=0
virtual Clause GetFirstClause()=0
virtual int GetBudgetUsed()
virtual int GetMaxDLevel()
virtual float GetSATTime()
virtual int GetNumConflicts()
virtual int GetNumDeletedLiterals()
virtual Clause AddClause(std::vector< Lit > &lits)=0
virtual int GetNumDecisions()
virtual int GetNumImplications()
virtual bool SetMemLimit(int mem_limit)
virtual Var GetFirstVar()=0
virtual int GetNumDeletedClauses()
virtual int NumClauses()=0
virtual Var GetVar(int varIndex)=0
virtual void RegisterDeductionHook(void(*f)(void *), void *cookie)=0
virtual void RegisterAssignmentHook(void(*f)(void *, Var, int), void *cookie)=0
virtual int GetNumExtConflicts()
virtual void RegisterDLevelHook(void(*f)(void *, int), void *cookie)=0
static SatSolver * Create()
void PrintStatistics(std::ostream &os=std::cout)
virtual float GetTotalTime()
virtual int GetPhaseFromLit(Lit lit)=0
virtual Var GetNextVar(Var var)=0
virtual bool EnableClauseDeletion()
virtual int GetVarIndex(Var v)=0