- 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 -- 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])) | |
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 | |
;; Direct style | |
(define (filter f l) | |
(match l | |
['() '()] | |
[`(,hd . ,tl) (if (f hd) (cons hd (filter f tl)) (filter f tl))])) | |
;; Tail recursive version | |
(define (filter-tl f l) |
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 | |
(provide (all-defined-out)) | |
;; | |
;; CIS352 (Fall '24) Racket Warmup | |
;; | |
(define (square x) (* x x)) | |
;; return the Euclidian distance between x0,y0 and x1,y1 | |
(define (euclid-distance x0 y0 x1 y1) |
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
;; Relational algebra | |
#lang racket | |
(define relation? symbol?) | |
(define atom? symbol?) ;; atomic lits are symbols | |
;; variables must be explicitly tagged, not 'x, but '(var x) | |
(define (var? x) (match x [`(var ,(? symbol? x)) #t] [_ #f])) | |
(define (var-or-atom? x) (or (atom? x) (var? x))) |
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
;; Challenge: find all the bugs in this small functional compiler | |
#lang racket | |
(provide (all-defined-out)) | |
(define verbose-mode (make-parameter #t)) | |
(define i-am-a-mac (make-parameter #f)) | |
;; | |
;; Our compiler will have several layers |
NewerOlder