1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3 
4 Module Name:
5 
6     maxlex.h
7 
8 Abstract:
9 
10     MaxLex solves weighted max-sat problems where weights impose lexicographic order.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2019-25-1
15 
16 Notes:
17 
18 --*/
19 
20 #pragma once
21 
22 namespace opt {
23 
24     bool is_maxlex(weights_t & ws);
25 
26     maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
27 
28 
29 };
30 
31