This commit is contained in:
Alex Ozdemir
2021-02-16 12:27:18 -08:00
parent 6de075aef5
commit 3132977a23
5 changed files with 19 additions and 15 deletions

View File

@@ -168,7 +168,10 @@ mod test {
let b = mem.load(id0, bv_lit(1, 4));
let t = term![Op::BvBinPred(BvBinPred::Ugt); a, b];
cs.borrow_mut().assertions.push(t);
let sys = term(Op::BoolNaryOp(BoolNaryOp::And), cs.borrow().assertions.clone());
let sys = term(
Op::BoolNaryOp(BoolNaryOp::And),
cs.borrow().assertions.clone(),
);
assert!(check_sat(&sys))
}
}

View File

@@ -643,12 +643,19 @@ mod test {
("a".to_owned(), false),
("b.0".to_owned(), false),
("b.1".to_owned(), false),
].into_iter().collect();
let e = BoolPair { values: Some(values) };
]
.into_iter()
.collect();
let e = BoolPair {
values: Some(values),
};
let mut c = Circify::new(e);
c.declare("a".to_owned(), &Ty::Bool, true);
c.declare("b".to_owned(), &Ty::Pair(Box::new(Ty::Bool), Box::new(Ty::Bool)), true);
c.declare(
"b".to_owned(),
&Ty::Pair(Box::new(Ty::Bool), Box::new(Ty::Bool)),
true,
);
}
}
}

View File

@@ -221,4 +221,3 @@ impl Display for BitVector {
Ok(())
}
}

View File

@@ -11,4 +11,3 @@ pub fn to_width(t: &Term, w: usize) -> Term {
term(Op::BvExtract(w - 1, 0), vec![t.clone()])
}
}

View File

@@ -746,11 +746,11 @@ mod test {
use super::*;
use crate::ir::term::dist::test::*;
use crate::ir::term::dist::*;
use crate::target::r1cs::opt::reduce_linearities;
use quickcheck::{Arbitrary, Gen};
use quickcheck_macros::quickcheck;
use rand::distributions::Distribution;
use rand::SeedableRng;
use crate::target::r1cs::opt::reduce_linearities;
use std::sync::Arc;
#[test]
@@ -887,13 +887,9 @@ mod test {
#[test]
fn not_opt_test() {
let t = term![Op::Not; leaf_term(Op::Var("b".to_owned(), Sort::Bool))];
let values: HashMap<String, Value> =
vec![(
"b".to_owned(),
Value::Bool(true),
)]
.into_iter()
.collect();
let values: HashMap<String, Value> = vec![("b".to_owned(), Value::Bool(true))]
.into_iter()
.collect();
let v = eval(&t, &values);
let t = term![Op::Eq; t, leaf_term(Op::Const(v))];
let cs = Constraints {