$INCSAT_SATISFIABLE = INCSAT_SATISFIABLE
[ Constant: int ]
$INCSAT_UNSATISFIABLE = INCSAT_UNSATISFIABLE
[ Constant: int ]
$INCSAT_UNSOLVED = INCSAT_UNSOLVED
[ Constant: int ]
$INCSAT_GREATER_EQUAL = INCSAT_GREATER_EQUAL
[ Constant: int ]
$INCSAT_LESS_EQUAL = INCSAT_LESS_EQUAL
[ Constant: int ]
$INCSAT_EQUAL = INCSAT_EQUAL
[ Constant: int ]
$INCSAT_TRUE = INCSAT_TRUE
[ Constant: int ]
$INCSAT_FALSE = INCSAT_FALSE
[ Constant: int ]
$INCSAT_UNASSIGNED = INCSAT_UNASSIGNED
[ Constant: int ]
$INCSAT_CONSTR_UNRESOLVED = INCSAT_CONSTR_UNRESOLVED
[ Constant: int ]
$INCSAT_CONSTR_PENDING_IMPLY = INCSAT_CONSTR_PENDING_IMPLY
[ Constant: int ]
$INCSAT_CONSTR_SATISFIED = INCSAT_CONSTR_SATISFIED
[ Constant: int ]
$INCSAT_CONSTR_UNSATISFIED = INCSAT_CONSTR_UNSATISFIED
[ Constant: int ]
$Incsat_Info
[ Global : Messenger Info ]
$Incsat_Error
[ Global : Messenger Error ]
$Incsat_Warn
[ Global : Messenger Warn ]
$Incsat_Debug
[ Global : Messenger Debug ]
SetInfoVerbosity(verbosity);
[ returns void ]
SetInfoVerbosity(verbosity)
SetWarnVerbosity(verbosity);
[ returns void ]
SetWarnVerbosity(verbosity)
SetDebugVerbosity(verbosity);
[ returns void ]
SetDebugVerbosity(verbosity)
new_Ostream(filename,heading);
[ returns std::ostream * ]
delete_Ostream(fout);
[ returns void ]
new_Istream(filename);
[ returns std::istream * ]
delete_Istream(fin);
[ returns void ]
new_IncsatState();
[ Constructor: returns IncsatState * ]
delete_IncsatState(self);
[ Destructor: returns void ]
IncsatState_IsSatisfied(self);
[ Member : returns bool ]
IncsatState_IsConflicted(self);
[ Member : returns bool ]
IncsatState_IsPendingImplication(self);
[ Member : returns bool ]
IncsatState_GetVariable(self,name);
[ Member : returns Variable ]
IncsatState_ResetAssignments(self);
[ Member : returns void ]
Get rid of all learned constraints.
IncsatState_ResetConflictGeneratedConstraints(self);
[ Member : returns void ]
Selectively get rid of conflict clauses
IncsatState_RemoveConflictGeneratedConstraints(self,limit);
[ Member : returns void ]
IncsatState_GetNumVariables(self);
[ Member : returns int ]
IncsatState_GetNumAssignedVariables(self);
[ Member : returns int ]
IncsatState_GetNumConstraints(self);
[ Member : returns int ]
IncsatState_GetImpl(self);
[ Member : returns IncsatStateImpl * ]
IncsatState_DumpImplicationGraph(self);
[ Member : returns void ]
IncsatState_DumpIGraph(self,fname);
[ Member : returns void ]
delete_DecisionEngine(self);
[ Destructor: returns void ]
DecisionEngine_Decide(self,state);
[ Member : returns bool ]
DecisionEngine_GetDecisionCnt(self);
[ Member : returns int ]
new_DecisionEngineDlcs();
[ Constructor: returns DecisionEngineDlcs * ]
delete_DecisionEngineDlcs(self);
[ Destructor: returns void ]
DecisionEngineDlcs_GetImpl(self);
[ Member : returns DecisionEngineImpl * ]
DecisionEngineDlcs_Decide(self,state);
[ Member : returns bool ]
new_DecisionEngineDlis();
[ Constructor: returns DecisionEngineDlis * ]
delete_DecisionEngineDlis(self);
[ Destructor: returns void ]
DecisionEngineDlis_GetImpl(self);
[ Member : returns DecisionEngineImpl * ]
new_DecisionEngineFixed();
[ Constructor: returns DecisionEngineFixed * ]
delete_DecisionEngineFixed(self);
[ Destructor: returns void ]
DecisionEngineFixed_GetImpl(self);
[ Member : returns DecisionEngineImpl * ]
DecisionEngineFixed_Decide(self,state);
[ Member : returns bool ]
new_DimacsParser(inputStream,state,strict);
[ Constructor: returns DimacsParser * ]
delete_DimacsParser(self);
[ Destructor: returns void ]
DimacsParser_Parse(self);
[ Member : returns int ]
ConflictAnalysisEngine_Backtrack(self,state);
[ Member : returns bool ]
ConflictAnalysisEngine_GetBacktrackCnt(self);
[ Member : returns int ]
new_ConflictEngineNonchrono();
[ Constructor: returns ConflictEngineNonchrono * ]
delete_ConflictEngineNonchrono(self);
[ Destructor: returns void ]
ConflictEngineNonchrono_Backtrack(self,state);
[ Member : returns bool ]
ImplicationEngine_Imply(self,state);
[ Member : returns void ]
ImplicationEngine_GetImplicationCnt(self);
[ Member : returns int ]
new_ImplicationEngineBcp();
[ Constructor: returns ImplicationEngineBcp * ]
delete_ImplicationEngineBcp(self);
[ Destructor: returns void ]
ImplicationEngineBcp_GetImpl(self);
[ Member : returns ImplicationEngineImpl * ]
ImplicationEngineBcp_Imply(self,state);
[ Member : returns void ]
new_ImplicationEngineOneBcp();
[ Constructor: returns ImplicationEngineOneBcp * ]
delete_ImplicationEngineOneBcp(self);
[ Destructor: returns void ]
ImplicationEngineOneBcp_GetImpl(self);
[ Member : returns ImplicationEngineImpl * ]
ImplicationEngineOneBcp_Imply(self,state);
[ Member : returns void ]
delete_Constraint(self);
[ Destructor: returns void ]
Virtual -- base class
Constraint_GetStatus(self);
[ Member : returns ConstraintStatusType ]
Constraint_Print(self);
[ Member : returns void ]
Writes the constraint to the Info stream.
Constraint_GetString(self);
[ Member : returns delete_this_char * ]
GetString()
new_CnfConstraint(IncsatState *);
[ Constructor: returns CnfConstraint * ]
delete_CnfConstraint(self);
[ Destructor: returns void ]
Definitely should be virtual -- base class
CnfConstraint_GetImpl(self);
[ Member : returns ConstraintImpl * ]
CnfConstraint_GetStatus(self);
[ Member : returns ConstraintStatusType ]
CnfConstraint_AddLiteral(self,pVar,sign);
[ Member : returns void ]
new_ConstraintPseudoBoolean(state,constr_type);
[ Constructor: returns ConstraintPseudoBoolean * ]
delete_ConstraintPseudoBoolean(self);
[ Destructor: returns void ]
ConstraintPseudoBoolean_AddTerm(self,pVar,literalSign,coefficient);
[ Member : returns void ]
ConstraintPseudoBoolean_SetRhs(self,rhs);
[ Member : returns void ]
ConstraintPseudoBoolean_GetStatus(self);
[ Member : returns ConstraintStatusType ]
new_Variable(name,decisionVariable,state);
[ Constructor: returns Variable * ]
The Variable(VariableImpl) constructor is for Incsat library use only! Variable(VariableImpl *implementation);
delete_Variable(self);
[ Destructor: returns void ]
Variable_GetName(self);
[ Member : returns char * ]
Variable_GetValue(self);
[ Member : returns VarValueType ]
new_Incsat(state,conflictEngine);
[ Constructor: returns Incsat * ]
delete_Incsat(self);
[ Destructor: returns void ]
Incsat_SetDecisionEngine(self,decisionEngine);
[ Member : returns void ]
Set the Implication engine.
Incsat_SetImplicationEngine(self,implicationEngine);
[ Member : returns void ]
Incsat_SetTimeLimit(self,seconds);
[ Member : returns void ]
Incsat_Solve(self);
[ Member : returns SatResultType ]
Incsat_SolveDecisionLimited(self,maxDecisions);
[ Member : returns SatResultType ]
Incsat_CreateSnapshot(self);
[ Member : returns int ]
Restore the search state to match the snapshot specified. Return value indicates only whether the snapshot was valid, and does not indicated whether the restored state actually matches the snapshot.
Incsat_RestoreSnapshot(self,snapshotId);
[ Member : returns bool ]
Release the resources associated with the specified snapshot.
Incsat_DeleteSnapshot(self,snapshotId);
[ Member : returns void ]
new_Messenger(os,verbosity,header);
[ Constructor: returns Messenger * ]
delete_Messenger(self);
[ Destructor: returns void ]
Messenger_SetOstream(self,os);
[ Member : returns void ]
Messenger_SetVerbosity(self,verbosity);
[ Member : returns void ]
Messenger_SetHeader(self,header);
[ Member : returns void ]
Messenger_Out(self);
[ Member : returns std::ostream * ]
Messenger_GetOstream(self);
[ Member : returns std::ostream * ]