#ifndef GOOSE_VERIFY_CONDITION_H
#define GOOSE_VERIFY_CONDITION_H

namespace goose::builtins
{
    class FuncType;
}

namespace goose::verify
{
    // Checks that a function's pre/post consitions are
    // satisfiable, and emits any necessary diagnostic.
    class Condition
    {
        public:
            Condition( const sema::Context& c );
            Condition( const sema::Context& c, const builtins::FuncType& funcType );

            // Add an assertion list in the form of a Vector of values.
            // Emits a diagnostic and returns false if any of the expression
            // can't be represented as a z3 expression.
            bool addConditionsList( const pvec& assList );

            // Checks the satisfiability of the conditions. Emits diagnostics and return
            // false if they aren't.
            bool verify();

        private:
            const sema::Context& m_context;
            z3::solver m_solver;
            Builder m_builder;

            // Keep track of the ids of bool constants we generated to track which
            // conditions have failed, along with the location of the corresponding expressions.
            vector< pair< uint32_t, uint32_t > > m_idAndLocs;

            uint32_t m_nextIndex = 0;
    };
}

#endif