- fn run(clauses: &Clauses) {
let mut state = DpllState::Running(Vec::new(), Assignment::new(), clauses.clone()); loop {
- match &state {
- DpllState::Unsat => {
- println!("UNSAT"); break;
} DpllState::Sat(trail) => {
println!("SAT {:?}", trail);
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; CIS352 -- P3 Builtins help | |
;; | |
;; I wrote up these notes based on some student meetings. | |
;; This project is intentionally a bit vague about how to | |
;; handle the builtins. That is because I want you to have | |
;; some ability to have the experience of figuring out how | |
;; you might want to engineer your own solution, considering | |
;; the various trade-offs. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; Consider the folllowing λ-calculus expression, write | |
;; a reduction sequence where each β reduction in the | |
;; sequence uses CBV evaluation order | |
((λ (x) x) | |
((λ (y) y) (λ (z) z))) | |
((λ (x) x) | |
((λ (z) (z z)) (λ (y) (y y)))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; CIS352 -- March 20, 2025 | |
;; For the past few lectures, we've talked about the idea of "in-context" β: | |
;; the idea that we can "just do all the βs." So for example: | |
((λ (b) b) | |
(((λ (x) x) (λ (a) a)) | |
((λ (y) y) (λ (z) z)))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; CIS 352 -- Spring '25 | |
;; March 18, 2025 | |
;; This week in class: | |
;; [ ] λ-calculus refresher | |
;; [ ] λ-calculus β reduction motivation | |
;; [ ] Extending the λ-calculus with numbers | |
;; [ ] Building an interpreter with closures |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; CIS352 -- Feb 25, 2025 | |
;; How do you calculate the transitive closure of a graph given using | |
;; the layout we've discussed? | |
;; | |
;; | |
;; Let's define a function `(step gr)`, which take a graph as |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; Algebraic Data II | |
;; | |
;; CIS352 2/6/25 | |
;; Note: for this lecture I am transliterating some very nice | |
;; notes from https://abhiroop.github.io/Haskell-Red-Black-Tree/ | |
;; (written by Abhiroop Sarkar) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#lang racket | |
;; 0 argument function which calls itself | |
;; (with zero arguments...) | |
(define (loop) (loop)) | |
(if #t 42 (loop)) | |
;; if cannot be a function, because if it were, |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
use std::collections::{HashMap, HashSet}; | |
type Clause = Vec<i32>; | |
type Clauses = HashSet<Clause>; | |
type Trail = Vec<TrailEntry>; | |
type Assignment = HashMap<i32, bool>; | |
#[derive(Debug, Clone)] | |
enum TrailEntry { | |
Decision(i32), |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; Traditional Abstract DPLL (no clause learning) | |
;; See this paper: https://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf | |
#lang racket | |
(define (clause? cl) | |
(match cl | |
[`(,(? integer? x) ...) #t] | |
[_ #f])) | |
NewerOlder