#include <arith_theorem_producer3.h>
Methods that compute the subterms used in eqElimIntRule()
Definition at line 32 of file arith_theorem_producer3.h.
CVC3::ArithTheoremProducer3::ArithTheoremProducer3 | ( | TheoremManager * | tm, | |
TheoryArith3 * | theoryArith | |||
) | [inline] |
Constructor.
Definition at line 66 of file arith_theorem_producer3.h.
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().
Create the term 't'. See eqElimIntRule().
Definition at line 2167 of file arith_theorem_producer3.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 ArithTheoremProducer3::create_t2 | ( | const Expr & | lhs, | |
const Expr & | rhs, | |||
const Expr & | t | |||
) | [private] |
Create the term 't2'. See eqElimIntRule().
Definition at line 2186 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialModM(), CVC3::plusExpr(), rat(), sumModM(), and CVC3::Rational::toString().
Referenced by eqElimIntRule().
Expr ArithTheoremProducer3::create_t3 | ( | const Expr & | lhs, | |
const Expr & | rhs, | |||
const Expr & | t | |||
) | [private] |
Create the term 't3'. See eqElimIntRule().
Definition at line 2206 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getRational(), CVC3::isPlus(), CVC3::Expr::isRational(), monomialMulF(), CVC3::plusExpr(), rat(), sumMulF(), and CVC3::Rational::toString().
Referenced by eqElimIntRule().
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] |
Compute the special modulus: i - m*floor(i/m+1/2).
Definition at line 2263 of file arith_theorem_producer3.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 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().
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().
Compute the special modulus: i - m*floor(i/m+1/2).
Definition at line 2328 of file arith_theorem_producer3.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 70 of file arith_theorem_producer3.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(), simplifiedMultExpr(), sumModM(), sumMulF(), uMinusToMult(), and varToMult().
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().
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().
Definition at line 56 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 64 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 72 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 82 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 91 of file arith_theorem_producer3.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 110 of file arith_theorem_producer3.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 138 of file arith_theorem_producer3.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 161 of file arith_theorem_producer3.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 2354 of file arith_theorem_producer3.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 196 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::multExpr(), and rat().
Referenced by canonMultConstMult(), canonMultLeafLeaf(), canonMultLeafOrPowMult(), canonMultPowLeaf(), and canonMultPowPow().
Definition at line 209 of file arith_theorem_producer3.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 231 of file arith_theorem_producer3.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 250 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::POW, CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 290 of file arith_theorem_producer3.cpp.
References DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 329 of file arith_theorem_producer3.cpp.
References CVC3::powExpr(), rat(), and simplifiedMultExpr().
Referenced by canonMultMtermMterm().
Definition at line 357 of file arith_theorem_producer3.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().
Expr ArithTheoremProducer3::canonCombineLikeTerms | ( | const std::vector< Expr > & | sumExprs | ) | [virtual] |
Definition at line 429 of file arith_theorem_producer3.cpp.
References CVC3::Expr::arity(), CVC3::Expr::begin(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Theorem::getRHS(), CVC3::Expr::isRational(), CVC3::MULT, CVC3::multExpr(), CVC3::plusExpr(), and rat().
Referenced by canonMultLeafOrPowOrMultPlus(), canonMultPlusPlus(), and canonPlus().
Expr ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus | ( | const Expr & | e1, | |
const Expr & | e2 | |||
) | [virtual] |
Definition at line 510 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), and CVC3::Expr::getKind().
Referenced by canonMultMtermMterm().
Definition at line 529 of file arith_theorem_producer3.cpp.
References CVC3::Expr::begin(), canonCombineLikeTerms(), canonMultMtermMterm(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::PLUS.
Referenced by canonMultMtermMterm().
Definition at line 553 of file arith_theorem_producer3.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 canonCombineLikeTerms(), canonInvertMult(), canonMult(), canonMultConstPlus(), canonMultLeafOrPowOrMultPlus(), and canonMultPlusPlus().
Definition at line 718 of file arith_theorem_producer3.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 769 of file arith_theorem_producer3.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 785 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::powExpr(), rat(), and CVC3::TheoremProducer::withProof().
Referenced by canonInvert().
Definition at line 797 of file arith_theorem_producer3.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 816 of file arith_theorem_producer3.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 839 of file arith_theorem_producer3.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 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().
e[0]/e[1] ==> e[0]*(e[1])^-1
Definition at line 907 of file arith_theorem_producer3.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 751 of file arith_theorem_producer3.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 925 of file arith_theorem_producer3.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 939 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, and CVC3::Expr::toString().
Definition at line 952 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Referenced by canonMultMtermMterm().
Definition at line 960 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), rat(), and CVC3::TheoremProducer::withProof().
Referenced by canonMultMtermMterm().
Definition at line 969 of file arith_theorem_producer3.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 ArithTheoremProducer3::canonMultConstTerm | ( | const Expr & | c1, | |
const Expr & | c2, | |||
const Expr & | t | |||
) | [virtual] |
Definition at line 987 of file arith_theorem_producer3.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 1007 of file arith_theorem_producer3.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 1030 of file arith_theorem_producer3.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 1057 of file arith_theorem_producer3.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 1084 of file arith_theorem_producer3.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 1142 of file arith_theorem_producer3.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 1165 of file arith_theorem_producer3.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 1192 of file arith_theorem_producer3.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().
Theorem ArithTheoremProducer3::elimPowerConst | ( | const Expr & | expr, | |
const Rational & | root | |||
) | [virtual] |
Definition at line 1217 of file arith_theorem_producer3.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 1241 of file arith_theorem_producer3.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 ArithTheoremProducer3::intEqIrrational | ( | const Expr & | expr, | |
const Theorem & | isInt | |||
) | [virtual] |
Definition at line 1260 of file arith_theorem_producer3.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 1287 of file arith_theorem_producer3.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 1326 of file arith_theorem_producer3.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 1344 of file arith_theorem_producer3.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 ArithTheoremProducer3::plusPredicate | ( | const Expr & | x, | |
const Expr & | y, | |||
const Expr & | z, | |||
int | kind | |||
) | [virtual] |
Definition at line 1362 of file arith_theorem_producer3.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 1381 of file arith_theorem_producer3.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 ArithTheoremProducer3::divideEqnNonConst | ( | const Expr & | x, | |
const Expr & | y, | |||
const Expr & | z | |||
) | [virtual] |
Definition at line 1394 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), rat(), and CVC3::TheoremProducer::withProof().
Definition at line 1406 of file arith_theorem_producer3.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::GE, CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::GT, CVC3::Expr::isRational(), CVC3::LE, CVC3::LT, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 1433 of file arith_theorem_producer3.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 1455 of file arith_theorem_producer3.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 1475 of file arith_theorem_producer3.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 1504 of file arith_theorem_producer3.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 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::finiteInterval | ( | const Theorem & | aLEt, | |
const Theorem & | tLEac, | |||
const Theorem & | isInta, | |||
const Theorem & | isIntt | |||
) |
Definition at line 1571 of file arith_theorem_producer3.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 ArithTheoremProducer3::darkGrayShadow2ab | ( | const Theorem & | betaLEbx, | |
const Theorem & | axLEalpha, | |||
const Theorem & | isIntAlpha, | |||
const Theorem & | isIntBeta, | |||
const Theorem & | isIntx | |||
) |
Definition at line 1635 of file arith_theorem_producer3.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 ArithTheoremProducer3::darkGrayShadow2ba | ( | const Theorem & | betaLEbx, | |
const Theorem & | axLEalpha, | |||
const Theorem & | isIntAlpha, | |||
const Theorem & | isIntBeta, | |||
const Theorem & | isIntx | |||
) |
Definition at line 1726 of file arith_theorem_producer3.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 1811 of file arith_theorem_producer3.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 1826 of file arith_theorem_producer3.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 1852 of file arith_theorem_producer3.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 3024 of file arith_theorem_producer3.cpp.
References DebugAssert.
Definition at line 1889 of file arith_theorem_producer3.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 1920 of file arith_theorem_producer3.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 1985 of file arith_theorem_producer3.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::TheoryArith3::separateMonomial(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
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().
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 2095 of file arith_theorem_producer3.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::TheoryArith3::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 2480 of file arith_theorem_producer3.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::TheoryArith3::isInteger(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer3::eqElimIntRule | ( | const Theorem & | eqn, | |
const Theorem & | isIntx, | |||
const std::vector< Theorem > & | isIntVars | |||
) |
Definition at line 2506 of file arith_theorem_producer3.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::TheoryArith3::separateMonomial(), CVC3::Expr::setType(), CVC3::Rational::toString(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().
Definition at line 2598 of file arith_theorem_producer3.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 2614 of file arith_theorem_producer3.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 2643 of file arith_theorem_producer3.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 2672 of file arith_theorem_producer3.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 2701 of file arith_theorem_producer3.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 2729 of file arith_theorem_producer3.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 2748 of file arith_theorem_producer3.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::ExprManager::trueExpr().
Definition at line 2753 of file arith_theorem_producer3.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 ArithTheoremProducer3::clashingBounds | ( | const Theorem & | lowerBound, | |
const Theorem & | upperBound | |||
) |
Definition at line 2774 of file arith_theorem_producer3.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 2814 of file arith_theorem_producer3.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 3061 of file arith_theorem_producer3.cpp.
References DebugAssert.
Definition at line 2859 of file arith_theorem_producer3.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 2906 of file arith_theorem_producer3.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 2951 of file arith_theorem_producer3.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 2938 of file arith_theorem_producer3.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Theorem ArithTheoremProducer3::rafineStrictInteger | ( | const Theorem & | isIntConstrThm, | |
const Expr & | constr | |||
) |
Definition at line 2970 of file arith_theorem_producer3.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 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.
Definition at line 3088 of file arith_theorem_producer3.cpp.
References DebugAssert.
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.
Definition at line 3039 of file arith_theorem_producer3.cpp.
References DebugAssert.
Definition at line 3044 of file arith_theorem_producer3.cpp.
References DebugAssert.
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.
Definition at line 3066 of file arith_theorem_producer3.cpp.
References DebugAssert.
Definition at line 33 of file arith_theorem_producer3.h.
Referenced by canonDivide(), canonMultConstPlus(), canonMultMtermMterm(), darkShadow(), eqElimIntRule(), grayShadow(), grayShadowConst(), intType(), intVarEqnConst(), IsIntegerElim(), and realType().