Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Make builtins.rkt depend on the parser rather than the other way round

  • Loading branch information...
commit bdff332fbae935d2114a32324b8959adbd05ee8e 1 parent 81bcd8c
@sid0 authored
Showing with 29 additions and 27 deletions.
  1. +3 −7 builtins.rkt
  2. +20 −2 main.rkt
  3. +6 −18 parser.rkt
View
10 builtins.rkt
@@ -1,14 +1,10 @@
#lang racket/base
(require (prefix-in z3: "z3-wrapper.rkt")
- "utils.rkt")
+ "utils.rkt"
+ "parser.rkt")
(require racket/list)
-;; Helper function to make a symbol with the given name (Racket symbol)
-(define (make-symbol symbol-name)
- (z3:mk-string-symbol (ctx) (symbol->string symbol-name)))
-(provide make-symbol)
-
;; Initialize builtins. (The current context is assumed to be a parameter.)
(define (init-builtins)
(define-values (context vals sorts)
@@ -23,7 +19,7 @@
(for ([(k fn) (in-hash builtin-sorts)])
(new-sort k (fn context)))
;; XXX This is a giant hack and needs to be generalized.
- (define int-list-instance (z3:mk-list-sort (ctx) (make-symbol 'IntList) (get-sort 'Int)))
+ (define int-list-instance (z3:mk-list-sort (ctx) (smt:make-symbol 'IntList) (get-sort 'Int)))
(new-sort 'IntList (datatype-instance-z3-sort int-list-instance))
(hash-set! vals int-list-key int-list-instance))
(provide init-builtins)
View
22 main.rkt
@@ -1,8 +1,26 @@
#lang racket/base
-(require "parser.rkt"
+(require (prefix-in z3: "z3-wrapper.rkt")
+ "utils.rkt"
+ "parser.rkt"
"builtins.rkt")
+(define (make-config #:model? [model? #t])
+ (let ([config (z3:mk-config)])
+ (z3:set-param-value! config "MODEL" (if model? "true" "false"))
+ config))
+
+(define (smt:new-context-info #:model? [model? #t])
+ (define ctx (z3:mk-context (make-config #:model? model?)))
+ (define vals (make-hash))
+ (define sorts (make-hash))
+ (define new-info (z3ctx ctx vals sorts (box #f)))
+ (smt:with-context
+ new-info
+ (init-builtins))
+ new-info)
+
(provide
(all-from-out "parser.rkt"
- "builtins.rkt"))
+ "builtins.rkt")
+ smt:new-context-info)
View
24 parser.rkt
@@ -1,8 +1,7 @@
#lang racket/base
(require (prefix-in z3: "z3-wrapper.rkt")
- "utils.rkt"
- "builtins.rkt")
+ "utils.rkt")
(require racket/match
racket/contract/base)
@@ -20,21 +19,6 @@
(define (set-current-model! new-model)
(set-box! (z3ctx-current-model (current-context-info)) new-model))
-(define (make-config #:model? [model? #t])
- (let ([config (z3:mk-config)])
- (z3:set-param-value! config "MODEL" (if model? "true" "false"))
- config))
-
-(define (new-context-info #:model? [model? #t])
- (define ctx (z3:mk-context (make-config #:model? model?)))
- (define vals (make-hash))
- (define sorts (make-hash))
- (define new-info (z3ctx ctx vals sorts (box #f)))
- (with-context
- new-info
- (init-builtins))
- new-info)
-
(define-syntax-rule (with-context info body ...)
(parameterize ([current-context-info info])
body ...))
@@ -113,6 +97,10 @@
(for/list ([i (in-range 0 n)])
(make-uninterpreted (gensym) 'args ...)))
+;; Helper function to make a symbol with the given name (Racket symbol)
+(define (make-symbol symbol-name)
+ (z3:mk-string-symbol (ctx) (symbol->string symbol-name)))
+
;; We only support plain symbol for now
(define (constr->_z3-constructor expr)
(z3:mk-constructor (ctx)
@@ -163,13 +151,13 @@
smt:
(combine-out
with-context
- new-context-info
declare-datatypes
declare-sort
declare-fun
make-fun
make-fun/vector
make-fun/list
+ make-symbol
assert
check-sat
get-model))
Please sign in to comment.
Something went wrong with that request. Please try again.