Public Member Functions | Static Public Member Functions | Private Attributes

CVC3::ArithTheoremProducerOld Class Reference

#include <arith_theorem_producer_old.h>

Inheritance diagram for CVC3::ArithTheoremProducerOld:
CVC3::ArithProofRules CVC3::TheoremProducer

List of all members.

Public Member Functions

Static Public Member Functions

Private Member Functions

Auxiliary functions for eqElimIntRule()

Methods that compute the subterms used in eqElimIntRule()

Private Attributes


Detailed Description

Definition at line 31 of file arith_theorem_producer_old.h.


Constructor & Destructor Documentation

CVC3::ArithTheoremProducerOld::ArithTheoremProducerOld ( TheoremManager tm,
TheoryArithOld theoryArith 
) [inline]

Constructor.

Definition at line 66 of file arith_theorem_producer_old.h.


Member Function Documentation

Rational ArithTheoremProducerOld::modEq ( const Rational i,
const Rational m 
) [private]

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2429 of file arith_theorem_producer_old.cpp.

References DebugAssert, CVC3::Rational::toString(), and CVC3::TRACE.

Referenced by f(), monomialModM(), and sumModM().

Expr ArithTheoremProducerOld::create_t ( const Expr eqn  )  [private]
Expr ArithTheoremProducerOld::create_t2 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
Expr ArithTheoremProducerOld::create_t3 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
void ArithTheoremProducerOld::sumModM ( std::vector< Expr > &  summands,
const Expr sum,
const Rational m,
const Rational divisor 
) [private]

Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the vector of similar monomials (in 'summands') with coefficients mod(a_i, m). If divide flag is true, the coefficients will be mod(a_i,m)/m.

Definition at line 2445 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), modEq(), monomialModM(), rat(), and CVC3::Rational::toString().

Referenced by create_t(), and create_t2().

Expr ArithTheoremProducerOld::monomialModM ( const Expr e,
const Rational m,
const Rational divisor 
) [private]
void ArithTheoremProducerOld::sumMulF ( std::vector< Expr > &  summands,
const Expr sum,
const Rational m,
const Rational divisor 
) [private]

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2493 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CLASS_NAME, DebugAssert, CVC3::Expr::end(), f(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), monomialMulF(), rat(), and CVC3::Rational::toString().

Referenced by create_t3().

Expr ArithTheoremProducerOld::monomialMulF ( const Expr e,
const Rational m,
const Rational divisor 
) [private]

Compute the special modulus: i - m*floor(i/m+1/2).

Definition at line 2513 of file arith_theorem_producer_old.cpp.

References DebugAssert, f(), CVC3::isMult(), CVC3::multExpr(), rat(), and CVC3::Rational::toString().

Referenced by create_t3(), and sumMulF().

Rational ArithTheoremProducerOld::f ( const Rational i,
const Rational m 
) [private]

Compute floor(i/m+1/2) + mod(i,m).

Definition at line 2438 of file arith_theorem_producer_old.cpp.

References DebugAssert, modEq(), and CVC3::Rational::toString().

Referenced by monomialMulF(), and sumMulF().

Expr ArithTheoremProducerOld::substitute ( const Expr term,
ExprMap< Expr > &  eMap 
) [private]
void ArithTheoremProducerOld::getLeaves ( const Expr e,
std::set< Rational > &  s,
ExprHashMap< bool > &  cache 
) [private]
Type CVC3::ArithTheoremProducerOld::realType (  )  [inline]

Definition at line 71 of file arith_theorem_producer_old.h.

References d_theoryArith, and CVC3::TheoryArith::realType().

Type CVC3::ArithTheoremProducerOld::intType (  )  [inline]

Definition at line 72 of file arith_theorem_producer_old.h.

References d_theoryArith, and CVC3::TheoryArith::intType().

Referenced by eqElimIntRule().

Expr CVC3::ArithTheoremProducerOld::darkShadow ( const Expr lhs,
const Expr rhs 
) [inline]

Construct the dark shadow expression representing lhs <= rhs.

Definition at line 74 of file arith_theorem_producer_old.h.

References d_theoryArith, and CVC3::TheoryArith::darkShadow().

Expr CVC3::ArithTheoremProducerOld::grayShadow ( const Expr v,
const Expr e,
const Rational c1,
const Rational c2 
) [inline]

Construct the gray shadow expression representing c1 <= v - e <= c2.

Alternatively, v = e + i for some i s.t. c1 <= i <= c2

Definition at line 80 of file arith_theorem_producer_old.h.

References d_theoryArith, and CVC3::TheoryArith::grayShadow().

Referenced by darkGrayShadow2ab(), darkGrayShadow2ba(), finiteInterval(), grayShadowConst(), implyDiffLogicBothBounds(), and splitGrayShadow().

Theorem ArithTheoremProducerOld::varToMult ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::uMinusToMult ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::minusToPlus ( const Expr x,
const Expr y 
) [virtual]
Theorem ArithTheoremProducerOld::canonUMinusToDivide ( const Expr e  )  [virtual]
bool ArithTheoremProducerOld::greaterthan ( const Expr l,
const Expr r 
) [static]
Expr ArithTheoremProducerOld::simplifiedMultExpr ( std::vector< Expr > &  mulKids  )  [virtual]
Expr ArithTheoremProducerOld::canonMultPowPow ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducerOld::canonMultPowLeaf ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducerOld::canonMultLeafLeaf ( const Expr e1,
const Expr e2 
) [virtual]

Definition at line 330 of file arith_theorem_producer_old.cpp.

References CVC3::powExpr(), rat(), and simplifiedMultExpr().

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducerOld::canonMultLeafOrPowMult ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducerOld::canonMultPlusPlus ( const Expr e1,
const Expr e2 
) [virtual]
Theorem ArithTheoremProducerOld::canonInvertLeaf ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::canonInvert ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::moveSumConstantRight ( const Expr e  )  [virtual]

Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first sum term (r) must be a rational and t1 ... tn terms must be canonised.

Parameters:
e the expression to transform
Returns:
rewrite theorem representing the transformation

Definition at line 911 of file arith_theorem_producer_old.cpp.

References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::isEq(), CVC3::isIneq(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), MiniSat::right(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::canonMultTerm1Term2 ( const Expr t1,
const Expr t2 
) [virtual]

Definition at line 989 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().

Theorem ArithTheoremProducerOld::canonMultZero ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::canonMultOne ( const Expr e  )  [virtual]
Theorem ArithTheoremProducerOld::divideEqnNonConst ( const Expr x,
const Expr y,
const Expr z 
) [virtual]
Theorem ArithTheoremProducerOld::realShadowEq ( const Theorem alphaLEt,
const Theorem tLEalpha 
)

alpha <= t <= alpha ==> t = alpha

takes two ineqs "|- alpha LE t" and "|- t LE alpha" and returns "|- t = alpha"

Definition at line 1737 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isLE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Rational ArithTheoremProducerOld::constRHSGrayShadow ( const Rational c,
const Rational b,
const Rational a 
)

Implements j(c,b,a).

accepts 3 integers a,b,c and returns (b > 0)? (c+b) mod a : (a - (c+b)) mod a

Definition at line 2227 of file arith_theorem_producer_old.cpp.

References DebugAssert, and CVC3::Rational::isInteger().

Referenced by expandGrayShadowConst().

Theorem ArithTheoremProducerOld::lessThanToLE ( const Theorem less,
const Theorem isIntLHS,
const Theorem isIntRHS,
bool  changeRight 
)

Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) where \alpha and \beta are integer expressions

Definition at line 2245 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::lessThanToLERewrite ( const Expr ineq,
const Theorem isIntLHS,
const Theorem isIntRHS,
bool  changeRight 
)

Takes a Theorem(\alpha < \beta) and returns Theorem(\alpha < \beta <==> \alpha <= \beta -1) where \alpha and \beta are integer expressions

Definition at line 3416 of file arith_theorem_producer_old.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isIntPred(), CVC3::isLT(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArithTheoremProducerOld::intVarEqnConst ( const Expr eqn,
const Theorem isIntx 
)
Theorem ArithTheoremProducerOld::dummyTheorem ( const Expr e  ) 
Theorem ArithTheoremProducerOld::trustedRewrite ( const Expr expr1,
const Expr expr2 
)
Theorem ArithTheoremProducerOld::implyEqualities ( const std::vector< Theorem > &  inequalities  ) 
Theorem ArithTheoremProducerOld::implyWeakerInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)
Theorem ArithTheoremProducerOld::implyNegatedInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)
Theorem ArithTheoremProducerOld::implyDiffLogicBothBounds ( const Expr x,
std::vector< Theorem > &  c1_le_x,
Rational  c1,
std::vector< Theorem > &  x_le_c2,
Rational  c2 
)

Member Data Documentation


The documentation for this class was generated from the following files: