#include <arith_theorem_producer.h>
Methods that compute the subterms used in eqElimIntRule()
Definition at line 32 of file arith_theorem_producer.h.
CVC3::ArithTheoremProducer::ArithTheoremProducer | ( | TheoremManager * | tm, | |
TheoryArithNew * | theoryArith | |||
) | [inline] |
Constructor.
Definition at line 67 of file arith_theorem_producer.h.
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().
Create the term 't'. See eqElimIntRule().
Definition at line 2192 of file arith_theorem_producer.cpp.
References CLASS_NAME, DebugAssert, CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isPlus(), monomialModM(), CVC3::multExpr(), CVC3::plusExpr(), rat(), sumModM(), CVC3::Rational::toString(), and CVC3::Expr::toString().
Expr ArithTheoremProducer::create_t2 | ( | const Expr & | lhs, | |
const Expr & | rhs, | |||
const Expr & | t | |||
) | [private] |
Create the term 't2'. See eqElimIntRule().
Definition at line 2211 of file arith_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialModM(), CVC3::plusExpr(), rat(), sumModM(), and CVC3::Rational::toString().
Referenced by eqElimIntRule().
Expr ArithTheoremProducer::create_t3 | ( | const Expr & | lhs, | |
const Expr & | rhs, | |||
const Expr & | t | |||
) | [private] |
Create the term 't3'. See eqElimIntRule().
Definition at line 2231 of file arith_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialMulF(), CVC3::plusExpr(), rat(), sumMulF(), and CVC3::Rational::toString().
Referenced by eqElimIntRule().
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] |
Compute the special modulus: i - m*floor(i/m+1/2).
Definition at line 2288 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getRational(), CVC3::isMult(), modEq(), CVC3::multExpr(), rat(), CVC3::Expr::toString(), CVC3::Rational::toString(), and CVC3::TRACE.
Referenced by create_t(), create_t2(), and sumModM().
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().
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().
Compute the special modulus: i - m*floor(i/m+1/2).
Definition at line 2353 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::isMult(), CVC3::isPlus(), and CVC3::plusExpr().
Create Expr from Rational (for convenience).
Definition at line 71 of file arith_theorem_producer.h.
References CVC3::TheoremProducer::d_em, and CVC3::ExprManager::newRatExpr().
Referenced by canonCombineLikeTerms(), canonComboLikeTerms(), canonDivideConst(), canonDivideMult(), canonDividePlus(), canonDivideVar(), canonInvertConst(), canonInvertLeaf(), canonInvertMult(), canonInvertPow(), canonMultConstConst(), canonMultConstMult(), canonMultConstTerm(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultOne(), canonMultPowLeaf(), canonMultPowPow(), canonMultZero(), canonPowConst(), canonUMinusToDivide(), create_t(), create_t2(), create_t3(), darkGrayShadow2ab(), darkGrayShadow2ba(), divideEqnNonConst(), elimPowerConst(), eqElimIntRule(), expandGrayShadow(), expandGrayShadowConst(), grayShadowConst(), integerSplit(), intVarEqnConst(), leftMinusRight(), lessThanToLE(), lessThanToLERewrite(), minusToPlus(), monomialModM(), monomialMulF(), moveSumConstantRight(), multEqZero(), powEqZero(), rafineStrictInteger(), rightMinusLeft(), sumModM(), sumMulF(), uMinusToMult(), and varToMult().
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().
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().
Definition at line 55 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 62 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 75 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 89 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 98 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::TheoremProducer::d_hole, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 117 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 145 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::isPlus(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 168 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 2379 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::PLUS, CVC3::POW, and CVC3::RATIONAL_EXPR.
Referenced by MonomialLess::operator()().
Definition at line 203 of file arith_theorem_producer.cpp.
References DebugAssert, and CVC3::multExpr().
Referenced by canonMultConstMult(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultPowLeaf(), and canonMultPowPow().
Definition at line 214 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::Expr::isRational(), rat(), simplifiedMultExpr(), and CVC3::Expr::toString().
Referenced by canonMultMtermMterm().
Definition at line 237 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), d_theoryArith, DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Theorem::getRHS(), CVC3::Expr::isRational(), CVC3::PLUS, and CVC3::Theory::substitutivityRule().
Referenced by canonMultMtermMterm().
Definition at line 256 of file arith_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 296 of file arith_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 335 of file arith_theorem_producer.cpp.
References CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 363 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 434 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::multExpr(), CVC3::plusExpr(), and rat().
Referenced by canonMultLeafOrPowOrMultPlus(), canonMultPlusPlus(), and canonPlus().
Expr ArithTheoremProducer::canonMultLeafOrPowOrMultPlus | ( | const Expr & | e1, | |
const Expr & | e2 | |||
) | [virtual] |
Definition at line 532 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), and CVC3::Expr::getKind().
Referenced by canonMultMtermMterm().
Definition at line 551 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Referenced by canonMultMtermMterm().
Definition at line 574 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultConstConst(), canonMultConstMult(), canonMultConstPlus(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultLeafOrPowOrMultPlus(), canonMultOne(), canonMultPlusPlus(), canonMultPowLeaf(), canonMultPowPow(), canonMultZero(), CHECK_PROOFS, CHECK_SOUND, d_theoryArith, CVC3::Assumptions::emptyAssump(), FatalAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::POW, CVC3::RATIONAL_EXPR, CVC3::Theory::reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvertMult(), canonMult(), canonMultConstPlus(), canonMultLeafOrPowOrMultPlus(), and canonMultPlusPlus().
Definition at line 746 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), canonCombineLikeTerms(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 815 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvert().
Definition at line 831 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::powExpr(), rat(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvert().
Definition at line 843 of file arith_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::powExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvert().
Definition at line 862 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), canonInvert(), canonMultMtermMterm(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvert().
Definition at line 885 of file arith_theorem_producer.cpp.
References canonInvertConst(), canonInvertLeaf(), canonInvertMult(), canonInvertPow(), DebugAssert, CVC3::Expr::getKind(), CVC3::MULT, CVC3::POW, CVC3::RATIONAL_EXPR, and CVC3::Expr::toString().
Referenced by canonDivide(), and canonInvertMult().
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.
e | the expression to transform |
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().
e[0]/e[1] ==> e[0]*(e[1])^-1
Definition at line 907 of file arith_theorem_producer.cpp.
References canonInvert(), canonMult(), d_theoryArith, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and CVC3::TheoremProducer::withProof().
Multiply out the operands of the multiplication (each of them is expected to be canonised
Definition at line 781 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Referenced by canonDivide().
Definition at line 931 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 945 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().
Definition at line 958 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Referenced by canonMultMtermMterm().
Definition at line 967 of file arith_theorem_producer.cpp.
References d_theoryArith, CVC3::Assumptions::emptyAssump(), CVC3::Theory::isLeaf(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Theory::reflexivityRule(), and CVC3::TheoremProducer::withProof().
Referenced by canonMultMtermMterm().
Definition at line 983 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by canonMultMtermMterm().
Theorem ArithTheoremProducer::canonMultConstTerm | ( | const Expr & | c1, | |
const Expr & | c2, | |||
const Expr & | t | |||
) | [virtual] |
Definition at line 1001 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1021 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1043 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::pow(), CVC3::POW, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1070 of file arith_theorem_producer.cpp.
References CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1097 of file arith_theorem_producer.cpp.
References CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::ExprMap< Data >::count(), CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::isMult(), CVC3::isPlus(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::plusExpr(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 1155 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::OR, rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1178 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1205 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1230 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::pow(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1254 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::intEqIrrational | ( | const Expr & | expr, | |
const Theorem & | isInt | |||
) | [virtual] |
Definition at line 1273 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Expr::isEq(), CVC3::isIntegerConst(), CVC3::isIntPred(), CVC3::isPow(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ratRoot(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1300 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::ExprManager::falseExpr(), CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isRational(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 1340 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 1357 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::GT, CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::plusPredicate | ( | const Expr & | x, | |
const Expr & | y, | |||
const Expr & | z, | |||
int | kind | |||
) | [virtual] |
Definition at line 1376 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::EQ, CVC3::GE, CVC3::GT, CVC3::LE, MiniSat::left(), CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), MiniSat::right(), and CVC3::TheoremProducer::withProof().
Definition at line 1395 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::divideEqnNonConst | ( | const Expr & | x, | |
const Expr & | y, | |||
const Expr & | z | |||
) | [virtual] |
Definition at line 1408 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 1420 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::GE, CVC3::geExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::GT, CVC3::gtExpr(), CVC3::isIneq(), CVC3::Expr::isRational(), CVC3::LE, CVC3::leExpr(), CVC3::LT, CVC3::ltExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 2818 of file arith_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::geExpr(), CVC3::Expr::isEq(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1498 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::isGE(), CVC3::isGT(), CVC3::LE, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1518 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::GE, CVC3::GT, CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::Expr::isNot(), CVC3::LE, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1547 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isLE(), CVC3::isLT(), CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
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::finiteInterval | ( | const Theorem & | aLEt, | |
const Theorem & | tLEac, | |||
const Theorem & | isInta, | |||
const Theorem & | isIntt | |||
) |
Definition at line 1614 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isPlus(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::darkGrayShadow2ab | ( | const Theorem & | betaLEbx, | |
const Theorem & | axLEalpha, | |||
const Theorem & | isIntAlpha, | |||
const Theorem & | isIntBeta, | |||
const Theorem & | isIntx | |||
) |
Definition at line 1678 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, darkShadow(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isMult(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::darkGrayShadow2ba | ( | const Theorem & | betaLEbx, | |
const Theorem & | axLEalpha, | |||
const Theorem & | isIntAlpha, | |||
const Theorem & | isIntBeta, | |||
const Theorem & | isIntx | |||
) |
Definition at line 1769 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, darkShadow(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isIntPred(), CVC3::isLE(), CVC3::isMult(), CVC3::minusExpr(), CVC3::multExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
takes a dark shadow and expands it into an inequality.
Definition at line 1854 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isDarkShadow(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1869 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::isGrayShadow(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1894 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 3190 of file arith_theorem_producer.cpp.
References DebugAssert.
Definition at line 1931 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1962 of file arith_theorem_producer.cpp.
References CVC3::abs(), CHECK_PROOFS, CHECK_SOUND, constRHSGrayShadow(), CVC3::TheoremProducer::d_em, CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GRAY_SHADOW, CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::orExpr(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 2027 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), grayShadow(), CVC3::isGrayShadow(), CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithNew::separateMonomial(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
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().
eqn | is an equation 0 = a.x or 0 = c + a.x | |
isIntx | is a proof of IS_INTEGER(x) |
It also handles the special case of 0 = a.x <==> x = 0
Definition at line 2138 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::Expr::eqExpr(), CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isMult(), CVC3::isPlus(), CVC3::Expr::isRational(), CVC3::isRational(), MiniSat::left(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), MiniSat::right(), CVC3::TheoryArithNew::separateMonomial(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
IS_INTEGER(x) |= EXISTS (y : INT) y = x where x is not already known to be an integer.
Definition at line 2505 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, d_theoryArith, DebugAssert, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::TheoryArith::intType(), CVC3::TheoryArithNew::isInteger(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::eqElimIntRule | ( | const Theorem & | eqn, | |
const Theorem & | isIntx, | |||
const std::vector< Theorem > & | isIntVars | |||
) |
Definition at line 2531 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, create_t2(), create_t3(), CVC3::TheoremProducer::d_em, d_theoryArith, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::int2string(), intType(), CVC3::isDivide(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isPlus(), CVC3::isRational(), CVC3::Theorem::isRewrite(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), rat(), CVC3::TheoryArithNew::separateMonomial(), CVC3::Expr::setType(), CVC3::Rational::toString(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().
Definition at line 2623 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getRational(), CVC3::isInt(), CVC3::Rational::isInteger(), CVC3::isIntPred(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 2639 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().
Definition at line 2668 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().
Definition at line 2697 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().
Definition at line 2726 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::MULT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::PLUS, CVC3::RATIONAL_EXPR, and CVC3::TheoremProducer::withProof().
Definition at line 2754 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::gtExpr(), CVC3::Expr::isEq(), CVC3::Expr::isNot(), CVC3::ltExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 2839 of file arith_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::ExprManager::trueExpr().
Definition at line 2844 of file arith_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::isMult(), CVC3::Expr::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::clashingBounds | ( | const Theorem & | lowerBound, | |
const Theorem & | upperBound | |||
) |
Definition at line 2865 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getRational(), CVC3::isGE(), CVC3::isGT(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 2905 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::plusExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 3227 of file arith_theorem_producer.cpp.
References DebugAssert.
Definition at line 2950 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 3004 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getRational(), CVC3::Expr::impExpr(), CVC3::isGE(), CVC3::isGT(), CVC3::isIneq(), CVC3::isLE(), CVC3::isLT(), CVC3::isRational(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 3049 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::geExpr(), CVC3::IS_INTEGER, CVC3::Rational::isInteger(), CVC3::leExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::orExpr(), rat(), CVC3::Rational::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 3036 of file arith_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer::rafineStrictInteger | ( | const Theorem & | isIntConstrThm, | |
const Expr & | constr | |||
) |
Definition at line 3068 of file arith_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::GE, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::Expr::getRational(), CVC3::GT, CVC3::isIneq(), CVC3::Rational::isInteger(), CVC3::isRational(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
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.
Definition at line 3138 of file arith_theorem_producer.cpp.
References DebugAssert.
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.
Definition at line 3205 of file arith_theorem_producer.cpp.
References DebugAssert.
Definition at line 3210 of file arith_theorem_producer.cpp.
References DebugAssert.
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.
Definition at line 3232 of file arith_theorem_producer.cpp.
References DebugAssert.
Definition at line 33 of file arith_theorem_producer.h.
Referenced by canonDivide(), canonMultConstPlus(), canonMultMtermMterm(), canonMultOne(), darkShadow(), eqElimIntRule(), grayShadow(), grayShadowConst(), intType(), intVarEqnConst(), IsIntegerElim(), and realType().