issues
search
zkincaid
/
duet
Duet: static analysis for unbounded concurrency
http://duet.cs.toronto.edu
MIT License
23
stars
17
forks
source link
Polynomial cone cutting plane closure
#31
Closed
nclskoh
closed
2 years ago
nclskoh
commented
2 years ago
PolynomialConeCpClosure: computing cutting plane closure with respect to polynomial lattice.
Polyhedron: add integer hull computation
IntLattice: compute lattice for a set of rational vectors
PolynomialUtil: conversion between polynomials and vectors and utility functions for printing
Weaksolver: propositional relaxation instead of LIA
Nonlinear: eliminate floor, mod, div by introducing fresh variables and defining equations
SrkSimplify: purifying expressions matching some predicate
Syntax: generalize signature of rewriter slightly, add IsInt for lattice
SrkZ3: parse is_int
Interpretation: evaluate is_int