SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions
smtrat::mcsat::arithmetic::AssignmentFinder Struct Reference

#include <AssignmentFinder.h>

Public Member Functions

std::optional< AssignmentOrConflict > operator() (const mcsat::Bookkeeping &data, carl::Variable var) const
 
bool active (const mcsat::Bookkeeping &data, const FormulaT &f) const
 

Detailed Description

Definition at line 11 of file AssignmentFinder.h.

Member Function Documentation

◆ active()

bool smtrat::mcsat::arithmetic::AssignmentFinder::active ( const mcsat::Bookkeeping &  data,
const FormulaT &  f 
) const

Definition at line 52 of file AssignmentFinder.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ operator()()

std::optional< AssignmentOrConflict > smtrat::mcsat::arithmetic::AssignmentFinder::operator() ( const mcsat::Bookkeeping &  data,
carl::Variable  var 
) const

Definition at line 10 of file AssignmentFinder.cpp.

Here is the call graph for this function:
The documentation for this struct was generated from the following files: