arith_theorem_producer.cpp File Reference

#include "arith_theorem_producer.h"
#include "theory_core.h"
#include "theory_arith_new.h"

Go to the source code of this file.

Classes

• class MonomialLess

Defines

• #define _CVC3_TRUSTED_
• #define CLASS_NAME   "ArithTheoremProducer"

Typedefs

• typedef map< Expr, Rational,
  MonomialLess > MonomMap

---

Detailed Description

Author: Vijay Ganesh, Sergey Berezin

Created: Dec 13 02:09:04 GMT 2002

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file arith_theorem_producer.cpp.

---

Define Documentation

#define _CVC3_TRUSTED_

Definition at line 30 of file arith_theorem_producer.cpp.

#define CLASS_NAME   "ArithTheoremProducer"

Definition at line 52 of file arith_theorem_producer.cpp.

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

---

Typedef Documentation

typedef map<Expr,Rational,MonomialLess> MonomMap

Definition at line 432 of file arith_theorem_producer.cpp.