vc_api.h

Go to the documentation of this file.

#ifndef SVC_API_impl_h
#define SVC_API_impl_h

#include "SVC_API.h"
#include "Atomifier.h"
#include "CNF_Converter.h"
#include "SAT_API.h"
#include "compat_hash_map.h"

namespace CVCL {

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: SVC_API                                                            //
// Description: This class provides an external interface to SVC for SAT.    //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////
class SVC_API_impl : public SVC_API {
protected:
  Expr_Manager *_pem;
  Prop_Var_Manager* _ppvm;
  std::hash_map<int, std::vector<Expr>*> *_pfanout_table;
  std::vector<Expr> _vecMap;
  std::vector<Expr> _connectQueue;
  std::vector<Expr> _conditions;
  std::vector<int> _conditionVars;
  std::vector<int> _conditionIndex;
  std::vector<Expr> _assumptionStack;
  std::vector<int> _assumptionIndex;
  int _verbosity;

  PAtomifier _patomifier;
  CNF_Formula_For_Exprs *_cnfFormula;
  CNF_Converter *_cnfConverter;
  PSAT_API _psatapi;
  bool _ready;

  class varinfo {
  public:
    int kind;
    std::vector<int> fanins;
    std::vector<int> fanouts;
    int value;
    int next;
    int prev;
    varinfo() : kind(-1), value(-1), next(0), prev(0) {}
  };

  std::vector<varinfo> _vars;
  int _splitterCacheTag;
  int _splitterCacheTag2;

  bool AddConditions(long lVar);
  void UpdateValue(long v, int value);
  bool FindSplitterRec(long v, int value, long *pv);
  bool GetImplicationsRec(long v, long *pv, int *pvalue);
  bool IsStable() { return _nonassertable_facts->Done(); }

public:
  SVC_API_impl(Expr_Manager *pem);
  ~SVC_API_impl();
  bool CheckSat(const Expr &e);

  void Push();
  void Pop();
  bool SVCAssert(long lVar);
  bool SVCDeny(long lVar);
  bool GetConfClause(std::vector<int>* literals);
  bool IsConsistent();

  bool HasSVCExpr(long lVar);
  bool OKToSplit(long lVar);
  void ResetVariable(long v);

  void Connect(const Expr& e, long v);
  void Connect1(const Expr& eFrom, const Expr& eTo);

  bool FindSplitter(long *v);
  void GetImplications(long *pv, int *pvalue);

  void SetVerbosity(int i) { _verbosity = i; _patomifier->SetVerbosity(i); }
  int Verbosity() { return _verbosity; }
  void PrintVar(long lVar);
  void PrintWithType(const Expr& e);
  void Reset(void);
  bool Ready(void);

  PSAT_API SatAPI() { return _psatapi; }
  std::vector<Expr>& VecMap() { return _vecMap; }
};

}

#endif

---