- 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 |
This file contains hidden or 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 | |
| ;; v0.0 April 8, 2024 -- WORKING NOTES (could have bugs!) | |
| ;; Apply/Eval Refactoring -- Semantics Homework | |
| ;; | |
| ;; Kris Micinski (kkmicins@syr.edu and krismicinski@gmail.com) | |
| ;; | |
| ;; Warning: may be buggy, please contact kris if you notice | |
| ;; obvious bugs. | |
| (provide (all-defined-out)) |
This file contains hidden or 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 | |
| ;; The Church-encoded number N is represented as: | |
| ;; - A function (λ (f) ...) which takes a function f | |
| ;; - Returns a function which accepts an argument x | |
| ;; and applies f N times to x | |
| ;; two, Church-encoded as a *Racket* lambda | |
| (λ (f) (λ (x) (f (f x)))) |