pblib-rs 0.1.0

Rust safe bindings for pblib
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

#ifndef INCPBCONSTRAINT_H
#define INCPBCONSTRAINT_H

#include <vector>
#include <assert.h>
#include "weightedlit.h"
#include "pbconstraint.h"
#include "clausedatabase.h"
#include "IncSimplePBConstraint.h"
#include "auxvarmanager.h"

class IncPBConstraint
{
private:
    int64_t leq;
    int64_t geq;
    int64_t init_leq;
    int64_t init_geq;

    std::vector<PBLib::WeightedLit> weighted_literals;
    PBLib::Comparator comparator;

    std::shared_ptr<IncSimplePBConstraint> inc_simple_pb_constraint;

    bool isDualEncoded;
    std::shared_ptr<IncSimplePBConstraint> leq_inc_simple_pb_constraint;
    std::shared_ptr<IncSimplePBConstraint> geq_inc_simple_pb_constraint;

    std::vector<int32_t> conditionals;

public:
    IncPBConstraint(std::vector<PBLib::WeightedLit> const & literals, PBLib::Comparator comparator, int64_t less_eq, int64_t greater_eq);
    IncPBConstraint(std::vector<PBLib::WeightedLit> const & literals, PBLib::Comparator comparator, int64_t bound);
    IncPBConstraint();
    virtual ~IncPBConstraint() = default;

    void addConditional(int32_t lit);
    void addConditionals(std::vector<int32_t> lits);
    void clearConditionals();
    std::vector<int32_t> const & getConditionals() const;

    std::vector<PBLib::WeightedLit> const & getWeightedLiterals() const;
    int64_t getLeq() const;
    int64_t getGeq() const;

    std::shared_ptr< IncSimplePBConstraint > getIncSimplePBConstraint();

    void setComparator(PBLib::Comparator comp);
    void setIncSimplePBConstraint(std::shared_ptr< IncSimplePBConstraint > incSimplePBConstraint);

    void setLeqIncSimplePBConstraint(std::shared_ptr< IncSimplePBConstraint > incSimplePBConstraint);
    void setGeqIncSimplePBConstraint(std::shared_ptr< IncSimplePBConstraint > incSimplePBConstraint);

    void encodeNewGeq(int64_t newGeq, ClauseDatabase & formula, AuxVarManager & auxVars);
    void encodeNewLeq(int64_t newLeq, ClauseDatabase & formula, AuxVarManager & auxVars);

    PBLib::PBConstraint getNonIncConstraint();

    IncPBConstraint getGeqConstraint() const;
    IncPBConstraint getLeqConstraint() const;

    PBLib::Comparator getComparator() const;

    int getN() const;

    void print() const;

};

#endif // INCPBCONSTRAINT_H