Struct Theory

pub struct Theory {
    pub id: String,
    pub statements: Vec<Statement>,
}

A Theory is a list of statements with a common name (id).

Fields

id: String

statements: Vec<Statement>

Implementations

impl Theory

pub fn propagate(&self) -> HashMap<u32, (i64, i64)>

Propagates all information bottoms-up in the Theory and compiles into a HashMap from variable id to bounds.

Example:

use puanrs::Theory;
use puanrs::Statement;
use puanrs::Sign;
use puanrs::AtLeast;
use puanrs::polyopt::Variable;
use std::collections::HashMap;
let theory: Theory = Theory {
   id          : String::from("A"),
   statements  : vec![
       Statement {
           variable    : Variable {
             id      : 0,
             bounds  : (0,1),
           },
           expression  : Some(
               AtLeast {
                   ids     : vec![1,2],
                   bias    : -1,
                   sign    : Sign::Positive
               }
           )
      },
      Statement {
          variable    : Variable {
              id      : 1,
              bounds  : (0,1),
          },
          expression  : None
      },
      Statement {
          variable    : Variable {
              id      : 2,
              bounds  : (1,1),
          },
          expression  : None
      },
   ]
};
let actual: HashMap<u32, (i64, i64)> = theory.propagate();
let expected: HashMap<u32, (i64, i64)> = vec![
    (0, (1,1)),
    (1, (0,1)),
    (2, (1,1)),
].into_iter().collect();
assert_eq!(actual, expected);

pub fn to_lineqs(&self, active: bool, reduced: bool) -> Vec<GeLineq>

Transforms all Statements in Theory into GeLineq’s such that if all GeLineq’s are true <-> Theory is true.

Example:

use puanrs::Theory;
use puanrs::Statement;
use puanrs::Sign;
use puanrs::AtLeast;
use puanrs::polyopt::Variable;
use puanrs::polyopt::GeLineq;
let theory: Theory = Theory {
    id          : String::from("A"),
    statements  : vec![
        Statement {
            variable    : Variable {
                id      : 0,
                bounds  : (0,1),
            },
            expression  : Some(
                AtLeast {
                    ids     : vec![1,2],
                    bias    : -1,
                    sign    : Sign::Positive
                }
            )
        },
        Statement {
            variable    : Variable {
                id      : 1,
                bounds  : (0,1),
            },
            expression  : None
        },
        Statement {
            variable    : Variable {
                id      : 2,
                bounds  : (0,1),
            },
            expression  : None
        },
    ]
};
let actual: Vec<GeLineq> = theory.to_lineqs(false, false);
assert_eq!(actual.len(), 1);
assert_eq!(actual[0].bias, 0);
assert_eq!(actual[0].coeffs, vec![-1,1,1]);
assert_eq!(actual[0].indices, vec![0,1,2]);

pub fn to_ge_polyhedron(&self, active: bool, reduced: bool) -> CsrPolyhedron

Converts Theory into a polyhedron. Set active param to true to activate polyhedron, meaning assuming the top node to be true. Set reduced to true to potentially retrieve a reduced polyhedron.

pub fn solve( &self, objectives: Vec<HashMap<u32, f64>>, reduce_polyhedron: bool, ) -> Vec<(HashMap<u32, i64>, i64, usize)>

Find solutions to this Theory. objectives is a vector of HashMap’s pointing from an id to a value. The solver will try to find a valid configuration that maximizes those values, for each objective in objectives.

Note

• Ids given in objectives which are not in Theory will be ignored.
• Ids which have not been given a value will be given 0 as default.

Returns

A tuple of (solution: HashMap<u32, i64>, objective value: i64, status code: usize)

Example:

use puanrs::Theory;
use puanrs::Statement;
use puanrs::Sign;
use puanrs::AtLeast;
use puanrs::polyopt::Variable;
let t = Theory {
   id: String::from("A"),
    statements: vec![
        Statement {
           variable: Variable { id: 0, bounds: (0,1) },
           expression: Some(
               AtLeast {
                   ids: vec![1,2],
                   bias: -1,
                   sign: Sign::Positive
               }
           )
       },
       Statement {
           variable: Variable { id: 1, bounds: (0,1) },
           expression: Some(
               AtLeast {
                   ids: vec![3,4],
                   bias: 1,
                   sign: Sign::Negative
               }
           )
       },
       Statement {
           variable: Variable { id: 2, bounds: (0,1) },
           expression: Some(
               AtLeast {
                   ids: vec![5,6,7],
                   bias: -3,
                   sign: Sign::Positive,
               }
           )
       },
       Statement {
           variable: Variable { id: 3, bounds: (0,1) },
           expression: None
       },
       Statement {
           variable: Variable { id: 4, bounds: (0,1) },
           expression: None
       },
       Statement {
           variable: Variable { id: 5, bounds: (0,1) },
           expression: None
       },
       Statement {
           variable: Variable { id: 6, bounds: (0,1) },
           expression: None
       },
       Statement {
           variable: Variable { id: 7, bounds: (0,1) },
           expression: None
       },
    ]
};
let actual_solutions = t.solve(
    vec![
        vec![(3, 1.0), (4, 1.0)].iter().cloned().collect(),
    ],
    true
);
let expected_solutions = vec![
   vec![(3,1),(4,1),(5,1),(6,1),(7,1)].iter().cloned().collect(), // <- notice that these are from reduced columns (3,4,5,6,7)
];
assert_eq!(actual_solutions[0].0, expected_solutions[0]);

pub fn instance(width: u32, depth: u32, id: String) -> Theory

Given two positive integers n (width) and m (depth), this function creates a n-ary Theory/tree, with variable size $ n^0 + n^1 + … + n^m $. Each Statement with Some expression has bias -1 and n number of children. For eaxmple, Theory::instance(2, 3, String::from("my-id")) would create a binary tree/Theory of variable size $ 2^3 = 8 $.

Note

This function was mainly created to support benchmarking tests for different Theory sizes.

Trait Implementations

impl Clone for Theory

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.