Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Add exporting formats and string diagram-based optimizer #124

Draft
wants to merge 70 commits into
base: main
Choose a base branch
from

Conversation

AHartNtkn
Copy link
Collaborator

@AHartNtkn AHartNtkn commented Aug 1, 2023

This repo consists of two main features.
Firstly, it adds additional export formats, specifically for Z3, Mathematica, Prolog, and a generic format. As an example, one can run

cargo run generate three-address-file -s tests/fresh.pir -o tests/fresh.3ac

it will generate a file with the following contents in tests/fresh.3ac

0 = Var191 * Var239,
0 = Var197 * Var237,
Var195 = 1 + Var235,
Var191 = 1 + Var239,
Var216 = 2 * Var233,
0 = Var195 * Var235,
Var222 = 16 * Var238,
Var193 = 1,
Var223 = Var221 + Var222,
0 = Var193 * Var241,
Var197 = 1 + Var237,
Var193 = 1 + Var241,
Var199 = 1 + Var240,
Var219 = Var217 + Var218,
0 = Var199 * Var240,
Var217 = Var191 + Var216,
Var221 = Var219 + Var220,
Var220 = 8 * Var236,
Var218 = 4 * Var234,
Var191 = 0,

This, additionally, adds additional functions which will simplify a module using an intermediate string diagram representation. This functionality is stored in string.rs. Core functionality is accessed through the function

pub fn simplify_3ac(
    equations: &mut Vec<TExpr>,
    input_ids: &HashSet<VarId>,
    defs: &mut Vec<Definition>,
    field_ops: &dyn FieldOps,
)

which will modify the components of a module in place. Example usage would be something like

let mut module_3ac = compile(module, &PrimeFieldOps::<Fp>::default(), config);

let input_ids: HashSet<u32> = module_3ac.pubs.iter().map(|var| var.id).collect();

simplify_3ac(
    &mut module_3ac.exprs,
    &input_ids,
    &mut module_3ac.defs,
    &Halo2PrimeFieldOps::<Fp>::default(),
);

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant