refined_arith_theorem_producer.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file refined_arith_theorem_producer.h
 * \brief TRUSTED implementation of arithmetic proof rules
 * 
 * Author: Sean McLaughlin
 * 
 * Created: Jan 23 00:00:00 GMT 2004
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

#ifndef _CVC_lite__refined_arith_theorem_producer_h_
#define _CVC_lite__refined_arith_theorem_producer_h_

#include "arith_proof_rules.h"
#include "theory.h"
#include "common_proof_rules.h"
#include "arith_theorem_producer.h"
#include "vcl.h"
#include "type.h"
#include "typecheck_exception.h"

namespace CVCL {


  ////////////////////////
  //
  // This is a reimplimentation of the arithmetic rules going back to the 
  // axioms of the reals.  
  // 
  // 1) x + (y + z) = (x + y) + z         (Addition is associative) 
  // 2) x * (y * z) = (x * y) * z         (Multiplication is associative) 
  // 3) x + y = y + x                     (Addition is commutative) 
  // 4) x * y = y * x                     (Multiplication is commutative) 
  // 5) x * (y + z) = x * y + x * z       (Distributivity)
  // 6) 0 + x = x                         (Additive identity)
  // 7) 1 * x = x                         (Multiplicative identity)
  // 8) x + -x = 0                        (Additive inverse)
  // 9) x * 1/x = 1                       (Multiplicative inverse)
  // 10) x < y -> x + z < y + z           (Invariance of order)
  // 11) x < y -> y < z -> x < z          (Transitivity of order)
  // 12) x < y -> 0 < z -> xz < yz        (Scaling of order)
  // 14) arithmetic                       (rational number calculation)

  class RefinedArithTheoremProducer: public ArithTheoremProducer{
  private:
    // structures
    ExprManager* d_em;
    TheoryCore* core;
    VCL* vcl;

    // constants
    const Expr zero,one;

    // util 
    Rational eval(const Expr& rational_expr);

    // Axioms
    Theorem addAssoc(const Expr& x,const Expr& y,const Expr& z);
    Theorem multAssoc(const Expr& x,const Expr& y,const Expr& z);
    Theorem addSymm(const Expr& x,const Expr& y);
    Theorem multSymm(const Expr& x,const Expr& y);
    Theorem distribL(const Expr& x,const Expr& y,const Expr& z);
    Theorem addLID(const Expr& x);
    Theorem multLID(const Expr& x);
    Theorem addInvR(const Expr& x);
    Theorem multInvR(const Expr& x);public:
    Theorem ltAddR(const Expr& x,const Expr& y,const Expr& z);
    Theorem ltTrans(const Expr& x,const Expr& y,const Expr& z);
    Theorem ltScale(const Expr& x,const Expr& y,const Expr& z);
    Theorem arithmetic(const Expr& lhs,const Expr& rhs);
    Theorem minusDef(const Expr& x,const Expr& y);
    Theorem divideDef(const Expr& x,const Expr& y);
    
    // Derived Rules
    Theorem distribR(const Expr& x,const Expr& y,const Expr& z);
    Theorem addR(const Theorem& xEy,const Expr& z);
    Theorem addRID(const Expr& x);
    Theorem cancelR(const Expr& x,const Expr& y);
    Theorem addRCancel(const Theorem& t);
    Theorem multZeroL(const Expr& e);  

    // Core util
    Expr neg(const Expr& x);
    Expr inv(const Expr& x);
    Expr frac(const Expr& x,const Expr& y);
    Expr plus(const Expr& x,const Expr& y);
    Theorem trans(const Theorem& t1,const Theorem& t2);
    Theorem trans(const Expr& e);
    Theorem symm(const Theorem& t);
    Theorem subst(Op op,const Expr& x,const Theorem& t);
    Theorem subst(Op op,const Theorem& t,const Expr& x);
    Theorem subst(Op op,const Theorem& t1,const Theorem& t2);

  public:

    // Constructor
    RefinedArithTheoremProducer(VCL* vcl):
      ArithTheoremProducer(vcl),d_em(vcl->getEM()),zero(rat(0)),one(rat(1)),vcl(vcl) { 
      core = vcl->theoryCore();
    }

    // For convenience
    Expr rat(Rational r) { return Expr(d_em, r); }

    // Decision Prodedure Rules
    Theorem uMinusToMult(const Expr& e);
    Theorem minusToPlus(const Expr& x,const Expr& y);


    // test
    Theorem canonPlus(const Expr & e);

  };
  
   
}
#endif

---