cnf_theorem_producer.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file cnf_theorem_producer.cpp
 *\brief Implementation of CNF_TheoremProducer
 *
 * Author: Clark Barrett
 *
 * Created: Thu Jan  5 05:49:24 2006
 *
 * <hr>
 * Copyright (C) 2006 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>
 * 
 */
/*****************************************************************************/

#include "cnf_manager.h"

#define _CVCL_TRUSTED_
#include "cnf_theorem_producer.h"


using namespace std;
using namespace CVCL;
using namespace SAT;


/////////////////////////////////////////////////////////////////////////////
// class CNF_Manager trusted methods
/////////////////////////////////////////////////////////////////////////////


CNF_Rules* CNF_Manager::createProofRules(TheoremManager* tm) {
  return new CNF_TheoremProducer(tm);
}


/////////////////////////////////////////////////////////////////////////////
// Proof rules
/////////////////////////////////////////////////////////////////////////////


Theorem CNF_TheoremProducer::learnedClause(const Theorem& thm)
{
  IF_DEBUG(if(debugger.trace("cnf proofs")) {
    ostream& os = debugger.getOS();
    os << "learnedClause {" << endl;
    os << thm;
  });

  if(CHECK_PROOFS) {
    CHECK_SOUND(withAssumptions(),
                "learnedClause: called while running without assumptions");
  }

  vector<Expr> assumptions;

  thm.getLeafAssumptions(assumptions, true /*negate*/);

  vector<Expr>::iterator iend = assumptions.end();
  for (vector<Expr>::iterator i = assumptions.begin();
       i != iend; ++i) {
    DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions");
  }

  if (!thm.getExpr().isFalse())
    assumptions.push_back(thm.getExpr());

  Assumptions a;
  Proof pf;

  if(withProof()) {
    pf = newPf("learned_clause", thm.getProof());
  }

  // Use ExprManager in newExpr, since assumptions may be empty
  DebugAssert(assumptions.size() > 0, "Expected at least one entry");

  if (assumptions.size() == 1) {
    return newTheorem(assumptions[0], a, pf);
  }
  else {
    return newTheorem(Expr(OR, assumptions), a, pf);
  }
}


Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) {
  if(CHECK_PROOFS) {
    CHECK_SOUND(e.getType().isBool(),
                "CNF_TheoremProducer::ifLiftRule("
                "input must be a Predicate: e = " + e.toString()+")");
    CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos));
    CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(),
                "CNF_TheoremProducer::ifLiftRule("
                "input does not have an ITE: e = " + e.toString()+")");
  }
  const Expr& ite = e[itePos];
  const Expr& cond = ite[0];
  const Expr& t1 = ite[1];
  const Expr& t2 = ite[2];

  if(CHECK_PROOFS) {
    CHECK_SOUND(cond.getType().isBool(),
                "CNF_TheoremProducer::ifLiftRule("
                "input does not have an ITE: e = " + e.toString()+")");
  }    

  vector<Expr> k1 = e.getKids();
  Op op(e.getOp());

  k1[itePos] = t1;
  Expr pred1 =  Expr(op, k1);

  k1[itePos] = t2;
  Expr pred2 =  Expr(op, k1);

  Expr resultITE = cond.iteExpr(pred1, pred2);

  Assumptions a; Proof pf;
  if (withProof())
    pf = newPf("if_lift_rule", e, d_em->newRatExpr(itePos));
  return newRWTheorem(e, resultITE, a, pf);
}

---