SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
#include <carl-common/datastructures/Bitset.h>
#include <smtrat-common/smtrat-common.h>
#include <iostream>
#include <map>
Go to the source code of this file.
Data Structures | |
class | smtrat::mcsat::arithmetic::Covering |
Semantics: The space is divided into a number of intervals: (-oo,a)[a,a](a,b)[b,b](b,oo) A bit is set if the constraints refutes the corresponding interval. More... | |
Namespaces | |
smtrat | |
Class to create the formulas for axioms. | |
smtrat::mcsat | |
smtrat::mcsat::arithmetic | |
Functions | |
std::ostream & | smtrat::mcsat::arithmetic::operator<< (std::ostream &os, const Covering &ri) |