Skip to content

Commit

Permalink
lit: Remove VarOrLit trait
Browse files Browse the repository at this point in the history
  • Loading branch information
jix committed Oct 4, 2024
1 parent 26e213a commit ed3e5e9
Show file tree
Hide file tree
Showing 9 changed files with 58 additions and 221 deletions.
5 changes: 1 addition & 4 deletions ir/src/env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,7 @@ use imctk_ids::{id_vec::IdVec, Id, Id32};
use imctk_transparent::{NewtypeCast, SubtypeCast};
use imctk_util::give_take::Take;

use crate::{
index::{DefsIndex, UsesIndex},
var::VarOrLit,
};
use crate::index::{DefsIndex, UsesIndex};

use super::{
index::{DynamicIndex, StructuralHashIndex},
Expand Down
32 changes: 20 additions & 12 deletions ir/src/env/node_builders.rs
Original file line number Diff line number Diff line change
Expand Up @@ -236,8 +236,8 @@ impl RawEnvNodes {
.find_term(&self.0.nodes, &term)
{
if def_mode.is_when_acyclic() {
let output_var =
<T::Output>::process_var_or_lit(output, |var| var, |lit| lit.var());
let output_var = output.into().var();

let encoded_var_repr = &self.0.var_defs.var_defs[output_var];

let old_level_bound = encoded_var_repr.level_bound();
Expand All @@ -257,7 +257,7 @@ impl RawEnvNodes {
}

let (new_var, _) = self.0.var_defs.var_defs.push(EncodedVarDef::default());
let output = <T::Output>::build_var_or_lit(new_var, |var| var, |var| var.as_lit());
let output = T::Output::from(new_var);

let (node_id, _) = self.insert_unique_irreducible_node(def_mode, TermNode { output, term });

Expand Down Expand Up @@ -483,12 +483,16 @@ impl NodeBuilder for Env {
let pol = term.apply_var_map(|var| self.var_defs.update_lit_repr(var.as_lit()));

if let Some(output) = term.reduce(self) {
return output ^ pol;
return T::Output::try_from(output.into() ^ pol).unwrap();
}

self.raw_nodes()
.insert_irreducible_term(DefMode::WhenMissing, term)
^ pol
T::Output::try_from(
self.raw_nodes()
.insert_irreducible_term(DefMode::WhenMissing, term)
.into()
^ pol,
)
.unwrap()
}

fn node<T: Node>(&mut self, mut node: T) {
Expand Down Expand Up @@ -571,13 +575,17 @@ impl NodeBuilder for DefBuilder {
let pol = term.apply_var_map(|var| self.0.var_defs.update_lit_repr(var.as_lit()));

if let Some(output) = term.reduce(self) {
return output ^ pol;
return T::Output::try_from(output.into() ^ pol).unwrap();
}

self.0
.raw_nodes()
.insert_irreducible_term(DefMode::WhenAcyclic, term)
^ pol
T::Output::try_from(
self.0
.raw_nodes()
.insert_irreducible_term(DefMode::WhenAcyclic, term)
.into()
^ pol,
)
.unwrap()
}

fn node<T: Node>(&mut self, mut node: T) {
Expand Down
6 changes: 3 additions & 3 deletions ir/src/node/builder.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//! Generic interface for adding equivalences, nodes and terms.
use crate::var::{Lit, VarOrLit};
use crate::var::Lit;
use imctk_util::give_take::{give, Take};

use super::generic::{DynNode, DynTerm, Node, Term};
Expand All @@ -14,7 +14,7 @@ pub trait NodeBuilder: NodeBuilderDyn {
/// variable or literal.
fn term<T: Term>(&mut self, term: T) -> T::Output {
give!(term: DynTerm = term);
<T::Output as VarOrLit>::build_var_or_lit(self.dyn_term(term), |lit| lit.var(), |lit| lit)
self.dyn_term(term).try_into().unwrap()
}
/// Ensure the presence of the given node.
fn node<T: Node>(&mut self, node: T) {
Expand Down Expand Up @@ -62,7 +62,7 @@ impl NodeBuilder for DynNodeBuilder {

let lit = self.dyn_term(term);

<T::Output as VarOrLit>::build_var_or_lit(lit, |lit| lit.var(), |lit| lit)
T::Output::try_from(lit).unwrap()
}

fn node<T: Node>(&mut self, node: T) {
Expand Down
4 changes: 2 additions & 2 deletions ir/src/node/collections/buf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use crate::{
vtables::{DynNodeType, DynTermType, GenericNodeType, GenericTermType},
NodeId,
},
var::{Lit, Var, VarOrLit},
var::{Lit, Var},
};

#[derive(Clone, Copy, Debug)]
Expand Down Expand Up @@ -120,7 +120,7 @@ impl NodeBuilder for NodeBuf {
self.nodes.insert(TermWrapper { term }).0,
));

<T::Output as VarOrLit>::build_var_or_lit(lit, |lit| lit.var(), |lit| lit)
T::Output::try_from(lit).unwrap()
}

fn node<T: Node>(&mut self, node: T) {
Expand Down
5 changes: 1 addition & 4 deletions ir/src/node/fine/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -129,10 +129,7 @@ impl Term for Xor {
self.inputs.into_iter()
}

fn apply_var_map(
&mut self,
mut var_map: impl FnMut(Var) -> Lit,
) -> <Self::Output as crate::var::VarOrLit>::Pol {
fn apply_var_map(&mut self, mut var_map: impl FnMut(Var) -> Lit) -> Pol {
let mut composed_pol = Pol::Pos;
self.inputs = self.inputs.map(|var| {
let mapped = var_map(var);
Expand Down
88 changes: 29 additions & 59 deletions ir/src/node/generic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use zwohash::ZwoHasher;

use crate::{
env::Env,
var::{Lit, Pol, Var, VarOrLit},
var::{Lit, Pol, Var},
};

use super::{
Expand Down Expand Up @@ -298,7 +298,15 @@ impl DynNode {
/// Everything that is object-safe is part of the [`TermDyn`] supertrait.
pub trait Term: Debug + Clone + Eq + Hash + TermDyn + 'static {
/// Whether the output can be represented as a variable or can require a literal.
type Output: VarOrLit + 'static;
type Output: Into<Lit>
+ From<Var>
+ TryFrom<Lit, Error: Debug>
+ Copy
+ Ord
+ Hash
+ Debug
+ Default
+ 'static;

/// A short name identifying the operation.
const NAME: &'static str;
Expand All @@ -319,8 +327,7 @@ pub trait Term: Debug + Clone + Eq + Hash + TermDyn + 'static {

/// Rewrites all variables in the term using a given mapping.
#[must_use]
fn apply_var_map(&mut self, var_map: impl FnMut(Var) -> Lit)
-> <Self::Output as VarOrLit>::Pol;
fn apply_var_map(&mut self, var_map: impl FnMut(Var) -> Lit) -> Pol;

/// Returns whether two [`Term`]s define the same value.
///
Expand Down Expand Up @@ -383,9 +390,7 @@ pub fn default_reduce_node<T: Term>(
};

if new_output != output {
builder.equiv(
[output, new_output].map(|x| x.process_var_or_lit(|var| var.as_lit(), |lit| lit)),
);
builder.equiv([output, new_output].map(|x| x.into()));
}

true
Expand Down Expand Up @@ -545,13 +550,11 @@ impl<T: Term> TermDynAuto for T {

#[must_use]
fn dyn_apply_var_map(&mut self, var_repr: &mut dyn FnMut(Var) -> Lit) -> Pol {
<T::Output as VarOrLit>::process_pol(self.apply_var_map(var_repr), || Pol::Pos, |pol| pol)
self.apply_var_map(var_repr)
}

fn dyn_reduce_into_buf(&mut self, buf: &mut NodeBuf) -> Option<Lit> {
self.reduce(buf).map(|output| {
<T::Output as VarOrLit>::process_var_or_lit(output, |var| var.as_lit(), |lit| lit)
})
self.reduce(buf).map(|output| output.into())
}

fn dyn_add_to_buf_with_var_map(
Expand All @@ -560,14 +563,8 @@ impl<T: Term> TermDynAuto for T {
var_map: &mut dyn FnMut(Var) -> Lit,
) -> Lit {
let mut clone = self.clone();
let pol = <<Self as Term>::Output>::process_pol(
clone.apply_var_map(var_map),
|| Pol::Pos,
|pol| pol,
);
buf.term(clone)
.process_var_or_lit(|var| var.as_lit(), |lit| lit)
^ pol
let pol = clone.apply_var_map(var_map);
buf.term(clone).into() ^ pol
}

fn dyn_add_to_env_with_var_map(
Expand All @@ -576,15 +573,9 @@ impl<T: Term> TermDynAuto for T {
var_map: &mut dyn FnMut(Var) -> Lit,
) -> Lit {
let mut clone = self.clone();
let pol = <<Self as Term>::Output>::process_pol(
clone.apply_var_map(var_map),
|| Pol::Pos,
|pol| pol,
);
let pol = clone.apply_var_map(var_map);

env.term(clone)
.process_var_or_lit(|var| var.as_lit(), |lit| lit)
^ pol
env.term(clone).into() ^ pol
}
}

Expand Down Expand Up @@ -733,26 +724,14 @@ impl<T: Term> Node for TermNode<T> {
}

fn apply_var_map(&mut self, mut var_map: impl FnMut(Var) -> Lit) {
let mut new_output_lit = self
.output
.process_var_or_lit(|var| var.as_lit(), |lit| lit)
.lookup(&mut var_map);
let mut new_output_lit = self.output.into().lookup(&mut var_map);

let term_pol = self.term.apply_var_map(var_map);

new_output_lit ^= term_pol.into();
new_output_lit ^= term_pol;

let new_output = <T::Output>::build_var_or_lit(
new_output_lit,
|lit| {
assert!(
lit.is_pos(),
"Term output of non-Boolean type mapped to negative literal"
);
lit.var()
},
|lit| lit,
);
let new_output = T::Output::try_from(new_output_lit)
.expect("Term output of non-Boolean type mapped to negative literal");

self.output = new_output
}
Expand All @@ -772,20 +751,15 @@ impl<T: Term> NodeDyn for TermNode<T> {
}

fn output_var(&self) -> Option<Var> {
Some(self.output.process_var_or_lit(|var| var, |lit| lit.var()))
Some(self.output.into().var())
}

fn output_lit(&self) -> Option<Lit> {
Some(
self.output
.process_var_or_lit(|var| var.as_lit(), |lit| lit),
)
Some(self.output.into())
}

fn max_var(&self) -> Var {
self.output
.process_var_or_lit(|var| var, |lit| lit.var())
.max(self.term.max_var())
self.output.into().var().max(self.term.max_var())
}

fn dyn_term(&self) -> Option<&DynTerm> {
Expand All @@ -811,10 +785,8 @@ mod tests {
[].into_iter()
}

fn apply_var_map(
&mut self,
_var_map: impl FnMut(Var) -> Lit,
) -> <Self::Output as VarOrLit>::Pol {
fn apply_var_map(&mut self, _var_map: impl FnMut(Var) -> Lit) -> Pol {
Pol::Pos
}
}

Expand All @@ -832,13 +804,11 @@ mod tests {
[self.0].into_iter()
}

fn apply_var_map(
&mut self,
mut var_map: impl FnMut(Var) -> Lit,
) -> <Self::Output as VarOrLit>::Pol {
fn apply_var_map(&mut self, mut var_map: impl FnMut(Var) -> Lit) -> Pol {
let var = var_map(self.0);
assert!(var.is_pos());
self.0 = var.var();
Pol::Pos
}
}

Expand Down
7 changes: 2 additions & 5 deletions ir/src/node/vtables.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,7 @@ use std::{
ops::Deref,
};

use crate::{
var::{Lit, VarOrLit},
wide_ptr::WidePtr,
};
use crate::{var::Lit, wide_ptr::WidePtr};

use super::{
collections::nodes::Nodes,
Expand Down Expand Up @@ -177,7 +174,7 @@ impl TermTypeVTable {
|output: Lit, term_ptr: *mut u8, callback: &mut dyn FnMut(*mut u8)| {
let term_ptr = term_ptr as *mut T;
let mut term_node = ManuallyDrop::new(TermNode {
output: VarOrLit::build_var_or_lit(output, |lit| lit.var(), |lit| lit),
output: output.try_into().unwrap(),
term: term_ptr.read(),
});
callback(&mut term_node as *mut ManuallyDrop<TermNode<T>> as *mut u8);
Expand Down
2 changes: 0 additions & 2 deletions ir/src/var.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,2 @@
//! Numeric identifiers for variables and Boolean literals
pub use imctk_lit::{lit::Lit, pol::Pol, var::Var};

pub use imctk_lit::var_or_lit::VarOrLit;
Loading

0 comments on commit ed3e5e9

Please sign in to comment.