Home
last modified time | relevance | path

Searched refs:num_implications (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dxchaff_solver.h134 int num_implications; member
280 int num_implications() { return _stats.num_implications; } in num_implications() function
H A Dxchaff.h138 { return _solver->num_implications(); } in GetNumImplications()
H A Dxchaff_solver.cpp89 _stats.num_implications = 0; in CSolver()
303 ++_stats.num_implications ; in set_var_value()
/dports/math/py-or-tools/or-tools-9.2/ortools/sat/
H A Dsat_inprocessing.cc132 << " num_implications: " << implication_graph_->num_implications() in PresolveLoop()
200 << " num_implications: " << implication_graph_->num_implications() in InprocessingRound()
587 if (implication_graph_->num_implications() == 0) return true; in DoOneRound()
620 if (implication_graph_->num_implications() == 0) return true; in ComputeStampsForNextRound()
H A Dcp_model_expand.cc1073 int num_implications = 0; in AddSizeTwoTable() local
1077 [context, &num_clause_added, &num_large_clause_added, &num_implications]( in AddSizeTwoTable()
1083 num_implications++; in AddSizeTwoTable()
1106 << num_large_clause_added << " large clauses, " << num_implications in AddSizeTwoTable()
H A Dclause.h636 int64_t num_implications() const { return num_implications_; } in num_implications() function
H A Dsat_solver.cc141 const bool init = binary_implication_graph_->num_implications() == 0; in AddClauseDuringSearch()
1135 << binary_implication_graph_->num_implications(); in SolveInternal()
1538 binary_implication_graph_->num_implications(), restart_->NumRestarts(), in RunningStatisticsString()