#ifdef FPROTO_ap
    int indexof(T x);
    void remove_adj_dups();
    void dealloc();
    ap<T> dup();
#endif
#ifdef FPROTO_garr
    int realloc_grow(int DemandSize);
    void realloc_shrink(int NewSize=-1);
    T* AppendBlank();
    void extend(garr<T> items);
    void extend(ap<T> items);
    void dealloc();
    garr<T> dup();
    int indexof(T x, int start=0);
    T RemoveAndFill(int ix);
    T PopLast();
    void RemoveVal_AndFill(T val);
    garr<T> dup_shuffle();
    garr<T> dup_apply(T (*fn)(T));
    void apply(T (*fn)(T));
    void stl_sort();
    void remove_adj_dups();
    void remove_value(int badval);
#endif
#ifdef FPROTO_ap
    void remove_value(int badval);
#endif
#ifdef FPROTO_garr
    T find_median_destructively();
#endif
#ifdef FPROTO_GsT
    void init();
    vector<LitT>* AsLitVec();
#endif
#ifdef FPROTO_ChlitListT
    void append(int lit);
    int pop();
    int last();
    void dump();
#endif
#ifdef FPROTO_AsgnT
    GsT* GetDepByLit(int lit);
    void SetDepByLit(int lit, GsT* pDepGs);
    void ResetDepByLit(int lit, bool KeepDepLocked);
    void init();
    void PrintFormula(char const* outname);
    void PrintFormulaQdimacs(char const* outname);
    bool HasMoreVars();
    int CegarExtend(garri AsgnLits, map<LitT,LitT>* hit, int ElimQb);
    garr<signed char>* GetMonoLits();
    int Restrict(int glit, map<LitT,LitT>* hit, int ElimQb);
    GsT* Augment(int glit, garri AsgnLits, map<LitT,LitT>* hit, int ElimQb);
    int NewConj(int OrigGate, garri args);
    int GenNewVar(int orig, int align=2);
#endif
#ifdef FPROTO_GsT
    int GetWinner();
    int HasBlockedImps();
    ap<LitT>* GetWinrLits(int winr);
#endif
#ifdef FPROTO_AsgnT
    int GetUpstreamMissingLit(int ForcedLit, GsT* pCurLs);
    int GetUpstreamMissingLitAp(int flit, ap<int> LitList);
    int GetFirstFreeLit(ap<int>& LitList);
#endif
#ifdef FPROTO_GsT
    int HasAllWatchedTrigs();
    int TrigRipe();
    int Is_ExactlyOne_LosrLit_Free();
    void InitTrigLits(ap<int> args);
    int PrintIndex();
    void RegisterLitsHave();
    void dealloc();
    bool is_subsumed_by(GsT* pOther);
    void bump_activity();
    FullStratT* get_strat();
    Fmla* get_strat_as_list_fmla();
    void set_strat(FullStratT* strat);
    void dump_strat();
#endif
#ifdef FPROTO_AsgnT
    void bump_var_act(LitT var);
    void InsertVarActOrder(LitT var);
    inline int GetWinner();
    void cut_clause_act();
    void cut_var_act();
    void cut_lit_hit();
    void cla_decay_activity();
    void var_decay_activity();
    double get_median_clause_adj_activity();
    void delete_excess_learned_clauses();
#endif
#ifdef FPROTO_GsT
    void dump();
    void DumpBrief();
    void DumpRaw();
#endif
#ifdef FPROTO_AsgnT
    int ChlitByDL(int dl);
    int QbFromDL(int dl);
    int QtypeFromDL(int dl);
    int GlitToMinChrono(int lit, int ply);
    void AddPendingLs(GsT* pCurLs, int score);
    AntecedT PopFirstPendingLs(int flag);
    bool HasPendingForced();
    int HasConflict();
    inline void FastFixWatch(GsT* pCurLs, int OldLit);
    void SimpFixWatch(GsT* pCurLs);
    void FixWatchedRes(GsT* pCurLs);
    void EraseWatchedLits(GsT* pCurLs);
    int PickNewResWatch(GsT* pCurLs);
    void ChangeWatchedFut(GsT* pCurLs, int NewFut);
    int Backtrack(bool KeepDepsLocked=false);
    void AddUndoLit(int chlit, int flit);
    garri& GetCurUndoList();
    void AppendChlit(int NewChlit, bool IsRedo=false);
    void AppendForcedLit(int lit, GsT* pRef);
    void RandomizePolPref();
    int ChooseRandLit(int preferred, bool NoExpu=false);
    void DumpCurUndo();
    void dump(int GatesToo);
    void dump();
    void DumpChlits();
    void DumpLits(int narf);
    void DumpAsgn();
    void DumpQuantPfx();
    void restart();
    void clean_up_sequents();
    void WatchSanityChk1(GsT* pCurLs);
    void WatchSanityChk3();
    void LatentExecsChk();
    short ReEval(int v);
    int ExecLitSet(GsT* pCurLs, int mode);
    int ExecForced(GsT* pCurLs, int mode);
    void SchedForProp(int CurLit);
    int Propagate();
#endif
#ifdef FPROTO_TrigHeapT
    void dump(const char* end);
#endif
#ifdef FPROTO_GsBuilder
    void CopyTrigsTo(garri& TrigLits);
#endif
#ifdef FPROTO_AsgnT
    bool HasUIP(GsBuilder& gb);
    int GetChronoLastLit(ap<int> Lits);
    int GetChronoLastTwoLits(ap<int> Lits, int* p2nd);
    void PrintDischargeMsg(int CurLit, GsT* pCurLs);
    void Resolve(GsBuilder& gb, int CurLit);
    GsT* MakeLearnedGs();
    inline bool IsRedundantBySeq(int CurLit, GsBuilder& gb, GsT* pDepLs, int mode);
    bool IsRedundant(int CurLit, GsBuilder& gb, int mode);
    void MinimizeConflict(GsBuilder& gb, garri& TrigLits);
#endif
#ifdef FPROTO_GsT
    void InitWatchedLitsPart1();
#endif
#ifdef FPROTO_AsgnT
    GsT* CreateGsFromGb(GsBuilder& gb);
    void AssignLrnId(GsT* pCurLs);
    void AddNewLitSet(GsT* pCurLs);
    void PrintNewLitSet(GsT* pCurLs, const char* extra, int DeltaBT);
    GsT* LearnAndBacktrack(int GotTwo);
    void PreSolve();
    int choose_lit_and_prop(int choice);
    GsT* solve();
    void NewDefnGsAlt(LitT ixExpr, garri args);
    GsT* NewLrnGs_Top(LitT top, int winr);
    GsT* NewLrnGs_Mixed(garri AsgnLits, int winr);
    GsT* NewLrnGs(garri args, garri WinrLits, FmlaT winr);
    void PrintStats();
#endif
