arith_theorem_producer_old.cpp File Reference

#include "arith_theorem_producer_old.h"
#include "theory_core.h"
#include "theory_arith_old.h"
#include <algorithm>

Go to the source code of this file.

Classes

• class MonomialLess

Defines

• #define _CVC3_TRUSTED_
• #define CLASS_NAME   "ArithTheoremProducerOld"

Typedefs

• typedef map< Expr, Rational,
  MonomialLess > MonomMap

---

Define Documentation

#define _CVC3_TRUSTED_

Definition at line 30 of file arith_theorem_producer_old.cpp.

#define CLASS_NAME   "ArithTheoremProducerOld"

Definition at line 53 of file arith_theorem_producer_old.cpp.

Referenced by CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducerOld::sumModM(), and CVC3::ArithTheoremProducerOld::sumMulF().

---

Typedef Documentation

typedef map<Expr,Rational,MonomialLess> MonomMap

Definition at line 427 of file arith_theorem_producer_old.cpp.