satqe and vcegar from CVS

src/satqe/Makefile

@@ -0,0 +1,20 @@
+SRC = cube_set.cpp cubes.cpp satqe_satcheck.cpp
+
+LIBS =
+
+include ../config.inc
+include ../common
+
+all: satqe$(LIBEXT)
+
+ifneq ($(MINISAT),)
+MINISAT_INCLUDE=-I ../$(MINISAT)
+endif
+
+INCLUDES= $(MINISAT_INCLUDE) -I .. -I ../util
+
+###############################################################################
+
+satqe$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+

src/satqe/cube_set.cpp

@@ -0,0 +1,125 @@
+/*******************************************************************\
+
+Module: Cube Subsumption
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <assert.h>
+#include <iostream>
+
+#include "cube_set.h"
+
+#define ENABLE_SUBSUMPTION
+
+/*******************************************************************\
+
+Function: cube_sett::insert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cube_sett::_insert(const bitvt &stars, const bitvt &bits)
+{
+  bitssett &star=star_map[stars];
+
+  if(bits.size()==0)
+  {
+    all=true;
+    star.insert(bits);
+    return;
+  }
+
+  if(star.find(bits)!=star.end())
+  {
+    //assert(0);
+    return;
+  }
+
+  #if 0
+  std::cout << "SIZE: " << star.size() << std::endl;
+  #endif
+
+  bitvt tmp_bits(bits);
+  bool subsumed=false;
+
+  #ifdef ENABLE_SUBSUMPTION
+  for(unsigned i=0; i<tmp_bits.size(); i++)
+  {
+    bool old_bit=tmp_bits[i];
+    tmp_bits[i]=!old_bit;
+
+    #if 0
+    std::cout << "FIND ";
+    for(unsigned x=0; x<tmp_bits.size(); x++)
+      std::cout << " " << tmp_bits[x];
+    std::cout << "\n";
+    #endif
+
+    bitssett::iterator it=star.find(tmp_bits);
+
+    if(it!=star.end())
+    {
+      #if 0
+      std::cout << "FOUND\n";
+      #endif
+
+      // found it!
+      subsumed=1;
+      star.erase(it);
+      elements--;
+      bitvt tmp_stars(stars);
+
+      unsigned count=i+1, j;
+      for(j=0; j<tmp_stars.size(); j++)
+      {
+        if(!tmp_stars[j]) count--;
+
+        if(count==0)
+        {
+          tmp_stars[j]=1;
+          tmp_bits.erase(tmp_bits.begin()+i);
+
+          #if 0
+          std::cout << "Subsuming: " << tmp_bits.size() << std::endl;
+          #endif
+
+          _insert(tmp_stars, tmp_bits);
+          break;
+        }
+      }
+
+      assert(j<tmp_stars.size());
+    }
+
+    tmp_bits[i]=old_bit;
+  }
+  #endif
+
+  if(!subsumed)
+  {
+    star.insert(bits);
+    elements++;
+
+    #if 0
+    std::cout << "STARS: ";
+    for(unsigned i=0; i<stars.size(); i++)
+      std::cout << " " << stars[i];
+    std::cout << "\n";
+    #endif
+
+    #if 0
+    std::cout << "INSERTING ";
+    for(unsigned i=0; i<bits.size(); i++)
+      std::cout << " " << bits[i];
+    std::cout << "\n";
+    #endif
+  }
+}
+

src/satqe/cube_set.h

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+Module: Cube Subsumption
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef __CUBE_SET_H
+#define __CUBE_SET_H
+
+#include "cubes.h"
+
+class cube_sett:public cubest
+{
+ public:
+  cube_sett():elements(0), all(false), _no_insertions(0)
+  {
+  }
+ 
+  void insert(const bitvt &stars, const bitvt &bits)
+  {
+    _no_insertions++;
+    _insert(stars, bits);
+  }
+   
+  void _insert(const bitvt &stars, const bitvt &bits);
+
+  unsigned size() { return elements; }
+  
+  unsigned no_insertions() { return _no_insertions; }
+  
+  void clear()
+  {
+    star_map.clear();
+    elements=0;
+    all=false;
+    _no_insertions=0;
+  }
+   
+  void swap(cube_sett &b)
+  {
+    star_map.swap(b.star_map);
+    std::swap(elements, b.elements);
+    std::swap(all, b.all);
+  }
+   
+  bool is_all() const { return all; }
+
+ protected:
+  unsigned elements;
+  bool all;
+  unsigned _no_insertions;
+};
+
+#endif

src/satqe/cubes.cpp

@@ -0,0 +1,105 @@
+/*******************************************************************\
+
+Module: Cubes
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <assert.h>
+#include "cubes.h"
+
+/*******************************************************************\
+
+Function: cubest::make_vector
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cubest::make_vector(
+  const std::vector<unsigned> &map,
+  const bitvt &stars,
+  const bitvt &bits,
+  bvt &dest)
+{
+  dest.resize(bits.size());
+
+  unsigned bit=0;
+
+  for(unsigned i=0; i<stars.size(); i++)
+    if(!stars[i])
+    {
+      assert(bit<bits.size());
+      dest[bit].set(map[i], bits[bit]);
+      bit++;
+    }
+
+  assert(bit==bits.size());
+}
+
+/*******************************************************************\
+
+Function: cubest::make_vector
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cubest::make_vector(
+  const bitvt &stars,
+  const bitvt &bits,
+  std::set<unsigned> &dest)
+{
+  for(unsigned i=0; i<stars.size(); i++)
+    if(!stars[i])
+      dest.insert(i);
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream &operator<<(std::ostream &out, const cubest &cubes)
+{
+  for(cubest::star_mapt::const_iterator it=cubes.star_map.begin();
+      it!=cubes.star_map.end(); it++)
+  {
+    for(cubest::bitssett::const_iterator it2=it->second.begin();
+        it2!=it->second.end(); it2++)
+    {
+      unsigned bit=0;
+
+      for(unsigned i=0; i<it->first.size(); i++)
+      {
+        if(it->first[i])
+          out << "*";
+        else
+        {
+          out << ((*it2)[bit]?'1':'0');
+          bit++;
+        }
+      }
+
+      out << std::endl;
+    }
+  }
+  
+  return out;
+}

src/satqe/cubes.h

@@ -0,0 +1,70 @@
+/*******************************************************************\
+
+Module: Cubes
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef __CUBES_H
+#define __CUBES_H
+
+#include <vector>
+#include <set>
+#include <iostream>
+#include <map>
+
+#include <solvers/prop/literal.h>
+
+typedef std::vector<literalt> bvt;
+
+class cubest
+{
+ public:
+  cubest()
+  {
+  }
+ 
+  typedef std::vector<bool> bitvt;
+  typedef std::set<bitvt> bitssett;
+  
+  typedef std::map<bitvt, bitssett> star_mapt;
+  star_mapt star_map;
+  
+  void make_vector(
+    const std::vector<unsigned> &map,
+    const bitvt &stars,
+    const bitvt &bits,
+    bvt &dest);
+
+  void make_vector(
+    const bitvt &stars,
+    const bitvt &bits, std::set<unsigned> &dest);
+                   
+  void swap(cubest &cubes)
+  {
+    star_map.swap(cubes.star_map);
+  }
+   
+  void clear()
+  {
+    star_map.clear();
+  }
+   
+  bool empty() const
+  {
+    return star_map.empty();
+  }
+   
+  bool all_stars(const bitvt &starmap) const
+  {
+    for(unsigned i=0; i<starmap.size(); i++)
+      if(!starmap[i]) return false;
+
+    return true;
+  }
+   
+  friend std::ostream &operator<<(std::ostream &out, const cubest &cubes);
+};
+
+#endif

src/satqe/sat_cubes.cpp

@@ -0,0 +1,485 @@
+/*******************************************************************\
+
+Module: Satisfiablility Cube Generation
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <algorithm>
+
+#include "sat_cubes.h"
+
+//#define DEBUG
+
+/*******************************************************************\
+
+Function: sat_hook
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool sat_hook(CSolver *solver)
+{
+  ((class sat_cubest *)solver)->found_sat();
+  return true; // continue solving
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::set_important_variables
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::set_important_variables(
+  const std::vector<unsigned> &_important_variables)
+{
+  important_variables.clear();
+
+  for(std::vector<unsigned>::const_iterator
+      it=_important_variables.begin();
+      it!=_important_variables.end(); it++)
+    important_variables.insert(*it);
+
+  important_variablesv=_important_variables;
+}
+
+/*******************************************************************\
+
+Function: compare_var_stat
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+inline bool compare_var_stat(const pair<vector<CVariable>::iterator,int> &v1,
+                             const pair<vector<CVariable>::iterator,int> &v2);
+
+/*******************************************************************\
+
+Function: sat_cubest::update_var_stats
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+#if 0
+void sat_cubest::update_var_stats(void)
+{
+  for(unsigned int i=1; i<variables().size(); ++i)
+  {
+    CVariable &var=variable(i);
+
+    // normal Chaff scoring
+    var.score(0) = var.score(0)/2 + var.lits_count(0) - _last_var_lits_count[0][i];
+    var.score(1) = var.score(1)/2 + var.lits_count(1) - _last_var_lits_count[1][i];
+
+    #if 0 // decide target state variables last
+    if(is_important(i)) 
+    {
+      var.score(0)=0;
+      var.score(1)=0;
+    }
+    #else
+    #if 1 // decide target state variables first
+    if(is_important(i))
+    {
+      var.score(0)+=100000;
+      var.score(1)+=100000;
+    }
+    #endif
+    #endif
+
+    // normal Chaff scoring
+    _last_var_lits_count[0][i] = var.lits_count(0);
+    _last_var_lits_count[1][i] = var.lits_count(1);
+    _var_order[i-1] = pair<CVariable * , int>( &var, var.score());
+  }
+
+  // from here as in Chaff
+
+  ::stable_sort(_var_order.begin(), _var_order.end(), compare_var_stat);
+
+  for(int i=0; i<_var_order.size(); ++i)
+    _var_order[i].first->var_score_pos() = i;
+
+  _max_score_pos = 0;
+  
+  CSolver::update_var_stats();
+}
+#endif
+
+/*******************************************************************\
+
+Function: sat_cubest::decide_next_branch
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+#if 0
+bool sat_cubest::decide_next_branch(void)
+{
+    ++_stats.num_decisions;
+    if (!_implication_queue.empty()) {
+	//some hook function did a decision, so skip my own decision making.
+	//if the front of implication queue is 0, that means it's finished
+	//because var index start from 1, so 2 *vid + sign won't be 0. 
+	//else it's a valid decision.
+	_max_score_pos = 0; //reset the max_score_position.
+	return _implication_queue.front().first;
+    }
+	
+    int s_var = 0;
+
+    for (int i=_max_score_pos; i<_var_order.size(); ++i) {
+	CVariable & var = *_var_order[i].first;
+	if (var.value()==UNKNOWN) {
+	    //move th max score position pointer
+	    _max_score_pos = i;
+	    //make some randomness happen
+	    if (--_params.randomness < _params.base_randomness)
+		_params.randomness = _params.base_randomness;
+
+	    int randomness = _params.randomness;
+  	    if (randomness >= num_free_variables())
+  		randomness = num_free_variables() - 1;
+            int skip;
+            if(num_free_variables()==0)
+              skip=0;
+            else
+	      skip =random()%(1+randomness);
+
+	    int index = i;
+	    while (skip > 0) {
+		++index;
+		if (_var_order[index].first->value()==UNKNOWN)
+		    --skip;
+	    }
+	    vector<CVariable>::iterator ptr = _var_order[index].first;
+	    assert (ptr->value() == UNKNOWN);
+	    int sign = ptr->score(0) > ptr->score(1) ? 0 : 1;
+	    int var_idx = ptr - variables().begin();
+
+            #ifdef USE_PREVIOUS_ASSIGNMENT
+            if(!previous_assignment.empty())
+              sign=(previous_assignment[var_idx]&1);
+            #endif
+
+            #if 0
+            if(is_important(var_idx))
+              std::cout << "DECISION ON IMPORTANT VARIABLE: "
+                        << var_idx << " SIGN " << sign 
+                        << "LEVEL " << dlevel()+1 << std::endl;
+            else
+              std::cout << "DECISION ON " << var_idx << std::endl;
+            #endif
+
+	    s_var = var_idx + var_idx + sign;
+	    break;
+	}
+    }
+
+    if (s_var<2) //no more free vars, solution found,  quit
+	return false;
+    ++dlevel();
+    if (dlevel() > _stats.max_dlevel) _stats.max_dlevel = dlevel();
+    CHECK (cout << "**Decision at Level " << dlevel() ;
+	   cout <<": " << s_var << "\te.g. " << (s_var&0x1?"-":" ") ;
+	   cout <<(s_var>>1)  << endl; );
+    queue_implication(s_var, NULL_CLAUSE);
+    return true;
+}
+#endif
+
+/*******************************************************************\
+
+Function: sat_cubest::store_assignment
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::store_assignment()
+{
+  #ifdef USE_PREVIOUS_ASSIGNMENT
+  previous_assignment.resize(variables().size());
+  for(unsigned int i=0; i<variables().size(); i++)
+    previous_assignment[i]=variable(i).value();
+  #endif
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::show_assignment
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::show_assignment()
+{
+  std::cout << "ASSIGNMENT: " << std::endl;
+  for(std::vector<unsigned>::const_iterator
+      it=important_variablesv.begin();
+      it!=important_variablesv.end(); it++)
+  {
+    int i=*it;
+    switch(variable(i).value()) {
+     case DONT_CARE: std::cout << "(*" << i << "*) "; break;
+          case 0: std::cout << "-" << i << " "; break;
+          case 1: std::cout << i << " "; break;
+          default: std::cerr << "Unknown variable value state" << std::endl; exit(1);
+    }
+  }
+
+  std::cout << std::endl;
+
+  //dump_assignment_stack();
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::found_sat
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::found_sat()
+{
+  // clear stars
+  stars.clear();
+
+  // store assignment
+  store_assignment();
+
+  // maybe print assignment  
+  #ifdef DEBUG
+  show_assignment();
+  #endif
+
+  // enlarge
+  enlarge();
+
+  // build blocking clause
+  add_blocking_clause();
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::enlarge
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::enlarge()
+{
+  for(std::vector<unsigned>::const_iterator
+      it=important_variablesv.begin();
+      it!=important_variablesv.end(); it++)
+  {
+    unsigned int index=*it;
+
+    if(not_used.find(index)!=not_used.end())
+      stars.insert(index); 
+  }
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::add_blocking_clause
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void sat_cubest::add_blocking_clause()
+{
+  std::vector<int> blocking_clause;
+
+  blocking_clause.reserve(important_variablesv.size());
+
+  cube_sett::bitvt bits, stars_v;
+  bits.reserve(important_variablesv.size());
+  stars_v.reserve(important_variablesv.size());
+
+  for(std::vector<unsigned>::const_iterator
+      it=important_variablesv.begin();
+      it!=important_variablesv.end(); it++)
+  {
+    unsigned int index=*it;
+
+    if(stars.find(index)!=stars.end())
+      stars_v.push_back(1);
+    else
+      switch(variable(index).value())
+      {
+       case 0: blocking_clause.push_back(2*index);   stars_v.push_back(0); bits.push_back(0); break;
+       case 1: blocking_clause.push_back(2*index+1); stars_v.push_back(0); bits.push_back(1); break;
+       default: stars_v.push_back(1); break;
+      }
+  }
+
+  // show some progress
+  {
+    static unsigned cnt=0;
+    cnt++;
+    if((cnt&0x1ff)==0x100)
+      std::cout << "SIZE: " << cnt << std::endl;
+  }
+
+  #ifdef USE_CUBE_SET
+  if(cube_set1!=NULL)
+    cube_set1->insert(stars_v, bits);
+
+  if(cube_set2!=NULL)
+    cube_set2->insert(stars_v, bits);
+  #endif
+
+  #ifdef DEBUG
+  std::cout << "Blocking clause: ";
+  for(unsigned i=0; i<blocking_clause.size(); i++)
+    std::cout << " " 
+              << ((blocking_clause[i]&1)?"-":"")
+              << (blocking_clause[i] >> 1);
+  std::cout << "\n";
+  #endif
+
+  if(cube_list!=NULL)
+    cube_list->push_back(blocking_clause);
+
+  if(blocking_clause.size()==0)
+  {
+    // DONE
+    _stats.outcome = UNSATISFIABLE;
+  }
+  else if(add_blocking_clause(blocking_clause)<0)
+  {
+    _stats.outcome = UNSATISFIABLE;
+    // done, unsat
+    //std::cout << "DONE, UNSAT\n";
+  }
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::add_blocking_clause
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int sat_cubest::add_blocking_clause(
+  std::vector<int> &blocking_clause)
+{
+  int *lits=&blocking_clause.front();
+
+  ClauseIdx added_cl=
+    CSolver::add_orig_clause(lits, blocking_clause.size());
+
+  if(added_cl<0) //memory out.
+    abort();
+  
+  //adjust_variable_order(lits, blocking_clause.size());
+
+  int back_dl=0;
+    
+  for(unsigned i=0; i<clause(added_cl).num_lits(); ++i)
+  {
+    int vid=clause(added_cl).literal(i).var_index();
+    //int sign=clause(added_cl).literal(i).var_sign();
+    assert(variable(vid).value()!=UNKNOWN);
+    assert(literal_value(clause(added_cl).literal(i))==0);
+    int dl=variable(vid).dlevel();
+
+    //std::cout << "DL: " << dl << " " << dlevel() << std::endl;
+
+    back_dl=std::max(dl, back_dl);
+  }
+
+  //std::cout << "BDL: " << back_dl << " " << dlevel() << std::endl;
+
+  if(back_dl<dlevel())
+    back_track(back_dl+1);
+
+  _conflicts.push_back(added_cl);
+  return analyze_conflicts();
+}
+
+/*******************************************************************\
+
+Function: sat_cubest::preprocess
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int sat_cubest::preprocess(void) 
+{
+  not_used.clear();
+
+  for(int i=1, sz=variables().size(); i<sz; ++i)
+  {
+    CVariable &v=variable(i);
+
+    if(v.lits_count(0)==0 && v.lits_count(1)==0)
+      not_used.insert(i);
+  }
+
+  int r=CSolver::preprocess();
+
+  return r;
+}

src/satqe/sat_cubes.h

@@ -0,0 +1,104 @@
+/*******************************************************************\
+
+Module: Satisfiablility Cube Generation
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SAT_CUBES_H
+#define CPROVER_SAT_CUBES_H
+
+// options
+
+// #define USE_PREVIOUS_ASSIGNMENT
+#define USE_CUBE_SET
+
+#include <list>
+#include <map>
+#include <set>
+
+#include <zchaff_solver.h>
+
+#ifdef USE_CUBE_SET
+#include "cube_set.h"
+#endif
+
+#define DONT_CARE       3
+
+#if 0
+class varct
+{
+ public:
+  typedef std::list<int> clause_listt;
+  clause_listt clause_list;
+};
+#endif
+
+bool sat_hook(CSolver *solver);
+
+class sat_cubest:public CSolver
+{
+public:
+  sat_cubest(const CSolver &_solver):CSolver(_solver)
+  { 
+    init();
+  }
+   
+  sat_cubest() { init(); }
+  
+  virtual ~sat_cubest() { }
+
+  void set_important_variables(const std::vector<unsigned> &_important_variables);
+
+  typedef std::list<std::vector<int> > cube_listt;
+  cube_listt *cube_list;
+
+  cube_sett *cube_set1;
+  cube_sett *cube_set2;
+
+  virtual void found_sat();   
+
+protected:
+  // chaff overloads
+  virtual int preprocess();
+  //virtual bool decide_next_branch(void);
+  //virtual void update_var_stats(void);
+  
+  int add_blocking_clause(std::vector<int> &clause);
+
+  std::set<int> not_used;
+
+protected:
+  // new methods
+  void show_assignment();
+  void store_assignment();
+  virtual void add_blocking_clause();
+  virtual void enlarge();
+
+  typedef std::set<unsigned> important_variablest;  
+  important_variablest important_variables;
+  std::vector<unsigned> important_variablesv;
+
+  std::set<unsigned> stars;
+  
+  #ifdef USE_PREVIOUS_ASSIGNMENT
+  std::vector<char> previous_assignment;
+  #endif
+
+protected:
+  void init()
+  {
+    cube_list=NULL;
+    cube_set1=cube_set2=NULL;
+    add_sat_hook(sat_hook);
+  }
+ 
+  bool is_important(unsigned int i)
+  {
+    return important_variables.find(i)!=
+           important_variables.end();
+  }
+};
+
+#endif

src/satqe/satqe_satcheck.cpp

@@ -0,0 +1,122 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <i2string.h>
+
+#include "satqe_satcheck.h"
+
+/*******************************************************************\
+
+Function: satqe_satcheckt::satqe_satcheckt
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+satqe_satcheckt::satqe_satcheckt()
+{
+  cube_set1=NULL;
+  cube_set2=NULL;
+}
+
+/*******************************************************************\
+
+Function: satqe_satcheckt::~satqe_satcheckt
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+satqe_satcheckt::~satqe_satcheckt()
+{
+}
+
+/*******************************************************************\
+
+Function: satqe_satcheckt::prop_solve
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+propt::resultt satqe_satcheckt::prop_solve()
+{
+  {
+    std::string msg=
+      i2string(no_variables())+" variables, "+
+      i2string(no_clauses())+" clauses";
+    messaget::status(msg);
+  }
+  
+  while(true)
+  {  
+    switch(SUB::prop_solve())
+    {
+    case P_SATISFIABLE:
+      // SAT, record cube and add blocking clause
+      {
+        cubest::bitvt stars, bits;
+
+        stars.resize(important_variables.size(), false);
+        bits.resize(important_variables.size(), false);
+        
+        bvt c;
+        c.resize(important_variables.size());
+    
+        for(unsigned i=0; i<important_variables.size(); i++)
+        {
+          unsigned v=important_variables[i];
+
+          assert(v<no_variables());
+
+          tvt value=l_get(literalt(v, false));
+
+          if(value.is_true())
+          {
+            bits[i]=true;
+            c[i]=literalt(v, true);
+          }
+          else if(value.is_false())
+          {
+            bits[i]=false;
+            c[i]=literalt(v, false);
+          }
+          else
+            assert(false);
+        }
+
+        if(cube_set1!=NULL) cube_set1->insert(stars, bits);
+        if(cube_set2!=NULL) cube_set2->insert(stars, bits);
+
+        lcnf(c);
+      }
+      break;
+    
+    case P_UNSATISFIABLE:
+      // UNSAT
+     return P_UNSATISFIABLE;
+      
+    default:
+      return P_ERROR;
+    }
+  }
+  
+  return P_ERROR;
+}

src/satqe/satqe_satcheck.h

@@ -0,0 +1,50 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SATQE_SATCHECK_H
+#define CPROVER_SATQE_SATCHECK_H
+
+#include <solvers/sat/satcheck.h>
+
+#include "cube_set.h"
+
+class satqe_satcheckt:public satcheckt
+{
+public:
+  satqe_satcheckt();
+  virtual ~satqe_satcheckt();
+
+  void set_cube_set(cube_sett &_cube_set)
+  {
+    cube_set1=&_cube_set;
+  }
+  
+  cube_sett *cube_set1;
+  cube_sett *cube_set2;
+  
+  void quantify(literalt l)
+  {
+    assert(!l.sign());
+    important_variables.push_back(l.var_no());
+  }
+  
+  virtual resultt prop_solve();
+  
+  void set_important_variables(
+    std::vector<unsigned> &_important_variables)
+  {
+    important_variables=_important_variables;
+  }
+  
+  typedef satcheckt SUB;
+  
+protected:
+  std::vector<unsigned> important_variables;
+};
+
+#endif

src/vcegar/Makefile

@@ -0,0 +1,38 @@
+SRC = vcegar.cpp parseoptions.cpp discover_predicates.cpp \
+      canonicalize.cpp partitioning.cpp instantiate_guards.cpp \
+      abstractor.cpp  main.cpp vcegar_loop.cpp bmc.cpp \
+      predicates.cpp refiner.cpp  simulator.cpp \
+      modelchecker_smv.cpp predabs_aux.cpp \
+      abstract_expression.cpp vcegar_util.cpp network_info.cpp \
+      abstract_counterexample.cpp
+
+OBJ = $(SRC:.cpp=$(OBJEXT)) \
+      ../util/util$(LIBEXT) \
+      ../langapi/langapi$(LIBEXT) \
+      ../smvlang/smvlang$(LIBEXT) \
+      ../verilog/verilog$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) \
+      ../satqe/satqe$(LIBEXT) \
+      ../big-int/bigint$(OBJEXT) \
+      ../ebmc/ebmc_base$(LIBEXT) \
+      ../trans/trans$(LIBEXT)
+
+INCLUDES= -I ../$(CHAFF)  -I ../util
+
+LIBS =
+
+include ../config.inc
+include ../common
+
+all: vcegar$(EXEEXT)
+
+GCCFLAGS += -Wall -g  
+
+###############################################################################
+
+vcegar$(EXEEXT): $(OBJ)
+	$(CXX) $(LINKFLAGS) -o $@ $(OBJ) $(LIBS) 
+
+clean:
+	rm -f $(SRC:.cpp=$(OBJEXT)) vcegar$(EXEEXT)
+

src/vcegar/abstract_counterexample.cpp

@@ -0,0 +1,126 @@
+/*******************************************************************\
+
+Module: Counterexamples
+
+Author: Daniel Kroening
+
+  Date: June 2003
+
+\*******************************************************************/
+
+#include "abstract_counterexample.h"
+
+#include <langapi/mode.h>
+#include <langapi/languages.h>
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream &operator<<
+ (std::ostream &out, const abstract_statet &state)
+{
+  for(unsigned i=0; i<state.predicate_values.size(); i++)
+    out << " b" << i << "=" << state.predicate_values[i] <<" ";
+  
+  out << std::endl;
+  
+  return out;
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream &operator<< 
+(std::ostream &out, const abstract_counterexamplet &cex)
+{
+  unsigned i = 0;
+  
+  for (abstract_counterexamplet::const_iterator accit  = cex.begin();
+       accit != cex.end(); accit++)
+  {
+    out << "State: " <<i<<"\n";
+    out << *accit; 
+    i++;
+  }
+
+  out << std::endl;
+
+  return out;
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream &operator<<
+ (std::ostream &out, const abstract_constraintt &constraint)
+{
+  for(unsigned i=0; i<constraint.size(); i++)
+    {
+      
+      switch (constraint[i]) { 
+      case ZERO :
+	out << " b" << i << "=" << 0 <<" ";
+	break;
+      case ONE:
+	out << " b" << i << "=" << 1 <<" ";
+	break;
+      case NON_DET:
+	out << " b" << i << "= *"   <<" ";
+	break;
+      }
+    }
+    
+  out << std::endl;
+
+  return out;
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream& operator<< (
+  std::ostream& out,
+  const abstract_transition_constraintt &abstract_transition_constraint)
+{
+  out << abstract_transition_constraint.first;
+  out << "--------> \n";
+  out << abstract_transition_constraint.second;
+
+  return out;
+}

src/vcegar/abstract_counterexample.h

@@ -0,0 +1,74 @@
+/*******************************************************************\
+
+Module: Counterexamples
+
+Author: Daniel Kroening
+        Karen Yorav 
+        Himanshu Jain
+   
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_ABSTRACT_COUNTEREXAMPLE_H
+#define CPROVER_ABSTRACT_COUNTEREXAMPLE_H
+
+#include <iostream>
+#include <vector>
+#include <list>
+
+#include "abstract_trans.h"
+
+/* An abstract state */
+class abstract_statet
+{
+public:
+  typedef std::vector<bool> predicate_valuest;
+  predicate_valuest predicate_values;
+
+  friend std::ostream& operator<<
+    (std::ostream& out,
+     const abstract_statet &state);
+  
+  friend bool operator<(const abstract_statet &as1, const abstract_statet &as2)
+  {
+    return (as1.predicate_values < as2.predicate_values);
+  }
+};
+
+/* An abstract conterexample */
+
+typedef std::vector<abstract_statet> abstract_counterexamplet;
+typedef std::vector<std::pair<abstract_statet, abstract_statet> > 
+				 spurious_abstract_stepst;
+
+typedef std::pair<abstract_statet, abstract_statet> abstract_transitiont;
+typedef std::set<abstract_transitiont> abstract_transitionst;
+
+typedef enum {ZERO, ONE, NON_DET} valuet;
+
+//Exactly similar to spurious abstract state. Only that it contains
+//vector of boolean values, whereas here we also have a NON_DET value possible 
+//in valuet.
+typedef std::vector<valuet> abstract_constraintt;
+
+typedef std::pair<abstract_constraintt,  abstract_constraintt> abstract_transition_constraintt;
+
+typedef std::set<abstract_transition_constraintt> abstract_transition_constrainst;
+
+typedef std::set<std::pair<abstract_transition_constraintt, abstract_transition_constraintt > > weakest_precondition_constrainst;
+
+typedef std::set<abstract_constraintt> abstract_initial_constrainst;
+
+std::ostream& operator<<
+     (std::ostream& out,
+      const abstract_constraintt &state);
+
+std::ostream& operator<<
+     (std::ostream& out,
+      const abstract_transition_constraintt &abstract_transition_constraint);
+
+std::ostream &operator<< 
+(std::ostream &out, const abstract_counterexamplet &cex);
+                          
+#endif

src/vcegar/abstract_expression.cpp

@@ -0,0 +1,146 @@
+/*******************************************************************\
+
+Module: Create abstract expression from concrete one
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <i2string.h>
+
+#include "abstract_expression.h"
+#include "canonicalize.h"
+
+/*******************************************************************\
+
+Function: make_it_a_predicate
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void make_it_a_predicate(const predicatest &predicates,
+                         exprt &expr)
+ {
+  bool negation;
+
+  canonicalize(expr, negation);
+
+  // see if we have it
+  unsigned nr;
+  if(predicates.find(expr, nr))
+   {
+    // yes, we do!
+
+    // see if it is a constant
+    if(predicates[nr].is_true())
+      expr.make_true();
+    else if(predicates[nr].is_false())
+      expr.make_false();
+    else
+     {
+      expr=exprt("predicate_symbol", typet("bool"));
+      expr.set("identifier", nr);
+     }
+
+    if(negation)
+      expr.make_not();
+   }
+  else
+   {
+    // nah, we don't
+    // make it nondeterministic choice
+    exprt tmp("nondet_symbol", typet("bool"));
+    tmp.add("expression").swap(expr);
+    expr.swap(tmp);
+   }
+ }
+
+/*******************************************************************\
+
+Function: abstract_expression
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void abstract_expression(const predicatest &predicates,
+                         exprt &expr)
+ {
+  if(expr.type().id()!="bool")
+    {
+      std::cout << expr << "\n";
+      throw "abstract_expression expects expression of type Boolean";
+    }
+
+  if(expr.id()=="and" || expr.id()=="or" ||
+     expr.id()=="not" || expr.id()=="=>" ||
+     expr.id()=="xor" ||
+     expr.id()=="AG" 
+     )
+   {
+    Forall_operands(it, expr)
+      abstract_expression(predicates, *it);
+   }
+  else if(expr.id()=="=" || expr.id()=="notequal")
+   {
+    if(expr.operands().size()!=2)
+      throw expr.id_string()+" takes two operands";
+
+    // Is it equality on Booleans?
+
+    if(expr.operands()[0].type().id()=="bool" &&
+       expr.operands()[1].type().id()=="bool")
+     {
+      // leave it in
+
+      Forall_operands(it, expr)
+        abstract_expression(predicates, *it);
+     }
+    else // other types, make it a predicate
+      make_it_a_predicate(predicates, expr);
+   }
+  else if(expr.is_constant())
+   {
+    // leave it as is
+   }
+  else
+    make_it_a_predicate(predicates, expr);
+ }
+
+/*******************************************************************\
+
+Function: abstract_expression
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void abstract_expression(const predicatest &predicates,
+                         exprt &expr, int choice)
+ {
+   switch(choice) {
+   case 1:{ 
+     abstract_expression(predicates,expr); 
+     break;
+   }
+   case 2: {
+     //property is itself a predicate
+     make_it_a_predicate(predicates, expr); 
+     break;
+   }
+   }
+   
+ }

src/vcegar/abstract_expression.h

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Create abstract expression from concrete one
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_ABSTRACT_EXPRESSION_H
+#define CPROVER_ABSTRACT_EXPRESSION_H
+
+#include "predicates.h"
+
+void abstract_expression(const predicatest &predicates,
+                       exprt &expr);
+
+void abstract_expression(const predicatest &predicates,
+                         exprt &expr, int choice);
+
+
+#endif

src/vcegar/abstract_initial_states.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module: Predicate Abstraction of a Predicate
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CEGAR_ABSTRACT_PREDICATE_H
+#define CEGAR_ABSTRACT_PREDICATE_H
+
+#include <set>
+#include <satqe/cubes.h>
+
+class abstract_initial_statest
+ {
+ public:
+  cubest cubes;
+  std::vector<unsigned> input_predicates;
+  
+  void clear()
+   {
+    cubes.clear();
+    input_predicates.clear();
+   }
+ };
+
+#endif

src/vcegar/abstract_trans.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: An Abstract Transition System
+
+Author: Daniel Kroening
+        Karen Yorav 
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_ABSTRACT_TRANS_H
+#define CPROVER_ABSTRACT_TRANS_H
+
+#include "abstract_trans_rel.h"
+#include "abstract_initial_states.h"
+#include "specification.h"
+
+class abstract_transt
+{
+public:
+  //Vector of transition relation constrains
+  std::vector<abstract_transition_relationt> abstract_trans_vector;
+  std::vector<abstract_initial_statest> abstract_init_vector;
+     
+  std::vector<abstract_transition_relationt> refinement_preds_trans_vector;
+
+  // variables
+  struct variablet
+  {
+    std::string description;
+  };
+
+  typedef std::vector<variablet> variablest;
+  variablest variables;
+
+  specificationt abstract_spec;
+};
+
+#endif

src/vcegar/abstract_trans_rel.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+Module: Predicate Abstraction of circuits
+
+Author: Daniel Kroening, kroening@kroening.com
+         
+\*******************************************************************/
+
+#ifndef CEGAR_ABSTRACT_TRANS_REL_H
+#define CEGAR_ABSTRACT_TRANS_REL_H
+
+#include <set>
+#include <satqe/cubes.h>
+
+
+class abstract_transition_relationt
+ {
+ public:
+  cubest cubes;
+  std::vector<unsigned> input_predicates;
+  std::vector<unsigned> output_predicates;
+  std::vector<unsigned> unchanged_predicates;
+  
+  void clear()
+   {
+    cubes.clear();
+    input_predicates.clear();
+    output_predicates.clear();
+    unchanged_predicates.clear();
+   }
+ };
+
+
+#endif

src/vcegar/abstractor.cpp

@@ -0,0 +1,731 @@
+/*******************************************************************\
+
+Module: Abstractor (generates abstract program given a set of predicates)
+
+Author: Himanshu Jain
+
+Date: April 2004
+
+\*******************************************************************/
+
+#include <map>
+#include <vector>
+#include <i2string.h>
+#include <namespace.h>
+
+#include <find_symbols.h>
+#include <verilog/expr2verilog.h>
+#include <solvers/flattening/boolbv.h>
+#include <satqe/satqe_satcheck.h>
+#include <trans/instantiate.h>
+#include <trans/unwind.h>
+
+#include "abstractor.h"
+#include "predabs_aux.h"
+#include "partitioning.h"
+
+/*******************************************************************\
+
+Function: abstractort::abstract_variables
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void abstractort::abstract_variables(
+  const predicatest &predicates,
+  abstract_transt::variablest &variables)
+{
+  variables.clear();
+  variables.resize(predicates.size());
+
+  for(unsigned i=0; i<predicates.size(); i++) 
+    variables[i].description=expr2verilog(predicates[i]);
+}
+
+/*******************************************************************\
+
+Function: abstractort::calc_abstraction
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: compute abstraction according to set of predicates
+
+\*******************************************************************/
+
+void abstractort::calc_abstraction(
+  const predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const namespacet &ns,
+  const network_infot &network,
+  const partitioningt::pred_id_clusterst &pred_id_clusters)
+{
+  abstract_variables(predicates, abstract_trans.variables);
+
+  calc_abstraction_with_partition(
+    predicates, concrete_trans, 
+    ns, network, pred_id_clusters);
+}
+
+
+/*******************************************************************\
+
+Function: abstractort::calc_abstraction_with_partition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: compute abstraction according to set of predicates which 
+          will be partitioned for scalibility
+
+\*******************************************************************/
+
+void abstractort::calc_abstraction_with_partition(
+  const predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const namespacet &ns,
+  const network_infot &network,
+  const partitioningt::pred_id_clusterst &pred_id_clusters)
+{
+  // copy trans
+  transt trans(concrete_trans.trans_expr);
+   
+  ns.follow_macros(trans); 
+
+  if(abs_init_states)
+  {
+    calc_init_states_abstraction(
+      predicates, 
+      concrete_trans,
+      trans,
+      ns,
+      network);
+  }
+
+  calc_trans_rel_abstraction(
+    predicates, 
+    concrete_trans,
+    trans,
+    ns,
+    network);
+
+  // Using the clusters generated from the removal
+  // of spurious abstract counterexamples
+   
+  if(use_refinement_clusters) 
+  {
+    refinement_guided_partitioning_abstraction(
+      predicates, 
+      concrete_trans,
+      trans,
+      ns,
+      network,
+      pred_id_clusters);
+  }
+}
+
+/*******************************************************************\
+
+Function: abstractort::calc_init_states_abstraction
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Calculates initial states in the abstraction.
+
+\*******************************************************************/
+
+void abstractort::calc_init_states_abstraction(
+  const predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const transt &trans,
+  const namespacet &ns,
+  const network_infot &network)
+{
+  partitioningt partition;
+    
+  init_pred_clusters.clear();
+   
+  #ifdef DEBUG
+  std::cout << "Partitioning predicates for initial set of predicates";
+  #endif
+
+  partition.partition_initial_predicates(
+    predicates, 
+    ns,
+    trans,
+    concrete_trans.var_map,
+    network,
+    init_pred_clusters);
+  
+  #ifdef DEBUG
+  std::cout << "..done\n";
+  #endif
+
+  unsigned i=0;
+
+  //Remove the old init state clusters
+  abstract_trans.abstract_init_vector.clear();
+   
+  for(partitioningt::predicate_clusterst::const_iterator
+      it=init_pred_clusters.begin();
+      it!=init_pred_clusters.end();
+      it++) 
+  {
+       #ifdef DEBUG
+       std::cout <<"Initial states cluster no. "<<i <<" \n";
+       std::cout << *it;
+       #endif
+
+       abstract_trans.abstract_init_vector.
+	 push_back(abstract_initial_statest());
+       
+       unsigned insert_at = abstract_trans.abstract_init_vector.size()-1;
+       bool cache_hit = false;
+       
+       partitioningt::pred_id_set_pairt init_id_set;
+
+       if (init_state_caching)
+	 {
+	   it->get_pred_ids(init_id_set);
+	   
+	   states_cubes_cachet::const_iterator init_it =  init_cubes_cache.find(init_id_set);
+	   
+	   init_cache_num_access++;
+	   
+	   if (init_it != init_cubes_cache.end())
+	     {
+	       abstract_trans.abstract_init_vector[insert_at] = init_it -> second;
+	       cache_hit = true;
+	       init_cache_num_hits ++ ;
+	     }
+	 }
+       
+       if (!init_state_caching || !cache_hit)
+	 {
+    	   calc_abstract_initial_states(
+    	     *it, 
+	     concrete_trans,
+	     trans, //follow macros is assumed to be done
+	     abstract_trans.abstract_init_vector[insert_at],
+	     ns);
+	   
+	   if (init_state_caching)
+	     {
+	       init_cubes_cache.insert(std::pair <partitioningt::pred_id_set_pairt, 
+				       abstract_initial_statest>
+				       (init_id_set, abstract_trans.abstract_init_vector[insert_at]));
+	       
+	     }
+
+	   i++;
+	 }
+       
+       if (it->size() > max_init_state_cluster_size)
+	 max_init_state_cluster_size = it->size();
+  }
+
+  num_init_clusters = abstract_trans.abstract_init_vector.size();
+   
+}
+
+/*******************************************************************\
+
+Function: abstractort::calc_trans_rel_abstraction
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Calculates transition relation of the abstraction.
+
+\*******************************************************************/
+
+void abstractort::calc_trans_rel_abstraction(
+  const predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const transt &trans,
+  const namespacet &ns,
+  const network_infot &network)
+{
+  partitioningt partition;
+    
+  pred_clusters.clear();
+   
+  if(verbose)
+    status("Computing partitioned transition relation of the abstraction");
+   
+  partition.partition_predicates(
+    predicates, 
+    trans, 
+    ns,
+    concrete_trans.var_map,
+    network,
+    pred_clusters,
+    partitioning_strategy,
+    verbose);
+   
+  unsigned i=0;
+   
+  //Remove the old clusters
+  abstract_trans.abstract_trans_vector.clear();
+   
+  for(partitioningt::predicate_clusterst::const_iterator
+      it=pred_clusters.begin();
+      it!=pred_clusters.end();
+      it++)
+  {
+    if(verbose)
+    {
+      std::cout <<"Transition relation cluster no. "<<i <<" \n";
+      std::cout << *it;
+    }
+
+    abstract_trans.abstract_trans_vector.
+      push_back(abstract_transition_relationt());
+
+    bool cache_hit = false;
+       
+    partitioningt::pred_id_set_pairt trans_id_set;
+
+    if(trans_rel_caching)
+    {
+      it->get_pred_ids(trans_id_set);
+	 
+      trans_cubes_cachet::const_iterator trans_it =  
+        trans_cubes_cache.find(trans_id_set);
+	 
+      trans_cache_num_access++;
+	 
+      if (trans_it != trans_cubes_cache.end())
+      {
+        abstract_trans.abstract_trans_vector.back() = trans_it -> second;
+        cache_hit = true;
+        trans_cache_num_hits ++ ;
+      }
+    }
+       
+    if(!trans_rel_caching || !cache_hit)
+    {
+      calc_abstract_trans_rel(
+        *it, 
+	concrete_trans,
+	trans, //follow macros is assumed to be done
+	abstract_trans.abstract_trans_vector.back(),
+	ns);
+	 
+      trans_cubes_cache.insert(
+        std::pair <partitioningt::pred_id_set_pairt, 
+		   abstract_transition_relationt>
+	  (trans_id_set, abstract_trans.abstract_trans_vector.back()));
+      i++;
+    }
+     
+    if(it->size() > max_trans_cluster_size)
+      max_trans_cluster_size = it->size();
+  }
+   
+  num_trans_clusters = abstract_trans.abstract_trans_vector.size();
+}
+
+/*******************************************************************\
+
+Function: abstractort::refinement_guided_partitioning_abstraction
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Calculates transition relation of clusters generated from 
+refinement.
+
+\*******************************************************************/
+
+void abstractort::refinement_guided_partitioning_abstraction(
+  const predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const transt &trans,
+  const namespacet &ns,
+  const network_infot &network,
+  const partitioningt::pred_id_clusterst &pred_id_clusters)
+{
+   partitioningt partition;
+
+   abstract_trans.refinement_preds_trans_vector.clear();
+   
+   #ifdef DEBUG
+   std::cout <<"Refinement generated clusters \n";
+   partition.print_clusters (pred_id_clusters);
+   #endif
+       
+   for (partitioningt::pred_id_clusterst::const_iterator it = pred_id_clusters.begin();
+	it != pred_id_clusters.end(); it++)
+     {
+       abstract_trans.refinement_preds_trans_vector.
+	 push_back(abstract_transition_relationt());
+       
+       unsigned insert_at = abstract_trans.refinement_preds_trans_vector.size()-1;
+       bool cache_hit = false;
+       
+       if (pred_id_clusters_caching)
+	 {
+	   trans_cubes_cachet::const_iterator pcit =  refine_cubes_cache.find(*it);
+	
+	   pred_id_cache_num_access++;
+
+	   if (pcit != refine_cubes_cache.end())
+	     {
+	       abstract_trans.refinement_preds_trans_vector[insert_at] = pcit -> second;
+	       cache_hit = true;
+	       pred_id_cache_num_hits ++ ;
+	     }
+	 }
+       
+       #ifdef DEBUG
+       std::cout <<"Refine clusters cache: "<<pred_id_cache_num_hits<<"\n";
+       #endif
+
+       if (!pred_id_clusters_caching || !cache_hit)
+	 {
+	   //compute actual predicates from the pred id set
+	   predicatest pred_cluster; 
+	   
+	   partition.obtain_refinement_cluster
+	     (predicates,
+	      network,
+	      ns,
+	      *it,
+	      pred_cluster);
+	   
+	   calc_abstract_trans_rel
+	     (pred_cluster, 
+	      concrete_trans,
+	      trans, //follow macros is assumed to be done
+	      abstract_trans.refinement_preds_trans_vector[insert_at],
+	      ns);
+	   
+	   if (pred_id_clusters_caching) 
+	     {
+	       refine_cubes_cache.insert(std::pair <partitioningt::pred_id_set_pairt, 
+					 abstract_transition_relationt>
+					 (*it, 
+					  abstract_trans.refinement_preds_trans_vector[insert_at]));
+	     }
+	   
+	   if (pred_cluster.size() > max_trans_cluster_size)
+	     max_trans_cluster_size = pred_cluster.size();
+	 }
+     }
+
+}
+
+
+
+/*******************************************************************\
+
+Function: abstractort::calc_abstract_trans_rel
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: compute abstract transition relation according to the
+          given set of predicates.
+          Predicates contains a mixture of current state and next
+          state predicates.  
+
+\*******************************************************************/
+
+void abstractort::calc_abstract_trans_rel(
+  const predicatest &cluster, 
+  const concrete_transt &concrete_trans,
+  const transt &trans, //follow macros is assumed to be done
+  abstract_transition_relationt &abstract_transition_relation,
+  const namespacet &ns)
+{
+  //It is assumed that follow macros has already been called for
+  // the concrete transition relation and predicates in the "cluster".
+
+  //Obtain the initial and final set of predicates
+  std::vector<exprt> initial_predicates, final_predicates;
+  std::vector<unsigned> input, output;
+
+
+  for(unsigned i=0; i<cluster.size(); i++) //No test is made to test if the value
+  {                                        //of a predicate does not change.    
+    predicatest::statet state;
+
+    unsigned nr;
+    cluster.get_info(cluster[i], nr, state);
+
+    switch(state)
+    {
+    case predicatest::INITIAL:
+      {
+        input.push_back(nr);
+        initial_predicates.push_back(cluster[i]);
+        break;
+      }
+
+    case predicatest::FINAL:
+      {
+        output.push_back(nr);
+        final_predicates.push_back(cluster[i]);
+
+        break;
+      }
+    case predicatest::NOT_DEFINED:
+      {
+	assert(false);
+	break;
+      }
+    }
+  }
+
+  #ifdef DEBUG
+  std::cout <<" ASSERTITION REMOVED FOR GCR\n";
+  #endif
+  //   assert(output.size()!=0);
+    
+  // Now obtain the cubes for the abstract transition relation.
+  // We will create a new SAT solver object.
+
+  satqe_satcheckt satqe_satcheck;
+  satqe_satcheck.set_message_handler(message_handler);
+   
+  boolbvt boolbv(satqe_satcheck);
+  boolbv.set_message_handler(message_handler);
+  
+  exprt instantiated_trans(trans.trans());
+  instantiate(instantiated_trans, 0, ns);
+  
+  exprt instantiated_invar0(trans.invar());
+  instantiate(instantiated_invar0, 0, ns);
+
+  exprt instantiated_invar1(trans.invar());
+  instantiate(instantiated_invar1, 1, ns);
+  
+  boolbv.set_to_true(instantiated_invar0);
+  boolbv.set_to_true(instantiated_invar1);
+  boolbv.set_to_true(instantiated_trans);
+
+  cube_sett trans_cube_set;
+  satqe_satcheck.set_cube_set(trans_cube_set);
+    
+  std::vector<unsigned> important_variables;
+  important_variables.reserve(input.size() + output.size());
+    
+  if(show_cubes) 
+    std::cout << " Order of cubes:";
+
+  for(unsigned i=0; i<input.size(); i++)
+  {
+    unsigned p=input[i];
+    exprt tmp(initial_predicates[i]);
+    instantiate(tmp, 0, ns);
+    
+    literalt l=make_pos(boolbv, tmp);
+    important_variables.push_back(l.var_no());
+    abstract_transition_relation.input_predicates.push_back(p);
+       
+    if(show_cubes)
+      std::cout << " " << p;
+  }
+   
+  if(show_cubes)
+    std::cout <<" |";
+   
+  for(unsigned i=0; i<output.size(); i++)
+  {
+    unsigned p=output[i];
+    exprt tmp(final_predicates[i]);
+    instantiate(tmp, 0, ns);
+    literalt l=make_pos(boolbv, tmp);
+    important_variables.push_back(l.var_no());
+    abstract_transition_relation.output_predicates.push_back(p);
+
+    if(show_cubes)
+      std::cout << " " << p;
+  }
+
+  if(show_cubes)
+    std::cout << std::endl;
+
+  // set important variables
+  satqe_satcheck.set_important_variables(important_variables);
+
+  // solve it
+  switch(boolbv.dec_solve())
+  {
+  case decision_proceduret::D_UNSATISFIABLE:
+    // OK, this is what we expect
+    break;
+
+  default:
+    throw "unexpected result from predabs_sat1.solve()";
+  }
+
+  print(9, "Generated "+
+    i2string(trans_cube_set.no_insertions())+" cube(s)");
+
+  if(show_cubes)
+    std::cout << trans_cube_set;
+
+  abstract_transition_relation.cubes.swap(trans_cube_set);
+}
+
+/*******************************************************************\
+
+Function: abstractort::calc_abstract_initial_states
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: computes set of abstract initial states according to the given set of predicates.
+          Predicates contains only current state predicates.  
+
+\*******************************************************************/
+
+void abstractort::calc_abstract_initial_states(
+  const predicatest &cluster, 
+  const concrete_transt &concrete_trans,
+  const transt &trans, //follow macros is assumed to be done
+  abstract_initial_statest 
+  &abstract_initial_states,
+  const namespacet &ns)
+{
+  //It is assumed that follow macros has already been called for
+  // the concrete transition relation and predicates in the "cluster".
+
+  //Obtain the initial set of predicates
+  std::vector<exprt> initial_predicates;
+  std::vector<unsigned> input;
+
+  for(unsigned i=0; i<cluster.size(); i++) //No test is made to test if the value
+  {                                        //of a predicate does not change.    
+    predicatest::statet state;
+    unsigned nr;
+    cluster.get_info(cluster[i], nr, state);
+
+    switch(state)
+    {
+    case predicatest::INITIAL:
+      {
+        input.push_back(nr);
+        exprt input(cluster[i]); 
+	initial_predicates.push_back(input);
+	
+	break;
+      }
+
+    case predicatest::FINAL:
+      {
+	assert(0);
+	break;
+      }
+
+    case predicatest::NOT_DEFINED:
+      {
+	assert(0);
+	break;
+      }
+    }
+  }
+
+  assert(input.size()!=0);
+    
+  // Now obtain the cubes for the abstract transition relation.
+  // We will create a new SAT solver object.
+  
+  satqe_satcheckt satqe_satcheck;
+  boolbvt boolbv(satqe_satcheck);
+
+  boolbv.set_message_handler(message_handler);
+  satqe_satcheck.set_message_handler(message_handler);
+
+  cube_sett initial;
+  satqe_satcheck.set_cube_set(initial);
+
+
+  exprt instantiated_invar(trans.invar());
+  instantiate(instantiated_invar, 0, ns);
+
+  exprt instantiated_init(trans.init());
+  instantiate(instantiated_init, 0, ns);
+
+  boolbv.set_to_true(instantiated_invar);  
+  boolbv.set_to_true(instantiated_init);
+
+
+  std::vector<unsigned> important_variables;
+  important_variables.reserve(input.size());
+
+  for(unsigned i=0; i<input.size(); i++)
+  {
+    unsigned p=input[i];
+    exprt tmp(initial_predicates[i]);
+    instantiate(tmp, 0, ns);
+    literalt l=make_pos(boolbv, tmp);
+    important_variables.push_back(l.var_no());
+    abstract_initial_states.input_predicates.push_back(p);
+  }
+
+  // set important variables
+  satqe_satcheck.set_important_variables(important_variables);
+
+  // solve it
+  switch(boolbv.dec_solve())
+  {
+  case decision_proceduret::D_UNSATISFIABLE:
+    // OK, this is what we expect
+    break;
+
+  default:
+    throw "unexpected result from predabs_sat1.solve()";
+  }
+
+  // std::cout<<" The abstract transition relation \n";
+  print(9, "Generated "+
+    i2string(initial.no_insertions())+" cube(s)\n");
+
+  if(show_cubes)
+    std::cout << initial;
+
+  //store the cubes
+  abstract_initial_states.cubes.swap(initial);
+}
+
+/*******************************************************************\
+
+Function: abstractort::out_cache_stats
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void abstractort::out_stats(std::ostream &out)
+{
+  status("#Cache sizes: "+i2string(trans_cubes_cache.size())+","+
+	 i2string(refine_cubes_cache.size())+","+
+	 i2string(init_cubes_cache.size()));
+  status("#[hits/access] Trans cache:["+i2string(trans_cache_num_hits)+"/"+
+	 i2string(trans_cache_num_access)+"], "+
+	 "Refine cache:["+i2string(pred_id_cache_num_hits)+"/"+
+	 i2string(pred_id_cache_num_access)+"], "+
+	 "Init cache:["+i2string(init_cache_num_hits)+"/"+
+	 i2string(init_cache_num_access)+"]");
+}
+

src/vcegar/abstractor.h

@@ -0,0 +1,228 @@
+/*******************************************************************\
+
+Module: Abstractor (generates abstract program given a set of predicates)
+
+Author: Himanshu Jain
+
+Date: June 2004 
+
+\*******************************************************************/
+
+#ifndef CPROVER_ABSTRACTOR_H
+#define CPROVER_ABSTRACTOR_H
+
+#include <message.h>
+#include <namespace.h>
+#include <cmdline.h>
+
+#include "concrete_trans.h"
+#include "abstract_trans.h"
+#include "predicates.h"
+#include "partitioning.h"
+#include "network_info.h"
+
+class abstractort:public messaget
+{
+public:
+  abstractort(message_handlert &_message_handler,
+	      const cmdlinet &_cmdline) : 
+    messaget(_message_handler),
+    cmdline(_cmdline)
+  {
+    //some initializations
+    max_trans_cluster_size = 0;
+    max_init_state_cluster_size = 0;
+    num_trans_clusters = 0;
+    num_init_clusters = 0;
+
+    if(!cmdline.isset("partition"))
+      partitioning_strategy = 6; //default
+    else 
+      partitioning_strategy=atoi(cmdline.getval("partition"));
+     
+    #ifdef DEBUG
+    std::cout <<"partitioning_strategy is: "<<partitioning_strategy<<"\n";
+    #endif
+
+    if (!(partitioning_strategy==1 || 
+	  partitioning_strategy==2 || 
+	  partitioning_strategy==3 || 
+	  partitioning_strategy==4 ||
+	  partitioning_strategy==5 ||
+	  partitioning_strategy==6 ||
+	  partitioning_strategy==7 ||
+	  partitioning_strategy==8)) 
+	 throw "--partition option takes only 1, 2, 3, 4, 5, 6, 7, 8 as values ";
+
+    if(!cmdline.isset("showcubes"))
+      show_cubes = 0; //default
+    else 
+      show_cubes = 1;
+
+    if(!cmdline.isset("gcr"))
+      use_refinement_clusters = 0; //default
+    else 
+      use_refinement_clusters = 1;
+
+    refinement_clusters.clear();
+
+    if(!cmdline.isset("relate-init"))
+      relate_init_predicates = 0; //default
+    else 
+      relate_init_predicates = 1;
+
+    //for refinement generated clusters
+    if(!cmdline.isset("nocache"))
+    {
+       pred_id_clusters_caching = 1; //default
+       init_state_caching = 1;
+       trans_rel_caching = 1;
+    }
+    else
+    {
+      pred_id_clusters_caching = 0;
+      init_state_caching = 0;
+      trans_rel_caching = 0;
+    }
+
+    pred_id_cache_num_access = 0;
+    init_cache_num_access = 0;
+    trans_cache_num_access = 0;
+     
+    pred_id_cache_num_hits = 0;
+    init_cache_num_hits = 0;
+    trans_cache_num_hits = 0;
+
+    if(!cmdline.isset("noinit")) //do not compute initial states of abstraction
+      abs_init_states = 1; //default
+    else 
+      abs_init_states = 0;
+
+    if (cmdline.isset("verbose"))
+      verbose=true;
+    else
+      verbose=false;
+   }
+
+  ~abstractort()
+  {
+  }
+
+  const cmdlinet &cmdline;
+  unsigned abstraction_strategy; //to be implemented
+  unsigned partitioning_strategy;
+  unsigned max_trans_cluster_size;
+  unsigned max_init_state_cluster_size;
+  unsigned num_init_clusters;
+  unsigned num_trans_clusters;
+
+  unsigned int pred_id_cache_num_access;
+  unsigned int init_cache_num_access ;
+  unsigned int trans_cache_num_access ;
+  unsigned int init_cache_num_hits;
+  unsigned int trans_cache_num_hits;
+  unsigned int pred_id_cache_num_hits;
+  bool pred_id_clusters_caching;
+  bool init_state_caching;
+  bool trans_rel_caching;
+
+  bool show_cubes;
+  bool use_refinement_clusters;
+  bool relate_init_predicates;
+
+  bool abs_init_states;
+
+  // Generates the abstract program given a concrete program
+  // and a set of predicates. The concrete program will not be touched.
+  // The concrete program is assumed not to change between calls.
+  void calc_abstraction(
+    const predicatest &predicates,
+    const concrete_transt &concrete_trans,
+    const namespacet &ns,
+    const network_infot &network,
+    const partitioningt::pred_id_clusterst &pred_id_clusters);
+
+  void abstract_variables(
+    const predicatest &predicates,
+    abstract_transt::variablest &variables);
+
+  abstract_transt abstract_trans;
+
+  partitioningt::predicate_clusterst pred_clusters, 
+    init_pred_clusters;
+  
+  //These are generated by simulator based upon
+  //the unsatisfiable cores for abstract spurious steps.
+  partitioningt::predicate_clusterst 
+    refinement_clusters;
+
+  void out_stats(std::ostream &out);
+
+protected:
+  typedef std::map<partitioningt::pred_id_set_pairt, abstract_transition_relationt> trans_cubes_cachet;
+  typedef std::map<partitioningt::pred_id_set_pairt, abstract_initial_statest> states_cubes_cachet;
+
+  trans_cubes_cachet refine_cubes_cache;  
+  trans_cubes_cachet trans_cubes_cache;  //cluster transition relation cache 
+  states_cubes_cachet init_cubes_cache;  //initial states cache
+
+  static void rename_to_next(exprt &current_pred);
+
+
+
+  void calc_abstract_trans_rel
+    (const predicatest &cluster, 
+     const concrete_transt &concrete_trans,
+     const transt &trans, //follow macros is assumed to be done
+     abstract_transition_relationt 
+     &abstract_transition_relation,
+     const namespacet &ns);
+
+  void calc_abstract_initial_states
+    (const predicatest &cluster, 
+     const concrete_transt &concrete_trans,
+     const transt &trans, //follow macros is assumed to be done
+     abstract_initial_statest 
+     &abstract_initial_states,
+     const namespacet &ns);
+
+  void calc_abstraction_with_partition(
+    const predicatest &predicates, 
+    const concrete_transt &concrete_trans,
+    const namespacet &ns,
+    const network_infot &network,
+    const partitioningt::pred_id_clusterst &pred_id_clusters);
+
+  void relate_initial_state_predicates(
+    const predicatest &cluster, 
+    const concrete_transt &concrete_trans,
+    abstract_transition_relationt 
+    &abstract_transition_relation,
+    const namespacet &ns);
+
+  void calc_init_states_abstraction(
+    const predicatest &predicates, 
+    const concrete_transt &concrete_trans,
+    const transt &trans,
+    const namespacet &ns,
+    const network_infot &network);
+
+  void calc_trans_rel_abstraction(
+    const predicatest &predicates, 
+    const concrete_transt &concrete_trans,
+    const transt &trans,
+    const namespacet &ns,
+    const network_infot &network);
+
+  void refinement_guided_partitioning_abstraction(
+    const predicatest &predicates, 
+    const concrete_transt &concrete_trans,
+    const transt &trans,
+    const namespacet &ns,
+    const network_infot &network,
+    const partitioningt::pred_id_clusterst &pred_id_clusters);
+
+  bool verbose;
+};
+
+#endif

src/vcegar/bmc.cpp

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Basic BMC
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <i2string.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+
+#include "bmc.h"
+
+/*******************************************************************\
+
+Function: bmct::do_sat
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int bmct::do_sat()
+{
+  satcheckt satcheck;
+  boolbvt boolbv(satcheck);
+  return do_ebmc(boolbv, false);
+}

src/vcegar/bmc.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Basic BMC
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_VCEGAR_BMC_H
+#define CPROVER_VCEGAR_BMC_H
+
+#include <ebmc/ebmc_base.h>
+
+class bmct:public ebmc_baset
+{
+public:
+  bmct(cmdlinet &_cmdline):ebmc_baset(_cmdline)
+  {
+  }
+
+  int do_sat();
+};
+
+#endif

src/vcegar/canonicalize.cpp

@@ -0,0 +1,108 @@
+/*******************************************************************\
+
+Module: Partial Canonicalization of a Predicate
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <simplify_expr.h>
+#include <verilog/expr2verilog.h>
+
+#include "canonicalize.h"
+
+/*******************************************************************\
+
+Function: canonicalize_rec
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void canonicalize_rec(exprt &expr, bool &negation)
+ {
+  if(expr.id()=="not")
+   {
+    if(expr.operands().size()==1)
+     {
+      exprt tmp;
+      tmp.swap(expr.operands()[0]);
+      negation=!negation;
+      canonicalize_rec(tmp, negation);
+      expr.swap(tmp);
+     }
+   }
+  else if(expr.id()=="notequal")
+   {
+    if(expr.operands().size()==2)
+     {
+      negation=!negation;
+      expr.id("=");
+     }
+   } 
+  else if(expr.id()=="<=" || expr.id()=="<" ||
+          expr.id()==">=" || expr.id()==">")
+   {
+    if(expr.operands().size()==2)
+     {
+       
+     }
+   } 
+ }
+
+/*******************************************************************\
+
+Function: canonicalize
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void canonicalize(exprt &expr, bool &negation)
+{
+  // we expect an expression of type Boolean
+  if(expr.type().id()!="bool")
+  {
+    std::cerr << expr << "\n";
+    std::cerr <<"Debug: expr is \n" << expr2verilog(expr) << "\n";
+    std::cerr <<"Debug: type is \n" << expr.type().id_string() << "\n";
+	 
+    throw "canonicalize expects expression of Boolean type";
+  }
+
+  simplify(expr);
+
+  negation=false;
+
+  canonicalize_rec(expr, negation);
+}
+
+/*******************************************************************\
+
+Function: canonicalize
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void canonicalize(exprt &expr)
+{
+  bool negation;
+
+  canonicalize(expr, negation);
+
+  if(negation) expr.make_not();
+}
+

src/vcegar/canonicalize.h

@@ -0,0 +1,17 @@
+/*******************************************************************\
+
+Module: Partial Canonicalization of a Predicate
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_CANONICALIZE_H
+#define CPROVER_CANONICALIZE_H
+
+#include <expr.h>
+
+void canonicalize(exprt &expr, bool &negation);
+void canonicalize(exprt &expr);
+
+#endif

src/vcegar/concrete_counterexample.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: Counterexamples
+
+Author: Daniel Kroening
+        Karen Yorav 
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_CONCRETE_COUNTEREXAMPLE_H
+#define CPROVER_CONCRETE_COUNTEREXAMPLE_H
+
+#include <trans/trans_trace.h>
+
+typedef trans_tracet concrete_counterexamplet;
+                          
+#endif
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

src/vcegar/concrete_trans.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: The concrete transition system
+
+Author: Daniel Kroening
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_CONCRETE_TRANS_H
+#define CPROVER_CONCRETE_TRANS_H
+
+#include <trans/var_map.h>
+
+#include <std_expr.h>
+
+class concrete_transt
+{
+public:
+  transt trans_expr;
+  var_mapt var_map; //Mapping of variables present
+};                  //in verilog file to literals. 
+
+#endif

src/vcegar/discover_predicates.cpp

@@ -0,0 +1,338 @@
+/*******************************************************************\
+
+Module: Predicate Discovery
+
+Author:  Himanshu Jain, hjain@cs.cmu.edu
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include "discover_predicates.h"
+#include "canonicalize.h"
+#include "vcegar_util.h"
+#include <simplify_expr.h>
+
+
+
+
+void discover_simple_preds_simplified(const exprt &expr,
+                             std::set<predicatet> &predicates,
+                             bool canonicalized, bool &isAtomic)
+ {
+   if (expr.type().id() != "bool" && !(expr.has_operands())) {
+     return;
+   }
+
+   if (expr.has_operands()) {
+      std::set<predicatet> new_predicates;
+
+      if (expr.id() == "if")
+	{
+	  discover_simple_preds_simplified(expr.op0(), new_predicates, canonicalized, isAtomic);
+	  assert (!new_predicates.empty());
+	}
+      else
+	{
+	  forall_operands(it, expr)
+	    {
+	      discover_simple_preds_simplified(*it, new_predicates, canonicalized, isAtomic);
+	    }
+	}
+
+      if (new_predicates.size() > 0) {
+	//move the predicates from new_predicates to the predicates
+	for (std::set<exprt>::const_iterator it = new_predicates.begin();
+	     it != new_predicates.end(); it++ ) 
+	  {
+	    exprt pred (*it);
+	    predicates.insert(pred);
+	  }
+	
+	new_predicates.clear();
+	
+	isAtomic = false;
+	
+	return;
+      }
+   }
+   else if(expr.id()=="constant")
+     {
+       return;
+     }
+
+   if (expr.type().id() == "bool") {
+
+    if(!canonicalized)
+      {
+	exprt tmp(expr);
+	bool negation;
+	canonicalize(tmp, negation);
+	discover_simple_preds_simplified(tmp, predicates, true, isAtomic);
+      }
+    else {
+      #if 1
+      exprt tmp_expr(expr);
+      simplify(tmp_expr);
+
+      if (!(tmp_expr.is_true() || tmp_expr.is_false()) && containsSymbol(tmp_expr))
+	{
+	  isAtomic = true;
+	  predicates.insert(tmp_expr);
+	}
+      #else
+      isAtomic = true;
+      predicates.insert(expr);
+      #endif
+    }
+   }
+ }
+
+
+
+
+/*******************************************************************\
+
+Function: collect_case_assignments
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: For an expr of form say (a==1)?b:(a==2)?c+d:c-d, we obtain
+the assignment set as {b, c+d, c-d}.
+
+\*******************************************************************/
+
+void collect_case_assignments(const exprt &expr, std::set<exprt> &assignments, 
+			      unsigned select)
+{
+  if (select == 1) {
+    if (expr.id()=="typecast") {
+      if ((expr.operands()[0]).id() == "if")
+	return collect_case_assignments(expr.operands()[0], assignments, 2);
+      else
+	assert(0);
+    }
+  }
+
+  if (expr.id() == "if") {
+    collect_case_assignments((expr.operands())[1], assignments, 2);
+    collect_case_assignments((expr.operands())[2], assignments, 2);
+    return;
+  }
+
+  exprt new_assign(expr);
+  assignments.insert(expr);
+}
+
+/*******************************************************************\
+
+Function: involves_case
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Predicates of the  {if ()..... } == 2 ; case statement is 
+made up of nested if's.
+
+\*******************************************************************/
+
+bool involves_case(const exprt &expr)
+{
+  if (expr.id() == "if") {
+     return true;
+  }
+  
+  if (expr.id() == "typecast") {
+    if (((expr.operands())[0]).id() == "if")
+      return true;
+  }
+  return false;
+}
+
+
+/*******************************************************************\
+
+Function: gen_lhs_eq_rhs_preds
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: For two sets of the form {x,y, x+y} and {x, f, a+b}
+ generates a set of predicates as {x==x, y==x, x+y==x, ....}
+Cartesian product basically!! 
+\*******************************************************************/
+
+void gen_lhs_eq_rhs_preds(const std::set<exprt> &lhs_assignment, 
+			  const std::set<exprt> &rhs_assignment,  
+			  std::set<predicatet> &predicates)
+{
+  for (std::set<exprt>::const_iterator it1 = lhs_assignment.begin();
+       it1 != lhs_assignment.end(); it1++){
+    for (std::set<exprt>::const_iterator it2 = rhs_assignment.begin();
+       it2 != rhs_assignment.end(); it2++){
+      
+      if (it1->is_constant() && it2->is_constant())
+	break;
+
+       exprt new_variable_expr(*it1);
+       exprt new_definition_expr(*it2);
+       
+       exprt new_predicate("=", typet("bool"));
+       new_predicate.copy_to_operands(new_variable_expr);
+       new_predicate.copy_to_operands(new_definition_expr);
+       predicates.insert(new_predicate);
+       
+    }
+    
+  }
+}
+
+
+/*******************************************************************\
+
+Function: discover_case_assign_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void discover_case_assign_predicates(const exprt &expr,
+				     std::set<predicatet> &predicates,
+				     bool canonicalized)
+{
+   if (expr.type().id() != "bool" && !(expr.has_operands())) {
+     return;
+   }
+
+  if(expr.id()=="and" || expr.id()=="=>" ||
+     expr.id()=="not" || expr.id()=="or" || expr.id()=="if" || 
+     expr.id()=="typecast" || 
+     expr.id()=="extractbit" ||
+     expr.id()=="reduction_or" ||
+     expr.id()=="reduction_and" ||
+     expr.id()=="reduction_nor" ||
+     expr.id()=="reduction_nand" ||
+     expr.id()=="reduction_xor" ||
+     expr.id()=="reduction_xnor" 
+     || expr.id()=="AG"
+     )
+    {
+    forall_operands(it, expr)
+      discover_case_assign_predicates(*it, predicates, canonicalized);
+
+    return;
+   }
+  else if(expr.id()=="=" || expr.id()=="notequal")
+   {
+     if(expr.operands().size()==2)
+       {
+	 bool complex1=false, complex2=false;
+
+	 if(expr.operands()[0].type().id()=="bool" &&
+	    expr.operands()[1].type().id()=="bool")
+	   {
+	     discover_case_assign_predicates(expr.operands()[0], predicates, canonicalized);
+	     discover_case_assign_predicates(expr.operands()[1], predicates, canonicalized);
+	     return;
+	   }
+
+	 if ((expr.operands()[0]).has_operands()){
+	   complex1 = involves_case(expr.operands()[0]);
+	   discover_case_assign_predicates(expr.operands()[0], predicates, canonicalized);
+	 }
+
+	 if ((expr.operands()[1]).has_operands()){
+	   complex2 = involves_case(expr.operands()[1]);
+	   discover_case_assign_predicates(expr.operands()[1], predicates, canonicalized);
+	 }
+
+	 std::set<exprt> lhs_assignments;
+	 std::set<exprt> rhs_assignments;
+	 
+	 if (complex1 || complex2){
+	   if (complex1) 
+	     collect_case_assignments(expr.operands()[0], lhs_assignments, 1);
+	   else
+	     lhs_assignments.insert(expr.operands()[0]);
+	   
+	   if (complex2) 
+	     collect_case_assignments(expr.operands()[1], rhs_assignments, 1);
+	   else
+	     rhs_assignments.insert(expr.operands()[1]);
+
+	   gen_lhs_eq_rhs_preds(lhs_assignments, rhs_assignments, predicates);
+
+	   return;
+	 }
+       }
+   }
+  else if(expr.id()=="constant")
+    {
+    // we don't care about Boolean constants
+      return;
+    }
+
+
+  
+  if (expr.type().id() == "bool") {
+    if(!canonicalized)
+      {
+	exprt tmp(expr);
+	bool negation;
+	canonicalize(tmp, negation);
+	discover_case_assign_predicates(tmp, predicates, true);
+      }
+    else {
+      predicates.insert(expr);
+    }
+  }
+}
+
+
+
+
+
+/*******************************************************************\
+
+Function: discover_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void discover_predicates(const exprt &expr,
+                         std::set<predicatet> &predicates,
+			 int choice, bool &isAtomic)
+ {
+   if (choice == 1) {
+     throw "Support for discover=1 removed \n";
+   }
+   else if (choice == 2) {
+     throw "Support for discover=2 removed \n";
+   }
+   else if (choice == 3) {
+     discover_case_assign_predicates(expr, predicates, false);
+   }
+   else if (choice == 4) {
+     #if 0
+     discover_simple_preds_simplified(expr, predicates, false, isAtomic);
+     #else
+     if (containsSymbol(expr))
+       discover_simple_preds_simplified(expr, predicates, false, isAtomic);
+     else
+       isAtomic = false; //some constant predicate
+     #endif
+   }
+ }

src/vcegar/discover_predicates.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Predicate Discovery
+
+Author: Daniel Kroening, kroening@kroening.com
+                
+\*******************************************************************/
+
+#ifndef CPROVER_DISCOVER_PREDICATES_H
+#define CPROVER_DISCOVER_PREDICATES_H
+
+#include <verilog/expr2verilog.h>
+
+#include "predicates.h"
+
+#include <set>
+
+void discover_predicates(const exprt &expr,
+                         std::set<predicatet> &predicates, 
+			 int choice, bool &isAtomic);
+
+void discover_simple_preds_simplified(const exprt &expr,
+				      std::set<predicatet> &predicates,
+				      bool canonicalized,
+				      bool &isAtomic);
+
+#endif

src/vcegar/instantiate_guards.cpp

@@ -0,0 +1,119 @@
+/*******************************************************************\
+
+Module: Used for instantiating guards in the weakest preconditions from
+the values obtained from abstract counterexample.
+
+Author: Himanshu Jain, hjain@cs.cmu.edu
+
+\*******************************************************************/
+
+#include <i2string.h>
+#include <verilog/expr2verilog.h>
+#include <simplify_expr.h>
+
+#include "instantiate_guards.h"
+#include "canonicalize.h"
+#include "vcegar_util.h"
+
+/*******************************************************************\
+
+Function: instantiate_predicate
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void instantiate_predicate(
+  const predicatest &predicates,
+  const abstract_statet &abstract_state,
+  exprt &expr,
+  std::set<unsigned> &preds_used_to_simplify)
+{
+  bool negation;
+
+  canonicalize(expr, negation);
+
+  // see if we have it
+  unsigned nr;
+  if(predicates.find(expr, nr))
+   {
+     preds_used_to_simplify.insert(nr);
+
+
+
+     if(abstract_state.predicate_values[nr] == 0) {
+      expr.make_false();
+
+     }
+     else {
+      expr.make_true();
+
+     }
+
+     if(negation) {
+      expr.make_not();
+     }
+     else {
+     }
+  }
+}
+
+
+void instantiate_guards_simplify(
+  const predicatest &predicates,
+  const abstract_statet &abstract_state,
+  exprt &expr,
+  std::set<unsigned> &preds_used_to_simplify)
+{
+  if (expr.type().id() != "bool" && !(expr.has_operands())) 
+    return;
+
+  if (expr.has_operands()) {
+    if (expr.id()  == "if")
+      {
+	//instantiate the condition as much as possible
+	//not sure if while loop is needed or not
+
+	instantiate_guards_simplify(predicates, abstract_state, expr.op0(), preds_used_to_simplify);
+	simplify (expr.op0());
+	    
+
+	//pick the appropriate branch depending on the condition
+	if (expr.op0().is_true()) 
+	  {
+	    exprt tmp;
+	    tmp.swap(expr.op1());
+	    expr.swap(tmp);
+	    
+	    instantiate_guards_simplify(predicates, abstract_state, expr, preds_used_to_simplify);
+	  }
+	else if (expr.op0().is_false())
+	  {
+	    exprt tmp;
+	    tmp.swap(expr.op2());
+	    expr.swap(tmp);
+	    instantiate_guards_simplify(predicates, abstract_state, expr, preds_used_to_simplify);
+	  }
+	//else we do nothing as the condition is not atomic so no need to instantiate other stuff
+      }
+    else
+      {
+	Forall_operands(it, expr)
+	  instantiate_guards_simplify(predicates, abstract_state, *it, preds_used_to_simplify);
+      }
+  }
+  
+  simplify(expr);
+ 
+  if (!expr.is_constant())
+    if (expr.type().id() == "bool")
+      instantiate_predicate(predicates, abstract_state, expr, preds_used_to_simplify);
+}
+
+
+
+

src/vcegar/instantiate_guards.h

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Replace guards by truth values
+
+Author: Daniel Kroening, Himanshu Jain
+
+\*******************************************************************/
+
+#ifndef CPROVER_INSTANTIATE_GUARDS_H
+#define CPROVER_INSTANTIATE_GUARDS_H
+
+#include "predicates.h"
+#include "abstract_counterexample.h"
+
+void instantiate_guards_main(
+  const predicatest &predicates,
+  const abstract_statet &abstract_state,
+  exprt &expr,
+  std::set<unsigned> &preds_used_to_simplify);
+
+void instantiate_guards_simplify(
+  const predicatest &predicates,
+  const abstract_statet &abstract_state,
+  exprt &expr,
+  std::set<unsigned> &preds_used_to_simplify);
+
+#endif

src/vcegar/main.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Main Module 
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "parseoptions.h"
+
+/*******************************************************************\
+
+Function: main
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int main(int argc, const char **argv)
+{
+  vcegar_parseoptionst vcegar_parseoptions(argc, argv);
+  return vcegar_parseoptions.main();
+}

src/vcegar/modelchecker.h

@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Model Checker Base Class
+
+Author: Daniel Kroening
+        Karen Yorav 
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_MODELCHECKER_H
+#define CPROVER_MODELCHECKER_H
+
+#include <message.h>
+
+#include "abstract_counterexample.h"
+
+/* A general purpose model checker */
+class modelcheckert:public messaget
+ {
+ public:
+  modelcheckert(message_handlert &_message_handler):
+    messaget(_message_handler)
+    {
+    }
+
+  // A return value of TRUE means the program is correct,
+  // if FALSE is returned, counterexample will contain the counterexample
+   virtual bool check
+     (const abstract_transt &abstract_trans, 
+      const abstract_transition_constrainst &abstract_transition_constrains,
+      const weakest_precondition_constrainst &weakest_precondition_constrains,
+      const abstract_initial_constrainst &abstract_initial_constrains,
+      abstract_counterexamplet &abstract_counterexample)=0;
+ };
+
+#endif
+
+
+

src/vcegar/modelchecker_smv.h

@@ -0,0 +1,185 @@
+/*******************************************************************\
+
+Module: SMV Model Checker Interface
+
+Author: Daniel Kroening
+        Himanshu Jain
+  
+  Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_MODELCHECKER_SMV_H
+#define CPROVER_MODELCHECKER_SMV_H
+
+#include <iostream>
+
+#include "modelchecker.h"
+
+class modelchecker_smvt:public modelcheckert
+ {
+ public:
+  typedef enum { CMU_SMV, NUSMV, CADENCE_SMV } enginet;
+ 
+  modelchecker_smvt(message_handlert &_message_handler,
+		    enginet _engine, bool v, bool claims_option, bool _absref3):
+    modelcheckert(_message_handler),
+    engine(_engine),
+    verbose(v),
+    claim(claims_option),
+    absref3(_absref3)
+    {
+      switch(engine)
+	{
+	case CMU_SMV:     status("Using the modelchecker: CMU_SMV"); 
+	  break;
+	case NUSMV:       status("Using the modelchecker: NUSMV"); 
+	  break;
+	case CADENCE_SMV: status("Using the modelchecker: CADENCE_SMV");
+	  break;
+	default:
+	  throw "Unknown modelchecker  \n";
+	}
+      
+      if (absref3)
+	status("Absref3 set to true for Cadence SMV");
+    }
+
+  // A return value of TRUE means the program is correct,
+  // if FALSE is returned, counterexample will contain the counterexample
+  virtual bool check
+   (const abstract_transt &abstract_trans,
+    const abstract_transition_constrainst &abstract_transition_constrains,
+    const weakest_precondition_constrainst &weakest_precondition_constrains,
+    const abstract_initial_constrainst &abstract_initial_constrains,
+    abstract_counterexamplet &abstract_counterexample);
+
+ private:
+  enginet engine;
+
+  std::vector<std::string> variable_names;
+
+  bool verbose; 
+  bool claim;
+  bool absref3;
+
+  void print_constrain
+    (const abstract_constraintt &start,
+     const abstract_constraintt &final,
+     std::ostream &out) ; 
+
+  void add_weakest_precondition_constrain
+    (const abstract_constraintt &start1,
+     const abstract_constraintt &final1,
+     const abstract_constraintt &start2,
+     const abstract_constraintt &final2,
+     std::ostream &out);
+ 
+ 
+  void build_smv_file
+   (const abstract_transt &abstract_trans,
+    const abstract_transition_constrainst &abstract_transition_constrains,
+    const weakest_precondition_constrainst &weakest_precondition_constrains,
+    const abstract_initial_constrainst &abstract_initial_constrains,
+    std::ostream &out);
+
+
+  void build_smv_file
+    (const abstract_transt &abstract_trans,  
+     const abstract_transition_constrainst &abstract_transition_constrains,
+     const weakest_precondition_constrainst &weakest_precondition_constrains,
+     const abstract_initial_constrainst &abstract_initial_constrains,
+     bool threaded,
+     std::ostream &out);
+    
+  void build_smv_file_global_variables
+   (const abstract_transt &abstract_trans,
+    std::ostream &out);
+
+  void build_smv_file_trans_cluster
+    (const abstract_transt &abstract_trans,
+     const abstract_transition_relationt &cluster_trans,
+     unsigned clsuter_no,
+     bool threaded,
+     std::ostream &out);
+
+  void build_smv_file_spec
+   (const abstract_transt &abstract_trans,
+    bool threaded,
+    std::ostream &out);
+    
+  void build_smv_file_init_cluster
+    (const abstract_transt &abstract_trans,
+     const abstract_initial_statest &initial_states,
+     unsigned cluster_no,
+     std::ostream &out);
+
+  void remove_spurious_transition
+    (const abstract_constraintt &start,
+     const abstract_constraintt &final,
+     std::ostream &out);
+    
+  bool read_result
+   (std::istream &out1,
+    std::istream &out2,
+    std::istream &out_ce, //result from cadence smv
+    const abstract_transt &abstract_trans,
+    abstract_counterexamplet &counterexample);
+
+  void read_counterexample
+   (const std::list<std::string> &file,
+    std::list<std::string>::const_iterator it,
+    const abstract_transt &abstract_trans,
+    abstract_counterexamplet &counterexample);
+
+  class smv_ce_thread_infot
+  {
+  public:
+    std::vector<bool> guards;
+    unsigned PC;
+    bool runs;
+  };
+
+  typedef std::vector<smv_ce_thread_infot> thread_infost;
+    
+  void read_counterexample_store
+   (abstract_counterexamplet &counterexample,
+    thread_infost &thread_infos,
+    abstract_statet abstract_state);
+    
+   void instantiate_expression(exprt &expr); 
+    
+   
+  
+  bool is_variable_name(const std::string &variable_name);
+  void get_variable_names(const abstract_transt &abstract_trans);
+  
+  typedef std::map<exprt, std::string> nondet_symbolst;
+  nondet_symbolst nondet_symbols;
+
+
+  void read_counterexample_loop_cadence_smv
+    (const std::list<std::string> &file,
+     std::list<std::string>::const_iterator it,
+     const abstract_transt &abstract_trans,
+     abstract_counterexamplet &counterexample);
+  
+  
+  void read_counterexample_cadence_smv
+    (const std::list<std::string> &file,
+     std::list<std::string>::const_iterator it,
+     const abstract_transt &abstract_trans,
+     abstract_counterexamplet &counterexample);
+  
+  bool read_result_cadence_smv
+    (std::istream &out_ce,
+     const abstract_transt &abstract_trans,
+     abstract_counterexamplet &counterexample);
+
+  void remove_spurious_initial_state
+    (const abstract_constraintt &start,
+     std::ostream &out);
+  
+ }; 
+
+#endif

src/vcegar/network_info.cpp

@@ -0,0 +1,821 @@
+/*******************************************************************\
+
+Module: Creates network for a given circuit. 
+
+Author: Himanshu Jain
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <cout_message.h>
+#include <verilog/expr2verilog.h>
+#include <simplify_expr.h>
+
+#include "network_info.h"
+#include "instantiate_guards.h"
+
+//#define DEBUG
+
+
+/*******************************************************************\
+
+Function: create
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Fills the next state function cache and collect symbols
+          which belong to a same network
+
+\*******************************************************************/
+
+void network_infot::create(
+  const exprt &constraints,
+  const exprt &trans,
+  const var_mapt &var_map)
+{
+   exprt copy_constraints(constraints);
+   namespacet ns(context);
+   ns.follow_macros(copy_constraints);
+
+   create_network(copy_constraints, 
+		  vector_symbolsets, 
+		  vector_exprsets, 
+		  var_map);
+   #ifdef DEBUG
+   print_network(vector_symbolsets, 
+		  vector_exprsets, 
+		  var_map);
+
+   std::cout <<"Now building the next state function cache \n";
+   
+   #endif
+
+   exprt copy_trans(trans);
+   ns.follow_macros(copy_trans);
+ 
+
+
+   std::cout << "Build next state functions cache\n";
+   build_next_state_function_cache(copy_trans,
+				   vector_symbolsets, 
+				   vector_exprsets,
+				   var_map,
+				   next_state_function_cache);
+
+}
+
+/*******************************************************************\
+
+Function: lookup
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Looks for an element in a vector of sets
+
+\*******************************************************************/
+
+bool network_infot::lookup(
+  const std::vector<std::set<std::string> > &vector_symbolsets,
+  const std::string &name,
+  unsigned& nr) const
+{
+  for (unsigned i=0; i<vector_symbolsets.size(); i++) {
+    std::set<std::string>::const_iterator it = 
+      vector_symbolsets[i].find(name);
+    
+    if (it != vector_symbolsets[i].end()) {
+      nr =i;
+      return true;
+    }
+  }
+  
+  return false;
+}
+
+
+//This needs to be replaced by a union find data structure!!
+
+/*******************************************************************\
+
+Function: create_network
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Creates sets of symbols which are equal to each other.
+
+\*******************************************************************/
+
+void network_infot::create_network (
+  const exprt& general_constrains,
+  std::vector<std::set<std::string> > &vector_symbolsets,
+  std::vector<std::set<exprt> > &vector_exprsets,
+  const var_mapt &var_map)
+{
+  if (!general_constrains.has_operands()) return;
+  
+  if(general_constrains.id()=="=")
+    {
+      
+      if (!( (general_constrains.operands()[0]).id()=="symbol" ||
+	     (general_constrains.operands()[1]).id()=="symbol"))
+	return;
+
+      
+
+      unsigned pos0;
+      unsigned pos1;
+
+      std::string id0 = "", id1 = "";
+
+      bool is_symbol0=false, is_symbol1=false;
+      int var_type0=-1, var_type1=-1;
+      
+      if ((general_constrains.operands()[0]).id()=="symbol") {
+
+
+	id0= (general_constrains.operands()[0]).get("identifier").as_string();
+
+	var_type0 = get_type_integer(var_map, id0);
+	is_symbol0 = true;
+      }
+	
+      if ((general_constrains.operands()[1]).id()=="symbol") {
+	id1= (general_constrains.operands()[1]).get("identifier").as_string();
+
+	var_type1 = get_type_integer(var_map, id1);
+	is_symbol1 = true;
+      }
+
+      assert(is_symbol0 || is_symbol1);
+      assert(!(var_type0 ==4 || var_type1==4));
+
+      if (!lookup(vector_symbolsets, id0, pos0)) {
+	if (!lookup(vector_symbolsets, id1, pos1)) {
+	  std::set<std::string> new_set;
+
+	  if (is_symbol0)
+	    new_set.insert(id0);
+
+	  if (is_symbol1)
+	    new_set.insert(id1);
+	  
+	  vector_symbolsets.push_back(new_set);
+	  
+	  std::set<exprt> new_expr_set;
+	  exprt copy0(general_constrains.operands()[0]);
+	  exprt copy1(general_constrains.operands()[1]);
+
+	  if (var_type0 == 1 || !is_symbol0) //latch or macro definition
+	    new_expr_set.insert(copy0);
+	  
+	  if (var_type1 == 1 || !is_symbol1) //latch or macro definition
+	    new_expr_set.insert(copy1);
+
+	  vector_exprsets.push_back(new_expr_set);
+
+	}
+	else {
+	  if (is_symbol0)
+	    vector_symbolsets[pos1].insert(id0);
+
+	  exprt copy(general_constrains.operands()[0]);
+	  if (var_type0 == 1 || !is_symbol0)
+	    vector_exprsets[pos1].insert(copy);
+	}
+      }
+      else {
+
+	if (!lookup(vector_symbolsets, id1, pos1))
+	  {
+	    if (is_symbol1)
+	      vector_symbolsets[pos0].insert(id1);
+	    
+	    exprt copy(general_constrains.operands()[1]);
+	    
+	    if (var_type1 == 1 || !is_symbol1)
+	      vector_exprsets[pos0].insert(copy);
+	  }
+	else
+	  {
+	    if (pos1 < pos0)
+	      {
+		unsigned tmp = pos1;
+		pos1 = pos0;
+		pos0 = tmp;
+	      }
+
+	    vector_symbolsets[pos0].insert(vector_symbolsets[pos1].begin(),
+					   vector_symbolsets[pos1].end());
+	    vector_symbolsets[pos1].clear();
+
+	    vector_exprsets[pos0].insert(vector_exprsets[pos1].begin(),
+					 vector_exprsets[pos1].end());
+	    vector_exprsets[pos1].clear();
+	  }
+      }
+      return;
+    }
+  
+  if(general_constrains.has_operands())
+    forall_operands(it, general_constrains)
+      create_network(*it, vector_symbolsets, vector_exprsets, var_map);
+  
+}
+
+
+/*******************************************************************\
+
+Function: print_network
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints the set of symbols in the network
+
+\*******************************************************************/
+
+void network_infot::print_network (const std::vector<std::set<std::string> > &vector_symbolsets,
+				   const std::vector<std::set<exprt> > &vector_exprsets,
+				   const var_mapt &var_map) 
+{
+  for (unsigned i=0;i<vector_symbolsets.size();i++) {
+    std::cout <<"Symbol set ["<< i<<"]\n";
+    print_symbolset(vector_symbolsets[i], var_map);
+    print_exprset(vector_exprsets[i]);
+    std::cout <<"\n";
+  }
+}
+
+
+/*******************************************************************\
+
+Function: print_symbolset
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints the set of symbols in the network
+
+\*******************************************************************/
+
+void network_infot::print_symbolset (const std::set<std::string>  &symbolset,
+		      const var_mapt &var_map) {
+  for (std::set<std::string>::const_iterator it = symbolset.begin();
+       it != symbolset.end(); it++) {
+    var_mapt::vart::vartypet var_type = var_map.get_type(*it);
+
+    std::cout <<*it <<"  ";
+    
+    switch(var_type) 
+      {
+      case var_mapt::vart::VAR_LATCH:
+	std::cout <<"LATCH";
+	break;
+      case var_mapt::vart::VAR_INPUT: 
+	std::cout <<"INPUT";
+	break;
+      case var_mapt::vart::VAR_WIRE : 
+	std::cout <<"WIRE";
+	break;
+	
+      default: 
+	std::cout <<"NOT FOUND ";
+	break;
+      }
+    std::cout <<"\n"; 
+  }
+}
+
+
+
+/*******************************************************************\
+
+Function: print_exprset
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints the set of symbols in the network
+
+\*******************************************************************/
+
+void network_infot::print_exprset (const std::set<exprt>  &exprset) {
+
+  if (exprset.size() == 0) {
+    std::cout <<"Exprset is empty \n";
+    return;
+  }
+
+  unsigned count = 0;
+
+  for (std::set<exprt>::const_iterator it = exprset.begin();
+       it != exprset.end(); it++) {
+    std::string code="";
+    //expr2verilog(*it,code);
+    code = expr2verilog(*it);
+
+    std::cout <<" ["<<count<<"] "<<code <<"\n";
+    count ++;
+  }
+  
+
+  if (exprset.size() > 1) 
+    std::cout << "WARNING: Network has multiple definitions: \n";
+
+}
+
+
+
+/*******************************************************************\
+
+Function: replace_outputs
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Replaces (not external) inputs and wires with their definitions 
+ in terms of latches and other expressions if any.
+\*******************************************************************/
+
+void network_infot::replace_outputs 
+(exprt& property,
+ const std::vector<std::set<std::string> > &vector_symbolsets,
+ const std::vector<std::set<exprt> > &vector_exprsets,
+ const var_mapt &var_map) const
+{
+  #ifdef DEBUG
+  std::cout <<"property is "<<property<<"\n";
+  #endif
+
+  if(property.has_operands())
+    Forall_operands(it, property)
+      replace_outputs(*it, vector_symbolsets, vector_exprsets, var_map);
+  
+
+  if(property.id()=="symbol")
+    {
+
+      std::string module_variable = property.get("identifier").as_string();
+
+
+      var_mapt::vart::vartypet var_type = var_map.get_type(module_variable);
+
+      #ifdef DEBUG
+      std::cout <<"module variable is "<<module_variable<<"\n";
+      #endif
+
+      switch(var_type) 
+	{
+	case var_mapt::vart::VAR_LATCH: 
+	  { //Its a latch do nothing.
+	    break;
+	  }
+	case var_mapt::vart::VAR_INPUT: //Input
+	  {
+	    unsigned pos0;
+	    exprt def;
+	    
+	    if (lookup(vector_symbolsets, module_variable, pos0)) {
+	      if (!vector_exprsets[pos0].empty()) {
+		property = *(vector_exprsets[pos0].begin());
+		replace_outputs(property, vector_symbolsets, vector_exprsets,  var_map);
+	      }
+	    }
+	    break;
+	  }
+	case var_mapt::vart::VAR_WIRE : //wire
+	  {
+	    unsigned pos0;
+	    exprt def;
+
+	    if (lookup(vector_symbolsets, module_variable, pos0)) {
+	      if (!vector_exprsets[pos0].empty()) {
+		property = *(vector_exprsets[pos0].begin());
+		replace_outputs(property, vector_symbolsets, vector_exprsets,  var_map);
+	      }
+	    }
+	    break;
+	  }
+
+	default: 
+	  {
+	     std::cout <<"Warning !!" <<module_variable <<" is not defined in the internal variable map \n";
+	     assert(0);
+	     break;
+	  }
+	}
+    }
+}	  
+
+/*******************************************************************\
+
+Function: build_next_state_function_cache
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Creates the next state function cache and also performs 
+          replace outputs on the stored function. 
+\*******************************************************************/
+
+void network_infot::build_next_state_function_cache
+(const exprt &trans_rel, 
+ const std::vector<std::set<std::string> > &vector_symbolsets,
+ const std::vector<std::set<exprt> > &vector_exprsets,
+ const var_mapt &var_map,
+ next_state_function_cachet &next_state_function_cache)
+{
+  
+  if (!trans_rel.has_operands()) return;
+
+  if(trans_rel.id()=="=")
+    {
+
+      exprt t1= (trans_rel.operands())[0];
+      exprt t2= (trans_rel.operands())[1];
+      
+      if (t1.id()== "next_symbol") {
+
+	#ifdef DEBUG
+	std::cout <<"Found "<< t1.get("identifier")<<"\n";
+	#endif
+
+	exprt def(t2); 
+	replace_outputs(def, 
+			vector_symbolsets, 
+			vector_exprsets,
+			var_map);
+	
+
+	next_state_function_cache.insert(std::pair<std::string, exprt>
+					 (t1.get("identifier").as_string(), def));
+	
+	  return;
+      }   
+    }
+  
+  if(trans_rel.has_operands())
+    forall_operands(it, trans_rel) {
+      build_next_state_function_cache(*it, 
+				      vector_symbolsets,
+				      vector_exprsets,
+				      var_map,
+				      next_state_function_cache);
+  
+  }
+}
+
+/*******************************************************************\
+
+Function: Print the cache of the next state functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void network_infot::print_next_state_function_cache
+(const next_state_function_cachet &next_state_function_cache)
+{
+  unsigned count =0;
+  for ( next_state_function_cachet::const_iterator it= next_state_function_cache.begin();
+	it != next_state_function_cache.end();
+	it++)
+    {
+      std::cout <<"[" << count <<" "<<it->first<<"]--\n";
+      std::cout<<expr2verilog(it->second)<<"\n\n";
+      count++;
+    }
+}
+
+
+
+/*******************************************************************\
+
+Function: print_members() ;
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Public method
+
+\*******************************************************************/
+
+void network_infot::print_members() {
+   print_network (vector_symbolsets, vector_exprsets, var_map);
+}
+
+/*******************************************************************\
+
+Function: print_next_state_function_cache
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Public method
+
+\*******************************************************************/
+
+void network_infot::print_next_state_function_cache() {
+  print_next_state_function_cache (next_state_function_cache);
+}
+
+
+/*******************************************************************\
+
+Function: weakest_precondition_recur
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Computes the weakest precondition of a given property. Takes case splits
+          into account.
+
+\*******************************************************************/
+
+
+void network_infot::weakest_precondition_recur (exprt& property) const
+{
+  if (property.id() == "with") {
+    std::cout <<"Giving up accuracy here ! \n";
+    return;
+  }
+  
+  if(property.has_operands())
+    Forall_operands(it, property)
+      weakest_precondition_recur(*it);
+  
+  if(property.id()=="next_symbol")
+    {
+
+      const std::string &next_state_variable = property.get("identifier").as_string();
+
+
+      next_state_function_cachet::const_iterator pair = 
+	next_state_function_cache.find(next_state_variable);
+      
+      
+      if (pair != next_state_function_cache.end()) {
+	property = pair->second;
+      }
+      else {
+	property.id("symbol"); 
+      }
+    }
+}
+
+/*******************************************************************\
+
+Function: weakest_precondition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Computes the weakest precondition of a given property. Takes case splits
+          into account.
+
+\*******************************************************************/
+
+
+void network_infot::weakest_precondition (exprt& property) const
+{
+  rename (property);
+  weakest_precondition_recur (property);
+}
+ 
+/*******************************************************************\
+
+Function: Wrapper for the internal replace_outputs routine.
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+
+void network_infot::replace_outputs (exprt& property) const
+{
+  replace_outputs(property, vector_symbolsets, vector_exprsets, var_map);
+}
+
+
+
+/*******************************************************************\
+
+Function: weakest_precondition_recur
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Computes the weakest precondition of a given property. Takes case splits
+          into account. Use the next state function cache supplied by the user.
+
+\*******************************************************************/
+
+
+void network_infot::weakest_precondition_recur (exprt& property, const next_state_function_cachet &ns_cache) const
+{
+  if (property.id() == "with") {
+    std::cout <<"Giving up accuracy here ! \n";
+    return;
+  }
+
+  if(property.has_operands())
+    Forall_operands(it, property)
+      weakest_precondition_recur(*it, ns_cache);
+   
+  if(property.id()=="next_symbol")
+    {
+
+      const std::string &next_state_variable = property.get("identifier").as_string();
+
+      next_state_function_cachet::const_iterator pair = 
+	ns_cache.find(next_state_variable);
+
+
+      if (pair != ns_cache.end()) {
+	property = pair->second;
+      }
+      else {
+	#ifdef DEBUG
+	const std::string &next_state_variable = property.get("identifier");
+	
+	std::cout <<"Identifier "<<next_state_variable<<" has no next state function\n";
+	#endif
+	property.id("symbol");
+      }
+    }
+}
+
+/*******************************************************************\
+
+Function: simplified_weakest_precondition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Before substituting the next state functions. First try to
+simplify them.
+
+\*******************************************************************/
+
+void network_infot::simplified_weakest_precondition(
+  exprt  &property, 
+  const abstract_statet &abstract_state, 
+  const predicatest &predicates,
+  std::set<unsigned> &preds_used_to_simplify,
+  bool &containsInput) const
+{
+
+  next_state_function_cachet simplified_ns_funcs;
+
+  rename (property);
+
+
+  weakest_precondition_recur_demand(
+    abstract_state, predicates,
+    property, simplified_ns_funcs, 
+    preds_used_to_simplify,
+    containsInput); 
+
+
+  simplify(property);
+
+
+  instantiate_guards_simplify(predicates, abstract_state, 
+			      property, preds_used_to_simplify);
+
+
+  #ifdef DEBUG
+  std::cout <<"The size of simplified cache is "<<simplified_ns_funcs.size()<<"\n";
+  #endif
+
+  simplified_ns_funcs.clear(); 
+}
+
+
+/*******************************************************************\
+
+Function: weakest_precondition_recur_demand
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Before substituting the next state functions. First try to
+simplify them. But only simplify on demand.
+
+Also collect the predicates which are useful for simplication. 
+(useful for syntactic abstraction)
+
+Date : Dec 24, 2004
+\*******************************************************************/
+
+
+void network_infot::weakest_precondition_recur_demand (const abstract_statet &abstract_state, 
+						       const predicatest &predicates,
+						       exprt& property, 
+						       next_state_function_cachet &ns_cache,
+						       std::set<unsigned> &preds_used_to_simplify,
+						       bool &containsInput) const 
+{
+
+  if(property.has_operands())
+    Forall_operands(it, property)
+      weakest_precondition_recur_demand(abstract_state, predicates, *it, 
+					ns_cache, 
+					preds_used_to_simplify,
+					containsInput);
+   
+  if(property.id()=="next_symbol")
+    {
+      const std::string &next_state_variable = property.get("identifier").as_string();
+
+      next_state_function_cachet::const_iterator pair = 
+	ns_cache.find(next_state_variable);
+      
+      
+      if (pair != ns_cache.end()) {
+	property = pair->second;
+      }
+      else {
+	// Let us try to get the next state function, simplify it, and cache it.
+
+	next_state_function_cachet::const_iterator it= 
+	  next_state_function_cache.find(next_state_variable);
+
+	if (it != next_state_function_cache.end()) {
+
+	  exprt simplify_ns (it->second);
+
+	  #ifdef DEBUG  
+	  std::cout << "Before simplification \n";
+	  std::cout <<"[" <<it->first<<"]--\n";
+	  std::cout <<simplify_ns << "\n";
+	  #endif
+
+
+
+	  instantiate_guards_simplify (predicates, abstract_state, 
+				       simplify_ns, preds_used_to_simplify);
+
+
+
+	  #ifdef DEBUG  
+	  std::cout << "After simplification \n";
+	  std::cout <<"[" <<it->first<<"]--\n";
+	  //  std::cout<<simplify_ns<<"\n\n";
+	  std::cout<<expr2verilog(simplify_ns)<<"\n\n";
+	  #endif
+
+	  //update the property
+	  property = simplify_ns;
+	  
+
+	  //Insert simplified next state function in the cache.
+	  ns_cache.insert(std::pair<std::string, exprt>
+			  (it->first, simplify_ns));
+	  
+      
+
+	}
+	else {
+	
+	  property.id("symbol");
+	  
+	  containsInput = true;
+	  
+          #ifdef DEBUG
+	  const dstring &next_state_variable = property.get("identifier");
+	  std::cout <<"Identifier "<<next_state_variable<<" has no next state function\n";
+          #endif
+	}
+      }
+    }
+}
+
+

src/vcegar/network_info.h

@@ -0,0 +1,133 @@
+/*******************************************************************\
+
+Module: Performs pre-processing on the given verilog program and
+        collects information which will be used later. Builds the
+        network for a given circuit.
+
+Author: Himanshu Jain
+
+Date: July 2004
+
+\*******************************************************************/
+
+#ifndef CPROVER_NETWORK_INFO_H
+#define CPROVER_NETWORK_INFO_H
+
+#include <message.h>
+#include <context.h>
+#include <namespace.h>
+
+#include <trans/var_map.h>
+#include <verilog/expr2verilog.h>
+
+#include "concrete_trans.h"
+#include "abstract_trans.h"
+#include "predicates.h"
+#include "vcegar_util.h"
+#include "abstract_counterexample.h"
+
+class network_infot
+{
+  std::vector<std::set<std::string> > vector_symbolsets;
+  std::vector<std::set<exprt> > vector_exprsets;
+  next_state_function_cachet next_state_function_cache;
+ 
+  const var_mapt &var_map;
+  const contextt &context;
+
+  void create_network (const exprt& general_constrains,
+		       std::vector<std::set<std::string> > &vector_symbolsets,
+		       std::vector<std::set<exprt> > &vector_exprsets,
+		       const var_mapt &var_map);
+
+
+  void print_network (const std::vector<std::set<std::string> > &vector_symbolsets,
+		      const std::vector<std::set<exprt> > &vector_exprsets,
+		      const var_mapt &var_map);
+  
+  void print_symbolset (const std::set<std::string>  &symbolset,
+			const var_mapt &var_map);
+  
+  void print_exprset (const std::set<exprt>  &exprset);
+  
+  void replace_outputs 
+    (exprt& property,
+     const std::vector<std::set<std::string> > &vector_symbolsets,
+     const std::vector<std::set<exprt> > &vector_exprsets,
+     const var_mapt &var_map) const;
+
+  void build_next_state_function_cache
+    (const exprt &trans_rel, 
+     const std::vector<std::set<std::string> > &vector_symbolsets,
+     const std::vector<std::set<exprt> > &vector_exprsets,
+     const var_mapt &var_map,
+     next_state_function_cachet &next_state_function_cache);
+
+  void print_next_state_function_cache
+    (const next_state_function_cachet &next_state_function_cache);
+
+  void create (const exprt& constraints, 
+	       const exprt& trans, 
+	       const var_mapt& var_map);
+  
+  bool lookup (const std::vector<std::set<std::string> > &vector_symbolsets,
+	       const std::string &name, unsigned& nr) const;
+  
+  void weakest_precondition_recur (exprt& property) const;
+
+  void weakest_precondition_recur (exprt& property, const next_state_function_cachet &ns_cache) const;
+
+  void weakest_precondition_recur_demand (const abstract_statet &abstract_state, 
+					  const predicatest &predicates,
+					  exprt& property, 
+					  next_state_function_cachet &ns_cache,
+					  std::set<unsigned> &preds_used_to_simplify,
+					  bool &containsInput) const ;
+
+ 
+
+ public:
+  
+  network_infot(const exprt& constraints, 
+		const exprt& trans, 
+		const var_mapt& _var_map,
+		const contextt& _context):
+    var_map(_var_map),
+    context (_context)
+    { 
+      create (constraints, trans, var_map);
+    }
+  
+  ~network_infot() { }
+
+  void print_members() ;
+
+  void print_next_state_function_cache() ;
+ 
+  void weakest_precondition (exprt& property) const ;
+  
+  void replace_outputs (exprt &property) const;
+
+  void simplified_weakest_precondition (exprt  &property, 
+					const abstract_statet &abstract_state, 
+					const predicatest &predicates, 
+					std::set<unsigned> &preds_used_to_simplify,
+					bool &containsInput) const ;
+
+  void build_next_state_function_cache
+    (const exprt &trans_rel, 
+     const std::vector<std::set<std::string> > &vector_symbolsets,
+     const std::vector<std::set<exprt> > &vector_exprsets,
+     const var_mapt &var_map,
+     std::vector<std::set<exprt> > &outputs_replaced_definitions,
+     next_state_function_cachet &next_state_function_cache);
+
+  void replace_outputs 
+    (const std::vector<std::set<std::string> > &vector_symbolsets,
+     const std::vector<std::set<exprt> > &vector_exprsets,
+     const var_mapt &var_map,
+     std::vector<std::set<exprt> > &outputs_replaced_definitions, //kind of cache
+     exprt& property) const;
+};
+
+#endif

src/vcegar/parseoptions.cpp

@@ -0,0 +1,127 @@
+/*******************************************************************\
+
+Module: Main Module 
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "bmc.h"
+#include "parseoptions.h"
+#include "vcegar.h"
+
+/*******************************************************************\
+
+Function: vcegar_parseoptionst::doit
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: invoke main modules
+
+\*******************************************************************/
+
+int vcegar_parseoptionst::doit()
+{
+  if(cmdline.isset("bmc") ||
+     cmdline.isset("show-claims") ||
+     cmdline.isset("show-modules"))
+  {
+    bmct bmc(cmdline);
+  
+    int result=bmc.get_model();
+    if(result!=-1) return result;
+
+    return bmc.do_sat();
+  }
+  
+  // do CEGAR
+  return do_vcegar(cmdline);
+}
+
+/*******************************************************************\
+
+Function: vcegar_parseoptionst::help
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: display command line help
+
+\*******************************************************************/
+
+void vcegar_parseoptionst::help()
+{
+  std::cout <<
+    "\n"
+    "* *             VCEGAR Copyright 1.3 (C) 2003-2007          * *\n"
+    "* * Carnegie Mellon University, Computer Science Department * *\n"
+    "* *         ETH Zuerich, Computer Systems Institute         * *\n"
+    "* *                   hjain@cs.cmu.edu                      * *\n"
+    "* *                 kroening@kroening.com                   * *\n"
+    "\n"
+    "Usage:                          Purpose:\n"
+    "\n"
+    " vcegar [-?] [-h] [--help]      show help\n"
+    " vcegar file ...                source file name\n"
+    "\n"
+    "General options:\n"
+    " vcegar --p <propfile>          specify property in a file\n"
+    " vcegar --module <module>       set module (default: main)\n"
+    " vcegar --claim <nr>            Specify property number from the model file (similar to Cadence SMV)\n"
+    " vcegar --partition <nr>        Strategy for partitioning the predicates \n" 
+    "    nr = 2                      All related (by weakest preconditions) next state and current\n"
+    "                                state predicates together. (Not very scalable) \n"
+    "    nr = 6                      Only next state predicates with exactly same symbols kept together (default)\n"
+    "    nr = 8                      Initial abstraction is simply true (completely lazy)\n"
+    "\n"
+    "Less frequently used options:\n"
+    " vcegar --i <nr>                Limit the number of iterations in the CEGAR loop to <nr>\n"
+    " vcegar --pred <file>           Use predicates from the given file  \n"
+    " vcegar --mapping               Write predicate to boolean variable mapping in vcegar.map\n"
+    " vcegar --modelchecker <num>    Which modelchecker to use for checking abstractions\n"
+    "   num=nusmv                    Use NuSMV binary named NuSMV  \n"
+    "   num=cadencesmv               Use Cadence SMV binary named smv (default)\n"
+    " vcegar --absref3               Give this option to Cadence SMV              \n"
+    " vcegar --gcr                   Generates clusters from refinement of spurious transitions. \n"  
+    " vcegar --gcrsize <nr>          Maximum cluster size when generating clusters from refinement  \n"
+    " vcegar --noinit                Do not compute initial set of abstract states\n"
+ 
+   "\n"
+    "Even less frequently used (use at your own risk):\n"
+    "---------------------\n"
+
+    " vcegar --discover <nr>         How to extract predicates from weakest preconditions etc. \n" 
+    "    nr = 1                      takes guards and boolean expressions involving case as predicates\n"  
+    "    nr = 2                      only simple expressions allowed in predicates (default)\n"  
+    " vcegar --noconstrain           Refine using new predicates only. \n"  
+    "                                Don't constrain using abstract spurious transitions.\n"
+    " vcegar --init-pred <nr>        Choice of initial set of predicates \n"
+    "    nr = 1                      property itself is taken as initial predicate \n"
+    "    nr = 2                      initial predicates are extracted from property (default)\n"   
+    " vcegar --showcubes             Shows the cubes generated for each cluster\n"  
+    " vcegar --one_cex_only          Remove only one spurious abstract transition\n"  
+    "                                And not as much as possible using unsat cores\n"
+
+    " vcegar --more-stats            Prints runtime statistics after each iteration\n"
+    " vcegar --relate-init           Find constrains between current state predicates having same symbols\n"
+    " vcegar --discover <nr>         Predicate discovery technique (default=2)\n"
+    " vcegar --nowpcons              Do not add weakest pre-condition constraints\n"
+    " vcegar --nocache               Do not cache already computed abstractions\n"
+    " vcegar --no-simplify           disable simplificaton\n"
+    "\n"
+    "Bounded Model checking:\n"
+    "----------------------\n"
+    " vcegar --bmc                   For bounded model checking (default: predicate abstraction)\n"
+    " vcegar --bound <nr>            Set bound for BMC\n"
+    " vcegar --dimacs                Output CNF in Dimacs CNF format\n"
+    "\n"
+    "Debugging options:\n"
+    " vcegar --showparse           show parse trees\n"
+    " vcegar --showvarmap          show variable map\n"
+    " vcegar --showcontext         show the context\n"
+    " vcegar --showtrans           show the three components of the transition relation\n"
+    "\n";
+}

src/vcegar/parseoptions.h

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Command Line Parsing
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <parseoptions.h>
+
+class vcegar_parseoptionst:public parseoptions_baset
+{
+public:
+  virtual int doit();
+  virtual void help();
+
+  vcegar_parseoptionst(int argc, const char **argv):
+    parseoptions_baset(
+      "(bmc)(showcubes)(noconstrain)"
+      "(nowpcons)(refine1)(nocache)(siege)"
+      "(bound):(showparse)(p):(partition): (abstraction):"
+      "(showvarmap)(dimacs)(no-simplify)(module):(i):"
+      "(showtrans)(init-pred):(discover):"
+      "(verbose)(xml-ui)(showcontext)(v):(gcr)"
+      "(one_cex_only)(debug)(pred):(more-stats)(relate-init)"
+      "(gcrsize):(noinit)(mapping)(modelchecker):(ltl)"
+      "(show-modules)(show-claims)(claim):(num-threads):(absref3)",
+      argc, argv)
+  {
+  }
+   
+  virtual ~vcegar_parseoptionst() { }
+};

src/vcegar/partitioning.cpp

@@ -0,0 +1,697 @@
+/*******************************************************************\
+
+Module: Partitioning (partitioning of predicates)
+
+Author: Himanshu Jain
+
+Date: April 2004
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <map>
+#include <vector>
+#include <i2string.h>
+#include <verilog/expr2verilog.h>
+#include <namespace.h>
+
+#include "partitioning.h"
+#include "canonicalize.h"
+#include "vcegar_util.h"
+
+
+/*******************************************************************\
+
+Function: print_predicate_symbol_maps
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Useful for debugging
+
+\*******************************************************************/
+
+void partitioningt::print_predicate_symbol_maps 
+(
+ const predicate_symbol_mapt& initial_predicates,
+ const predicate_symbol_mapt& final_predicates
+) 
+{
+  std::cout <<"Initial predicates and symbols in them \n";
+  
+ unsigned i=0;
+ for (predicate_symbol_mapt::const_iterator 
+	it = initial_predicates.begin(); 
+      it != initial_predicates.end(); it++){
+   
+
+   std::cout <<"Predicate ["<< i <<"] \n"<<  expr2verilog(it->first) <<"\n";
+   std::cout <<"Symbols \n";
+   
+   for (std::set<std::string>::const_iterator it2= it->second.begin();
+	it2!= it->second.end(); it2++) {
+     
+     std::cout <<"  "<<*it2<<"\n";
+   }
+
+   std::cout <<"---------------\n";
+   i++;
+ }
+
+ std::cout <<"Final predicates and symbols in them \n";
+ 
+ i=0;
+ 
+ for (predicate_symbol_mapt::const_iterator 
+	it = final_predicates.begin(); 
+      it != final_predicates.end(); it++){
+   
+
+   std::cout <<"Predicate ["<< i <<"] \n"<<  expr2verilog(it->first) <<"\n";
+   
+   std::cout <<"Symbols \n";
+   
+   for (std::set<std::string>::const_iterator it2= it->second.begin();
+	it2!= it->second.end(); it2++) {
+     
+     std::cout <<"  "<<*it2<<"\n";
+   }
+   std::cout <<"---------------\n";
+      i++;
+ }
+}
+
+/*******************************************************************\
+
+Function: print_predicate_clusters
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints the various clusters of the predicates.
+
+\*******************************************************************/
+
+void partitioningt::print_predicate_clusters(const predicate_clusterst &pred_clusters)
+{
+  unsigned i=0;
+  for (predicate_clusterst::const_iterator it3 = pred_clusters.begin();
+       it3 != pred_clusters.end(); it3++) {
+    
+    std::cout << "Cluster no. "<<i<<"\n";
+    std::cout <<*it3;
+    i++;
+  }
+}
+
+
+/*******************************************************************\
+
+Function: partition_initial_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Partitions the current set of predicates, for the calculation 
+of initial set of states.
+
+\*******************************************************************/
+unsigned partitioningt::return_predicate_index
+(const predicate_index_mapt& predicate_index_map,
+ const exprt& expr
+ ) 
+{
+  predicate_index_mapt::const_iterator sit =
+    predicate_index_map.find(expr);
+  
+  if (sit == predicate_index_map.end())
+    assert(0);
+
+  return sit->second;
+
+}
+
+
+/*******************************************************************\
+
+Function: partition_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Given a set of current set of predicates, it first computes the next state
+set of predicates. This is followed by placing each next state predicate into a 
+new cluster together with the current state predicates which are identified using
+weakest precondition of the next state predicate (partitioningA strategy).
+
+\*******************************************************************/
+
+void partitioningt::partition_predicates(
+  const predicatest& predicates, 
+  const exprt& trans,
+  const namespacet &ns,
+  const var_mapt& varmap,
+  const network_infot &network,
+  predicate_clusterst& pred_clusters,
+  unsigned choice,
+  bool verbose)
+{   
+  if (choice == 8)
+    return;
+
+  predicate_symbol_mapt initial_predicates, final_predicates;
+  predicate_index_mapt predicate_index_map;
+
+
+  if (!( choice == 2 ||
+	 choice==6  || choice==4))
+    throw "--partition option takes only one of 2,4 (monolithic) ,6, 8 as values\n";
+
+ for(unsigned i=0; i<predicates.size(); i++) //No test is made to test if the value
+    {                                         //of a predicate does not change.    
+      if (!(choice==6 ||choice==7)){
+	exprt input(predicates[i]);
+        
+ 	ns.follow_macros(input);
+
+
+	exprt input_copy(input); 
+	//replace_outputs(input, (trans.operands())[0], varmap);
+ 	
+	network.replace_outputs (input);
+
+	std::set<std::string> input_symbols;
+	find_symbols(input, input_symbols, "symbol");
+
+
+	initial_predicates.insert(std::pair<exprt, std::set<std::string> >
+				  (input_copy, input_symbols));
+	predicate_index_map.insert(std::pair<exprt, unsigned >
+				   (input_copy, i));
+
+
+      }
+      
+
+      exprt final(predicates[i]); 
+
+
+      ns.follow_macros(final);
+
+
+      exprt final1(final); // need many copies :(
+
+  
+      network.replace_outputs(final);
+
+
+      exprt final_copy(final);
+
+
+      if (choice != 6 && choice != 7) {
+
+  
+	network.weakest_precondition (final_copy);
+    }
+      
+      if (!(choice==3 || choice==6 || choice==7)) {
+
+	network.replace_outputs (final_copy) ;
+      }
+
+      std::set<std::string> final_symbols;
+      find_symbols(final_copy, final_symbols, "symbol");
+      
+
+      rename(final1);
+      final_predicates.insert(std::pair<exprt, std::set<std::string> >
+			      (final1, final_symbols));
+      predicate_index_map.insert(std::pair<exprt, unsigned >
+				 (final1, i));
+
+    }
+
+ #if 0
+ print_predicate_symbol_maps(initial_predicates, final_predicates);
+ #endif
+
+ switch(choice){
+ case 2: {
+   if (verbose)
+     std::cout <<"Calling partitioning strategyB : option 2\n";
+   partitioningB(initial_predicates, final_predicates, 
+		 predicate_index_map, pred_clusters);
+   break;
+ }
+ case 4: { //monolithic, only one cluster is created.
+   if (verbose)
+     std::cout <<"Calling monolithic (no predicate partitioning) : option 4\n";
+   monolithic(initial_predicates, final_predicates, 
+	      predicate_index_map, pred_clusters);
+   break;
+ }
+ case 6: {
+   if (verbose)
+     std::cout <<"Calling partitioning strategyD: option 6\n";
+   partitioningD(final_predicates, 
+		 predicate_index_map, pred_clusters);
+   break;     
+ }
+ default:
+   throw "Must not reach here\n";
+ }
+ 
+}
+
+/*******************************************************************\
+
+Function: partition_initial_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Partitions the current set of predicates, for the calculation 
+of initial set of states.
+
+\*******************************************************************/
+void partitioningt::partition_initial_predicates
+(const predicatest& predicates, 
+ const namespacet &ns,
+ const exprt& trans,
+ const var_mapt& varmap,
+ const network_infot &network,
+ predicate_clusterst& pred_clusters
+ )
+{   
+  predicate_symbol_mapt initial_predicates;
+  predicate_index_mapt predicate_index_map;
+
+ for(unsigned i=0; i<predicates.size(); i++) 
+    {                                        
+      exprt input(predicates[i]); 
+      ns.follow_macros(input);
+      
+      network.replace_outputs ( input );
+
+
+      std::set<std::string> input_symbols;
+      find_symbols(input, input_symbols, "symbol");
+
+
+      exprt input1(predicates[i]);
+      ns.follow_macros(input1);
+      initial_predicates.insert(std::pair<exprt, std::set<std::string> >
+				(input1, input_symbols));
+      predicate_index_map.insert(std::pair<exprt, unsigned >
+				 (input1, i));
+      
+
+    }
+
+
+ 
+ //Trying to club the predicates sharing same symbols.
+ //Hopefully! not many share the same symbols. 
+ 
+ //which pred is mapped to which cluster
+ unsigned pred_cluster_map[predicates.size()];
+   
+   unsigned predno=0;
+
+   predicate_symbol_mapt::const_iterator 
+     it = initial_predicates.begin();
+   
+   pred_clusters.reserve(predicates.size());
+
+   while (it !=  initial_predicates.end()) {
+
+     pred_clusters.push_back(predicatest());
+
+     exprt p(it->first);
+     
+     unsigned index = return_predicate_index(predicate_index_map, p);
+
+     pred_clusters[pred_clusters.size()-1].lookup(p, index, 
+						  predicatest::INITIAL);
+     
+     pred_cluster_map[predno] = pred_clusters.size()-1;
+
+     predno++;
+     
+     bool continue_scan = true;
+     
+     it++;
+     while (it != initial_predicates.end() && continue_scan) {
+       unsigned count =0;
+       bool subset_found = false;
+       
+       for (predicate_symbol_mapt::const_iterator 
+	      it1 = initial_predicates.begin();
+	    it1 != it && (!subset_found) ; it1++)
+	 {
+
+	   if (subset(it->second, it1->second)) {
+	     exprt p(it->first);
+	     
+	     unsigned index = return_predicate_index(predicate_index_map, p);
+	     pred_clusters[pred_cluster_map[count]].lookup(p, index, 
+							   predicatest::INITIAL);
+	     
+
+	     pred_cluster_map[predno] = pred_cluster_map[count];
+	     predno++;
+	     subset_found = true;
+	   }
+	   count++;
+	 }
+       
+       if (subset_found) 
+	 it++; 
+       else
+	 continue_scan=false;
+       
+     }
+   
+   }
+}
+
+
+
+/*******************************************************************\
+
+Function:  partitioningB
+
+Inputs: 
+
+Outputs:
+
+Purpose: Merges all final state predicates which have same symbols in
+the weakest preconditions.
+
+\*******************************************************************/
+
+
+void partitioningt::partitioningB
+(const predicate_symbol_mapt& inputs, 
+ const predicate_symbol_mapt& finals,
+ const predicate_index_mapt& pred_index_map,
+ predicate_clusterst& pred_clusters
+ )
+{
+  symbolset_predicates_mapt symbolset_predicates_map;
+  //Add the symbol set associated with each next state predicate.
+
+  for (predicate_symbol_mapt::const_iterator 
+	 it1 = finals.begin();it1 != finals.end(); it1++)
+    {
+      exprt p(it1->first);
+
+      symbolset_predicates_mapt::iterator it2 = 
+	symbolset_predicates_map.find(it1->second);
+
+      if (it2 == symbolset_predicates_map.end()) {
+	symbolset_predicates_map.insert
+	  (std::pair<std::set<std::string>, predicatest> 
+	   (it1->second, predicatest()));
+
+	symbolset_predicates_mapt::iterator it3 = 
+	  symbolset_predicates_map.find(it1->second);
+	
+	unsigned index = return_predicate_index(pred_index_map, p);
+	(it3->second).lookup(p, 
+			     index,
+			     predicatest::FINAL);
+
+      }
+      else {
+	unsigned index = return_predicate_index(pred_index_map, p);
+	(it2->second).lookup(p, 
+			     index,
+			     predicatest::FINAL);
+      }
+    }
+  
+  unsigned i =0;
+
+  for(symbolset_predicates_mapt::iterator it1 = 
+	symbolset_predicates_map.begin();
+      it1 != symbolset_predicates_map.end(); it1++) {
+
+
+    for (predicate_symbol_mapt::const_iterator 
+	   it2 = inputs.begin();it2 != inputs.end(); it2++)
+      {
+	if (subset(it2->second, it1->first)) {
+	  exprt p(it2->first);
+
+	  unsigned index = return_predicate_index(pred_index_map, p);
+
+	  (it1->second).lookup(p, index, 
+			       predicatest::INITIAL);
+	}
+      }
+    
+  }
+  
+  i=0;
+  
+  for (i=0; i<symbolset_predicates_map.size(); i++)
+    pred_clusters.push_back(predicatest());
+   
+
+  i=0;
+  for(symbolset_predicates_mapt::const_iterator it = 
+	symbolset_predicates_map.begin();
+      it != symbolset_predicates_map.end(); it++) {
+    for(unsigned j =0; j < (it->second).size(); j++) 
+      {
+	predicatest::statet state;
+	unsigned nr;
+	(it->second).get_info((it->second)[j], nr, state);
+	exprt new_exprt((it->second)[j]);
+
+
+	pred_clusters[i].lookup(new_exprt, nr, state); 
+      }
+    
+    
+
+    i++;
+  }
+
+}
+
+/*******************************************************************\
+
+Function:  monolithic
+
+Inputs: 
+
+Outputs:
+
+Purpose: Puts all initial and final predicates in one cluster.
+
+\*******************************************************************/
+
+
+void partitioningt::monolithic
+(const predicate_symbol_mapt& inputs, 
+ const predicate_symbol_mapt& finals,
+ const predicate_index_mapt& pred_index_map,
+ predicate_clusterst& pred_clusters
+ )
+{
+  pred_clusters.push_back(predicatest());
+  
+  //add all initial state predicates
+
+  for (predicate_symbol_mapt::const_iterator 
+	 it2 = inputs.begin();it2 != inputs.end(); it2++)
+      {
+	exprt p(it2->first);
+	unsigned index = return_predicate_index(pred_index_map, p);
+	pred_clusters[0].lookup(p, index, predicatest::INITIAL);
+      }
+  
+  //add all final state predicates
+  
+  for (predicate_symbol_mapt::const_iterator 
+	 it2 = finals.begin();it2 != finals.end(); it2++)
+    {
+      exprt p(it2->first);
+      unsigned index = return_predicate_index(pred_index_map, p);
+      pred_clusters[0].lookup(p, index, predicatest::FINAL);
+    }
+
+  return;
+}
+
+
+/*******************************************************************\
+
+Function:  partitioningD
+
+Inputs: 
+
+Outputs:
+
+Purpose: Merges all final state predicates which have same symbols. No input
+preds are kept in the cluster. Very coarse partitioning.
+
+\*******************************************************************/
+
+void partitioningt::partitioningD
+(const  predicate_symbol_mapt& final_only_symbols,
+ const predicate_index_mapt& pred_index_map,
+ predicate_clusterst& pred_clusters
+ )
+{
+  symbolset_predicates_mapt symbolset_predicates_map;
+
+  //first cluster the final state predicates.
+  
+  for (predicate_symbol_mapt::const_iterator 
+	 it1 = final_only_symbols.begin(); 
+       it1 != final_only_symbols.end(); it1++)
+    {
+      exprt p(it1->first);
+
+      symbolset_predicates_mapt::iterator it2 = 
+	symbolset_predicates_map.find(it1->second);
+
+      if (it2 == symbolset_predicates_map.end()) {
+	symbolset_predicates_map.insert
+	  (std::pair<std::set<std::string>, predicatest> 
+	   (it1->second, predicatest()));
+
+	symbolset_predicates_mapt::iterator it3 = 
+	  symbolset_predicates_map.find(it1->second);
+	
+	unsigned index = return_predicate_index(pred_index_map, p);
+	(it3->second).lookup(p, 
+			     index,
+			     predicatest::FINAL);
+
+      }
+      else {
+	unsigned index = return_predicate_index(pred_index_map, p);
+	(it2->second).lookup(p, 
+			     index,
+			     predicatest::FINAL);
+      }
+    }
+  
+  
+  unsigned  i=0;
+  
+  for (i=0; i<symbolset_predicates_map.size(); i++)
+    pred_clusters.push_back(predicatest());
+   
+
+  i=0;
+  for(symbolset_predicates_mapt::const_iterator it = 
+	symbolset_predicates_map.begin();
+      it != symbolset_predicates_map.end(); it++) {
+    for(unsigned j =0; j < (it->second).size(); j++) 
+      {
+	predicatest::statet state;
+	unsigned nr;
+	(it->second).get_info((it->second)[j], nr, state);
+	exprt new_exprt((it->second)[j]);
+
+
+	pred_clusters[i].lookup(new_exprt, nr, state); 
+      }
+    
+    i++;
+  }
+
+}
+
+
+/*******************************************************************\
+
+Function: vcegar_loopt::obtain_refinement_cluster
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Copies predicate clusters to abstraction.refinement_clusters
+
+\*******************************************************************/
+
+void partitioningt::obtain_refinement_cluster
+(const predicatest& predicates,
+ const network_infot &network,
+ const namespacet &ns,
+ const pred_id_set_pairt &pred_id_set_pair,
+ predicatest& pred_cluster)
+{
+  //add initial state preds
+  
+  for (std::set<unsigned>::const_iterator isp = (pred_id_set_pair.first).begin();
+       isp != (pred_id_set_pair.first).end(); isp++)
+    {
+      unsigned pred_num = *isp;
+
+      exprt input(predicates[pred_num]);
+      ns.follow_macros(input);
+      network.replace_outputs (input);
+      
+      pred_cluster.lookup(input, pred_num, predicatest::INITIAL);
+    }
+  
+      //add final state preds
+
+  for (std::set<unsigned>::const_iterator fsp = (pred_id_set_pair.second).begin();
+       fsp != (pred_id_set_pair.second).end(); fsp++)
+    {
+      unsigned pred_num = *fsp;
+      
+      exprt final(predicates[pred_num]);
+      ns.follow_macros(final);
+      rename(final);
+      network.replace_outputs (final);
+
+      pred_cluster.lookup(final, pred_num, predicatest::FINAL);
+    }
+}
+
+
+
+
+/*******************************************************************\
+
+Function: vcegar_loopt::copy_clusters
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Copies predicate clusters to abstraction.refinement_clusters
+
+\*******************************************************************/
+
+
+void partitioningt::print_clusters(const partitioningt::pred_id_clusterst 
+				   &refine_clusters) 
+{
+
+  unsigned count = 0;
+  
+  for (partitioningt::pred_id_clusterst::const_iterator  it = refine_clusters.begin();
+       it != refine_clusters.end(); it++)
+    {
+      std::cout << "Cluster num[" << count << "]: ";
+      std::cout << it -> first;
+      std::cout << it -> second;
+    }
+}
+

src/vcegar/partitioning.h

@@ -0,0 +1,156 @@
+/*******************************************************************\
+
+Module: Routines for predicate partitioning
+
+Author: Himanshu Jain
+
+Date: June 2004
+
+\*******************************************************************/
+
+#ifndef CPROVER_PARTITIONING_H
+#define CPROVER_PARTITIONING_H
+
+#include <message.h>
+#include <namespace.h>
+
+#include <trans/var_map.h>
+#include <verilog/expr2verilog.h>
+
+#include "concrete_trans.h"
+#include "abstract_trans.h"
+#include "predicates.h"
+#include "network_info.h"
+
+class partitioningt
+ {
+ public:
+   partitioningt()
+     {
+
+     }
+
+   ~partitioningt()
+     {
+
+     }
+
+
+   typedef std::map<exprt, std::set<std::string> > 
+     predicate_symbol_mapt;
+
+   typedef std::vector<predicatest>
+     predicate_clusterst;
+
+   typedef std::pair<std::set<unsigned>, std::set<unsigned> > 
+     pred_id_set_pairt;
+
+
+   typedef std::set<pred_id_set_pairt> 
+     pred_id_clusterst;
+
+
+    typedef std::map<exprt, unsigned> 
+      predicate_index_mapt;
+    
+
+    typedef std::map<std::set<std::string>, 
+      predicatest> symbolset_predicates_mapt;
+
+    void print_clusters(const partitioningt::pred_id_clusterst 
+			&refine_clusters) ;
+
+
+    void print_predicate_symbol_maps 
+      (
+       const predicate_symbol_mapt& initial_predicates,
+       const predicate_symbol_mapt& final_predicates
+       );
+
+    void print_predicate_clusters(const predicate_clusterst 
+				  &pred_clusters);
+
+    unsigned return_predicate_index
+      (const predicate_index_mapt& predicate_index_map,
+       const exprt& expr
+       ) ;
+
+
+    void partitioningA
+      (const predicate_symbol_mapt& inputs,
+      const predicate_symbol_mapt& finals,
+       const predicate_index_mapt& pred_index_map, 
+       predicate_clusterst& pred_clusters
+       );
+    
+
+    void partition_predicates
+      (const predicatest& predicates, 
+      const exprt& trans,
+       const namespacet &ns,
+       const var_mapt& var_map,
+       const network_infot &network,
+       predicate_clusterst& pred_clusters,
+       unsigned choice,
+       bool verbose);
+    
+    void partition_initial_predicates
+      (const predicatest& predicates, 
+       const namespacet &ns,
+       const exprt& trans,
+       const var_mapt& var_map,
+       const network_infot &network,
+       predicate_clusterst& pred_clusters);
+    
+    void partitioningB
+      (const predicate_symbol_mapt& inputs,
+       const predicate_symbol_mapt& finals,
+	const predicate_index_mapt& pred_index_map,
+	 predicate_clusterst& pred_clusters
+       );
+
+    void monolithic
+      (const predicate_symbol_mapt& inputs, 
+       const predicate_symbol_mapt& finals,
+       const predicate_index_mapt& pred_index_map,
+       predicate_clusterst& pred_clusters
+       );
+
+    void partitioningC
+      (const predicate_symbol_mapt& inputs, 
+       const predicate_symbol_mapt& finals,
+       const  predicate_symbol_mapt& final_only_symbols,
+       const predicate_index_mapt& pred_index_map,
+       predicate_clusterst& pred_clusters
+       );
+
+    void partitioningD
+      (const  predicate_symbol_mapt& final_only_symbols,
+       const predicate_index_mapt& pred_index_map,
+       predicate_clusterst& pred_clusters
+       );
+
+    void partitioningE
+      (const predicate_symbol_mapt& final_only_symbols,
+       const predicate_index_mapt& pred_index_map,
+       predicate_clusterst& pred_clusters);
+
+    void activate_refinement_clusters
+      (const predicatest& predicates,
+       const network_infot &network,
+       const namespacet &ns,
+       const pred_id_clusterst &pred_id_clusters,
+       predicate_clusterst& pred_clusters
+       );
+
+
+    void obtain_refinement_cluster
+      (const predicatest& predicates,
+       const network_infot &network,
+       const namespacet &ns,
+       const pred_id_set_pairt &pred_id_set_pair,
+       predicatest& pred_cluster);
+
+ };
+
+#endif

src/vcegar/predabs_aux.cpp

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Predicate Abstraction Auxiliary Code
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include "predabs_aux.h"
+
+/*******************************************************************\
+
+Function: make_pos
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: ensures that the literal is positive
+          and that all literals that are quantified over
+          are unique
+
+\*******************************************************************/
+
+literalt make_pos(prop_convt &conv, const exprt &expr)
+ {
+   literalt l=conv.convert(expr);
+   literalt tmp=conv.prop.new_variable();
+   conv.prop.set_equal(tmp, l);
+   assert(!tmp.sign());
+   return tmp;
+ }
+
+/*******************************************************************\
+
+Function: uses_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool uses_symbol(const exprt &expr,
+                 const std::set<std::string> &symbols)
+ {
+  forall_operands(it, expr)
+    if(uses_symbol(*it, symbols))
+      return true;
+
+
+  if(expr.id()=="symbol")
+    return symbols.find(expr.get("identifier").as_string())!=symbols.end();
+
+  return false;
+ }

src/vcegar/predabs_aux.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Predicate Abstraction Auxiliary Code
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_PREDABS_AUX
+#define CPROVER_PREDABS_AUX
+
+
+#include <set>
+#include <string>
+
+#include <solvers/prop/prop_conv.h>
+
+literalt make_pos(prop_convt &conv, const exprt &expr);
+
+bool uses_symbol(const exprt &expr,
+                 const std::set<std::string> &symbols);
+
+#endif

src/vcegar/predicates.cpp

@@ -0,0 +1,176 @@
+/*******************************************************************\
+
+Module: Predicate Manager
+
+Author: Daniel Kroening, kroening@kroening.com
+        Himanshu Jain, hjain@cs.cmu.edu
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <verilog/expr2verilog.h>
+
+#include "predicates.h"
+
+/*******************************************************************\
+
+Function: predicatest::lookup
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: find (and add, if not found) a predicate
+
+\*******************************************************************/
+
+unsigned predicatest::lookup(const predicatet &predicate)
+ {
+    std::pair<predicate_mapt::iterator, bool> result=
+      predicate_map.insert(
+      std::pair<predicatet, unsigned>
+      (predicate, predicate_vector.size()));
+
+   if(result.second) // already there?
+    {
+     // actually inserted
+     predicate_vector.push_back(result.first);
+    }
+
+   predicate_state.insert(std::pair<predicatet, statet>
+			  (predicate, NOT_DEFINED));
+   
+
+   return result.first->second;
+ }
+
+
+/*******************************************************************\
+
+Function: predicatest::lookup
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: find (and add, if not found) a predicate
+
+\*******************************************************************/
+
+void predicatest::lookup(const predicatet &predicate, 
+			 unsigned predicate_num, 
+			 statet state)
+ {
+    std::pair<predicate_mapt::iterator, bool> result=
+      predicate_map.insert(
+      std::pair<predicatet, unsigned>
+      (predicate, predicate_num));
+
+
+   if(result.second) // already there?
+    {
+     // actually inserted
+     predicate_vector.push_back(result.first);
+    }
+
+   
+   predicate_state.insert(std::pair<predicatet, statet>
+			  (predicate, state));
+
+ }
+
+
+/*******************************************************************\
+
+Function: operator<<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream& operator<< (std::ostream& out,
+                          const predicatest &predicates)
+ {
+   for(unsigned i=0; i<predicates.size(); i++)
+    {
+     std::string code;
+
+     unsigned nr;
+     if (!predicates.find(predicates[i], nr)) 
+       nr = i;
+
+     out << "b" << nr << " <=> " << expr2verilog(predicates[i]) << std::endl;
+    }
+
+  return out;
+ }
+
+/*******************************************************************\
+
+Function: operator<<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+
+void predicatest::get_pred_ids(std::pair<std::set<unsigned>, std::set<unsigned> >
+			       &pred_id_set_pair) const
+{
+  for(unsigned i=0; i < size(); i++) 
+    {                                     
+      predicatest::statet state;
+      unsigned nr;
+      
+      this->get_info(predicate_vector[i]->first, nr, state);
+      
+      switch(state) {
+      case predicatest::INITIAL: {
+	pred_id_set_pair.first.insert(nr);
+	break;
+      }
+      case predicatest::FINAL: {
+	pred_id_set_pair.second.insert(nr);
+	break;
+      }
+      case predicatest::NOT_DEFINED: {
+	assert(0);
+	break;
+      }
+      }
+    }
+  
+  return;
+}
+
+
+/*******************************************************************\
+
+Function: operator<<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::ostream& operator<< (std::ostream& out,
+                          const std::set<predicatet> &ps)
+{
+  for(std::set<predicatet>::const_iterator psit = ps.begin(); psit != ps.end(); psit++)
+    {
+      out << expr2verilog(*psit)<< "\n";
+    }
+  return out;
+}

src/vcegar/predicates.h

@@ -0,0 +1,124 @@
+/*******************************************************************\
+
+Module: Predicate Manager
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_PREDICATES_H
+#define CPROVER_PREDICATES_H
+
+#include <set>
+#include <expr.h>
+
+typedef exprt predicatet;
+
+class predicatest
+ {
+ public:
+   typedef enum {INITIAL, FINAL, NOT_DEFINED} statet;
+
+   predicatest(){}
+   ~predicatest(){}
+
+  // find (and add, if not found) a predicate
+  unsigned lookup(const predicatet &predicate);
+
+  //Same task as the above function except that the
+  //the number for the predicate to be inserted is provided
+  //by the user as the second argument.
+  void lookup(const predicatet &predicate, 
+	      unsigned predicate_num, 
+	      statet state);
+  
+  // just find (and do not add, if not found) a predicate
+  // true = predicate found
+  bool find(const predicatet &predicate) const
+   {
+    return predicate_map.find(predicate)!=predicate_map.end();
+   }
+  
+  // just find (and do not add, if not found) a predicate
+  // true = predicate found
+  bool find(const predicatet &predicate, unsigned &nr) const
+   {
+    predicate_mapt::const_iterator it=
+      predicate_map.find(predicate);
+      
+    if(it==predicate_map.end())
+      return false;
+      
+    nr=it->second;
+    
+    return true;
+   }
+  
+  const predicatet &operator[](unsigned nr) const
+   {
+    return predicate_vector[nr]->first;
+   }
+
+  
+
+  statet get_state(const predicatet &predicate) const
+    {
+      predicate_statet::const_iterator it=
+	predicate_state.find(predicate);
+
+      if (it==predicate_state.end())
+	return NOT_DEFINED;
+      else
+	return it->second; 
+    }
+
+
+  bool get_info(const predicatet &predicate, 
+		unsigned& nr, statet& state) const
+    {
+      predicate_statet::const_iterator it=
+	predicate_state.find(predicate);
+
+      if (it==predicate_state.end()) {
+	state=NOT_DEFINED;
+	return false;
+      }
+      else {
+	state=it->second; 
+	return find(predicate, nr);
+      }
+    }
+
+
+
+   
+  // how many?
+  unsigned size() const
+   {
+    return predicate_vector.size();
+   }
+
+  void get_pred_ids(std::pair<std::set<unsigned>, std::set<unsigned> > &pred_id_set_pair) const;
+  
+ protected:
+  typedef std::map<predicatet, unsigned> predicate_mapt;
+  typedef std::vector<predicate_mapt::iterator> predicate_vectort;
+  
+
+  predicate_mapt predicate_map;
+  predicate_vectort predicate_vector;
+  
+
+  typedef std::map<predicatet, statet> predicate_statet;
+  
+  predicate_statet predicate_state;
+  
+  std::vector<bool> used_vector;
+ };
+
+std::ostream& operator<< (std::ostream& out,
+                        const predicatest &predicates);
+
+std::ostream& operator<< (std::ostream& out,
+                          const std::set<predicatet> &ps);
+#endif

src/vcegar/refiner.cpp

@@ -0,0 +1,468 @@
+/*******************************************************************\
+  
+Module: Refinement for VCEGAR. Finds new word level predicates. And
+        constraints for syntactic abstraction.
+
+Author: Himanshu Jain, Daniel Kroening 
+        
+
+Date: Nov 2004
+ 
+\*******************************************************************/
+
+#include <assert.h>
+#include <iostream>
+
+#include <verilog/expr2verilog.h>
+#include <namespace.h>
+#include <cnf_simplify.h>
+#include <simplify_expr.h>
+#include <i2string.h>
+
+#include "refiner.h"
+#include "discover_predicates.h"
+#include "canonicalize.h"
+#include "partitioning.h"
+#include "vcegar_util.h"
+#include "instantiate_guards.h"
+
+//#define DEBUG
+
+/*******************************************************************\
+
+Function: refinert::init_preds
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: generate initial set of predicates for a concrete program
+
+\*******************************************************************/
+
+void refinert::init_preds(predicatest &predicates, 
+			  const concrete_transt &concrete_trans, 
+			  const contextt &context // only for DEBUG
+			  )
+ {
+  status("Calculating initial set of predicates");
+  
+  return;
+ }
+
+/*******************************************************************\
+
+Function: refinert::init_preds
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: generate initial set of predicates for a concrete program
+
+\*******************************************************************/
+
+void refinert::init_preds(predicatest &predicates, 
+			  const std::vector<exprt> &initial_predicates)
+ {
+   #ifdef DEBUG
+  status("Using provided set of initial predicates");
+  #endif
+
+  for(std::vector<predicatet>::const_iterator
+      p_it=initial_predicates.begin();
+      p_it!=initial_predicates.end();
+      p_it++)
+   {
+    bool negation;
+    exprt p(*p_it);
+    canonicalize(p, negation);
+    predicates.lookup(p);
+   }
+
+ }
+
+
+
+/*******************************************************************\
+
+Function: refinert::relate_pred_and_wp
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Update weakest_precondition_constrains, by entering the 
+relationship between a predicate and its weakest pre-condition.
+
+Some valuation of consitions => p_j == wp (p_i, transition relation)
+
+
+Basically, we will add (trans1 | trans2) to the abstraction.
+
+\*******************************************************************/
+
+
+void refinert::relate_pred_and_wp
+(const abstract_statet &abstract_state,
+ const std::set<unsigned> preds_used_to_simplify,
+ weakest_precondition_constrainst &weakest_precondition_constrains,
+ unsigned pred_num, unsigned wp_pred_num
+ )
+{
+  abstract_transition_constraintt trans1;
+  abstract_transition_constraintt trans2;
+
+  //determine maximum pred_num occuring in preds_used_to_simplify
+  unsigned maxp_simplify = max(preds_used_to_simplify);
+
+  unsigned total_num_preds = 
+    (maxp_simplify > wp_pred_num)?
+    ((maxp_simplify > pred_num)?maxp_simplify:pred_num):
+    ((wp_pred_num > pred_num)?wp_pred_num:pred_num);
+
+  #ifdef DEBUG
+  std::cout <<"maxp_simplify, pred_num, wp_pred_num are"<<maxp_simplify
+	    <<" "<<pred_num<<" "<<wp_pred_num<<"\n";
+  #endif
+
+  // initialize
+
+  for (unsigned i = 0; i <= total_num_preds; i++) {
+    trans1.first.push_back(NON_DET); //initial state
+    trans1.second.push_back(NON_DET); //final state
+    trans2.first.push_back(NON_DET); //initial state
+    trans2.second.push_back(NON_DET); //final state
+  }
+
+  //now set the valuation for predicate used when simplifying monolithic weakest pre-condition
+
+  for (std::set<unsigned>::const_iterator it = preds_used_to_simplify.begin();
+       it != preds_used_to_simplify.end(); it++) 
+    {
+
+      if (abstract_state.predicate_values[*it] == 0) {
+	trans1.first[*it] = ZERO;
+	trans2.first[*it] = ZERO;
+      }
+      else {
+	assert (abstract_state.predicate_values[*it] == 1);
+	trans1.first[*it] = ONE;
+	trans2.first[*it] = ONE;
+      }
+    }
+
+
+  // now it pred no. i is wp of pred. no j, then make preds i and j ZERO in trans1
+  // and make preds i and j ONE in trans2 (since pred no. i == next (j))
+  assert(trans1.second[pred_num] == NON_DET);
+  assert(trans2.second[pred_num] == NON_DET);
+
+  trans1.second[pred_num] = ZERO;
+  trans2.second[pred_num] = ONE;
+
+  if (trans1.first[wp_pred_num] == NON_DET)
+    {
+      assert(trans1.first[wp_pred_num] == NON_DET);
+      trans1.first[wp_pred_num] = ZERO;
+      trans2.first[wp_pred_num] = ONE;
+    }
+  else
+    {
+      assert(trans1.first[wp_pred_num] == trans2.first[wp_pred_num]);
+      if (trans1.first[wp_pred_num] == ONE)
+	{
+	  trans1.first.clear();
+	  trans1.second.clear();
+	}
+      else
+	{
+	  trans2.first.clear();
+	  trans2.second.clear();
+	}
+    }
+
+  weakest_precondition_constrains.insert(std::pair<abstract_transition_constraintt, 
+					 abstract_transition_constraintt> 
+					 (trans1, trans2)) ;
+}
+
+
+/*******************************************************************\
+
+Function: refinert::compute_wp_seed_predicate
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Given a predicate and a bound takes wp till that bound.
+
+\*******************************************************************/
+
+
+void refinert::compute_wp_seed_predicate
+ (predicatest &predicates, 
+  const abstract_counterexamplet &spurious_counterexample,
+  const contextt &context, 
+  const network_infot &network,
+  weakest_precondition_constrainst &weakest_precondition_constrains,
+  unsigned pred_num, //we will take wp of this
+  int len, //no. of steps for which to take the weakest pre-condition
+  std::vector<std::set<unsigned> > &imp_preds_per_state,
+  bool generate_extra_preds
+  )
+{
+  namespacet ns(context);
+  
+  exprt failed_property(predicates[pred_num]);
+  ns.follow_macros(failed_property);
+  network.replace_outputs(failed_property);  
+
+  std::set<predicatet> predicate_set;
+
+  bool early_quit = false;
+
+  for (int i=len; i >= 0 && (!early_quit); i--) {
+    std::string code;
+
+    exprt failed_property_copy(failed_property);
+    std::set<unsigned> preds_used_to_simplify;
+    bool containsInput = false; //failed_property should not have an input symbol.
+                                // need to add quantifier intantiattion code
+    
+    network.simplified_weakest_precondition(failed_property, spurious_counterexample[i], 
+					    predicates, preds_used_to_simplify, containsInput);
+
+    simplify (failed_property);
+
+    //we want to avoid avoid adding new predicates as much as possible
+    //this condition is true only when we fail to find new predicates...
+    if (generate_extra_preds)
+      imp_preds_per_state[i].insert(preds_used_to_simplify.begin(), preds_used_to_simplify.end());
+
+
+    #ifdef DEBUG
+    //    std::cout << "failed property " << failed_property << "\n";
+    if (generate_extra_preds)
+      std::cout << "Adding "<<preds_used_to_simplify << " imp_preds["<<i<<"]\n";
+    std::cout <<"simplified_weakest_precondition is  \n"
+	      << expr2verilog (failed_property) << " \n";
+    std::cout <<"Discovering predicates in the intermediate weakest pre-cond containsInput "
+	      <<containsInput<<"\n";
+    #endif
+    
+    bool isAtomic = false;
+    discover_predicates(failed_property, predicate_set, discover, isAtomic);
+  
+    #ifdef DEBUG
+    std::cout << "predicates discovered \n";
+    std::cout << predicate_set << "\n";
+    #endif
+
+    if (add_wp_cons) {
+      if (isAtomic && !containsInput) {
+	assert (predicate_set.size() == 1);
+       	#ifdef DEBUG
+	
+	std::cout <<"An atomic predicate discovered: "
+		  << expr2verilog (*predicate_set.begin())<<"\n";
+	std::cout <<"Preds used in simplification \n";
+	std::cout << preds_used_to_simplify;
+        #endif
+      }
+      else if (isAtomic && containsInput) {
+	#ifdef DEBUG
+	std::cout << "Atomic but contains input \n";
+        #endif
+      }
+      else {
+	#ifdef DEBUG
+	std::cout << "Not atomic  \n";
+        #endif
+      }
+    }
+    
+    if (verbose)
+      status("Before refinement #predicates "+i2string(predicates.size()));
+    
+
+    for(std::set<predicatet>::const_iterator it= predicate_set.begin();
+	it != predicate_set.end(); it++) 
+      {
+	#ifdef DEBUG
+	std::cout << "Found predicate: "<< *it << "\n";
+	#endif
+
+ 	if (containsSymbol(*it)) {
+	  predicates.lookup(*it);
+	  
+	  if (add_wp_cons) { 
+	    if (isAtomic && !containsInput) {
+	      
+	      //find the predicate number assigned to this predicate
+
+	      unsigned nr_wp, nr_pred;
+	      
+	      if (predicates.find (failed_property_copy, nr_pred)) 
+		{
+		  if (predicates.find(*it, nr_wp)) 
+		    {
+
+		      relate_pred_and_wp
+			(spurious_counterexample[i],
+			 preds_used_to_simplify,
+			 weakest_precondition_constrains,
+			 nr_pred, nr_wp) ;
+		    }
+		}
+	    }
+	  }
+	}
+      }
+    
+    predicate_set.clear();
+       
+
+    if (!isAtomic || containsInput)
+      {
+        #if 0
+	std::cout << "Early quiting isatomic " <<isAtomic << " containsinput "
+		  <<containsInput<<"\n";
+	if (isAtomic )
+	  std::cout << expr2verilog(failed_property) << "\n";
+        #endif
+
+	early_quit = true;
+      }
+
+    if (verbose)
+      status("After refinement #predicates "+i2string(predicates.size()));
+
+
+    
+    if (failed_property.is_false() || 
+	failed_property.is_true() ||
+	!containsSymbol(failed_property))
+      {
+	#ifdef DEBUG
+	std::cout <<"setting early quit to true as the property is constant true/false \n";
+	#endif
+
+	early_quit = true;
+      }
+  }
+  
+}
+
+
+
+/*******************************************************************\
+
+Function: refinert::generate_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:  
+
+\*******************************************************************/
+
+
+void refinert::generate_predicates
+ (predicatest &predicates, 
+  const abstract_counterexamplet &spurious_counterexample,
+  const contextt &context, 
+  const network_infot &network,
+  std::vector<std::set<unsigned> > &imp_preds_per_state,
+  weakest_precondition_constrainst &weakest_precondition_constrains,
+  bool generate_extra_preds
+  )
+{
+  for (unsigned i = imp_preds_per_state.size()-1; i >=1 ; i--) {
+    
+    for(std::set<unsigned>::const_iterator it= imp_preds_per_state[i].begin();
+	it != imp_preds_per_state[i].end(); it++) {
+      
+      assert (*it >= 0);
+      assert (*it < predicates.size());
+
+      #ifdef DEBUG
+      std::cout << "Now computing wp of predicate no. "<<*it <<"for "<<i-1<<" steps \n";
+      #endif
+
+      compute_wp_seed_predicate(predicates, 
+				spurious_counterexample,
+				context, 
+				network,
+				weakest_precondition_constrains,
+				*it,
+				i-1,
+				imp_preds_per_state,
+				generate_extra_preds);
+
+      
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: refinert::spurious_ce
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: generate a new set of predicates given a spurious counterexample
+
+\*******************************************************************/
+
+
+void refinert::spurious_ce
+ (predicatest &predicates, 
+  const concrete_transt &concrete_trans,
+  const abstract_counterexamplet &spurious_counterexample,
+  const contextt &context, 
+  const exprt property,
+  const network_infot &network,
+  std::vector<std::set<unsigned> > &imp_preds_per_state,
+  weakest_precondition_constrainst &weakest_precondition_constrains, //obtain the weakest pre-condition constraints
+  bool generate_extra_preds
+  )
+ {
+   if (verbose)
+     status("Size of spurious counterexample "+i2string(spurious_counterexample.size()));
+
+   
+   #ifdef DEBUG
+   std::cout <<"Use unsat cores when computing the weakest pre-condition \n";	
+   #endif
+
+   generate_predicates(predicates, 
+		       spurious_counterexample,
+		       context, 
+		       network,
+		       imp_preds_per_state,
+		       weakest_precondition_constrains, 
+		       generate_extra_preds);
+
+
+
+   if (verbose)
+     {
+       std::cout <<" After refinement \n";
+       std::cout <<predicates;
+     }
+
+ }
+
+
+
+
+
+
+
+
+

src/vcegar/refiner.h

@@ -0,0 +1,123 @@
+/*******************************************************************\
+
+Module: Refiner
+
+Author: Himanshu Jain, Daniel Kroening
+
+Date: June 2004
+
+Purpose: Calculate predicates for predicate abstraction.
+
+\*******************************************************************/
+
+#ifndef CPROVER_REFINER_H
+#define CPROVER_REFINER_H
+
+#include <assert.h>
+
+#include <message.h>
+#include <context.h>
+#include <cmdline.h>
+
+#include "concrete_trans.h"
+#include "predicates.h"
+#include "abstract_counterexample.h"
+#include "network_info.h"
+
+class refinert:public messaget
+ {
+ public:
+  refinert(message_handlert &_message_handler, 
+	   const cmdlinet &_cmdline) :
+    messaget(_message_handler),
+    cmdline(_cmdline)
+   {
+     if(!cmdline.isset("discover")) {
+       discover = 4; //default old was 2
+       #ifdef DEBUG
+       std::cout << "Discovering preds in weakest pre-conditions with "<<discover<<"\n";
+       #endif
+     }
+     else 
+       discover=atoi(cmdline.getval("discover"));
+     
+     #ifdef DEBUG
+     std::cout <<"discover is: "<<discover<<"\n";
+     #endif
+
+     if(!cmdline.isset("nowpcons")) 
+       {
+	 add_wp_cons = true;
+	 #ifdef DEBUG
+	 std::cout << "Adding weakest pre-condition constraints \n";
+	 #endif
+       }
+     else 
+       {
+	 add_wp_cons = false;
+	 std::cout << "Not adding weakest pre-condition constraints \n";
+       }
+     
+     if (cmdline.isset("verbose"))
+       verbose=true;
+     else
+       verbose=false;
+     
+   }
+  
+  bool verbose;
+  const cmdlinet &cmdline;
+  int discover;
+  bool add_wp_cons;
+
+
+  // Calculates the initial set of predicates for the given program
+  void init_preds(predicatest &predicates, 
+		  const concrete_transt &concrete_trans, 
+		  const contextt &context); // context is for DEBUG
+
+  // Calculates the initial set of predicates for the given program
+  void init_preds(predicatest &predicates, 
+                  const std::vector<exprt> &initial_predicates);
+
+
+ void spurious_ce(predicatest &predicates,
+		  const concrete_transt &concrete_trans,
+		  const abstract_counterexamplet &spurious_counterexample,
+		  const contextt &context,
+		  const exprt property,
+		  const network_infot &network,
+		  std::vector<std::set<unsigned> > &imp_preds_per_state,
+		  weakest_precondition_constrainst &weakest_precondition_constrains,
+		  bool generate_extra_preds); 
+
+ void generate_predicates
+   (predicatest &predicates, 
+    const abstract_counterexamplet &spurious_counterexample,
+    const contextt &context, 
+    const network_infot &network,
+    std::vector<std::set<unsigned> > &imp_preds_per_state,
+    weakest_precondition_constrainst &weakest_precondition_constrains,
+    bool generate_extra_preds);
+
+ void compute_wp_seed_predicate
+   (predicatest &predicates, 
+    const abstract_counterexamplet &spurious_counterexample,
+    const contextt &context, 
+    const network_infot &network,
+    weakest_precondition_constrainst &weakest_precondition_constrains, //constraints relating a predicate and its wp
+    unsigned pred_num, //we will take wp of this
+    int len, //no. of steps for which to take the weakest pre-condition
+    std::vector<std::set<unsigned> > &imp_preds_per_state,
+    bool generate_extra_preds
+    );
+
+ void relate_pred_and_wp
+   (const abstract_statet &abstract_state,
+    const std::set<unsigned> preds_used_to_simplify,
+    weakest_precondition_constrainst &weakest_precondition_constrains,
+    unsigned pred_num, 
+    unsigned wp_pred_num);   
+ };
+
+#endif

src/vcegar/satqe_satcheck.h

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SATQE_SATCHECK_H
+#define CPROVER_SATQE_SATCHECK_H
+
+#include <solvers/sat/satcheck_zchaff.h>
+#include <satqe/sat_cubes.h>
+
+class satqe_satcheckt:public satcheck_zchaff_baset
+ {
+ public:
+  satqe_satcheckt():satcheck_zchaff_baset((solver_ptr=new sat_cubest)) { }
+  virtual ~satqe_satcheckt() { delete solver_ptr; }
+  
+  sat_cubest &solver()
+   {
+    return *solver_ptr;
+   }
+
+  
+ protected:
+  sat_cubest *solver_ptr;
+ };
+
+#endif

src/vcegar/simulator.cpp

@@ -0,0 +1,851 @@
+/*******************************************************************\
+
+Module: Simulator
+
+Author: Himanshu Jain
+
+Date: May 2004
+
+Purpose: Simulate an abstract counterexample on the concrete program
+to check whether the counterexample is spurious.
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <iostream>
+#include <map>
+#include <fstream>
+#include <str_getline.h>
+#include <vector>
+
+#include <cnf_simplify.h>
+#include <expr_util.h>
+#include <i2string.h>
+#include <find_symbols.h>
+#include <solvers/sat/satcheck.h>
+#include <solvers/sat/dimacs_cnf.h>
+#include <langapi/language_ui.h>
+
+#include <trans/property.h>
+#include <trans/counterexample.h>
+
+#include "simulator.h"
+#include "vcegar_util.h"
+
+
+/*******************************************************************\
+
+Function: simulatort::print_imp_preds_set
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+
+void print_imp_preds_set(std::set<unsigned> &imp_preds)
+{
+   for (std::set<unsigned>::const_iterator it = 
+	 imp_preds.begin();
+       it != imp_preds.end(); it++)
+    {
+      std::cout <<"b["<<*it<<"] "; 
+    }
+   std::cout <<"\n";
+}
+
+
+/*******************************************************************\
+
+Function: simulatort::check_spurious_using_bmc
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: check an abstract counterexample
+          Only THE LENGTH of the abstract counterexample is used.
+          Returns TRUE if the counterexample is spurious,
+          and FALSE otherwise
+
+\*******************************************************************/
+
+bool simulatort::check_spurious_using_bmc
+ (const contextt &context,
+  const concrete_transt &concrete_trans,
+  const abstract_counterexamplet &abstract_counterexample,
+  const exprt spec_property,
+  concrete_counterexamplet &concrete_counterexample,
+  bool verbose,
+  bool simplify) 
+{
+   
+   if (abstract_counterexample.size()>0) {
+
+     std::list<bvt> prop_bv;
+     satcheckt satcheck;
+     boolbvt solver(satcheck);
+
+     const transt &trans = concrete_trans.trans_expr;
+
+     int bound = abstract_counterexample.size();
+
+     unwind (trans,
+	     *this,
+	     solver, 
+	     bound, 
+	     namespacet(context),
+	     true); //add initial state
+
+
+     std::list<exprt> properties;
+
+     
+     if (!cmdline.isset("claim"))
+       {
+	 exprt new_property("AG");
+	 new_property.copy_to_operands(spec_property);
+	 properties.push_back(new_property); 
+       }
+     else
+       {
+	 exprt new_property(spec_property);
+	 properties.push_back(new_property); 
+       }
+
+
+     namespacet ns(context);
+
+
+     property(properties, 
+	      prop_bv, 
+	      *this,
+	      solver, 
+	      bound,
+	      ns);
+
+     //Run the SAT solver
+
+     if(verbose)
+       {
+         #ifdef DEBUG
+	 std::cout << std::endl;
+	 std::cout << "Variables: " << solver->no_literals() << std::endl;
+	 std::cout << "Clauses:   " << solver->no_clauses()  << std::endl;
+	 std::cout << std::endl;
+	 #endif
+
+	 status("Running "+satcheck.solver_text());
+       }
+     
+     switch(satcheck.prop_solve())
+       {
+       case propt::P_SATISFIABLE:
+	 {
+
+	   
+	   compute_trans_trace(properties, 
+			       prop_bv, 
+			       solver, 
+			       bound,
+			       ns,
+			       module_identifier,
+			       concrete_counterexample);
+
+	 }
+	 break;
+       case propt::P_UNSATISFIABLE:
+	 return true;
+	 break;
+       case propt::P_ERROR:
+	 std::cout << "Error from SAT solver\n";
+	 break;
+	 
+       default:
+	 std::cout << "Unexpected result from SAT solver\n";
+       }
+      }
+   else 
+     {
+       throw 
+	 "Trying to refine, but abstract counterexample has length = 0 !";
+     }
+   
+   return false;
+ }
+
+
+
+/*******************************************************************\
+
+Function: simulatort::copy_state
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void simulatort::copy_state(
+  const abstract_statet &abstract_state, 
+  abstract_constraintt &constraint)
+{
+  std::cout <<"Inside copy_state \n";
+
+  for (std::vector<bool>::const_iterator 
+	 p_it = (abstract_state.predicate_values).begin();
+       p_it != (abstract_state.predicate_values).end(); p_it++) {
+    
+    if (*p_it) {
+      constraint.push_back(ONE);
+    }
+    else
+      constraint.push_back(ZERO);
+  }
+}
+
+/*******************************************************************\
+
+Function: simulatort::copy_important_preds
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+void simulatort::copy_important_preds(const abstract_statet &abstract_state,
+				      const std::set<unsigned> &imp_preds,
+				      abstract_constraintt &constraint) const
+{
+  #ifdef DEBUG
+  std::cout << abstract_state;
+  #endif
+
+  unsigned maxp = max (imp_preds); //find maximum element here
+
+  for (unsigned i = 0; i <= maxp; i++)
+    {
+      std::set<unsigned>::const_iterator it = imp_preds.find(i);
+    
+      if (it != imp_preds.end()) {
+      
+	if (abstract_state.predicate_values[i]) {
+	  constraint.push_back(ONE);
+	}
+	else
+	  constraint.push_back(ZERO);
+      }
+      else {
+	constraint.push_back(NON_DET);
+      }
+    }
+
+  
+  #ifdef DEBUG 
+  std::cout << "Constrtaint is \n"<< constraint;
+  #endif
+}
+
+
+
+
+/*******************************************************************\
+
+Function: simulatort::generate_constrains
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Generate constrains for eliminating spurious counterexamples.
+
+\*******************************************************************/
+
+ void simulatort::generate_constrains
+    (const contextt &context,
+     const concrete_transt &concrete_trans,
+     const predicatest &predicates,
+     const spurious_abstract_stepst &spurious_abstract_steps,
+     abstract_transition_constrainst &abstract_transition_constrains)
+{
+  for(spurious_abstract_stepst::const_iterator it = spurious_abstract_steps.begin();
+      it != spurious_abstract_steps.end(); it++) {
+    abstract_constraintt start_state_constrain;
+    abstract_constraintt end_state_constrain;
+
+    copy_state(it->first, start_state_constrain);
+    copy_state(it->second, end_state_constrain);
+
+    abstract_transition_constrains.insert(std::pair <abstract_constraintt, abstract_constraintt >
+					     (start_state_constrain, end_state_constrain));
+    
+  }
+}
+
+/*******************************************************************\
+
+Function: simulatort::create_cluster
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Given a set of inmporant initial and final predicates, 
+it creates a cluster out of them.
+
+\*******************************************************************/
+
+ void simulatort::create_cluster
+ (const contextt &context,
+  const std::set<unsigned> init_imp_preds,
+  const std::set<unsigned> final_imp_preds,
+  const predicatest &predicates,
+  predicatest &cluster)
+{
+  namespacet ns(context);
+
+  for(std::set<unsigned>::const_iterator it = init_imp_preds.begin();
+      it != init_imp_preds.end(); it++) {
+    exprt p(predicates[*it]);
+    ns.follow_macros(p);
+
+    cluster.lookup(p, *it, predicatest::INITIAL);
+    
+  }
+  
+  
+  for(std::set<unsigned>::const_iterator it = final_imp_preds.begin();
+      it != final_imp_preds.end(); it++) {
+    exprt p(predicates[*it]);
+    ns.follow_macros(p);
+
+    rename(p);
+    cluster.lookup(p, *it, predicatest::FINAL);
+  }
+}
+
+/*******************************************************************\
+
+Function: abstractort::out_cache_stats
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void simulatort::out_stats(std::ostream &out)
+{
+  status("#Not spurious cache hits "+ i2string(not_spurious_cache_hits)+
+ 	 " simulated "+
+         i2string(num_steps_checked)+", spurious "+
+	 i2string(num_spurious_steps)+", new constraints "+
+         i2string(num_constraints_found));
+}
+
+/*******************************************************************\
+
+Function: simulatort::collect_fail_info
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: reason of unsatisfiability
+
+\*******************************************************************/
+
+void simulatort::collect_fail_info(
+  const pred_literal_mappingt &pred_literal_map,  
+  satcheck_minisat_coret &satcheck_core, 
+  std::set<unsigned> &imp_preds) const
+{
+  for(pred_literal_mappingt::const_iterator it=
+      pred_literal_map.begin();
+      it != pred_literal_map.end();
+      it++)
+  {
+      if (satcheck_core.is_in_core(it->second))
+	{
+	  imp_preds.insert(it->first);
+	}
+  }
+}
+
+/*******************************************************************\
+
+Function: simulatort::add_abstract_state_map
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Maintain the mapping from a predicate to literalt
+
+\*******************************************************************/
+
+void simulatort::add_abstract_state_map(
+  const contextt &context,
+  const abstract_statet &abstract_state,
+  const predicatest &predicates,
+  const bmc_mapt& map,
+  propt &solver,
+  bool simplify,
+  unsigned start,
+  pred_literal_mappingt &pred_literal_mapping) 
+{  
+  namespacet ns(context);
+
+  unsigned pred_num = 0;
+  for (std::vector<bool>::const_iterator 
+	 p_it = (abstract_state.predicate_values).begin();
+       p_it != (abstract_state.predicate_values).end(); p_it++) 
+    {
+      exprt predicate(predicates[pred_num]);
+      
+      literalt pl = instantiate_convert(
+					solver,
+					map,
+					predicate,
+					start, start+1,
+					ns,
+					*this); // message
+
+      bool pl_val = *p_it;
+      assert(!pl.is_constant() || (pl.is_true() && pl_val) || 
+	     (pl.is_false() && !pl_val));
+
+      if (!pl.is_constant())
+	{
+	  solver.l_set_to(pl, pl_val);
+
+	  assert(pl.var_no() <= solver.no_variables());
+      
+	  assert ( pl.dimacs() != 0);
+	  pred_literal_mapping.insert(std::pair<unsigned, literalt>
+				      (pred_num, pl)); 
+	}
+      
+      pred_num++;
+    }
+}
+
+
+
+/*******************************************************************\
+
+Function: simulatort::add_abstract_state_map
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Maintain the mapping from a predicate to literalt
+
+\*******************************************************************/
+
+bool simulatort::add_abstract_state_map_transition(
+  const contextt &context,
+  const abstract_statet &abstract_state,
+  const predicatest &predicates,
+  const bmc_mapt& map,
+  prop_convt &solver,
+  bool simplify,
+  unsigned start,
+  pred_literal_mappingt &pred_literal_mapping) const
+{  
+  namespacet ns(context);
+
+  unsigned pred_num = 0;
+  for (std::vector<bool>::const_iterator 
+	 p_it = (abstract_state.predicate_values).begin();
+       p_it != (abstract_state.predicate_values).end(); p_it++) 
+    {
+      exprt predicate(predicates[pred_num]);
+      
+      instantiate(predicate, start, ns);
+      literalt pl=solver.convert(predicate);
+
+
+      bool pl_val = *p_it;
+      
+      if (pl.is_true() && !pl_val) 
+	{
+	  //we do not care about the literal assigned to pred_num 
+	  pred_literal_mapping.clear();
+	  pred_literal_mapping.insert(std::pair<unsigned, literalt>
+				      (pred_num, pl));
+	  return false;
+	}
+      
+      if (pl.is_false() && pl_val) 
+	{
+	  pred_literal_mapping.clear();
+	  pred_literal_mapping.insert(std::pair<unsigned, literalt>
+				      (pred_num, pl));
+	  return false;
+	}
+      
+      
+      assert(!pl.is_constant() || (pl.is_true() && pl_val) || 
+	     (pl.is_false() && !pl_val));
+      
+      if(!pl.is_constant())
+	{
+	  assert(pl.var_no() <= solver.prop.no_variables());
+	  assert ( pl.dimacs() != 0);
+	  solver.prop.l_set_to(pl, pl_val);
+	  pred_literal_mapping.insert(std::pair<unsigned, literalt>
+				      (pred_num, pl)); 
+	}
+      
+      pred_num++;
+    }
+  return true;
+}
+
+/*******************************************************************\
+
+Function: simulatort::is_spurious_abstract_transition
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Generating CNF using dimacs so that ..proofs of 
+unsatisfiability can be extracted by using chaff externally.
+
+\*******************************************************************/
+
+bool simulatort::is_spurious_abstract_transition(
+  const contextt &context,
+  const concrete_transt &concrete_trans,
+  const abstract_counterexamplet &abstract_counterexample,
+  const predicatest &predicates,
+  std::set<unsigned> &imp_init_preds,
+  std::set<unsigned> &imp_final_preds,
+  bool verbose,
+  bool simplify,
+  unsigned stepno) 
+{
+  assert(stepno < abstract_counterexample.size()-1);
+  namespacet ns(context);
+  const transt &trans = concrete_trans.trans_expr;
+
+  satcheck_minisat_coret satcheck;
+  bmc_mapt map;
+
+  map.var_map = concrete_trans.var_map;
+  map.map_timeframes(satcheck, 2);
+
+  boolbvt boolbv(satcheck);
+  boolbv.set_message_handler(get_message_handler());
+
+
+  exprt instantiated_trans(trans.trans());
+  instantiate(instantiated_trans, 0, ns);
+
+  exprt instantiated_invar0(trans.invar());
+  instantiate(instantiated_invar0, 0, ns);
+  
+  exprt instantiated_invar1(trans.invar());
+  instantiate(instantiated_invar1, 1, ns);
+  
+  boolbv.set_to_true(instantiated_invar0);
+  boolbv.set_to_true(instantiated_invar1);
+  boolbv.set_to_true(instantiated_trans);
+
+
+  pred_literal_mappingt initial_pred_literal_map, 
+    final_pred_literal_map;
+
+  // Add the start abstract state
+  bool b1= add_abstract_state_map_transition
+    (context, 
+     abstract_counterexample[stepno],
+     predicates,
+     map, boolbv, simplify, 0, 
+     initial_pred_literal_map);
+
+  if (!b1)
+    {
+      assert(initial_pred_literal_map.size() == 1);
+      imp_init_preds.insert(initial_pred_literal_map.begin()->first);
+      return true;
+    }
+
+  // Add the end abstract state
+  bool b2 = add_abstract_state_map_transition
+    (context, 
+     abstract_counterexample[stepno+1],
+     predicates,
+     map, boolbv, simplify, 1,  
+     final_pred_literal_map);
+
+  if (!b2)
+    {
+      assert(final_pred_literal_map.size() == 1);
+      imp_final_preds.insert(final_pred_literal_map.begin()->first);
+      return true;
+    }
+
+  
+  if (verbose)
+    status("Running "+satcheck.solver_text()); 
+
+  switch(satcheck.prop_solve())
+    {
+    case propt::P_SATISFIABLE:
+      return false; //can be simulated
+      break;  
+      
+    case propt::P_UNSATISFIABLE: 
+      {
+	collect_fail_info(initial_pred_literal_map,  
+			  satcheck,
+			  imp_init_preds);
+	
+	collect_fail_info(final_pred_literal_map,  
+			  satcheck,
+			  imp_final_preds);
+
+        #ifdef DEBUG
+	std::cout <<"Important initial set of predicates \n";
+	print_imp_preds_set(imp_init_preds);
+
+	std::cout <<"Important final set of predicates \n";
+	print_imp_preds_set(imp_final_preds);
+        #endif
+      }
+      break;
+      
+    case propt::P_ERROR:
+      throw "Warning! Error from SAT solver when simulating abstract abstract transition \n";
+      break;
+      
+    default:
+      throw "Unexpected result from SAT solver\n";
+      break;
+    }
+  return true; //transition is spurious
+} 
+
+
+bool simulatort::check_abstract_steps_standard
+(const contextt &context,
+ const concrete_transt &concrete_trans,
+ const abstract_counterexamplet &abstract_counterexample,
+ const predicatest &predicates,
+ abstract_transition_constrainst &abstract_transition_constrains,
+ partitioningt::pred_id_clusterst &refinement_clusters,
+ bool verbose,
+ bool simplify) 
+{
+  bool     result = false;
+  unsigned num_new_clusters = 0;
+
+  for (unsigned i=0; i<abstract_counterexample.size()-1; i++) 
+  {
+    const abstract_statet &start = abstract_counterexample[i];
+    const abstract_statet &end   = abstract_counterexample[i+1];
+
+    if (not_spurious_transitions_cache.find(abstract_transitiont(start,end)) != 
+	not_spurious_transitions_cache.end())
+      {
+	not_spurious_cache_hits++;
+	continue;
+      }
+
+    std::set<unsigned> imp_init_preds, imp_final_preds;
+
+    #ifdef DEBUG
+    std::cout <<"Abstract transition ["<<i <<"]->["<<i+1<<"] \n";
+    #endif
+
+    num_steps_checked++;
+
+
+    bool status =  is_spurious_abstract_transition(
+      context,
+      concrete_trans,
+      abstract_counterexample,
+      predicates,
+      imp_init_preds,
+      imp_final_preds,
+      verbose,
+      simplify,
+      i) ;
+
+    if(status) 
+    {
+      #ifdef DEBUG
+      std::cout <<" is spurious\n";
+      #endif
+      result = true;
+      
+      num_spurious_steps++;
+      
+      abstract_constraintt start_state_constrain;
+      abstract_constraintt end_state_constrain;
+      
+      
+      copy_important_preds(abstract_counterexample[i], 
+                           imp_init_preds,
+                           start_state_constrain);
+      copy_important_preds(abstract_counterexample[i+1],
+                           imp_final_preds,
+                           end_state_constrain);
+      
+      if (generate_refinement_clusters ) 
+      {
+        //Also create a new cluster of important final and initial predicates. This
+        //will hopefully be small and will make the abstraction less coarse.
+        
+        if (!use_gcr_size || (imp_init_preds.size() + imp_final_preds.size() <= max_cluster_size ))
+        {
+          refinement_clusters.insert(std::pair<std::set<unsigned>, std::set<unsigned> >
+                                     (imp_init_preds, imp_final_preds));
+          
+          num_new_clusters++;
+        }
+      }
+     
+      unsigned old_size = abstract_transition_constrains.size();
+      abstract_transition_constrains.insert(
+        std::pair <abstract_constraintt, abstract_constraintt >
+        (start_state_constrain, end_state_constrain));
+
+      unsigned new_size = abstract_transition_constrains.size(); 
+      
+      if (new_size > old_size)
+        num_constraints_found++;
+    }
+    else 
+    {
+      #ifdef DEBUG
+      std::cout <<"NOT spurious\n";
+      #endif
+
+      //      std::cout << "Adding to cache "<<start<< "->"<<end<<"\n";
+
+      std::pair<abstract_transitionst::iterator, bool> at_b = 
+	not_spurious_transitions_cache.insert(abstract_transitiont(start,end));
+	
+      assert (at_b.second);
+    }
+  }
+
+  return result; 
+}
+
+/*******************************************************************\
+
+Function: simulatort::check_spurious_using_simulation_standard
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Does BMC but also takes the predicate values into account.
+          The aim is to make use of unsat cores and identify predicates
+          whose weakest pre-condition needs to be taken.  
+ 
+          Use standard interface for zcore.  
+\*******************************************************************/
+
+void simulatort::check_spurious_using_simulation_standard(
+  const contextt &context,
+  const concrete_transt &concrete_trans,
+  const abstract_counterexamplet &abstract_counterexample,
+  const predicatest &predicates,
+  std::vector<std::set<unsigned> > &imp_preds_per_state,
+  bool add_initial_state,
+  bool verbose,
+  bool simplify) 
+{
+  assert(!abstract_counterexample.empty());
+  assert(add_initial_state);
+
+  satcheck_minisat_coret satcheck;
+  bmc_mapt map;
+  namespacet ns(context);
+ 
+  map.var_map = concrete_trans.var_map;
+
+  map.map_timeframes(satcheck, abstract_counterexample.size());
+
+
+  const transt &trans = concrete_trans.trans_expr;
+  
+  boolbvt boolbv(satcheck);
+  boolbv.set_message_handler(get_message_handler());
+
+
+  //add initial state constrains depending on add_initial_state
+    unwind(trans,
+	   *this,
+	   satcheck, 
+	   map, 
+	   context); 
+
+
+  //now start adding abstract states
+  vector_pred_literal_mappingt mappings;
+
+  for (unsigned i = 0; i < abstract_counterexample.size() ; i++) 
+  {
+    pred_literal_mappingt mapping_i;
+ 
+    #ifdef DEBUG 
+    std::cout <<"Adding abstract state ["<< i <<"] \n";
+    std::cout << abstract_counterexample[i];
+    #endif
+
+    add_abstract_state_map(context, 
+                           abstract_counterexample[i],
+                           predicates,
+                           map, satcheck, simplify, i, 
+                           mapping_i);
+    
+    mappings.push_back(mapping_i);
+  }
+
+  switch(satcheck.prop_solve())
+  {
+  case propt::P_UNSATISFIABLE:
+    break;
+    
+  default:
+    throw "satcheck_zcore returned error";
+  }
+  
+  //Now collect fail info
+  
+  for (unsigned i = 0; i < abstract_counterexample.size() ; i++) 
+  {
+    std::set<unsigned> imp_preds_in_state_i;
+    
+    collect_fail_info(mappings[i],  
+                      satcheck,
+                      imp_preds_in_state_i);
+    
+    #ifdef DEBUG
+    std::cout << "Important predicates in state "<<i<<"\n";
+    print_imp_preds_set(imp_preds_in_state_i);
+    #endif
+
+    imp_preds_per_state.push_back(imp_preds_in_state_i);
+  }
+}
+
+

src/vcegar/simulator.h

@@ -0,0 +1,252 @@
+/*******************************************************************\
+
+Module: Simulator
+
+Author:  Himanshu Jain
+         Daniel Kroening
+         Karen Yorav
+    
+Date: June 2003
+
+Purpose: Simulate an abstract counterexample on the concrete program
+to determmine whether it is spurious.
+
+\*******************************************************************/
+
+#ifndef CPROVER_SIMULATOR_H
+#define CPROVER_SIMULATOR_H
+
+#include <message.h>
+#include <namespace.h>
+#include <cmdline.h>
+
+#include <solvers/sat/cnf.h>
+#include <solvers/sat/satcheck.h>
+
+#include <trans/bmc_map.h>
+#include <trans/var_map.h>
+#include <trans/instantiate.h>
+#include <trans/unwind.h>
+
+#include "concrete_counterexample.h"
+#include "concrete_trans.h"
+#include "abstract_trans.h"
+#include "predicates.h"
+#include "partitioning.h"
+#include "abstract_counterexample.h"
+
+
+class simulatort:public messaget
+ {
+ public:
+  simulatort(message_handlert &_message_handler,
+	     const cmdlinet &_cmdline,
+	     const irep_idt &_module_identifier,
+	     unsigned _num_threads) :
+    messaget(_message_handler),
+    cmdline(_cmdline),
+    module_identifier(_module_identifier),
+    num_threads(_num_threads)
+   {
+
+     //One time initializations
+
+     if(!cmdline.isset("gcr"))
+       generate_refinement_clusters = 0; //default
+     else {
+       generate_refinement_clusters = 1;
+     }
+
+
+     if(!cmdline.isset("gcrsize"))
+       use_gcr_size = 0; //default, useless if --gcr is not present 
+     else 
+       {
+	 use_gcr_size = 1;
+	 max_cluster_size = atoi(cmdline.getval("gcrsize"));
+       }
+
+     if(!cmdline.isset("one_cex_only"))
+       remove_one_cex_only = 0; //default
+     else 
+       remove_one_cex_only = 1;
+    
+     if(!cmdline.isset("run_till_fix"))
+       run_till_fix = 0; //default
+     else 
+       run_till_fix = 1;
+    
+     //stats
+     num_spurious_steps = 0;
+     num_steps_checked = 0;
+     num_constraints_found = 0;
+     not_spurious_cache_hits = 0;
+     
+     if(!cmdline.isset("verbose"))
+       verbose = false; //default
+     else 
+       verbose = true;
+   }
+
+  const cmdlinet &cmdline;
+
+  bool verbose;
+
+  //Use predicates appearing in the proof of unsatisfiability
+  bool generate_refinement_clusters;
+  unsigned max_cluster_size ;
+  bool use_gcr_size;
+
+
+  bool remove_one_cex_only;
+
+  bool run_till_fix;
+
+  void out_stats(std::ostream &out);
+
+
+  bool check_spurious_using_bmc(const contextt &context,
+				const concrete_transt &concrete_trans,
+				const abstract_counterexamplet &abstract_counterexample,
+				const exprt property,
+				concrete_counterexamplet &concrete_counterexample,
+				bool verbose,
+				bool simplify);
+
+  bool check_abstract_steps
+    (const contextt &context,
+     const concrete_transt &concrete_trans,
+     const abstract_counterexamplet &abstract_counterexample,
+     const predicatest &predicates,
+     abstract_transition_constrainst &abstract_transition_constrains,
+     partitioningt::pred_id_clusterst &refinement_clusters,
+     bool verbose,
+     bool simplify); 
+
+   void check_spurious_using_simulation_standard
+     (const contextt &context,
+      const concrete_transt &concrete_trans,
+      const abstract_counterexamplet &abstract_counterexample,
+      const predicatest &predicates,
+      std::vector<std::set<unsigned> > &imp_preds_per_state,
+      bool add_initial_state,
+      bool verbose,
+      bool simplify) ;
+
+
+
+  
+  void generate_constrains
+    (const contextt &context,
+     const concrete_transt &concrete_trans,
+     const predicatest &predicates,
+     const spurious_abstract_stepst &spurious_abstract_steps,
+     abstract_transition_constrainst &abstract_transition_constrains);
+  
+
+  typedef std::map<unsigned, literalt> pred_literal_mappingt;
+  typedef std::map<unsigned, int> pred_dimacsint_mappingt;
+
+  //When simulating a counterexample we wan't to remember the mappings of the
+  //predicates in each state to the corresponding literals in the SAT instance.
+  //Each element in the vector below stores such mapping for some abstract state.
+  typedef std::vector<pred_literal_mappingt> vector_pred_literal_mappingt;
+
+  typedef std::vector<pred_dimacsint_mappingt> vector_pred_dimacsint_mappingt;
+
+
+  bool is_spurious_abstract_transition
+    (const contextt &context,
+     const concrete_transt &concrete_trans,
+     const abstract_counterexamplet &abstract_counterexample,
+     const predicatest &predicates,
+     std::set<unsigned> &imp_init_preds,
+     std::set<unsigned> &imp_final_preds,
+     bool verbose,
+     bool simplify,
+     unsigned stepno) ;
+
+
+   void copy_important_preds(const abstract_statet &abstract_state,
+			     const std::set<unsigned> &imp_preds,
+			     abstract_constraintt &constraint) const;
+
+
+  bool check_abstract_steps_standard
+    (const contextt &context,
+     const concrete_transt &concrete_trans,
+     const abstract_counterexamplet &abstract_counterexample,
+     const predicatest &predicates,
+     abstract_transition_constrainst &abstract_transition_constrains,
+     partitioningt::pred_id_clusterst &refinement_clusters,
+     bool verbose,
+     bool simplify) ;
+  
+   
+protected:
+  struct constraintt
+   {
+    exprt guard, original_guard;
+    irept location;
+    abstract_counterexamplet::const_iterator abstract_step;
+   };
+
+  typedef std::list<constraintt> constraintst;
+  
+  const irep_idt &module_identifier;
+
+  const unsigned num_threads;
+
+  abstract_transitionst not_spurious_transitions_cache;
+
+  //stats
+
+  unsigned num_spurious_steps;
+  unsigned num_steps_checked;
+  unsigned num_constraints_found;
+  unsigned not_spurious_cache_hits;
+
+   void print_pred_literal_mapping
+     (const pred_literal_mappingt &pred_lit_map); 
+
+
+    void create_cluster
+      (const contextt &context,
+       const std::set<unsigned> init_imp_preds,
+       const std::set<unsigned> final_imp_preds,
+       const predicatest &predicates,
+       predicatest &cluster);
+
+  
+  bool add_abstract_state_map_transition(
+    const contextt &context,
+    const abstract_statet &abstract_state,
+    const predicatest &predicates,
+    const bmc_mapt& map,
+    prop_convt &solver,
+    bool simplify,
+    unsigned start,
+    pred_literal_mappingt &pred_literal_mapping) const;
+  
+  void add_abstract_state_map(
+    const contextt &context,
+    const abstract_statet &abstract_state,
+    const predicatest &predicates,
+    const bmc_mapt& map,
+    propt &solver,
+    bool simplify,
+    unsigned start,
+    pred_literal_mappingt &pred_literal_mapping) ;
+
+
+  void copy_state(const abstract_statet &abstract_state, 
+		  abstract_constraintt &constraint);
+  
+
+  void collect_fail_info(const pred_literal_mappingt &pred_literal_map,  
+			 satcheck_minisat_coret &satcheck_zcore, 
+			 std::set<unsigned> &imp_preds) const;
+ 
+ };
+
+#endif

src/vcegar/specification.h

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Properties and Initial preidcates for Predicate Abstraction
+
+Author: Himanshu Jain
+
+\*******************************************************************/
+
+#ifndef CPROVER_VCEGAR_SPEC
+#define CPROVER_VCEGAR_SPEC
+
+#include <expr.h>
+
+class specificationt
+{
+public:
+  std::string property_string;
+  exprt property;
+  std::vector<exprt> preds_from_property;
+};
+  
+#endif

src/vcegar/vcegar.cpp

@@ -0,0 +1,692 @@
+/*******************************************************************\
+
+Module: Main Module 
+
+Author: Himanshu Jain, hjain@cs.cmu.edu
+        Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+/*
+
+VCEGAR
+Counter Example Guided Abstraction Refinement for Verilog
+
+Copyright (C) 2002 Daniel Kroening <kroening@handshake.de>
+
+Purpose: Counter Example Guided Abstraction refinement for Verilog
+
+*/
+
+#include <memory>
+#include <fstream>
+
+#include <str_getline.h>
+#include <i2string.h>
+#include <config.h>
+#include <ui_message.h>
+#include <parseoptions.h>
+#include <namespace.h>
+#include <cnf_simplify.h>
+#include <get_module.h>
+#include <xml.h>
+#include <xml_irep.h>
+
+#include <langapi/languages.h>
+#include <langapi/mode.h>
+#include <langapi/language_ui.h>
+#include <langapi/language_util.h>
+#include <solvers/sat/dimacs_cnf.h>
+#include <solvers/sat/satcheck.h>
+#include <verilog/verilog_language.h>
+#include <verilog/expr2verilog.h>
+
+//General
+#include "vcegar.h"
+#include "discover_predicates.h"
+
+//Related to predicate abstraction
+#include "modelchecker_smv.h"
+#include "simulator.h"
+#include "abstractor.h"
+#include "vcegar_loop.h"
+#include "refiner.h"
+#include "specification.h"
+
+class vcegart:public language_uit
+{
+public:
+  virtual int doit();
+
+  vcegart(const cmdlinet &_cmdline):
+    language_uit("vcegar", _cmdline),
+    cmdline(_cmdline)
+  {
+  }
+
+protected:
+  const cmdlinet &cmdline;
+
+  var_mapt map;
+
+  irep_idt module_identifier;
+  const transt *trans_expr; // transition system expression
+
+  concrete_transt concrete_trans;  
+  specificationt user_provided_spec;
+  optionst options;
+  
+  unsigned max_iterations()
+  {
+    if(cmdline.isset("i"))
+      return atoi(cmdline.getval("i"));
+
+    return 1;    
+  }
+
+  bool get_main();
+
+  unsigned bound;
+
+  void get_properties_from_file();
+  void get_initial_predicates();
+  int pred_abs_init();
+  void get_user_provided_preds();
+
+  modelcheckert *select_modelchecker(
+    const cmdlinet &cmdline,
+    message_handlert &_message_handler);
+
+  std::vector<specificationt> specs;
+  std::vector<exprt> user_provided_preds;
+};
+
+/*******************************************************************\
+
+Function: vcegart::get_main
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool vcegart::get_main()
+{
+  const std::string module=
+    cmdline.isset("module")?cmdline.getval("module"):"main";
+
+  try
+  {
+    const symbolt &symbol=
+      get_module(context, module, get_message_handler());
+
+    trans_expr=&to_trans(symbol.value);
+    module_identifier=symbol.name;
+ 
+    status(std::string("Module identifier is ")+module_identifier.as_string());
+
+    if(cmdline.isset("showtrans"))
+    {
+      transt trans(*trans_expr);
+
+      exprt::operandst &op=trans.operands();
+      
+      std::cout <<"General constrains before follow macros \n"<<op[0]<<"\n";
+      std::cout <<"Initial constrains before follow macros \n"<<op[1]<<"\n";
+      std::cout <<"Transition relation before follow macros \n"<<op[2]<<"\n";
+      std::cout << "Operands.size "<<op.size() << "\n";
+
+      // expand defines (macros)
+      namespacet ns(context);
+      ns.follow_macros(op[0]);
+      ns.follow_macros(op[1]);
+      ns.follow_macros(op[2]);
+
+      std::cout <<"General constrains \n"<<op[0]<<"\n";
+      std::cout <<"Initial constrains \n"<<op[1]<<"\n";
+      std::cout <<"Transition relation \n"<<op[2]<<"\n";
+      std::cout << "Operands.size "<<op.size() << "\n";
+      return 1;
+    }
+  }
+
+  catch(int e)
+  {
+    return true;
+  }
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: vcegart::doit
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: invoke main modules
+
+\*******************************************************************/
+
+int vcegart::doit()
+{
+  if(parse()) return 1;
+
+  status("Parsing done");
+
+  if(cmdline.isset("showparse"))
+  {
+    language_files.show_parse(std::cout);
+    return 0;
+  }
+
+  //
+  // type checking
+  //
+
+  if(typecheck()) return 2;
+
+  status("typechecking done");
+
+  // get module name
+
+  if(get_main()) return 1;
+
+  map.map_vars(context, module_identifier);
+
+  if(cmdline.isset("showvarmap"))
+  {
+    map.output(std::cout);
+    return 0;
+  }
+
+  if(cmdline.isset("showcontext"))
+  {
+    context.show(std::cout);
+    return 0;
+  }
+
+  if(cmdline.isset("p"))
+  {
+    try
+    {
+      get_properties_from_file();
+      get_initial_predicates();
+
+      if(cmdline.isset("pred"))
+        get_user_provided_preds();
+          
+      pred_abs_init();
+    }
+  
+    catch(const char *e)
+    {
+      error(e);
+      return 1;
+    }
+
+    catch(const std::string &e)
+    {
+      error(e);
+      return 1;
+    }
+  }
+  else if(cmdline.isset("claim"))
+  {
+    // get properties from model
+
+    try
+    {
+      unsigned c=atoi(cmdline.getval("claim"));
+      unsigned i=0;
+    
+      forall_symbol_module_map(
+        it,
+        context.symbol_module_map, 
+        module_identifier)
+      {
+        namespacet ns(context);
+        const symbolt &symbol=ns.lookup(it->second);
+
+        if(symbol.theorem)
+        {
+          i++;
+          
+          if(c==i)
+          {
+            std::string string_value=
+              from_expr(ns, symbol.name, symbol.value);
+
+            status("Property: "+string_value);
+
+            specs.push_back(specificationt());
+            specificationt &spec=specs.back();
+            spec.property_string=string_value;
+            spec.property=symbol.value;
+            break;
+          }
+        }
+      }
+      
+      if(specs.empty())
+      {
+        error("Claim number "+i2string(c)+" out of range");
+        return true;
+      }
+
+      get_initial_predicates();
+          
+      if(cmdline.isset("pred"))
+        get_user_provided_preds();
+          
+      pred_abs_init();
+    }
+  
+    catch(const char *e)
+    {
+      error(e);
+      return 1;
+    }
+
+    catch(const std::string &e)
+    {
+      error(e);
+      return 1;
+    }
+  }
+  else
+  {
+    error("Please specify what property to verify");
+    return 1;
+  }
+  
+  return 0;
+}
+
+
+/*******************************************************************\
+
+Function: vcegart::get_initial_predicates
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void vcegart::get_initial_predicates()
+{
+  for(std::vector<specificationt>::iterator it=specs.begin();
+      it!=specs.end();
+      it++)
+  {
+    //For predicate abstraction
+    // calculationg the initial set of predicates.
+
+    int initp;
+    if(!cmdline.isset("init-pred"))
+      initp = 1;
+    else 
+      initp=atoi(cmdline.getval("init-pred"));
+    
+    switch(initp)
+    {
+    case 1:
+      { 
+        std::set<predicatet> predicate_set;
+      
+        int discover;
+        if(!cmdline.isset("discover"))
+          discover = 3;
+        else 
+          discover=atoi(cmdline.getval("discover"));
+  
+        assert(discover==1 || discover==2 || 
+               discover==3 || discover==4);
+
+        bool dummy_isAtomic;
+       
+        discover_predicates(it->property, predicate_set, 3, dummy_isAtomic);
+
+        for(std::set<predicatet>::const_iterator
+            p_it=predicate_set.begin();
+            p_it!=predicate_set.end();
+            p_it++) 
+          it->preds_from_property.push_back(*p_it);
+       
+        if(cmdline.isset("verbose"))
+        {
+          status("Initial set of predicates");
+           
+          int count =0;
+          for(std::set<predicatet>::const_iterator
+              p_it=predicate_set.begin();
+              p_it!=predicate_set.end();
+              p_it++)
+          {
+            count++;
+            status(std::string("[")+i2string(count)+std::string("]")+expr2verilog(*p_it));
+            status("--------------");
+          }
+        }
+        break;
+      }
+      
+    case 2:
+      {
+        status("Using the property itself as the initial predicate");
+
+        exprt init_pred(it->property);
+        it->preds_from_property.push_back(init_pred);
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: vcegart::get_properties_from_file
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void vcegart::get_properties_from_file()
+{
+  std::ifstream infile(cmdline.getval("p"));
+  
+  if(!infile)
+    throw std::string("failed to open ")+cmdline.getval("p");
+  
+  // use auto_ptr because of the exceptions
+  std::auto_ptr<languaget> language(new verilog_languaget);
+  
+  std::string line;
+  namespacet ns(context);
+    
+  while(str_getline(infile, line))
+  {
+    if(line=="") continue;
+    if(line[0]=='#') continue;
+    if(std::string(line, 0, 2)=="//") continue;
+  
+    exprt tmp_expr;
+
+
+    if(language->to_expr(
+         line, module_identifier.as_string(),
+         tmp_expr, get_message_handler(), ns))
+      throw "failed to parse the property";
+
+    exprt expr(tmp_expr);
+
+    if(expr.type().id()!="bool")
+    {
+      std::string type_string;
+      language->from_type(expr.type(), type_string, ns);
+      throw "expected boolean expression as predicate, but got "+type_string;
+    }
+    
+    if(cmdline.isset("verbose"))
+      status(std::string("Added the property: ")+line);
+
+    specificationt spec;
+    spec.property_string = line;
+    spec.property = expr;
+    
+    specs.push_back(spec);
+  }
+  
+  if(cmdline.isset("verbose"))
+    status("Total number of properties added "+i2string(specs.size()));
+}
+
+/*******************************************************************\
+
+Function: vcegart::get_user_provided_preds
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void vcegart::get_user_provided_preds()
+{
+  std::ifstream infile(cmdline.getval("pred"));
+  
+  if(!infile)
+    throw std::string("failed to open ")+cmdline.getval("pred");
+  
+  // use auto_ptr because of the exceptions
+  std::auto_ptr<languaget> language(new verilog_languaget);
+  
+  namespacet ns(context);
+  
+
+  const std::string module=
+    cmdline.isset("module")?cmdline.getval("module"):"main";
+
+  std::string modeule_indentifier;
+  const symbolt &symbol=get_module(context, module, get_message_handler());
+  module_identifier=symbol.name;
+    
+  std::string line;
+  while(str_getline(infile, line))
+  {
+    if(line!="" && line[0]!='#' &&
+       std::string(line, 0, 2)!="//")
+    {
+      exprt expr;
+      
+
+      if(language->to_expr(line, module_identifier.as_string(), expr, get_message_handler(), ns))
+        throw "failed to parse the user provided predicates";
+
+      #if 1
+      std::cout<<"The parsed predicate after conversion\n";
+      std::cout <<expr<<"\n\n";
+      #endif
+
+      if(expr.type().id()!="bool")
+      {
+        std::string type_string;
+        language->from_type(expr.type(), type_string, ns);
+        throw "expected boolean expression as predicate, but got "+type_string;
+      }
+      
+      user_provided_preds.push_back(expr);
+    }
+  }
+
+  status(std::string("Total number of predicates added")+
+         i2string(user_provided_preds.size()));
+   
+  #if 1
+  status("Predicates discovered from the predicate file are");
+   
+  for(unsigned i=0;i<user_provided_preds.size();i++)
+  {
+    status(std::string("[")+i2string(i)+std::string("] ")+expr2verilog(user_provided_preds[i]));
+    status("--------------");
+  }
+  #endif
+}
+
+/*******************************************************************\
+
+Function: select_modelchecker
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+modelcheckert *vcegart::select_modelchecker(
+  const cmdlinet &cmdline,
+  message_handlert &_message_handler)
+{
+  std::string name=
+    cmdline.isset("modelchecker")?
+      cmdline.getval("modelchecker"):"cadencesmv";
+
+  bool verbose = cmdline.isset("verbose");
+  bool claim   = cmdline.isset("claim");
+  bool absref3 = cmdline.isset("absref3");
+
+  if (name=="nusmv")
+    return new modelchecker_smvt(_message_handler,  modelchecker_smvt::NUSMV, verbose, claim, false);
+  else if (name=="cadencesmv")
+    return new modelchecker_smvt(_message_handler,  modelchecker_smvt::CADENCE_SMV, verbose, claim, absref3);
+  else
+    throw "unknown modelchecker: "+name;
+}
+
+/*******************************************************************\
+
+Function: vcegart::pred_abs_init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Starts the predicate abstraction routine.
+
+\*******************************************************************/
+
+int vcegart::pred_abs_init()
+{
+  config.set(cmdline);
+
+  // set the same verbosity for all
+  int verbosity=4;
+
+  if(cmdline.isset("v")) 
+    verbosity = atoi(cmdline.getval("v"));
+  
+
+  //Parsing and typecheking has already been done
+  //Properties have been collected
+  //Initial predicates have been obtained 
+  //So just give these to prepare.  
+  concrete_trans.var_map = map;
+
+  //Currently we doing the abstraction on monolithic
+  //transition relation. So there is only one thread 
+  
+  concrete_trans.trans_expr = *trans_expr;
+
+  //threads to create
+  int num_threads = 1;
+  
+  if (cmdline.isset("num-threads"))
+    {
+      num_threads = atoi(cmdline.getval("num-threads"));
+      
+      if (num_threads <= 0)
+	throw "Expected number of threads to be greater than zero\n";
+    }
+  //For each property start start new predicate abstraction
+
+  for(std::vector<specificationt>::const_iterator 
+      it=specs.begin();
+      it!=specs.end();
+      it++)
+  {
+    user_provided_spec = *it;
+    
+    status("Verififying property: "+it->property_string);
+    
+    try
+    {
+      // The tools we need
+      
+      // finds predicates
+      refinert refiner(get_message_handler(), cmdline);
+      
+      // calculates abstract program
+      abstractort abstractor(get_message_handler(), cmdline);
+      
+      // model checking engine
+      std::auto_ptr<modelcheckert> 
+        modelchecker(select_modelchecker(cmdline, get_message_handler()));      
+      
+      // checks counterexamples
+      simulatort simulator(get_message_handler(), cmdline, module_identifier, num_threads); 
+      
+      //controls various components of abstraction refinement loop
+      vcegar_loopt vcegar_loop(
+        concrete_trans,
+        user_provided_spec,
+        context,
+        abstractor,
+        refiner,
+        *modelchecker,
+        simulator,
+        get_message_handler(), // as a message handler
+        max_iterations(),
+        cmdline,
+        user_provided_preds,
+        get_ui());
+      
+      // set their verbosity -- all the same for now
+      refiner.set_verbosity(verbosity);
+      abstractor.set_verbosity(verbosity);
+      modelchecker->set_verbosity(verbosity);
+      simulator.set_verbosity(verbosity);
+      vcegar_loop.set_verbosity(verbosity);
+      
+      // Get going
+      vcegar_loop.go();
+    }
+    
+    catch(const char *e)
+    {
+      error(e);
+      return 1;
+    }
+    
+    catch(const std::string e)
+    {
+      error(e);
+      return 1;
+    }
+  }
+
+  return 0;
+}
+
+/*******************************************************************\
+
+Function: do_vcegar
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+int do_vcegar(const cmdlinet &cmdline)
+{
+  vcegart vcegar(cmdline);
+
+  return vcegar.doit();
+}

src/vcegar/vcegar.h

@@ -0,0 +1,11 @@
+/*******************************************************************\
+
+Module: CEGAR for Verilog
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <cmdline.h>
+
+int do_vcegar(const cmdlinet &cmdline);

src/vcegar/vcegar_loop.cpp

@@ -0,0 +1,644 @@
+/*******************************************************************\
+
+Module: VCEGAR Loop
+
+Author: Himanshu Jain
+        Daniel Kroening
+
+
+Date: June 2003
+
+\*******************************************************************/
+
+#include <i2string.h>
+#include <iostream>
+#include <time_stopping.h>
+#include <fstream>
+
+#include <xml.h>
+
+#include <smvlang/expr2smv.h>
+
+#include "vcegar_loop.h"
+#include "abstract_expression.h"
+#include "vcegar_util.h"
+#include "partitioning.h"
+
+
+/*******************************************************************\
+
+Function: vcegar_loopt::report_success
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void vcegar_loopt::report_success()
+{
+  status("VERIFICATION SUCCESSFUL");
+
+  switch(ui)
+  {
+  case ui_message_handlert::OLD_GUI:
+    std::cout << "SUCCESS" << std::endl
+              << "Verification successful" << std::endl
+              << ""     << std::endl
+              << ""     << std::endl
+              << ""     << std::endl
+              << ""     << std::endl;
+    break;
+    
+  case ui_message_handlert::PLAIN:
+    break;
+    
+  case ui_message_handlert::XML_UI:
+    {
+      xmlt xml("cprover-status");
+      xml.data="SUCCESS";
+      std::cout << xml;
+      std::cout << std::endl;
+    }
+    break;
+    
+  default:
+    assert(false);
+  }
+}
+
+/*******************************************************************\
+
+Function: ebmc_baset::report_failure
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void vcegar_loopt::report_failure()
+{
+  status("VERIFICATION FAILED");
+
+  switch(ui)
+  {
+  case ui_message_handlert::OLD_GUI:
+    break;
+    
+  case ui_message_handlert::PLAIN:
+    break;
+    
+  case ui_message_handlert::XML_UI:
+    {
+      xmlt xml("cprover-status");
+      xml.data="FAILURE";
+      std::cout << xml;
+      std::cout << std::endl;
+    }
+    break;
+    
+  default:
+    assert(false);
+  }
+}
+
+
+
+/*******************************************************************\
+
+Function: vcegar_loopt::obtain_abstract_property 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Abstracts the property according to the set of available predicates
+
+\*******************************************************************/
+
+void vcegar_loopt::obtain_abstract_property()
+{
+  int initp = 1; //default
+  
+  if(cmdline.isset("init-pred"))
+    initp=atoi(cmdline.getval("init-pred"));
+  
+  assert(initp == 1 || initp ==2);
+
+  exprt property(spec.property);
+
+  switch(initp) 
+    {
+    case 1: 
+	abstract_expression(predicates, property, 1);
+	break;
+    case 2: 
+	abstract_expression(predicates, property, 2);
+	break;
+    default:
+      throw "Illegal value for initp";
+    }
+  
+  abstractor.abstract_trans.abstract_spec.property_string 
+    = spec.property_string;
+
+  
+  if (verbose)
+    status("Property string "+abstractor.abstract_trans.abstract_spec.property_string);
+  
+  
+  abstractor.abstract_trans.abstract_spec.property 
+    = property;
+
+}
+
+/*******************************************************************\
+
+Function: vcegar_loopt::print_stats
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prints stats on succesful/unsuccesful run of VCEGAR
+
+\*******************************************************************/
+
+void vcegar_loopt::print_stats(
+  unsigned iterations, 
+  const fine_timet &start_time,
+  const fine_timet &abs_time,
+  const fine_timet &mc_time,
+  const fine_timet &ref_time) 
+{
+  status("Machine name");
+
+  status("#No. of iterations done: "+i2string(iterations));
+  status("#Max no. of iterations : "+i2string(max_iterations));
+  status("#Total number of predicates needed: "+i2string(predicates.size()));
+  status("#Partitioning technique: "+i2string(abstractor.partitioning_strategy));
+  status("#Total #trans clusters ["+i2string(abstractor.num_trans_clusters)+"] "+
+	 "Max trans cluster size ["+i2string(abstractor.max_trans_cluster_size)+"]");
+  
+  status("#Total time: "+time2string(current_time()-start_time));
+  status("#Abstraction time: "+time2string(abs_time));
+  status("#Abstract model checking time: "+time2string(mc_time));
+  status("#Simulation and Refinement time: "+time2string(ref_time));
+
+  //for LaTeX resuts 
+  status("#BENCH   &"+time2string(current_time()-start_time)+" & "+
+	 time2string(abs_time)+ " & "+time2string(mc_time)+" & "+
+	 time2string(ref_time)+ " & "+i2string(predicates.size())+"/"+
+	 i2string(abstractor.max_trans_cluster_size)+ " & "+i2string(iterations)+
+	 " & "+i2string(iteration_spurious_transition)+"/"+
+	 i2string(iteration_weakest_precondition));
+}
+
+/*******************************************************************\
+
+Function: vcegar_loopt::additional_stats
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void vcegar_loopt::additional_stats(
+  const fine_timet &spurious_trans_time,
+  const fine_timet &bmc_time,
+  const fine_timet &unsat_time,
+  const fine_timet &wp_time) 
+{
+  status("#Breakup of simulation and refinement time:");
+
+  status("#Simulating abstract transition steps: "+time2string(spurious_trans_time));
+  status("#Simulating the counterexample using BMC: "+time2string(bmc_time));
+  status("#Simulating the spurious counterexample for unsat core: "+time2string(unsat_time));
+  status("#Obtaining word level predicates using simplified weakest pre-conditions: "+
+	 time2string(wp_time));
+  abstractor.out_stats(std::cout); 
+  simulator.out_stats(std::cout); 
+  status("#Refinement due to spurious transition: "+i2string(iteration_spurious_transition));
+  status("#Refinement due to weakest pre-conditions: "+i2string(iteration_weakest_precondition)+" and "+
+	 i2string(iteration_weakest_precondition_extra));
+
+
+}
+
+/*******************************************************************\
+
+Function: vcegar_loopt::go
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: execute the VCEGAR loop
+
+\*******************************************************************/
+
+void vcegar_loopt::go()
+{
+  status("*** Starting Verilog CEGAR Loop ***");
+     
+  fine_timet start_time=current_time();
+  fine_timet abs_time=0; //for creating abstraction 
+  fine_timet mc_time=0; //for modelchecking
+  fine_timet ref_time=0; //for simulation and refinement
+
+  fine_timet time_spurious_trans = 0; //time taken when simulating each transition seperately
+  fine_timet time_doing_bmc = 0; //time taken for performing BMC
+  fine_timet time_doing_unsat_core = 0; //time taken when performing unsat core calculation for an 
+                                        //spurious counterexample
+  fine_timet time_doing_wp = 0; //time taken to obtain new predicates
+
+  unsigned old_counterexample_length = 0; //so that we do not do BMC if an abstract 
+                                          //counterexample of same length comes again
+                                          //useful if noconstrain is given
+
+  if (use_siege)
+    throw "Support for --siege option removed\n";
+
+  //check states marked in unsat proof correspond to spurious transitions
+  if(refine1) 
+    throw "--refine1 option no longer supported\n";
+
+  // New code passing network information around.
+  network_infot network(
+    concrete_trans.trans_expr.invar(), 
+    concrete_trans.trans_expr.trans(),
+    concrete_trans.var_map, context);
+
+  if(verbose)
+    status("Network built"); 
+
+  #ifdef DEBUG   
+  network.print_members();
+  network.print_next_state_function_cache();
+  #endif
+
+  // Create initial abstraction
+  if(spec.preds_from_property.empty())
+    throw "No predicates to start the CEGAR loop";
+
+  refiner.init_preds(predicates, spec.preds_from_property);
+
+  if(verbose)
+    std::cout << predicates;
+
+  //Add the user provided predicates if --pred option is given
+  if(cmdline.isset("pred")) 
+  { 
+    refiner.init_preds(predicates, user_provided_preds);
+      
+    if(verbose)
+    {
+      std::cout << "Added the predicates from the predicate file\n";
+      std::cout << predicates;
+    }
+  }
+
+  // Express property in terms of abstract variables
+  obtain_abstract_property();
+
+  unsigned iteration=0;
+  create_abstraction = true;
+
+  concrete_counterexamplet concrete_counterexample;
+
+  while(true) 
+  {
+    if(!unbounded_cegar_iterations && iteration==max_iterations)
+    {
+      error("Try increasing maximum number of iterations");
+      print_mapping();
+      return;
+    }
+      
+    iteration++;
+      
+    assert(unbounded_cegar_iterations || iteration <= max_iterations);
+
+    status("VCEGAR CEGAR Loop Iteration "+i2string(iteration));
+
+    // Abstract
+
+    if(create_abstraction) 
+    {
+      fine_timet abs_start_time=current_time();
+      
+      abstractor.calc_abstraction(
+        predicates,
+        concrete_trans,
+        context, 
+        network,
+        pred_id_clusters);
+
+        abs_time+=current_time()-abs_start_time; 
+    }
+    else 
+    {
+      if(verbose)
+        status("Using newly generated constrains, from abstract counterexample");
+    }
+
+    //abstract counterexample 
+    abstract_counterexamplet abstract_counterexample;
+      
+    // Verify
+    fine_timet mc_start_time=current_time();
+    
+    if(verbose)
+      status("Calling modelchecker\n");
+
+    bool pass =
+      modelchecker.check(
+        abstractor.abstract_trans,
+        abstract_transition_constrains,
+        weakest_precondition_constrains,
+	abstract_initial_constrains,
+        abstract_counterexample);
+      
+    mc_time += current_time() - mc_start_time; 
+
+    if(pass)
+    {
+      //result("VERIFICATION SUCCESSFUL"); 
+      report_success();
+      print_stats(iteration, start_time, abs_time, mc_time, ref_time);
+      additional_stats(time_spurious_trans, time_doing_bmc, 
+                       time_doing_unsat_core,  time_doing_wp);
+      print_mapping();
+      break;
+    }
+
+    // Refine
+
+    fine_timet ref_start_time=current_time();
+
+    bool contains_spurious_abstract_steps = false;
+
+    if(constrain)
+    {
+      spurious_abstract_stepst spurious_abstract_steps;
+
+      fine_timet time_spurious_trans_start=current_time();
+
+
+      if (verbose)
+	status("Calling check abstract steps standard");
+          
+      contains_spurious_abstract_steps = 
+	simulator.check_abstract_steps_standard
+	(context,
+	 concrete_trans,
+	 abstract_counterexample,
+	 predicates,
+	 abstract_transition_constrains,
+	 pred_id_clusters,
+	 verbose,
+	 true);
+
+
+	
+      if(verbose)
+	std::cout << "contains_spurious_abstract_steps "
+		  <<contains_spurious_abstract_steps<< "\n";
+
+      #ifdef DEBUG
+      partitioningt partition_dummy;
+      partition_dummy.print_clusters(pred_id_clusters) ; 
+      #endif
+
+
+      time_spurious_trans += current_time() - time_spurious_trans_start; 
+	   	  	    
+      if (contains_spurious_abstract_steps && !generate_clusters) 
+      {
+	iteration_spurious_transition++;
+        //refine abstract model without adding predicates
+        //we won't create new abstraction.
+        create_abstraction = false;
+      }
+    }
+	  
+    if(!contains_spurious_abstract_steps || !constrain) 
+    {
+      //Simulate the entire abstract counterexample only if each of the invidual
+      //steps are not spurious. (done by check_abstract_steps above)
+      // OR if given noconstrain option.
+
+      fine_timet time_doing_bmc_start = current_time();
+
+      bool is_spurious_using_bmc = true; 
+	      
+
+      if (old_counterexample_length < abstract_counterexample.size())
+      {
+        if (verbose)
+          std::cout << "Checking spurious using BMC for length = "
+                    << abstract_counterexample.size()<<"\n";
+        
+        is_spurious_using_bmc = 
+          simulator.check_spurious_using_bmc(context,
+                                             concrete_trans,
+                                             abstract_counterexample,
+                                             spec.property,
+					     concrete_counterexample,
+                                             verbose,
+                                             true);
+      }
+
+      time_doing_bmc += current_time() - time_doing_bmc_start;
+
+      if(!is_spurious_using_bmc)
+      {
+	//show the counterexample
+	messaget message(get_message_handler());
+	show_trans_trace(concrete_counterexample, 
+			 message,
+			 namespacet(context),
+			 ui);
+
+
+        // counterexample is not spurious. 
+        //result("Property does NOT hold!");
+	report_failure();
+        print_stats(iteration, start_time, abs_time, mc_time, ref_time);
+        
+        additional_stats (time_spurious_trans, time_doing_bmc, 
+                            time_doing_unsat_core,  time_doing_wp);
+        print_mapping();
+        break;
+      }
+
+      // remember that we did bmc-like computation for this length, and found that 
+      //there is no real counterexample of this length
+
+      old_counterexample_length = abstract_counterexample.size();
+
+      // it is spurious, refine by adding predicates
+
+      if(verbose)
+        std::cout <<"Encountered a spurious counterexample\n";
+    
+      std::vector<std::set<unsigned> > imp_preds_per_state;
+
+      //use unsat cores to determine predicates whose
+      // weakest pre-condition needs to be taken
+
+      fine_timet time_doing_unsat_core_start = current_time();
+       
+
+      simulator.check_spurious_using_simulation_standard
+	(context,
+	 concrete_trans,
+	 abstract_counterexample,
+	 predicates,
+	 imp_preds_per_state,
+	 true,
+	 verbose,
+	 true) ; 
+
+
+      time_doing_unsat_core += current_time() - time_doing_unsat_core_start; 
+
+      unsigned num_wp_constraints_before = weakest_precondition_constrains.size();
+      unsigned num_preds_after           = predicates.size();
+      unsigned num_wp_constraints_after  = weakest_precondition_constrains.size();
+      unsigned num_preds_before          = predicates.size();
+      unsigned num_abs_init_constraints  = abstract_initial_constrains.size();
+
+      fine_timet time_doing_wp_start = current_time();
+      num_wp_constraints_before =  weakest_precondition_constrains.size();
+      
+      iteration_weakest_precondition++;
+      
+      if (abstract_counterexample.size() > 1)
+	refiner.spurious_ce(predicates,
+			    concrete_trans,
+			    abstract_counterexample,
+			    context,
+			    spec.property, 
+			    network,
+			    imp_preds_per_state,
+			    weakest_precondition_constrains,
+			    false);
+      else
+	add_initial_state_constrain(abstract_counterexample, 
+				    imp_preds_per_state, 
+				    abstract_initial_constrains);
+
+      num_preds_after = predicates.size();
+      
+      num_wp_constraints_after =  weakest_precondition_constrains.size();
+      
+      time_doing_wp += current_time() - time_doing_wp_start;
+      
+      if((num_preds_after == num_preds_before) && 
+         (num_wp_constraints_after == num_wp_constraints_before) &&
+	 (num_abs_init_constraints == abstract_initial_constrains.size()))
+	{
+	  //try to find more predicates
+	  if (abstract_counterexample.size() > 1)
+	    {
+	      status("Additional predicate generation in iteration "+
+		     i2string(iteration));
+	      refiner.spurious_ce(predicates,
+				  concrete_trans,
+				  abstract_counterexample,
+				  context,
+				  spec.property, 
+				  network,
+				  imp_preds_per_state,
+				  weakest_precondition_constrains,
+				  true);
+	      iteration_weakest_precondition_extra++;
+	    }
+	  
+	  if (predicates.size() > num_preds_before)
+	    create_abstraction = true;
+	  else
+	    {
+	      status("No new predicates/ wp constraints  discovered from refinement in iteration no. "+
+		     i2string(iteration));
+	      throw "Reached a no difference state \n";
+	    }
+	}
+      else 
+	create_abstraction = true;
+    }
+
+    ref_time += current_time() - ref_start_time; 
+
+    if(cmdline.isset("more-stats")) 
+    { 
+      print_stats(iteration, start_time, abs_time, mc_time, ref_time);
+
+      additional_stats (time_spurious_trans, time_doing_bmc, 
+                        time_doing_unsat_core,  time_doing_wp);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: vcegar_loopt::add_initial_state_constrain
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void vcegar_loopt::add_initial_state_constrain(const abstract_counterexamplet &spurious_counterexample,
+					       const std::vector<std::set<unsigned> > &imp_preds_per_state,
+					       abstract_initial_constrainst &abstract_initial_constrains)
+{
+  assert(spurious_counterexample.size() == 1);
+  assert(imp_preds_per_state.size() == 1);
+
+  if (imp_preds_per_state[0].empty())
+    return;
+
+  const std::set<unsigned> &imp_ipreds = imp_preds_per_state[0];
+  abstract_constraintt new_constrain;
+
+  simulator.copy_important_preds(spurious_counterexample[0], imp_ipreds, new_constrain);
+
+  abstract_initial_constrains.insert(new_constrain);
+}
+
+
+
+/*******************************************************************\
+
+Function: vcegar_loopt::print_mapping
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: prints predicates and boolean vars mapping
+
+\*******************************************************************/
+
+void vcegar_loopt::print_mapping()
+{
+  if (cmdline.isset("mapping"))
+  {
+    std::ofstream mapfile("vcegar.map");
+    if(mapfile)
+      mapfile << predicates;
+  }
+}

src/vcegar/vcegar_loop.h

@@ -0,0 +1,176 @@
+/*******************************************************************\
+
+Module: VCEGAR Loop
+
+Author: Himanshu Jain, Daniel Kroening
+
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_VCEGAR_LOOP_H
+#define CPROVER_VCEGAR_LOOP_H
+
+#include <set>
+
+#include <message.h>
+#include <langapi/language_ui.h>
+
+#include <expr_util.h>
+#include <time_stopping.h>
+
+#include "concrete_trans.h" 
+#include "modelchecker.h" 
+#include "simulator.h" 
+#include "abstractor.h" 
+#include "refiner.h" 
+#include "specification.h"
+#include "network_info.h"
+
+/* This class implements the VCEGAR loop, given the proper tools */
+
+class vcegar_loopt: public messaget
+ {
+ public:
+  vcegar_loopt(
+    concrete_transt &_concrete_trans, 
+    const specificationt &_spec,
+    const contextt &_context,
+    abstractort &_abstractor,
+    refinert &_refiner,
+    modelcheckert &_modelchecker,
+    simulatort &_simulator,
+    message_handlert &_message_handler,
+    unsigned _max_iterations,
+    const cmdlinet &_cmdline,
+    const std::vector<exprt> &_user_provided_preds,
+    ui_message_handlert::uit _ui):
+    messaget(_message_handler),
+    concrete_trans(_concrete_trans),
+    spec(_spec),
+    context(_context),
+    abstractor(_abstractor),
+    refiner(_refiner),
+    modelchecker(_modelchecker),
+    simulator(_simulator),
+    max_iterations(_max_iterations),
+    cmdline(_cmdline),
+    user_provided_preds(_user_provided_preds),
+    ui(_ui)
+   {
+     
+     if(!cmdline.isset("noconstrain"))
+       constrain = 1; //default
+     else
+       constrain = 0;
+     
+     if(!cmdline.isset("refine1"))
+       {
+	 refine1 = 0; //default
+       }
+     else
+       {
+	 refine1 = 1;
+	 constrain = 0;
+       }
+
+     if(!cmdline.isset("gcr"))
+       {
+	 generate_clusters = 0; //default
+       }
+     else
+       {
+	 generate_clusters = 1;
+       }
+     
+     if(cmdline.isset("siege"))
+       use_siege = 1; 
+     else
+       use_siege = 0; //default
+
+     if(cmdline.isset("i"))
+       unbounded_cegar_iterations = false; 
+     else
+       unbounded_cegar_iterations = true; //default
+     
+     if (cmdline.isset("verbose"))
+       verbose = true;
+     else
+       verbose = false;
+
+
+
+     iteration_spurious_transition=0;
+     iteration_weakest_precondition=0;
+     iteration_weakest_precondition_extra=0;
+   }
+
+  void go();
+
+ private:  
+  void obtain_abstract_property();
+  void print_stats(unsigned iterations,
+		   const fine_timet&, 
+		   const fine_timet&, 
+		   const fine_timet&, 
+		   const fine_timet&);
+
+  void additional_stats(const fine_timet &spurious_trans_time,
+			const fine_timet &bmc_time,
+			const fine_timet &unsat_time,
+			const fine_timet &wp_time); 
+    
+
+  void copy_clusters(const partitioningt::predicate_clusterst 
+				   &refine_clusters); 
+  
+  void run_experimental_code();
+
+  void print_mapping();
+
+  void report_success();
+  void report_failure();
+
+  void add_initial_state_constrain(const abstract_counterexamplet &spurious_counterexample,
+				   const std::vector<std::set<unsigned> > &imp_preds_per_state,
+				   abstract_initial_constrainst &abstract_initial_constrains);
+
+  concrete_transt &concrete_trans;
+  const specificationt &spec;
+  const contextt &context;
+  abstractort &abstractor;
+  refinert &refiner;
+  modelcheckert &modelchecker;
+  simulatort &simulator;
+
+  //clusters (of predicate id) obtained by refinement
+  partitioningt::pred_id_clusterst pred_id_clusters;
+
+  abstract_transition_constrainst  abstract_transition_constrains; 
+  weakest_precondition_constrainst weakest_precondition_constrains; 
+  abstract_initial_constrainst     abstract_initial_constrains;
+
+  unsigned max_iterations;
+  predicatest predicates;  
+  const cmdlinet &cmdline;
+  bool constrain;
+  bool refine1; //use unsat core to check spurious transitions or take weakest pre-conditions
+  bool create_abstraction;
+  std::vector<exprt> user_provided_preds;
+  bool generate_clusters; //generate clusters from refinement 
+  bool use_siege; //use siege SAT solver
+  bool unbounded_cegar_iterations;
+  bool verbose;
+  ui_message_handlert::uit ui;
+
+  unsigned iteration_spurious_transition;
+  unsigned iteration_weakest_precondition;
+  unsigned iteration_weakest_precondition_extra;  
+ };
+
+#endif
+
+
+
+

src/vcegar/vcegar_util.cpp

@@ -0,0 +1,340 @@
+/*******************************************************************\
+
+Module: Utilities for VCEGAR
+
+Author: Himanshu Jain
+
+Date: April 2004
+
+\*******************************************************************/
+
+#include <assert.h>
+
+#include <map>
+#include <vector>
+#include <i2string.h>
+#include <verilog/expr2verilog.h>
+#include <namespace.h>
+
+#include "vcegar_util.h"
+#include "canonicalize.h"
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+std::ostream& operator<< (std::ostream& out,
+			  const std::set<unsigned> &uiset) 
+{
+
+  for(std::set<unsigned>::const_iterator it= uiset.begin(); it != uiset.end(); it++) {
+    out <<*it<<" ";
+  }
+  out <<"\n";
+
+  return out;
+}
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+std::ostream& operator<< (std::ostream& out,
+			  const literalt &lit)
+{
+  out <<lit.sign()<<"["<<lit.var_no()<<"] \n";
+  return out;
+}
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: return the maximum element of a set containing unsigned.
+
+\*******************************************************************/
+
+unsigned max (const std::set<unsigned> &uiset)
+{
+  unsigned max = 0;
+
+  for(std::set<unsigned>::const_iterator it= uiset.begin(); it != uiset.end(); it++) {
+    if (*it > max)
+      max = *it;
+  }
+
+  return max;
+}
+
+
+/*******************************************************************\
+
+Function: rename
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Renames a current state predicate to a next state predicate
+
+\*******************************************************************/
+
+void rename(exprt &expr)
+ {
+   if(expr.has_operands())
+     Forall_operands(it, expr)
+       rename(*it);
+   
+   if(expr.id()=="symbol")
+     {
+       expr.id("next_symbol");
+     }
+ }
+
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void containsSymbolRecur (const exprt &expr, bool &result)
+{
+  if(expr.has_operands())
+    forall_operands(it, expr)
+      containsSymbolRecur(*it, result);
+  
+  if(expr.id()=="symbol")
+    {
+      result = true;
+    }
+}
+
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Returns true if the given expr contains some variable
+          i.e., a register, input etc. Otherwise, returns false.
+          For example, it should return false for weird predicate
+         line 0[1].
+\*******************************************************************/
+
+bool containsSymbol (const exprt &expr)
+{
+  bool result  = false;
+
+  containsSymbolRecur (expr, result);
+  
+  return result;
+}
+
+
+
+/*******************************************************************\
+
+Function: get_next_state_function
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void get_next_state_function
+(std::string name, //Should be a latch
+ const exprt &trans_rel, //op[2] will be just fine. 
+ exprt& definition)
+{  
+  if (!trans_rel.has_operands()) return;
+
+
+  if (trans_rel.id()=="if") { 
+    return; //we don't expect to obtain definitions inside if statements
+  }
+
+  if(trans_rel.id()=="=")
+    {
+      exprt t1= (trans_rel.operands())[0];
+      exprt t2= (trans_rel.operands())[1];
+      
+      if (t1.id()== "next_symbol") {
+	if (t1.find("identifier").id() == name) {
+	  exprt prop(t2); 
+	  definition = prop;
+	  //definition = t2;
+	  return;
+	}   
+      }
+    }
+  
+  if(trans_rel.has_operands())
+    forall_operands(it, trans_rel)
+      get_next_state_function(name, *it, definition);
+}
+
+
+
+/*******************************************************************\
+
+Function: find_symbols
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+void find_symbols(
+  const exprt &predicate, 
+  std::set<std::string> &symbols, 
+  const std::string name)
+{
+  if(predicate.has_operands())
+    forall_operands(it, predicate)
+      find_symbols(*it, symbols, name);
+  
+
+  if(predicate.id()== name)
+    symbols.insert(predicate.get("identifier").as_string());
+}
+
+
+/*******************************************************************\
+
+Function: 
+
+Inputs: subset (A, B)
+
+Outputs:
+
+Purpose: returns true if A is a subset of B,  false otherwise.
+
+
+\*******************************************************************/
+
+bool subset(
+  const std::set<std::string>& set1,
+  const std::set<std::string>& set2) 
+{
+  for (std::set<std::string>::const_iterator it1= set1.begin();
+       it1 != set1.end(); it1++){
+    std::set<std::string>::const_iterator it2 = set2.find(*it1);
+    if (it2 == set2.end()){
+      return false;
+    }
+  }
+  return true;
+}
+
+
+/*******************************************************************\
+Function: get_type_as_integer
+
+ Inputs:
+
+ Outputs:
+
+ Purpose: Old vcegar code assumed that get_type returns an integer
+          but this is no longer the case. So this routine uses
+          get_type to get an enum and then converts it to integer.
+
+          just casting enum returned by get_type to integer wont' be
+          good  as the order to WIRE and MACRO in vartypet has changed.
+\*******************************************************************/
+
+int get_type_integer(const var_mapt &vmap, const std::string &s)
+{
+  switch (vmap.get_type(s))
+    {
+    case var_mapt::vart::VAR_LATCH: return 1;
+    case var_mapt::vart::VAR_INPUT: return 2; 
+    case var_mapt::vart::VAR_WIRE:  return 3;
+    default: return -1;
+    }
+}
+
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+std::ostream& operator<< (std::ostream& out,
+			  const std::vector<std::set<unsigned> > &vec_vec_unsigned)
+{
+  int count = 0;
+  for (std::vector<std::set<unsigned> >::const_iterator 
+	 it =  vec_vec_unsigned.begin(); 
+       it != vec_vec_unsigned.end(); it++)
+    {
+      out << "State "<<count <<":";
+      out <<*it ;
+      count++;
+    }
+
+  return out;
+}
+
+
+/*******************************************************************\
+
+Function: 
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: 
+
+\*******************************************************************/
+
+std::string double2string(const double& x)
+{
+  std::ostringstream o;
+  if (!(o << x)) 
+    throw "ERROR: when converting double to string";
+  return o.str();
+}

src/vcegar/vcegar_util.h

@@ -0,0 +1,120 @@
+/*******************************************************************\
+
+Module: Utilities for VCEGAR
+
+Author: Himanshu Jain
+
+Date: June 2003
+
+\*******************************************************************/
+
+#ifndef CPROVER_VCEGAR_UTIL_H
+#define CPROVER_VCEGAR_UTIL_H
+
+#include <sstream>
+
+#include <message.h>
+#include <context.h>
+#include <expr.h>
+
+#include <verilog/expr2verilog.h>
+#include <trans/var_map.h>
+
+#include "concrete_trans.h"
+#include "abstract_trans.h"
+#include "predicates.h"
+
+typedef std::map<const std::string, exprt> next_state_function_cachet;
+typedef std::map<const std::string, exprt> symbol_function_tablet;
+
+
+void rename (exprt& current_pred);
+  
+std::ostream& operator<< (std::ostream& out,
+			  const std::set<unsigned> &uint_set);
+
+std::ostream& operator<< (std::ostream& out,
+			  const literalt &lit);
+
+
+unsigned max (const std::set<unsigned> &uint_set);
+
+
+bool containsSymbol (const exprt &expr);
+
+
+void get_next_state_function(
+  std::string name, 
+  const exprt &trans_rel, 
+  exprt &definition);
+   
+void search_wire(
+  std::string name,
+  const exprt &trans_rel,
+  exprt& definition,
+  const var_mapt &var_map);
+    
+void search_input(
+  std::string name, 
+  const exprt &trans_rel,
+  exprt& definition);
+ 
+void replace_outputs(
+  exprt& property,
+  const exprt &general_constrains,
+  const var_mapt &var_map);
+   
+void find_symbols(
+  const exprt &predicate, 
+  std::set<std::string>& symbols, 
+  const std::string name);
+
+bool subset
+(const std::set<std::string>& set1,
+ const std::set<std::string>& set2
+ ) ;
+
+
+void preds_from_case_assignments
+(const exprt function, 
+ const exprt variable_expr,
+ std::set<exprt>& predicates
+ );
+
+
+void wp_with_predicates
+(exprt& property,
+ const exprt &trans_rel,
+ const var_mapt &var_map,
+ std::set<exprt> &predicates
+ );
+  
+void simplify_expr (exprt& expr);    
+
+void weakest_precondition
+(exprt& property,
+ const next_state_function_cachet& next_state_function_cache
+ );
+
+void weakest_precondition
+(exprt& property,
+ const exprt &trans_rel,
+ const var_mapt &var_map);
+
+void compute_pre_symbols 
+(const std::set<std::string> &symbols,
+ const exprt &trans_rel,
+ const var_mapt& var_map,
+ next_state_function_cachet &next_state_function_cache,
+ symbol_function_tablet &symbol_function_table,
+ std::set<std::string> &pre_symbols
+ );
+
+int get_type_integer(const var_mapt &vmap, const std::string &s);
+
+std::ostream& operator<< (std::ostream& out,
+			  const std::vector<std::set<unsigned> > &vec_vec_unsigned);
+
+std::string double2string(const double& x);
+
+#endif