mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-05-13 03:00:26 -04:00
Merge pull request #155 from chriseth/fixed_is_no_machine
Fixed lookup is not considered a machine.
This commit is contained in:
@@ -9,7 +9,7 @@ use super::affine_expression::AffineExpression;
|
||||
use super::bit_constraints::{BitConstraint, BitConstraintSet};
|
||||
use super::eval_error::EvalError;
|
||||
use super::expression_evaluator::ExpressionEvaluator;
|
||||
use super::machines::Machine;
|
||||
use super::machines::{FixedLookup, Machine};
|
||||
use super::symbolic_witness_evaluator::{SymoblicWitnessEvaluator, WitnessColumnEvaluator};
|
||||
use super::util::{contains_next_witness_ref, WitnessColumnNamer};
|
||||
use super::{Constraint, EvalResult, FixedData, WitnessColumn};
|
||||
@@ -19,6 +19,7 @@ where
|
||||
QueryCallback: FnMut(&'a str) -> Option<AbstractNumberType>,
|
||||
{
|
||||
fixed_data: &'a FixedData<'a>,
|
||||
fixed_lookup: &'a mut FixedLookup,
|
||||
identities: Vec<&'a Identity>,
|
||||
machines: Vec<Box<dyn Machine>>,
|
||||
query_callback: Option<QueryCallback>,
|
||||
@@ -51,6 +52,7 @@ where
|
||||
{
|
||||
pub fn new(
|
||||
fixed_data: &'a FixedData<'a>,
|
||||
fixed_lookup: &'a mut FixedLookup,
|
||||
identities: Vec<&'a Identity>,
|
||||
global_bit_constraints: BTreeMap<&'a str, BitConstraint>,
|
||||
machines: Vec<Box<dyn Machine>>,
|
||||
@@ -60,6 +62,7 @@ where
|
||||
|
||||
Generator {
|
||||
fixed_data,
|
||||
fixed_lookup,
|
||||
identities,
|
||||
machines,
|
||||
query_callback,
|
||||
@@ -305,11 +308,26 @@ where
|
||||
// Note that we should always query all machines that match, because they might
|
||||
// update their internal data, even if all values are already known.
|
||||
// TODO could it be that multiple machines match?
|
||||
|
||||
// query the fixed lookup "machine"
|
||||
if let Some(result) = self.fixed_lookup.process_plookup(
|
||||
self.fixed_data,
|
||||
identity.kind,
|
||||
&left,
|
||||
&identity.right,
|
||||
) {
|
||||
return result;
|
||||
}
|
||||
|
||||
for m in &mut self.machines {
|
||||
// TODO also consider the reasons above.
|
||||
if let Some(result) =
|
||||
m.process_plookup(self.fixed_data, identity.kind, &left, &identity.right)
|
||||
{
|
||||
if let Some(result) = m.process_plookup(
|
||||
self.fixed_data,
|
||||
self.fixed_lookup,
|
||||
identity.kind,
|
||||
&left,
|
||||
&identity.right,
|
||||
) {
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
@@ -3,7 +3,7 @@ use std::iter::once;
|
||||
|
||||
use itertools::{Either, Itertools};
|
||||
|
||||
use super::Machine;
|
||||
use super::{FixedLookup, Machine};
|
||||
use crate::analyzer::PolynomialReference;
|
||||
use crate::analyzer::{Expression, Identity, IdentityKind, SelectedExpressions};
|
||||
use crate::number::AbstractNumberType;
|
||||
@@ -65,6 +65,7 @@ impl Machine for DoubleSortedWitnesses {
|
||||
fn process_plookup(
|
||||
&mut self,
|
||||
fixed_data: &FixedData,
|
||||
_fixed_lookup: &mut FixedLookup,
|
||||
kind: IdentityKind,
|
||||
left: &[Result<AffineExpression, EvalError>],
|
||||
right: &SelectedExpressions,
|
||||
|
||||
@@ -2,7 +2,6 @@ use std::collections::{BTreeMap, HashMap, HashSet};
|
||||
|
||||
use num_bigint::BigInt;
|
||||
|
||||
use super::Machine;
|
||||
use crate::analyzer::{Identity, IdentityKind, SelectedExpressions};
|
||||
use crate::number::{AbstractNumberType, DegreeType};
|
||||
|
||||
@@ -95,10 +94,8 @@ impl FixedLookup {
|
||||
None
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Machine for FixedLookup {
|
||||
fn process_plookup(
|
||||
pub fn process_plookup(
|
||||
&mut self,
|
||||
fixed_data: &FixedData,
|
||||
kind: IdentityKind,
|
||||
@@ -134,15 +131,6 @@ impl Machine for FixedLookup {
|
||||
Some(self.process_plookup_internal(fixed_data, left, right))
|
||||
}
|
||||
|
||||
fn witness_col_values(
|
||||
&mut self,
|
||||
_fixed_data: &FixedData,
|
||||
) -> HashMap<String, Vec<AbstractNumberType>> {
|
||||
Default::default()
|
||||
}
|
||||
}
|
||||
|
||||
impl FixedLookup {
|
||||
fn process_plookup_internal(
|
||||
&mut self,
|
||||
fixed_data: &FixedData,
|
||||
|
||||
@@ -15,10 +15,10 @@ pub fn split_out_machines<'a>(
|
||||
fixed: &'a FixedData<'a>,
|
||||
identities: &'a [Identity],
|
||||
witness_cols: &'a [WitnessColumn],
|
||||
) -> (Vec<Box<dyn Machine>>, Vec<&'a Identity>) {
|
||||
// The lookup-in-fixed-columns machine, it always exists with an empty set of witnesses.
|
||||
let mut machines: Vec<Box<dyn Machine>> =
|
||||
vec![FixedLookup::try_new(fixed, &[], &Default::default()).unwrap()];
|
||||
) -> (FixedLookup, Vec<Box<dyn Machine>>, Vec<&'a Identity>) {
|
||||
let fixed_lookup = FixedLookup::try_new(fixed, &[], &Default::default()).unwrap();
|
||||
|
||||
let mut machines: Vec<Box<dyn Machine>> = vec![];
|
||||
|
||||
let all_witnesses = witness_cols.iter().map(|c| c.name).collect::<HashSet<_>>();
|
||||
let mut remaining_witnesses = all_witnesses.clone();
|
||||
@@ -91,7 +91,7 @@ pub fn split_out_machines<'a>(
|
||||
println!("Will try to continue as is, but this probably requires a specialized machine implementation.");
|
||||
}
|
||||
}
|
||||
(machines, base_identities)
|
||||
(*fixed_lookup, machines, base_identities)
|
||||
}
|
||||
|
||||
/// Extends a set of witnesses to the full set of row-connected witnesses.
|
||||
|
||||
@@ -3,6 +3,8 @@ use std::collections::HashMap;
|
||||
use crate::analyzer::{IdentityKind, SelectedExpressions};
|
||||
use crate::number::AbstractNumberType;
|
||||
|
||||
pub use self::fixed_lookup_machine::FixedLookup;
|
||||
|
||||
use super::EvalResult;
|
||||
use super::{affine_expression::AffineExpression, eval_error::EvalError, FixedData};
|
||||
|
||||
@@ -31,6 +33,7 @@ pub trait Machine {
|
||||
fn process_plookup(
|
||||
&mut self,
|
||||
fixed_data: &FixedData,
|
||||
fixed_lookup: &mut FixedLookup,
|
||||
kind: IdentityKind,
|
||||
left: &[Result<AffineExpression, EvalError>],
|
||||
right: &SelectedExpressions,
|
||||
|
||||
@@ -3,6 +3,7 @@ use std::collections::{BTreeMap, HashMap, HashSet};
|
||||
use itertools::{Either, Itertools};
|
||||
|
||||
use super::super::affine_expression::AffineExpression;
|
||||
use super::fixed_lookup_machine::FixedLookup;
|
||||
use super::Machine;
|
||||
use super::{EvalResult, FixedData};
|
||||
use crate::analyzer::{Expression, Identity, IdentityKind, SelectedExpressions};
|
||||
@@ -126,6 +127,7 @@ impl Machine for SortedWitnesses {
|
||||
fn process_plookup(
|
||||
&mut self,
|
||||
fixed_data: &FixedData,
|
||||
_fixed_lookup: &mut FixedLookup,
|
||||
kind: IdentityKind,
|
||||
left: &[Result<AffineExpression, EvalError>],
|
||||
right: &SelectedExpressions,
|
||||
|
||||
@@ -46,7 +46,7 @@ pub fn generate<'a>(
|
||||
witness_cols.iter().map(|w| (w.name, w.id)).collect(),
|
||||
verbose,
|
||||
);
|
||||
let (machines, identities) = machines::machine_extractor::split_out_machines(
|
||||
let (mut fixed_lookup, machines, identities) = machines::machine_extractor::split_out_machines(
|
||||
&fixed,
|
||||
&analyzed.identities,
|
||||
&witness_cols,
|
||||
@@ -55,6 +55,7 @@ pub fn generate<'a>(
|
||||
bit_constraints::determine_global_constraints(&fixed, identities);
|
||||
let mut generator = generator::Generator::new(
|
||||
&fixed,
|
||||
&mut fixed_lookup,
|
||||
identities,
|
||||
global_bit_constraints,
|
||||
machines,
|
||||
|
||||
Reference in New Issue
Block a user