Public Member Functions | Static Public Member Functions | Private Attributes

CVC3::ArithTheoremProducer Class Reference

#include <arith_theorem_producer.h>

Inheritance diagram for CVC3::ArithTheoremProducer:
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_producer.h.


Constructor & Destructor Documentation

CVC3::ArithTheoremProducer::ArithTheoremProducer ( TheoremManager tm,
TheoryArithNew theoryArith 
) [inline]

Constructor.

Definition at line 67 of file arith_theorem_producer.h.


Member Function Documentation

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

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

Definition at line 2252 of file arith_theorem_producer.cpp.

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

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

Expr ArithTheoremProducer::create_t ( const Expr eqn  )  [private]
Expr ArithTheoremProducer::create_t2 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
Expr ArithTheoremProducer::create_t3 ( const Expr lhs,
const Expr rhs,
const Expr t 
) [private]
void ArithTheoremProducer::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 2268 of file arith_theorem_producer.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 ArithTheoremProducer::monomialModM ( const Expr e,
const Rational m,
const Rational divisor 
) [private]
void ArithTheoremProducer::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 2316 of file arith_theorem_producer.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 ArithTheoremProducer::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 2336 of file arith_theorem_producer.cpp.

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

Referenced by create_t3(), and sumMulF().

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

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

Definition at line 2261 of file arith_theorem_producer.cpp.

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

Referenced by monomialMulF(), and sumMulF().

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

Definition at line 72 of file arith_theorem_producer.h.

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

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

Definition at line 73 of file arith_theorem_producer.h.

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

Referenced by eqElimIntRule().

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

Construct the dark shadow expression representing lhs <= rhs.

Definition at line 75 of file arith_theorem_producer.h.

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

Referenced by darkGrayShadow2ab(), and darkGrayShadow2ba().

Expr CVC3::ArithTheoremProducer::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 81 of file arith_theorem_producer.h.

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

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

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

Definition at line 335 of file arith_theorem_producer.cpp.

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

Referenced by canonMultMtermMterm().

Expr ArithTheoremProducer::canonMultLeafOrPowMult ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducer::canonCombineLikeTerms ( const std::vector< Expr > &  sumExprs  )  [virtual]
Expr ArithTheoremProducer::canonMultLeafOrPowOrMultPlus ( const Expr e1,
const Expr e2 
) [virtual]
Expr ArithTheoremProducer::canonMultPlusPlus ( const Expr e1,
const Expr e2 
) [virtual]
Theorem ArithTheoremProducer::canonInvertLeaf ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer::canonInvert ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer::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 2773 of file arith_theorem_producer.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 ArithTheoremProducer::canonMult ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer::canonMultTerm1Term2 ( const Expr t1,
const Expr t2 
) [virtual]

Definition at line 945 of file arith_theorem_producer.cpp.

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

Theorem ArithTheoremProducer::canonMultZero ( const Expr e  )  [virtual]
Theorem ArithTheoremProducer::divideEqnNonConst ( const Expr x,
const Expr y,
const Expr z 
) [virtual]
Theorem ArithTheoremProducer::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 1582 of file arith_theorem_producer.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 ArithTheoremProducer::splitGrayShadowSmall ( const Theorem grayShadow  ) 

Definition at line 3190 of file arith_theorem_producer.cpp.

References DebugAssert.

Rational ArithTheoremProducer::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 2067 of file arith_theorem_producer.cpp.

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

Referenced by expandGrayShadowConst().

Theorem ArithTheoremProducer::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 2085 of file arith_theorem_producer.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 ArithTheoremProducer::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 3152 of file arith_theorem_producer.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 ArithTheoremProducer::intVarEqnConst ( const Expr eqn,
const Theorem isIntx 
)
Theorem ArithTheoremProducer::dummyTheorem ( const Expr e  ) 
Theorem ArithTheoremProducer::addInequalities ( const std::vector< Theorem > &  thms  ) 

Definition at line 3227 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3123 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3133 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3138 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3143 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3195 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3200 of file arith_theorem_producer.cpp.

References DebugAssert.

Theorem ArithTheoremProducer::expandGrayShadowRewrite ( const Expr theShadow  ) 

Definition at line 3205 of file arith_theorem_producer.cpp.

References DebugAssert.

Theorem ArithTheoremProducer::compactNonLinearTerm ( const Expr nonLinear  ) 

Definition at line 3210 of file arith_theorem_producer.cpp.

References DebugAssert.

Theorem ArithTheoremProducer::nonLinearIneqSignSplit ( const Theorem ineqThm  ) 

Definition at line 3215 of file arith_theorem_producer.cpp.

References DebugAssert.

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

Definition at line 3220 of file arith_theorem_producer.cpp.

References DebugAssert.

Theorem ArithTheoremProducer::powerOfOne ( const Expr e  ) 

Definition at line 3232 of file arith_theorem_producer.cpp.

References DebugAssert.


Member Data Documentation


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