Public Member Functions | Static Public Member Functions | Private Attributes

CVC3::ArithTheoremProducer3 Class Reference

#include <arith_theorem_producer3.h>

Inheritance diagram for CVC3::ArithTheoremProducer3:
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 32 of file arith_theorem_producer3.h.


Constructor & Destructor Documentation

CVC3::ArithTheoremProducer3::ArithTheoremProducer3 ( TheoremManager tm,
TheoryArith3 theoryArith 
) [inline]

Constructor.

Definition at line 66 of file arith_theorem_producer3.h.


Member Function Documentation

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

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

Definition at line 2227 of file arith_theorem_producer3.cpp.

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

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

Expr ArithTheoremProducer3::create_t ( const Expr eqn  )  [private]
Expr ArithTheoremProducer3::create_t2 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
Expr ArithTheoremProducer3::create_t3 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
void ArithTheoremProducer3::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 2243 of file arith_theorem_producer3.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 ArithTheoremProducer3::monomialModM ( const Expr e,
const Rational m,
const Rational divisor 
) [private]
void ArithTheoremProducer3::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 2291 of file arith_theorem_producer3.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 ArithTheoremProducer3::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 2311 of file arith_theorem_producer3.cpp.

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

Referenced by create_t3(), and sumMulF().

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

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

Definition at line 2236 of file arith_theorem_producer3.cpp.

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

Referenced by monomialMulF(), and sumMulF().

Expr ArithTheoremProducer3::substitute ( const Expr term,
ExprMap< Expr > &  eMap 
) [private]
Type CVC3::ArithTheoremProducer3::realType (  )  [inline]

Definition at line 71 of file arith_theorem_producer3.h.

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

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

Definition at line 72 of file arith_theorem_producer3.h.

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

Referenced by eqElimIntRule().

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

Construct the dark shadow expression representing lhs <= rhs.

Definition at line 74 of file arith_theorem_producer3.h.

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

Referenced by darkGrayShadow2ab(), and darkGrayShadow2ba().

Expr CVC3::ArithTheoremProducer3::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_producer3.h.

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

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

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

Definition at line 329 of file arith_theorem_producer3.cpp.

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

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducer3::canonMultLeafOrPowMult ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducer3::canonMultPlusPlus ( const Expr e1,
const Expr e2 
) [virtual]
Theorem ArithTheoremProducer3::canonInvertLeaf ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer3::canonInvert ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer3::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 861 of file arith_theorem_producer3.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 ArithTheoremProducer3::canonMult ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer3::canonMultTerm1Term2 ( const Expr t1,
const Expr t2 
) [virtual]

Definition at line 939 of file arith_theorem_producer3.cpp.

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

Theorem ArithTheoremProducer3::canonMultZero ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer3::canonMultOne ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer3::divideEqnNonConst ( const Expr x,
const Expr y,
const Expr z 
) [virtual]
Theorem ArithTheoremProducer3::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 1539 of file arith_theorem_producer3.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().

Theorem ArithTheoremProducer3::splitGrayShadowSmall ( const Theorem grayShadow  ) 

Definition at line 3024 of file arith_theorem_producer3.cpp.

References DebugAssert.

Rational ArithTheoremProducer3::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 2025 of file arith_theorem_producer3.cpp.

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

Referenced by expandGrayShadowConst().

Theorem ArithTheoremProducer3::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 2043 of file arith_theorem_producer3.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 ArithTheoremProducer3::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 3103 of file arith_theorem_producer3.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 ArithTheoremProducer3::intVarEqnConst ( const Expr eqn,
const Theorem isIntx 
)
Theorem ArithTheoremProducer3::dummyTheorem ( const Expr e  ) 
Theorem ArithTheoremProducer3::addInequalities ( const std::vector< Theorem > &  thms  ) 

Definition at line 3061 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::trustedRewrite ( const Expr expr1,
const Expr expr2 
)
Theorem ArithTheoremProducer3::simpleIneqInt ( const Expr ineq,
const Theorem isIntRHS 
)

Definition at line 3073 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::intEqualityRationalConstant ( const Theorem isIntConstrThm,
const Expr constr 
)

Definition at line 3083 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::cycleConflict ( const std::vector< Theorem > &  inequalitites  ) 

Definition at line 3088 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyEqualities ( const std::vector< Theorem > &  inequalities  ) 

Definition at line 3093 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyWeakerInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)

Definition at line 3029 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyNegatedInequalityDiffLogic ( const std::vector< Theorem > &  antecedentThms,
const Expr implied 
)

Definition at line 3034 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::expandGrayShadowRewrite ( const Expr theShadow  ) 

Definition at line 3039 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::compactNonLinearTerm ( const Expr nonLinear  ) 

Definition at line 3044 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::nonLinearIneqSignSplit ( const Theorem ineqThm  ) 

Definition at line 3049 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::implyDiffLogicBothBounds ( const Expr x,
std::vector< Theorem > &  c1_le_x,
Rational  c1,
std::vector< Theorem > &  x_le_c2,
Rational  c2 
)

Definition at line 3054 of file arith_theorem_producer3.cpp.

References DebugAssert.

Theorem ArithTheoremProducer3::powerOfOne ( const Expr e  ) 

Definition at line 3066 of file arith_theorem_producer3.cpp.

References DebugAssert.


Member Data Documentation


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