z3-src 503.2.2

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

/*++
  Copyright (c) 2017 Microsoft Corporation

  Author:
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
  --*/
#pragma once
#include "util/rational.h"
#include "math/lp/factorization.h"
#include "math/lp/nla_common.h"

namespace nla {
class core;

struct point {
    rational x;
    rational y;
    point(const rational& a, const rational& b): x(a), y(b) {}
    point() = default;
    inline point& operator*=(rational a) {
        x *= a;
        y *= a;
        return *this;
    } 
    inline point& operator/=(rational a) {
        x /= a;
        y /= a;
        return *this;
    } 
    inline point operator+(const point& b) const {
        return point(x + b.x, y + b.y);
    } 

    inline point operator-(const point& b) const {
        return point(x - b.x, y - b.y);
    }
};

inline std::ostream& operator<<(std::ostream& out, point const& a) { return out << "(" << a.x <<  ", " << a.y << ")"; }


struct tangents : common {
    tangents(core *core);
    void tangent_lemma();    
}; // end of tangents
} // end of namespace