1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6     smt_farkas_util.h
7 
8 Abstract:
9 
10     Utility for combining inequalities using coefficients obtained from Farkas lemmas.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorne) 2013-11-2.
15 
16 Revision History:
17 
18     NB. This utility is specialized to proofs generated by the arithmetic solvers.
19 
20 --*/
21 
22 #pragma once
23 
24 #include "ast/arith_decl_plugin.h"
25 
26 namespace smt {
27 
28     class farkas_util {
29         ast_manager&     m;
30         arith_util       a;
31         app_ref_vector   m_ineqs;
32         vector<rational> m_coeffs;
33         rational         m_normalize_factor;
34         // utilities for separating coefficients
35         bool             m_split_literals;
36         unsigned         m_time;
37         unsigned_vector  m_roots, m_size, m_his, m_reps, m_ts;
38 
39         void mk_coerce(expr*& e1, expr*& e2);
40         app* mk_add(expr* e1, expr* e2);
41         app* mk_mul(expr* e1, expr* e2);
42         app* mk_le(expr* e1, expr* e2);
43         app* mk_ge(expr* e1, expr* e2);
44         app* mk_gt(expr* e1, expr* e2);
45         app* mk_lt(expr* e1, expr* e2);
46         void mul(rational const& c, expr* e, expr_ref& res);
47         bool is_int_sort(app* c);
48         bool is_int_sort();
49         void normalize_coeffs();
50         app* mk_one();
51         app* fix_sign(bool is_pos, app* c);
52         void partition_ineqs();
53         unsigned find(unsigned idx);
54         void merge(unsigned i, unsigned j);
55         unsigned process_term(expr* e);
56         expr_ref extract_consequence(unsigned lo, unsigned hi);
57         void fix_dl(expr_ref& r);
58 
59     public:
60         farkas_util(ast_manager& m);
61 
62         /**
63            \brief Reset state
64          */
65         void reset();
66 
67         /**
68             \brief add a multiple of constraint c to the current state
69             Fail if the constraint cannot be classified.
70          */
71         bool add(rational const & coef, app * c);
72 
73         /**
74            \brief Extract the complement of premises multiplied by Farkas coefficients.
75         */
76         expr_ref get();
77 
78         /**
79            \brief Coefficients are normalized for integer problems.
80            Retrieve multiplicant for normalization.
81          */
get_normalize_factor()82         rational const& get_normalize_factor() const { return m_normalize_factor; }
83 
84         /**
85            \brief extract one or multiple consequences based on literal partition.
86            Multiple consequences are strongst modulo a partition of variables.
87            Consequence generation under literal partitioning maintains difference logic constraints.
88            That is, if the original constraints are difference logic, then the consequent
89            produced by literal partitioning is also difference logic.
90          */
set_split_literals(bool f)91         void set_split_literals(bool f) { m_split_literals = f; }
92 
93     };
94 }
95 
96