bv_refinement_loop.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "bv_refinement.h"
 
#include <util/xml.h>
 
bv_refinementt::bv_refinementt(const infot &info)
  : bv_pointerst(*info.ns, *info.prop, *info.message_handler),
    progress(false),
    config_(info)
{
  // check features we need
  PRECONDITION(prop.has_assumptions());
  PRECONDITION(prop.has_set_to());
  PRECONDITION(prop.has_is_in_conflict());
}
 
decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption)
{
  // do the usual post-processing
  log.status() << "BV-Refinement: post-processing" << messaget::eom;
  finish_eager_conversion();
 
  log.debug() << "Solving with " << prop.solver_text() << messaget::eom;
 
  unsigned iteration=0;
 
  // now enter the loop
  while(true)
  {
    iteration++;
 
    log.status() << "BV-Refinement: iteration " << iteration << messaget::eom;
 
    // output the very same information in a structured fashion
    if(config_.output_xml)
    {
      xmlt xml("refinement-iteration");
      xml.data=std::to_string(iteration);
      log.status() << xml << '\n';
    }
 
    switch(prop_solve())
    {
    case resultt::D_SATISFIABLE:
      check_SAT();
      if(!progress)
      {
        log.status() << "BV-Refinement: got SAT, and it simulates => SAT"
                     << messaget::eom;
        log.status() << "Total iterations: " << iteration << messaget::eom;
        return resultt::D_SATISFIABLE;
      }
      else
        log.status() << "BV-Refinement: got SAT, and it is spurious, refining"
                     << messaget::eom;
      break;
 
    case resultt::D_UNSATISFIABLE:
      check_UNSAT();
      if(!progress)
      {
        log.status()
          << "BV-Refinement: got UNSAT, and the proof passes => UNSAT"
          << messaget::eom;
        log.status() << "Total iterations: " << iteration << messaget::eom;
        return resultt::D_UNSATISFIABLE;
      }
      else
        log.status()
          << "BV-Refinement: got UNSAT, and the proof fails, refining"
          << messaget::eom;
      break;
 
    case resultt::D_ERROR:
      return resultt::D_ERROR;
    }
  }
}
 
decision_proceduret::resultt bv_refinementt::prop_solve()
{
  // this puts the underapproximations into effect
  std::vector<exprt> assumptions;
 
  for(const approximationt &approximation : approximations)
  {
    assumptions.insert(
      assumptions.end(),
      approximation.over_assumptions.begin(),
      approximation.over_assumptions.end());
    assumptions.insert(
      assumptions.end(),
      approximation.under_assumptions.begin(),
      approximation.under_assumptions.end());
  }
 
  push(assumptions);
  propt::resultt result = prop.prop_solve(assumption_stack);
  pop();
 
  // clang-format off
  switch(result)
  {
  case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE;
  case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
  case propt::resultt::P_ERROR: return resultt::D_ERROR;
  }
  // clang-format off
 
  UNREACHABLE;
}
 
void bv_refinementt::check_SAT()
{
  progress=false;
 
  arrays_overapproximated();
 
  // get values before modifying the formula
  for(approximationt &approximation : this->approximations)
    get_values(approximation);
 
  for(approximationt &approximation : this->approximations)
    check_SAT(approximation);
}
 
void bv_refinementt::check_UNSAT()
{
  progress=false;
 
  for(approximationt &approximation : this->approximations)
    check_UNSAT(approximation);
}