types.h

Go to the documentation of this file.

// MIT License
//
// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved.
// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved.
// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved.
// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved.
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in all
// copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
// SOFTWARE.
 
#pragma once
 
#include "hal_core/defines.h"
#include "hal_core/netlist/boolean_function.h"
#include "hal_core/utilities/enums.h"
 
#include <map>
#include <optional>
#include <string>
 
namespace hal
{
    namespace SMT
    {
        enum class SolverType : int
        {
            Z3 = 0,    
            Boolector, 
            Bitwuzla,  
            Unknown,   
        };
 
        enum class SolverCall : int
        {
            Binary,  
            Library, 
        };
 
        struct QueryConfig final
        {
            // Member
 
            SolverType solver = SolverType::Z3;
            SolverCall call = SolverCall::Binary;
            bool local = true;
            bool generate_model = false;
            u64 timeout_in_seconds = 10;
 
            // Interface
 
            QueryConfig& with_solver(SolverType solver);
 
            QueryConfig& with_call(SolverCall call);
 
            QueryConfig& with_local_solver();
 
            QueryConfig& with_remote_solver();
 
            QueryConfig& with_model_generation();
 
            QueryConfig& without_model_generation();
 
            QueryConfig& with_timeout(u64 seconds);
 
            friend std::ostream& operator<<(std::ostream& out, const QueryConfig& config);
        };
 
        struct Constraint final
        {
            // Member
 
            std::variant<BooleanFunction, std::pair<BooleanFunction, BooleanFunction>> constraint;
 
            // Constructors, Destructors, Operators
 
            explicit Constraint(BooleanFunction&& constraint);
 
            explicit Constraint(BooleanFunction&& lhs, BooleanFunction&& rhs);
 
            friend std::ostream& operator<<(std::ostream& out, const Constraint& constraint);
 
            std::string to_string() const;
 
            bool is_assignment() const;
 
            Result<const std::pair<BooleanFunction, BooleanFunction>*> get_assignment() const;
 
            Result<const BooleanFunction*> get_function() const;
        };
 
        enum class SolverResultType
        {
            Sat,     
            UnSat,   
            Unknown, 
        };
 
        struct Model final
        {
            // Member
 
            std::map<std::string, std::tuple<u64, u16>> model;
 
            // Constructors, Destructors, Operators
 
            Model(const std::map<std::string, std::tuple<u64, u16>>& model = {});
 
            bool operator==(const Model& other) const;
 
            bool operator!=(const Model& other) const;
 
            friend std::ostream& operator<<(std::ostream& out, const Model& model);
 
            // Interface
 
            static Result<Model> parse(const std::string& model_str, const SolverType& solver);
 
            Result<BooleanFunction> evaluate(const BooleanFunction& bf) const;
        };
 
        struct SolverResult final
        {
            // Member
 
            SolverResultType type;
            std::optional<Model> model;
 
            // Constructors, Destructors, Operators
 
            SolverResult() : type(SolverResultType::Unknown), model({})
            {
            }
 
            static SolverResult Sat(const std::optional<Model>& model = {});
 
            static SolverResult UnSat();
 
            static SolverResult Unknown();
 
            bool is(const SolverResultType& type) const;
 
            bool is_sat() const;
 
            bool is_unsat() const;
 
            bool is_unknown() const;
 
            friend std::ostream& operator<<(std::ostream& out, const SolverResult& result);
 
        private:
            SolverResult(SolverResultType _type, std::optional<Model> _model);
        };
 
    }    // namespace SMT
 
    template<>
    std::map<SMT::SolverType, std::string> EnumStrings<SMT::SolverType>::data;
 
    template<>
    std::map<SMT::SolverResultType, std::string> EnumStrings<SMT::SolverResultType>::data;
}    // namespace hal