#lang racket
(provide (all-defined-out))
(struct unsat-exn (smt))
(struct sat-exn (smt))
(define (strength? x)
(or (exact-nonnegative-integer? x)
(eqv? x +inf.0)))
(define sat-satisfy (lambda (t-state literal) t-state))
(define T-Satisfy (make-parameter sat-satisfy))
(define sat-propagate (lambda (t-state strength dimacslit) (values t-state empty)))
(define T-Propagate (make-parameter sat-propagate))
(define sat-explain (lambda (t-state strength lit) (error "[internal error] T-propogation shouldn't have happened")))
(define T-Explain (make-parameter sat-explain))
(define sat-consistent? (lambda (t-state strength) #t))
(define T-Consistent? (make-parameter sat-consistent?))
(define sat-backjump (lambda (t-state backjump-by-sats) #f))
(define T-Backjump (make-parameter sat-backjump))
(define sat-restart (lambda (t-state) t-state))
(define T-Restart (make-parameter sat-restart))