Home
last modified time | relevance | path

Searched refs:sat_solver (Results 1 – 25 of 153) sorted by relevance

1234567

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/
H A DsatSolver.h41 typedef struct sat_solver_t sat_solver; typedef
43 extern sat_solver* sat_solver_new(void);
44 extern sat_solver* zsat_solver_new_seed(double seed);
45 extern void sat_solver_delete(sat_solver* s);
49 extern int sat_solver_simplify(sat_solver* s);
56 extern void sat_solver_pop(sat_solver* s);
58 extern void sat_solver_restart( sat_solver* s );
62 extern int sat_solver_nvars(sat_solver* s);
63 extern int sat_solver_nclauses(sat_solver* s);
65 extern double sat_solver_memory(sat_solver* s);
[all …]
H A DsatSolver.c1017 int sat_solver_propagate(sat_solver* s) in sat_solver_propagate()
1135 sat_solver* sat_solver_new(void) in sat_solver_new()
1137 sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver)); in sat_solver_new()
1202 sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver)); in zsat_solver_new_seed()
1265 int sat_solver_addvar(sat_solver* s) in sat_solver_addvar()
1339 void sat_solver_delete(sat_solver* s) in sat_solver_delete()
1480 double Mem = sizeof(sat_solver); in sat_solver_memory()
1513 int sat_solver_simplify(sat_solver* s) in sat_solver_simplify()
2043 void sat_solver_pop(sat_solver* s) in sat_solver_pop()
2367 int sat_solver_nvars(sat_solver* s) in sat_solver_nvars()
[all …]
H A DsatTrace.c53 void Sat_SolverTraceStart( sat_solver * pSat, char * pName ) in Sat_SolverTraceStart()
73 void Sat_SolverTraceStop( sat_solver * pSat ) in Sat_SolverTraceStop()
95 void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ) in Sat_SolverTraceWrite()
/dports/math/py-or-tools/or-tools-9.2/ortools/sat/
H A Dprobing.cc282 sat_solver->SetAssumptionLevel(0); in LookForTrivialSatSolution()
310 sat_solver->SetParameters(new_params); in LookForTrivialSatSolution()
311 sat_solver->ResetDecisionHeuristic(); in LookForTrivialSatSolution()
337 sat_solver->ResetDecisionHeuristic(); in LookForTrivialSatSolution()
351 return sat_solver->FinishPropagation(); in LookForTrivialSatSolution()
361 sat_solver->SetAssumptionLevel(0); in FailedLiteralProbingRound()
447 sat_solver->Decisions()[sat_solver->CurrentDecisionLevel() - 1] in FailedLiteralProbingRound()
474 sat_solver->Backtrack(sat_solver->CurrentDecisionLevel() - 1); in FailedLiteralProbingRound()
540 sat_solver->Backtrack(level - 1); in FailedLiteralProbingRound()
726 sat_solver->AddUnitClause(literal); in FailedLiteralProbingRound()
[all …]
H A DBUILD.bazel205 ":sat_solver",
281 ":sat_solver",
495 ":sat_solver",
512 ":sat_solver",
573 ":sat_solver",
662 ":sat_solver",
700 ":sat_solver",
718 ":sat_solver",
746 ":sat_solver",
764 ":sat_solver",
[all …]
H A Dinteger_search.cc316 SatSolver* sat_solver = model->GetOrCreate<SatSolver>(); in SatSolverHeuristic() local
319 return [sat_solver, trail, decision_policy] { in SatSolverHeuristic()
323 CHECK(!sat_solver->Assignment().LiteralIsAssigned(result)); in SatSolverHeuristic()
465 SatSolver* sat_solver = model->GetOrCreate<SatSolver>(); in RandomizeOnRestartHeuristic() local
536 if (sat_solver->CurrentDecisionLevel() == 0) { in RandomizeOnRestartHeuristic()
929 if (!sat_solver->FinishPropagation()) return sat_solver->UnsatStatus(); in SolveIntegerProblem()
944 if (!sat_solver->RestoreSolverToAssumptionLevel()) { in SolveIntegerProblem()
945 return sat_solver->UnsatStatus(); in SolveIntegerProblem()
972 sat_solver->CurrentDecisionLevel() == 0 && in SolveIntegerProblem()
980 DCHECK_EQ(sat_solver->CurrentDecisionLevel(), 0); in SolveIntegerProblem()
[all …]
H A Doptimization.cc1082 sat_solver->Backtrack(0); in MinimizeIntegerVariableWithLinearScanAndLazyEncoding()
1113 sat_solver->Backtrack(0); in RestrictObjectiveDomainWithBinarySearch()
1148 sat_solver->Backtrack(0); in RestrictObjectiveDomainWithBinarySearch()
1165 sat_solver->Backtrack(0); in RestrictObjectiveDomainWithBinarySearch()
1181 sat_solver->Backtrack(0); in RestrictObjectiveDomainWithBinarySearch()
1787 sat_solver->Backtrack(0); in MinimizeWithHittingSetAndLazyEncoding()
1788 sat_solver->SetAssumptionLevel(0); in MinimizeWithHittingSetAndLazyEncoding()
1863 sat_solver->Backtrack(0); in MinimizeWithHittingSetAndLazyEncoding()
1864 sat_solver->SetAssumptionLevel(0); in MinimizeWithHittingSetAndLazyEncoding()
1917 sat_solver->Backtrack(0); in MinimizeWithHittingSetAndLazyEncoding()
[all …]
/dports/math/py-or-tools/or-tools-9.2/ortools/bop/
H A Dbop_util.cc36 sat::SatSolver* sat_solver) { in InternalLoadStateProblemToSatSolver() argument
37 const bool first_time = (sat_solver->NumVariables() == 0); in InternalLoadStateProblemToSatSolver()
39 sat_solver->SetNumVariables( in InternalLoadStateProblemToSatSolver()
43 sat_solver->Backtrack(0); in InternalLoadStateProblemToSatSolver()
49 if (!sat_solver->AddUnitClause( in InternalLoadStateProblemToSatSolver()
59 !LoadBooleanProblem(problem_state.original_problem(), sat_solver)) { in InternalLoadStateProblemToSatSolver()
73 sat::Coefficient(problem_state.upper_bound() - 1), sat_solver)) { in InternalLoadStateProblemToSatSolver()
78 sat_solver->TrackBinaryClauses(true); in InternalLoadStateProblemToSatSolver()
82 sat_solver->ClearNewlyAddedBinaryClauses(); in InternalLoadStateProblemToSatSolver()
89 const ProblemState& problem_state, sat::SatSolver* sat_solver) { in LoadStateProblemToSatSolver() argument
[all …]
H A Dbop_lns.cc169 sat::SatSolver* sat_solver, TimeLimit* time_limit) { in UseLinearRelaxationForSatAssignmentPreference() argument
201 sat_solver->SetAssignmentPreference( in UseLinearRelaxationForSatAssignmentPreference()
346 sat::SatSolver sat_solver; in Optimize() local
347 sat_solver.SetParameters(params); in Optimize()
351 sat_solver.SetNumVariables(problem.num_variables()); in Optimize()
362 if (!LoadBooleanProblem(problem, &sat_solver)) { in Optimize()
370 parameters, problem, &sat_solver, time_limit)) { in Optimize()
379 &sat_solver)) { in Optimize()
386 const sat::SatSolver::Status status = sat_solver.Solve(); in Optimize()
390 SatAssignmentToBopSolution(sat_solver.Assignment(), in Optimize()
[all …]
H A DBUILD.bazel44 "//ortools/sat:sat_solver",
60 "//ortools/sat:sat_solver",
99 "//ortools/sat:sat_solver",
131 "//ortools/sat:sat_solver",
157 "//ortools/sat:sat_solver",
177 "//ortools/sat:sat_solver",
207 "//ortools/sat:sat_solver",
240 "//ortools/sat:sat_solver",
273 "//ortools/sat:sat_solver",
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/
H A DbmcClp.c205 sat_solver * pSat; in Bmc_CollapseIrredundant()
278 sat_solver * pSat; in Bmc_CollapseIrredundantFull()
679 sat_solver * pSat[3] = { in Bmc_CollapseOneInt2()
869 …sat_solver * pSat[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf… in Bmc_CollapseOneOld()
870 …sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf… in Bmc_CollapseOneOld()
1040 Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat0, sat_solver * pSat1, sat_solver * pSat2, sat_s… in Bmc_CollapseOne_int3()
1201 sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); in Bmc_CollapseOne3()
1202 sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); in Bmc_CollapseOne3()
1203 sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); in Bmc_CollapseOne3()
1204 sat_solver * pSat3 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); in Bmc_CollapseOne3()
[all …]
H A DbmcExpand.c51 int Abc_ObjExpandCubesTry( Vec_Str_t * vSop, sat_solver * pSat, Vec_Int_t * vVars ) in Abc_ObjExpandCubesTry()
53 …extern int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec… in Abc_ObjExpandCubesTry()
95 sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0); in Abc_ObjExpandCubes()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/opt/sbd/
H A DsbdInt.h104 extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet…
105 extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int P…
106 extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, wo…
107 extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConst…
H A DsbdLut.c54 int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 ) in Sbd_ProblemAddClauses()
101 void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * p… in Sbd_ProblemAddClausesInit()
192 …extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int … in Sbd_ProblemSolve()
197 …sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoot… in Sbd_ProblemSolve()
198 sat_solver * pSatQbf = sat_solver_new(); in Sbd_ProblemSolve()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/opt/res/
H A DresSat.c33 extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl );
34 extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl );
35 extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fComp…
55 sat_solver * pSat; in Res_SatProveUnsat()
143 sat_solver * pSat; in Res_SatSimulateConstr()
216 sat_solver * pSat; in Res_SatSimulate()
238 pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet ); in Res_SatSimulate()
338 int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl ) in Res_SatAddConst1()
357 int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) in Res_SatAddEqual()
385 int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) in Res_SatAddAnd()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/int/
H A DintUtil.c50 sat_solver * pSat; in Inter_ManCheckInitialState()
54 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 ); in Inter_ManCheckInitialState()
88 sat_solver * pSat; in Inter_ManCheckAllStates()
92 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); in Inter_ManCheckAllStates()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/
H A DpdrSat.c45 sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) in Pdr_ManCreateSolver()
47 sat_solver * pSat; in Pdr_ManCreateSolver()
77 sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ) in Pdr_ManFetchSolver()
79 sat_solver * pSat; in Pdr_ManFetchSolver()
181 sat_solver * pSat; in Pdr_ManSetPropertyOutput()
215 sat_solver * pSat; in Pdr_ManSolverAddClause()
238 sat_solver * pSat; in Pdr_ManCollectValues()
264 sat_solver * pSat; in Pdr_ManCheckCubeCs()
294 sat_solver * pSat; in Pdr_ManCheckCube()
H A DpdrCnf.c80 sat_solver * pSat = Pdr_ManSolver(p, k); in Pdr_ObjSatVar2FindOrAdd()
101 sat_solver * pSat; in Pdr_ObjSatVar2()
181 sat_solver * pSat = Pdr_ManSolver(p, k); in Pdr_ObjSatVar2FindOrAdd()
203 sat_solver * pSat; in Pdr_ObjSatVar2()
355 static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit ) in Pdr_ManNewSolver1()
371 pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit ); in Pdr_ManNewSolver1()
389 static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit ) in Pdr_ManNewSolver2()
439 sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit ) in Pdr_ManNewSolver()
H A DpdrInt.h44 #define sat_solver satoko_t macro
181 static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEnt… in Pdr_ManSolver()
202 extern sat_solver * Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit );
220 extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
221 extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/int2/
H A Dint2Core.c99 sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap ) in Int2_ManPreparePrefix()
102 sat_solver * pSat; in Int2_ManPreparePrefix()
110 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); in Int2_ManPreparePrefix()
132 sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, V… in Int2_ManPrepareSuffix()
137 sat_solver * pSat; in Int2_ManPrepareSuffix()
148 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); in Int2_ManPrepareSuffix()
197 Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuf… in Int2_ManComputePreimage()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/
H A DabcSat.c37 static sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes );
58 sat_solver * pSat; in Abc_NtkMiterSat()
75 pSat = (sat_solver *)Abc_NtkMiterSatCreate( pNtk, 0 ); in Abc_NtkMiterSat()
181 int Abc_NtkClauseTriv( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) in Abc_NtkClauseTriv()
201 int Abc_NtkClauseTop( sat_solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars ) in Abc_NtkClauseTop()
469 int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk ) in Abc_NtkMiterSatCreateInt()
634 sat_solver * pSat; in Abc_NtkMiterSatCreate()
767 int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) in Abc_NodeAddClausesTop()
840 sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes ) in Abc_NtkMiterSatCreateLogic()
842 sat_solver * pSat; in Abc_NtkMiterSatCreateLogic()
[all …]
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/
H A DgiaSatMap.c39 sat_solver * pSat; // SAT solver
225 static inline int sat_solver_add_and1( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp… in sat_solver_add_and1()
249 static inline int sat_solver_add_and2( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp… in sat_solver_add_and2()
283 static inline void Sbm_AddSorter( sat_solver * p, int * pVars, int i, int k, int * pnVars ) in Sbm_AddSorter()
308 static inline void Sbm_AddCardinConstrMerge( sat_solver * p, int * pVars, int lo, int hi, int r, in… in Sbm_AddCardinConstrMerge()
325 static inline void Sbm_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnV… in Sbm_AddCardinConstrRange()
337 int Sbm_AddCardinConstrPairWise( sat_solver * p, Vec_Int_t * vVars, int K ) in Sbm_AddCardinConstrPairWise()
344 sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars ) in Sbm_AddCardinSolver()
349 sat_solver * pSat = sat_solver_new(); in Sbm_AddCardinSolver()
361 sat_solver * pSat = Sbm_AddCardinSolver( LogN, &vVars ); in Sbm_AddCardinConstrTest()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/cnf/
H A DcnfMan.c372 sat_solver * pSat = (sat_solver *)pSolver; in Cnf_DataWriteIntoSolverInt()
573 sat_solver * pSat = (sat_solver *)p; in Cnf_DataWriteOrClause()
629 sat_solver * pSat = (sat_solver *)p; in Cnf_DataWriteAndClauses()
696 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) in Cnf_DataAddXorClause()
702 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) in Cnf_DataAddXorClause()
708 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) in Cnf_DataAddXorClause()
714 if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) ) in Cnf_DataAddXorClause()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/wlc/
H A Dwlc.c142 void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps,… in Wlc_BlastFullAdderCtrlCnf()
195 void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec… in Wlc_BlastMultiplierCnf()
215 sat_solver * Wlc_BlastMultiplierCnfMain( int nBits ) in Wlc_BlastMultiplierCnfMain()
226 sat_solver * pSat = sat_solver_new(); in Wlc_BlastMultiplierCnfMain()
256 sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits ); in Wlc_BlastMultiplierCnfTest()
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/fra/
H A DfraIndVer.c49 sat_solver * pSat; in Fra_InvariantVerify()
78 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 1 ); in Fra_InvariantVerify()
99 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames + 1, 0 ); in Fra_InvariantVerify()

1234567