SmtSolverOutput.h

 
#pragma once
 
#include <chrono>
#include <iosfwd>
#include <string>
 
#include "dlinear/libs/libgmp.h"
#include "dlinear/solver/LpResult.h"
#include "dlinear/solver/SatResult.h"
#include "dlinear/util/Box.h"
#include "dlinear/util/Config.h"
#include "dlinear/util/Stats.h"
#include "dlinear/util/Timer.h"
 
namespace dlinear {
 
enum class SmtResult {
  UNSOLVED,       
  SKIP_SAT,       
  SAT,            
  DELTA_SAT,      
  OPTIMAL,        
  DELTA_OPTIMAL,  
  UNBOUNDED,      
  INFEASIBLE,     
  UNSAT,          
  UNKNOWN,        
  ERROR,          
};
 
SmtResult parse_smt_result(SatResult sat_result);
SmtResult parse_smt_result(LpResult lp_result);
 
struct SmtSolverOutput {
  SmtSolverOutput() = delete;
  explicit SmtSolverOutput(const Config &config)
      : produce_models{config.produce_models()},
        with_timings{config.with_timings()},
        model{config.lp_solver()},
        complete_model{config.lp_solver()},
        precision{config.precision()},
        actual_precision{config.precision()} {}
 
  [[nodiscard]] double precision_upper_bound() const;
  [[nodiscard]] bool is_sat() const {
    return result == SmtResult::SAT || result == SmtResult::DELTA_SAT || result == SmtResult::OPTIMAL ||
           result == SmtResult::DELTA_OPTIMAL;
  }
  [[nodiscard]] int exit_code() const;
 
  [[nodiscard]] bool matches_expectation(SmtResult expectation) const;
 
  bool produce_models;  
  bool with_timings;    
 
  Stats parser_stats{with_timings, ""};                         
  IterationStats ite_stats{with_timings, ""};                   
  IterationStats cnfizer_stats{with_timings, ""};               
  IterationStats predicate_abstractor_stats{with_timings, ""};  
  IterationStats sat_stats{with_timings, ""};                   
  IterationStats theory_stats{with_timings, ""};                
  IterationStats preprocessor_stats{with_timings, ""};          
 
  Timer smt_solver_timer{};               
  unsigned int n_assertions{0};           
  SmtResult result{SmtResult::UNSOLVED};  
  mpq_class lower_bound{0};               
  mpq_class upper_bound{0};               
  Box model;                              
  Box complete_model;                     
  mpq_class precision;                    
  mpq_class actual_precision;             
};
 
std::ostream &operator<<(std::ostream &os, const SmtResult &result);
std::ostream &operator<<(std::ostream &os, const SmtSolverOutput &output);
 
}  // namespace dlinear