/*****************************************************************************/
/*!
* \file vcl.h
* \brief Main implementation of ValidityChecker for CVC lite.
*
* Author: Clark Barrett
*
* Created: Wed Dec 11 14:40:39 2002
*
* <hr>
* Copyright (C) 2003 by the Board of Trustees of Leland Stanford
* Junior University and by New York University.
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.  In particular:
*
* - The above copyright notice and this permission notice must appear
* in all copies of the software and related documentation.
*
* - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
* EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
*
* <hr>
*
*/
/*****************************************************************************/

#ifndef _cvcl__include__vcl_h_
#define _cvcl__include__vcl_h_

#include <vector>
#include <set>
#include <map>
#include <queue>
#include "vc.h"
#include "command_line_flags.h"
#include "statistics.h"
#include "theorem.h"
#include "cdmap.h"
#include "compat_hash_map.h"
#include <fstream>

namespace CVCL {

class ContextManager;
class TheoremManager;
class VariableManager;
class SearchEngine;
class Theory;
class TheoryCore;
class TheoryUF;
class TheoryArith;
class TheoryArray;
class TheoryQuant;
class TheoryRecords;
class TheorySimulate;
class TheoryBitvector;
class TheoryDatatype;
class CNF;

struct ltstr{
bool operator()(const std::string& s1, const std::string& s2) const{
return s1.compare(s2) < 0;
}
};

typedef std::map<const std::string, Expr, ltstr> Str_To_Expr;

class VCL : public ValidityChecker {
ExprManager* d_em;
ContextManager* d_cm;
TheoremManager* d_tm;
SearchEngine* d_se;
//! Pointers to theories
TheoryCore* d_theoryCore;
TheoryUF* d_theoryUF;
TheoryArith* d_theoryArith;
TheoryArray* d_theoryArray;
TheoryQuant* d_theoryQuant;
TheoryRecords* d_theoryRecords;
TheorySimulate* d_theorySimulate;
TheoryBitvector* d_theoryBitvector;
TheoryDatatype* d_theoryDatatype;
//! All theories are stored in this common vector
/*! This includes TheoryCore and TheoryArith. */
std::vector<Theory*> d_theories;
//! Command line flags
CLFlags *d_flags;
//! User-level view of the scope stack
std::vector<int> d_scopeStack;
//! What's that??
Str_To_Expr d_vars;
//! Run-time statistics
Statistics d_statistics;
//! Structure to hold user assertions indexed by declaration order
class UserAssertion {
size_t d_idx;
static size_t s_nextIdx;
Theorem d_thm; //! The theorem of the assertion (axiom a |- a)
Theorem d_tcc; //! The proof of its TCC
public:
//! Default constructor
UserAssertion() { }
//! Constructor
UserAssertion(const Theorem& thm, const Theorem& tcc)
: d_idx(s_nextIdx++), d_thm(thm), d_tcc(tcc) { }
//! Fetching a Theorem
const Theorem& thm() const { return d_thm; }
//! Fetching a TCC
const Theorem& tcc() const { return d_tcc; }
//! Auto-conversion to Theorem
operator Theorem() { return d_thm; }
//! Comparison for use in std::map, to sort in declaration order
friend bool operator<(const UserAssertion& a1, const UserAssertion& a2) {
return (a1.d_idx < a2.d_idx);
}
};
//! Backtracking map of user assertions
CDMap<Expr,UserAssertion>* d_userAssertions;
//! Result of the last query()
/*! Saved for printing assumptions and proofs.  Normally it is
* Theorem3, but query() on a TCC returns a 2-valued Theorem. */
Theorem3 d_lastQuery;
//! Result of the last query(e, true) (for a TCC).
Theorem d_lastQueryTCC;
//! Closure of the last query(e): |- Gamma => e
Theorem3 d_lastClosure;

// Private methods

//! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi"
Theorem3 deriveClosure(const Theorem3& thm);

//! Recursive assumption graph traversal to find user assumptions
/*!
*  If an assumption has a TCC, traverse the proof of TCC and add its
*  assumptions to the set recursively.
*/
void getAssumptionsRec(const Theorem& thm,
std::set<UserAssertion>& assumptions,
bool addTCCs);
//! Get set of user assertions from the set of assumptions
void getAssumptions(const Assumptions& a, std::vector<Expr>& assumptions);

//! The log file for top-level API calls in the CVCL input language
std::ofstream d_osdump,d_osdumpTranslate;
std::ifstream d_tmpFile;
bool d_translate;

// CNF* d_cnf;

public:
// Takes the vector of command line flags.
VCL(const CLFlags& flags);
~VCL();

// Implementation of vc.h virtual functions
Type boolType();
Type realType();
Type intType();
Type subrangeType(const Expr& l, const Expr& r);
Type subtypeType(const Expr& pred);
Type tupleType(const Type& type0, const Type& type1);
Type tupleType(const Type& type0, const Type& type1, const Type& type2);
Type tupleType(const std::vector<Type>& types);
Type recordType(const std::string& field, const Type& type);
Type recordType(const std::string& field0, const Type& type0,
const std::string& field1, const Type& type1);
Type recordType(const std::string& field0, const Type& type0,
const std::string& field1, const Type& type1,
const std::string& field2, const Type& type2);
Type recordType(const std::vector<std::string>& fields,
const std::vector<Type>& types);
Type dataType(const std::string& constructor,
const std::vector<std::string>& selectors,
const std::vector<Type>& types);
Type dataType(const std::vector<std::string>& constructors,
const std::vector<std::vector<std::string> >& selectors,
const std::vector<std::vector<Type> >& types);
Type arrayType(const Type& typeIndex, const Type& typeData);
Type funType(const Type& typeDom, const Type& typeRan);
Type funType(const std::vector<Type>& typeDom, const Type& typeRan);
Type createType(const std::string& typeName);
Type createType(const std::string& typeName, const Type& def);
Type lookupType(const std::string& typeName);
Expr varExpr(const std::string& name, const Type& type);
Expr varExpr(const std::string& name, const Type& type, const Expr& def);
Expr boundVarExpr(const std::string& name, const std::string& uid,
const Type& type);
Expr lookupVar(const std::string& name, Type* type);
Type getType(const Expr& e);
Expr getTypePred(const Type&t, const Expr& e);
Type getBaseType(const Expr& e);
Type getBaseType(const Type& e);
Expr importExpr(const Expr& e);
Type importType(const Type& t);
Expr eqExpr(const Expr& child0, const Expr& child1);
Expr trueExpr();
Expr falseExpr();
Expr notExpr(const Expr& child);
Expr andExpr(const Expr& left, const Expr& right);
Expr andExpr(const std::vector<Expr>& children);
Expr orExpr(const Expr& left, const Expr& right);
Expr orExpr(const std::vector<Expr>& children);
Expr impliesExpr(const Expr& hyp, const Expr& conc);
Expr iffExpr(const Expr& left, const Expr& right);
Expr iteExpr(const Expr& ifpart, const Expr& thenpart, const Expr& elsepart);
Expr ratExpr(int n, int d);
Expr ratExpr(const std::string& n, const std::string& d, int base);
Expr ratExpr(const std::string& n, int base);
Expr uminusExpr(const Expr& child);
Expr plusExpr(const Expr& left, const Expr& right);
Expr minusExpr(const Expr& left, const Expr& right);
Expr multExpr(const Expr& left, const Expr& right);
Expr powExpr(const Expr& x, const Expr& n);
Expr divideExpr(const Expr& left, const Expr& right);
Expr ltExpr(const Expr& left, const Expr& right);
Expr leExpr(const Expr& left, const Expr& right);
Expr gtExpr(const Expr& left, const Expr& right);
Expr geExpr(const Expr& left, const Expr& right);
Expr recordExpr(const std::string& field, const Expr& expr);
Expr recordExpr(const std::string& field0, const Expr& expr0,
const std::string& field1, const Expr& expr1);
Expr recordExpr(const std::string& field0, const Expr& expr0,
const std::string& field1, const Expr& expr1,
const std::string& field2, const Expr& expr2);
Expr recordExpr(const std::vector<std::string>& fields,
const std::vector<Expr>& exprs);
Expr recSelectExpr(const Expr& record, const std::string& field);
Expr recUpdateExpr(const Expr& record, const std::string& field,
const Expr& newValue);
Expr readExpr(const Expr& array, const Expr& index);
Expr writeExpr(const Expr& array, const Expr& index, const Expr& newValue);
Expr tupleExpr(const std::vector<Expr>& exprs);
Expr tupleSelectExpr(const Expr& tuple, int index);
Expr tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue);
Expr datatypeConsExpr(const std::string& constructor,
const std::vector<Expr>& args);
Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
Expr forallExpr(const std::vector<Expr>& vars, const Expr& body);
Expr existsExpr(const std::vector<Expr>& vars, const Expr& body);
Expr lambdaExpr(const std::vector<Expr>& vars, const Expr& body);
Expr simulateExpr(const Expr& f, const Expr& s0,
const std::vector<Expr>& inputs, const Expr& n);
Op createOp(const std::string& name, const Type& type);
Op createOp(const std::string& name, const Type& type, const Expr& def);
Expr funExpr(const Op& op, const Expr& child);
Expr funExpr(const Op& op, const Expr& left, const Expr& right);
Expr funExpr(const Op& op, const Expr& child0, const Expr& child1, const Expr& child2);
Expr funExpr(const Op& op, const std::vector<Expr>& children);
Expr stringExpr(const std::string& str);
Expr idExpr(const std::string& name);
Expr listExpr(const std::vector<Expr>& kids);
Expr listExpr(const Expr& e1);
Expr listExpr(const Expr& e1, const Expr& e2);
Expr listExpr(const Expr& e1, const Expr& e2, const Expr& e3);
Expr listExpr(const std::string& op, const std::vector<Expr>& kids);
Expr listExpr(const std::string& op, const Expr& e1);
Expr listExpr(const std::string& op, const Expr& e1,
const Expr& e2);
Expr listExpr(const std::string& op, const Expr& e1,
const Expr& e2, const Expr& e3);
void printExpr(const Expr& e);
void printExpr(const Expr& e, std::ostream& os);
Expr parseExpr(const Expr& e);
Type parseType(const Expr& e);
void assertFormula(const Expr& e);
Expr getImpliedLiteral();
Expr simplify(const Expr& e);
Theorem3 simplifyThm(const Expr& e);
Theorem simplifyThm2(const Expr& e);
void printV(const Expr& e);
// bool query(const Expr& e) { return query(e, false); }
bool query(const Expr& e, bool isTCC = false);
bool checkUnsat(const Expr& e);
bool checkContinue();
bool restart(const Expr& e);
void getAssertions(std::vector<Expr>& assertions);
void getCounterExample(std::vector<Expr>& assertions, bool inOrder);
void getConcreteModel(ExprMap<Expr> & m);
bool inconsistent(std::vector<Expr>& assumptions);
bool incomplete();
bool incomplete(std::vector<std::string>& reasons);
void setResourceLimit(unsigned limit);
Proof getProof();
void getAssumptions(std::vector<Expr>& assumptions);
const Expr& getTCC();
void getAssumptionsTCC(std::vector<Expr>& assumptions);
const Proof& getProofTCC();
const Expr& getClosure();
const Proof& getProofClosure();

int stackLevel();
void push();
void pop();
void popto(int stackLevel);

int scopeLevel();
void pushScope();
void popScope();
void poptoScope(int scopeLevel);

Context* getCurrentContext();

// Accessor methods
ExprManager* getEM() { return d_em; }
ContextManager* getCM() { return d_cm; }
TheoremManager* getTM() { return d_tm; }
SearchEngine* getSE() { return d_se; }
TheoryCore* theoryCore();
CLFlags& getFlags() const { return *d_flags; }
void loadFile(const std::string& fileName,
InputLanguage lang = PRESENTATION_LANG,
bool interactive = false);
void loadFile(std::istream& is,
InputLanguage lang = PRESENTATION_LANG,
bool interactive = false);

Statistics& getStatistics() { return d_statistics; }
void printStatistics() { std::cout << d_statistics << std::endl; }

// Some generally useful methods from TheoryCore
bool isLiteral(const Expr& e);
};


class CNF
{
VCL* d_vcl;
TheoryCore* d_core;
std::map<Expr,Expr> d_exprVars;
std::deque<Expr> d_q;
int d_nextNum;
Expr exprVar(const Expr& e);

public:
CNF(VCL* vcl) : d_vcl(vcl), d_core(vcl->theoryCore()), d_nextNum(0) { }
Expr cnf(const Expr& e);
TheoryCore * theoryCore();
};

}

#endif