arith_theorem_producer3.cpp File Reference

#include "arith_theorem_producer3.h"
#include "theory_core.h"
#include "theory_arith3.h"

Include dependency graph for arith_theorem_producer3.cpp:

Go to the source code of this file.

Classes

• class MonomialLess

Defines

• #define _CVC3_TRUSTED_
• #define CLASS_NAME   "ArithTheoremProducer3"

Typedefs

• typedef map< Expr, Rational,
  MonomialLess > MonomMap

---

Define Documentation

#define _CVC3_TRUSTED_

Definition at line 30 of file arith_theorem_producer3.cpp.

#define CLASS_NAME   "ArithTheoremProducer3"

Definition at line 52 of file arith_theorem_producer3.cpp.

---

Typedef Documentation

typedef map<Expr,Rational,MonomialLess> MonomMap

Definition at line 426 of file arith_theorem_producer3.cpp.