diff options
Diffstat (limited to 'test')
42 files changed, 395 insertions, 133 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6a3f3d021..ad4e8a602 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -105,10 +105,9 @@ CVC_TESTS = \ wiki.19.cvc \ wiki.20.cvc \ wiki.21.cvc \ - simplification_bug3.cvc \ queries0.cvc \ - print_lambda.cvc \ - trim.cvc + trim.cvc \ + print_lambda.cvc # Regression tests for TPTP inputs TPTP_TESTS = @@ -167,6 +166,7 @@ BUG_TESTS = \ bug578.smt2 \ bug585.cvc \ bug586.cvc \ + bug590.smt2 \ bug595.cvc \ bug596.cvc \ bug596b.cvc @@ -180,7 +180,8 @@ DISABLED_TESTS = \ EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect + bug216.smt2.expect \ + bug590.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index c11d68780..a90b238e2 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -40,11 +40,17 @@ TESTS = \ swap_t1_np_nf_ai_00005_007.cvc.smt \ x2.smt \ x3.smt \ + bug272.smt \ + bug272.minimized.smt \ + constarr.smt2 \ + constarr2.smt2 \ + constarr3.smt2 \ + constarr.cvc \ + constarr2.cvc \ + constarr3.cvc \ parsing_ringer.cvc -EXTRA_DIST = $(TESTS) \ - bug272.smt \ - bug272.minimized.smt +EXTRA_DIST = $(TESTS) #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/arrays/constarr.cvc b/test/regress/regress0/arrays/constarr.cvc new file mode 100644 index 000000000..406a1ce2b --- /dev/null +++ b/test/regress/regress0/arrays/constarr.cvc @@ -0,0 +1,7 @@ +% EXPECT: unsat +all1 : ARRAY INT OF INT; +a, i : INT; +ASSERT all1 = ARRAY(INT OF INT) : 1; +ASSERT a = all1[i]; +ASSERT a /= 1; +CHECKSAT TRUE; diff --git a/test/regress/regress0/arrays/constarr.smt2 b/test/regress/regress0/arrays/constarr.smt2 new file mode 100644 index 000000000..b1fb02bed --- /dev/null +++ b/test/regress/regress0/arrays/constarr.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_ALIA) +(set-info :status unsat) +(declare-const all1 (Array Int Int)) +(declare-const a Int) +(declare-const i Int) +(assert (= all1 ((as const (Array Int Int)) 1))) +(assert (= a (select all1 i))) +(assert (not (= a 1))) +(check-sat) diff --git a/test/regress/regress0/arrays/constarr2.cvc b/test/regress/regress0/arrays/constarr2.cvc new file mode 100644 index 000000000..90ff11430 --- /dev/null +++ b/test/regress/regress0/arrays/constarr2.cvc @@ -0,0 +1,7 @@ +% EXPECT: unsat +all1, all2 : ARRAY INT OF INT; +a, i : INT; +ASSERT all1 = ARRAY(INT OF INT) : 1; +ASSERT all2 = ARRAY(INT OF INT) : 2; +ASSERT all1 = all2; +CHECKSAT; diff --git a/test/regress/regress0/arrays/constarr2.smt2 b/test/regress/regress0/arrays/constarr2.smt2 new file mode 100644 index 000000000..c84e6781a --- /dev/null +++ b/test/regress/regress0/arrays/constarr2.smt2 @@ -0,0 +1,10 @@ +(set-logic QF_ALIA) +(set-info :status unsat) +(declare-const all1 (Array Int Int)) +(declare-const all2 (Array Int Int)) +(declare-const a Int) +(declare-const i Int) +(assert (= all1 ((as const (Array Int Int)) 1))) +(assert (= all2 ((as const (Array Int Int)) 2))) +(assert (= all1 all2)) +(check-sat) diff --git a/test/regress/regress0/arrays/constarr3.cvc b/test/regress/regress0/arrays/constarr3.cvc new file mode 100644 index 000000000..bf5cf961c --- /dev/null +++ b/test/regress/regress0/arrays/constarr3.cvc @@ -0,0 +1,12 @@ +% EXIT: 1 +% EXPECT: Array theory solver does not yet support write-chains connecting two different constant arrays +% should be unsat +all1, all2 : ARRAY INT OF INT; +aa, bb : ARRAY INT OF INT; +a, i : INT; +ASSERT all1 = ARRAY(INT OF INT) : 1; +ASSERT aa = all1 WITH [i] := 0; +ASSERT all2 = ARRAY(INT OF INT) : 2; +ASSERT bb = all2 WITH [i] := 0; +ASSERT aa = bb; +CHECKSAT; diff --git a/test/regress/regress0/arrays/constarr3.smt2 b/test/regress/regress0/arrays/constarr3.smt2 new file mode 100644 index 000000000..d514fff70 --- /dev/null +++ b/test/regress/regress0/arrays/constarr3.smt2 @@ -0,0 +1,16 @@ +; EXIT: 1 +; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") +(set-logic QF_ALIA) +(set-info :status unsat) +(declare-const all1 (Array Int Int)) +(declare-const all2 (Array Int Int)) +(declare-const aa (Array Int Int)) +(declare-const bb (Array Int Int)) +(declare-const a Int) +(declare-const i Int) +(assert (= all1 ((as const (Array Int Int)) 1))) +(assert (= aa (store all1 i 0))) +(assert (= all2 ((as const (Array Int Int)) 2))) +(assert (= bb (store all2 i 0))) +(assert (= aa bb)) +(check-sat) diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc index c9f8c9e22..2c2018ecd 100644 --- a/test/regress/regress0/arrays/parsing_ringer.cvc +++ b/test/regress/regress0/arrays/parsing_ringer.cvc @@ -9,6 +9,11 @@ % EXPECT: sat % EXPECT: sat % EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: unsat +% EXPECT: sat PUSH; @@ -57,3 +62,33 @@ b : ARRAY INT OF INT; ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2; CHECKSAT; + +RESET; + +% more mixed stores, this time with constant arrays +z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #]; + +ASSERT z.y.1[1] /= 1; +ASSERT (# x:=ARRAY(INT OF [# x:INT #]):(# x:=0 #), y:=(ARRAY(INT OF INT):1, ARRAY(INT OF INT):5) #) = z; + +CHECKSAT; + +ASSERT z.x[0].x /= z.y.0[5]; + +CHECKSAT; + +ASSERT z.y.0[1] = z.x[5].x; + +CHECKSAT; + +ASSERT z.y.0[5] = z.x[-2].x; + +CHECKSAT; + +RESET; + +a : ARRAY INT OF INT; + +ASSERT a = a WITH [0]:=0, [1]:=1; + +CHECKSAT; diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2 index 5a5886940..fd7b4a7cc 100644 --- a/test/regress/regress0/bug421.smt2 +++ b/test/regress/regress0/bug421.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --incremental --abstract-values ; EXPECT: sat -; EXPECT: ((a @1) (b @2)) +; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2 index 82f566a64..aed7f7c05 100644 --- a/test/regress/regress0/bug421b.smt2 +++ b/test/regress/regress0/bug421b.smt2 @@ -4,7 +4,7 @@ ; ; COMMAND-LINE: --incremental --abstract-values --check-models ; EXPECT: sat -; EXPECT: ((a @1) (b @2)) +; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/bug567.smt2 b/test/regress/regress0/bug567.smt2 index 109940090..37403d8a3 100644 --- a/test/regress/regress0/bug567.smt2 +++ b/test/regress/regress0/bug567.smt2 @@ -1,7 +1,7 @@ (set-logic ALL_SUPPORTED) ; COMMAND-LINE: --incremental ; EXPECT: unknown -; EXPECT: unknown +; EXPECT: unsat ; EXPECT: unknown (declare-datatypes () ((OptInt0 (Some (value0 Int)) (None)))) (declare-datatypes () ((List0 (Cons (head0 Int) (tail0 List0)) (Nil)))) diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2 new file mode 100644 index 000000000..68665f629 --- /dev/null +++ b/test/regress/regress0/bug590.smt2 @@ -0,0 +1,61 @@ +(set-logic QF_ALL_SUPPORTED) +(set-option :strings-exp true) +(set-option :produce-models true) +(set-info :smt-lib-version 2.0) +(set-info :status unknown) + +(declare-fun text () String) +(declare-fun output () String) + +; html_escape_table = { +; "&": "&", +; '"': """, +; "'": "'", +; ">": ">", +; "<": "<", +; } +(declare-fun html_escape_table () (Array String String)) +(assert (= html_escape_table + (store (store (store (store (store ((as const (Array String String)) "A") + "&" "&") + "\"" """) + "'" "'") + ">" ">") + "<" "<"))) +(declare-fun html_escape_table_keys () (Array Int String)) +(assert (= html_escape_table_keys + (store (store (store (store (store ((as const (Array Int String)) "B") + 0 "&") + 1 "\"") + 2 "'") + 3 ">") + 4 "<"))) + +; charlst = [c for c in text] +(declare-fun charlst () (Array Int String)) +(declare-fun charlstlen () Int) +(assert (= charlstlen (str.len text))) +(assert (forall ((i Int)) + (= (select charlst i) (str.at text i)) +)) + +; charlst2 = [html_escape_table.get(c, c) for c in charlst] +(declare-fun charlst2 () (Array Int String)) +(declare-fun charlstlen2 () Int) +(assert (= charlstlen2 charlstlen)) +(assert (forall ((i Int)) + (or (or (< i 0) (>= i charlstlen2)) + (and (exists ((j Int)) + (= (select html_escape_table_keys j) (select charlst i)) + ) + (= (select charlst2 i) (select html_escape_table (select charlst i))) + ) + (and (not (exists ((j Int)) + (= (select html_escape_table_keys j) (select charlst i)) + )) + (= (select charlst2 i) (select charlst i)) + ) + ) +)) +(check-sat) +(get-value (charlst2)) diff --git a/test/regress/regress0/bug590.smt2.expect b/test/regress/regress0/bug590.smt2.expect new file mode 100644 index 000000000..3d57288cf --- /dev/null +++ b/test/regress/regress0/bug590.smt2.expect @@ -0,0 +1,2 @@ +% EXPECT: unknown +% EXPECT: ((charlst2 (store ((as const (Array Int String)) "C") 0 "<"))) diff --git a/test/regress/regress0/crash_burn_locusts.smt2 b/test/regress/regress0/crash_burn_locusts.smt2 new file mode 100644 index 000000000..313d6f79c --- /dev/null +++ b/test/regress/regress0/crash_burn_locusts.smt2 @@ -0,0 +1,29 @@ +;; This is a nasty parsing test for define-fun-rec + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(define-fun-rec ( + (f ((x Int)) Int 5) ;; ok, f : Int -> Int + (g ((x Int)) Int (h 4)) ;; um, ok, so g : Int -> Int and h : Int -> Int? + (h ((x Real)) Int 4) ;; oops no we were wrong, **CRASH** +)) + +(reset) + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(define-fun-rec ( + (f ((x Int)) Int (g (h 4) 5)) ;; ok, f : Int -> Int and g : Int -> X -> Int and h : Int -> X ??! What the F?! (pun intended) + (g ((x Int)) Int 5) ;; wait, now g has wrong arity?!! **BURN** + (h ((x Int)) Int 2) +)) + +(reset) + +(set-logic UFLIRA) +(set-info :smt-lib-version 2.5) +(declare-const g Int 2) +(define-fun-rec ( + (f () Int g) ;; wait, which g does this refer to?! **LOCUSTS** + (g () Int 5) +)) diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index c02a70819..05eb710df 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -59,7 +59,8 @@ TESTS = \ bug286.cvc \ bug438.cvc \ bug438b.cvc \ - wrong-sel-simp.cvc + wrong-sel-simp.cvc \ + tenum-bug.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/tenum-bug.smt2 b/test/regress/regress0/datatypes/tenum-bug.smt2 new file mode 100644 index 000000000..bf82c7b8c --- /dev/null +++ b/test/regress/regress0/datatypes/tenum-bug.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status sat) + +(declare-datatypes () ((DNat (dnat (data Nat))) + (Nat (succ (pred DNat)) (zero)))) + +(declare-fun x () Nat) + +(assert (not (= x zero))) + +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index e3bfd39b8..ca3907b0b 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -34,12 +34,12 @@ TESTS = \ fc-unsat-tot-2.smt2 \ fc-unsat-pent.smt2 \ fc-pigeonhole19.smt2 \ - Hoare-z3.931718.smt + Hoare-z3.931718.smt \ + bug0909.smt2 \ + lst-no-self-rev-exp.smt2 EXTRA_DIST = $(TESTS) -# disabled for now : -# bug0909.smt2 #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 new file mode 100644 index 000000000..5e1f3de30 --- /dev/null +++ b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) + +(declare-fun app (Lst Lst) Lst) +(declare-fun rev (Lst) Lst) + +(declare-sort I_app 0) +(declare-sort I_rev 0) + +(declare-fun a () I_app) +(declare-fun b () I_app) +(assert (not (= a b))) + +(declare-fun app_0_3 (I_app) Lst) +(declare-fun app_1_4 (I_app) Lst) +(declare-fun rev_0_5 (I_rev) Lst) + +(declare-fun xs () Lst) + +(assert (and + +(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) + +(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) + +(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) + +(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) ))) + +)) + +(check-sat) + diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am index 389c80e09..eb27e797b 100644 --- a/test/regress/regress0/parser/Makefile.am +++ b/test/regress/regress0/parser/Makefile.am @@ -19,7 +19,9 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - declarefun-emptyset-uf.smt2 + declarefun-emptyset-uf.smt2 \ + strings20.smt2 \ + strings25.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/parser/strings20.smt2 b/test/regress/regress0/parser/strings20.smt2 new file mode 100644 index 000000000..6e9ea4434 --- /dev/null +++ b/test/regress/regress0/parser/strings20.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (define-fun s () String "\"") +; EXPECT: ) + +(set-logic QF_S) +(set-info :smt-lib-version 2.0) +(set-option :produce-models true) + +(declare-fun s () String) + +(assert (= s "\"")) + +(check-sat) +(get-model) diff --git a/test/regress/regress0/parser/strings25.smt2 b/test/regress/regress0/parser/strings25.smt2 new file mode 100644 index 000000000..90602e67d --- /dev/null +++ b/test/regress/regress0/parser/strings25.smt2 @@ -0,0 +1,15 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (define-fun s () String """") +; EXPECT: ) + +(set-logic QF_S) +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) + +(declare-fun s () String) + +(assert (= s """")) + +(check-sat) +(get-model) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 7e8e1ea99..41f66f92f 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -43,7 +43,8 @@ TESTS = \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ bi-artm-s.smt2 \ - simp-typ-test.smt2 + simp-typ-test.smt2 \ + macros-int-real.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/macros-int-real.smt2 b/test/regress/regress0/quantifiers/macros-int-real.smt2 new file mode 100644 index 000000000..d29ddfe8f --- /dev/null +++ b/test/regress/regress0/quantifiers/macros-int-real.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: unknown +(set-logic AUFLIRA) + +(declare-fun round2 (Real) Int) +(assert (forall ((i Int)) (= (round2 (to_real i)) i))) + +(assert (= (round2 1.5) 1)) +(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/simplification_bug3.cvc b/test/regress/regress0/simplification_bug3.cvc deleted file mode 100644 index 3f0ddc537..000000000 --- a/test/regress/regress0/simplification_bug3.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% COMMAND-LINE: --simplification=incremental -x, y: BOOLEAN; -ASSERT x OR y; -ASSERT NOT x; -ASSERT NOT y; -% EXPECT: unsat -CHECKSAT; diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index ddc0eae7c..bd8e9ea93 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -23,6 +23,7 @@ TESTS = \ bug001.smt2 \ cardinality.smt2 \ escchar.smt2 \ + escchar_25.smt2 \ str001.smt2 \ str002.smt2 \ str003.smt2 \ @@ -30,7 +31,6 @@ TESTS = \ str005.smt2 \ str006.smt2 \ str007.smt2 \ - fmf001.smt2 \ fmf002.smt2 \ type001.smt2 \ type003.smt2 \ @@ -53,6 +53,7 @@ TESTS = \ FAILING_TESTS = EXTRA_DIST = $(TESTS) \ + fmf001.smt2 \ regexp002.smt2 \ type002.smt2 diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2 index 508d7f3c1..aa2afb7e4 100644 --- a/test/regress/regress0/strings/escchar.smt2 +++ b/test/regress/regress0/strings/escchar.smt2 @@ -1,5 +1,6 @@ (set-logic QF_S)
(set-info :status sat)
+(set-info :smt-lib-version 2.0)
(declare-fun x () String)
(declare-const I Int)
diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2 new file mode 100644 index 000000000..f48995344 --- /dev/null +++ b/test/regress/regress0/strings/escchar_25.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S)
+(set-info :status sat)
+(set-info :smt-lib-version 2.5)
+
+(declare-fun x () String)
+(declare-const I Int)
+
+(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b"))
+(assert (= I (str.len x)))
+
+
+(check-sat)
diff --git a/test/regress/run_regression b/test/regress/run_regression index 4118e3bf6..062458055 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -41,6 +41,10 @@ while [ $# -gt 2 ]; do shift done +[[ "$VALGRIND" = "1" ]] && { + wrapper="libtool --mode=execute valgrind $wrapper" +} + cvc4=$1 benchmark_orig=$2 benchmark="$benchmark_orig" @@ -250,7 +254,15 @@ fi # we have to actual error file same treatment as other files. differences in # versions of echo/bash were causing failure on some platforms and not on others +# (also grep out valgrind output, if 0 errors reported by valgrind) actual_error=$(cat $errfile) +if [[ "$VALGRIND" = "1" ]]; then + #valgrind_output=$(cat $errfile|grep -E "^==[0-9]+== "|) + valgrind_num_errors=$(cat $errfile|grep -E "^==[0-9]+== "|tail -n1|awk '{print $4}') + echo "valgrind errors (not suppressed): $valgrind_num_errors" 1>&2 + + ((valgrind_num_errors == 0)) && actual_error=$(echo "$actual_error"|grep -vE "^==[0-9]+== ") +fi if [ -z "$actual_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h index 91e12a25e..4daab5cce 100644 --- a/test/unit/context/stacking_map_black.h +++ b/test/unit/context/stacking_map_black.h @@ -39,8 +39,8 @@ class StackingMapBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_ctxt = new Context(); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); d_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(d_ctxt); diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h index c7e185735..35305e469 100644 --- a/test/unit/context/stacking_vector_black.h +++ b/test/unit/context/stacking_vector_black.h @@ -39,8 +39,8 @@ class StackingVectorBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_ctxt = new Context(); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); d_vectorPtr = new StackingVector<TNode>(d_ctxt); diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 8fee6571d..5f9a7ebce 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -26,31 +26,35 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/attribute.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC4::smt; using namespace std; class AttributeBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; + ExprManager* d_exprManager; NodeManager* d_nodeManager; - NodeManagerScope* d_scope; + SmtEngine* d_smtEngine; + SmtScope* d_scope; public: void setUp() { - d_ctxt = new Context; - d_nodeManager = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nodeManager); + d_exprManager = new ExprManager(); + d_nodeManager = NodeManager::fromExprManager(d_exprManager); + d_smtEngine = new SmtEngine(d_exprManager); + d_scope = new SmtScope(d_smtEngine); } void tearDown() { delete d_scope; - delete d_nodeManager; - delete d_ctxt; + delete d_smtEngine; + delete d_exprManager; } class MyData { diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 11063cd1b..00ebc8b8d 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -18,7 +18,6 @@ #include <string> -#include "context/context.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" @@ -29,10 +28,12 @@ #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "util/cvc4_assert.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; +using namespace CVC4::smt; using namespace CVC4::expr; using namespace CVC4::expr::attr; using namespace std; @@ -60,26 +61,27 @@ typedef CDAttribute<Test2, bool> TestFlag2cd; class AttributeWhite : public CxxTest::TestSuite { - Context* d_ctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtScope* d_scope; TypeNode* d_booleanType; + SmtEngine* d_smtEngine; public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); - + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smtEngine = new SmtEngine(d_em); + d_scope = new SmtScope(d_smtEngine); d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { delete d_booleanType; delete d_scope; - delete d_nm; - delete d_ctxt; + delete d_smtEngine; + delete d_em; } void testAttributeIds() { @@ -145,7 +147,6 @@ public: lastId = attr::LastAttributeId<TypeNode, false>::getId(); TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId); - } void testCDAttributes() { @@ -162,7 +163,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 1 + d_smtEngine->push(); // level 1 // test that all boolean flags are FALSE to start Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; @@ -204,7 +205,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 2 + d_smtEngine->push(); // level 2 Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); @@ -225,7 +226,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->push(); // level 3 + d_smtEngine->push(); // level 3 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -244,7 +245,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be T)\n"; TS_ASSERT(c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 2 + d_smtEngine->pop(); // level 2 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -253,7 +254,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 1 + d_smtEngine->pop(); // level 1 Debug("cdboolattr") << "get flag 1 on a (should be T)\n"; TS_ASSERT(a.getAttribute(TestFlag1cd())); @@ -262,7 +263,7 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); - d_ctxt->pop(); // level 0 + d_smtEngine->pop(); // level 0 Debug("cdboolattr") << "get flag 1 on a (should be F)\n"; TS_ASSERT(! a.getAttribute(TestFlag1cd())); @@ -271,13 +272,11 @@ public: Debug("cdboolattr") << "get flag 1 on c (should be F)\n"; TS_ASSERT(! c.getAttribute(TestFlag1cd())); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException ); } void testAttributes() { - //Debug.on("bootattr"); + //Debug.on("boolattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 9f8ecb69e..7d6ee523a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -28,14 +28,12 @@ using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace std; class NodeBlack : public CxxTest::TestSuite { private: Options opts; - Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -51,8 +49,7 @@ public: free(argv[0]); free(argv[1]); - d_ctxt = new Context(); - d_nodeManager = new NodeManager(d_ctxt, NULL, opts); + d_nodeManager = new NodeManager(NULL, opts); d_scope = new NodeManagerScope(d_nodeManager); d_booleanType = new TypeNode(d_nodeManager->booleanType()); d_realType = new TypeNode(d_nodeManager->realType()); @@ -62,7 +59,6 @@ public: delete d_booleanType; delete d_scope; delete d_nodeManager; - delete d_ctxt; } bool imp(bool a, bool b) const { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index c71ba48c5..9bac0d818 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -25,19 +25,16 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" -#include "context/context.h" #include "util/cvc4_assert.h" #include "util/rational.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -47,8 +44,7 @@ private: public: void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); specKind = AND; @@ -63,7 +59,6 @@ public: delete d_realType; delete d_scope; delete d_nm; - delete d_ctxt; } diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 9ca086d06..b94e6a691 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -21,7 +21,6 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" -#include "context/context.h" #include "util/rational.h" #include "util/integer.h" @@ -29,26 +28,22 @@ using namespace CVC4; using namespace CVC4::expr; using namespace CVC4::kind; -using namespace CVC4::context; class NodeManagerBlack : public CxxTest::TestSuite { - Context* d_context; NodeManager* d_nodeManager; NodeManagerScope* d_scope; public: void setUp() { - d_context = new Context; - d_nodeManager = new NodeManager(d_context, NULL); + d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { delete d_scope; delete d_nodeManager; - delete d_context; } void testMkNodeNot() { diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 7bc279f47..aaa3256dd 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -19,33 +19,28 @@ #include <string> #include "expr/node_manager.h" -#include "context/context.h" #include "util/rational.h" #include "util/integer.h" using namespace CVC4; using namespace CVC4::expr; -using namespace CVC4::context; class NodeManagerWhite : public CxxTest::TestSuite { - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; public: void setUp() { - d_ctxt = new Context(); - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; - delete d_ctxt; } void testMkConstRational() { diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 9f90bd1b0..7240deed5 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -16,14 +16,12 @@ #include <cxxtest/TestSuite.h> -#include "context/context.h" #include "expr/node.h" #include "expr/node_self_iterator.h" #include "expr/node_builder.h" #include "expr/convenience_node_builders.h" using namespace CVC4; -using namespace CVC4::context; using namespace CVC4::kind; using namespace CVC4::expr; using namespace std; @@ -31,7 +29,6 @@ using namespace std; class NodeSelfIteratorBlack : public CxxTest::TestSuite { private: - Context* d_ctxt; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -40,8 +37,7 @@ private: public: void setUp() { - d_ctxt = new Context; - d_nodeManager = new NodeManager(d_ctxt, NULL); + d_nodeManager = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nodeManager); d_booleanType = new TypeNode(d_nodeManager->booleanType()); d_realType = new TypeNode(d_nodeManager->realType()); @@ -51,7 +47,6 @@ public: delete d_booleanType; delete d_scope; delete d_nodeManager; - delete d_ctxt; } void testSelfIteration() { diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index bcb3155e1..8a68db269 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -22,33 +22,28 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node.h" -#include "context/context.h" #include "util/cvc4_assert.h" using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::context; using namespace CVC4::expr; using namespace std; class NodeWhite : public CxxTest::TestSuite { - Context* d_ctxt; NodeManager* d_nm; NodeManagerScope* d_scope; public: void setUp() { - d_ctxt = new Context(); - d_nm = new NodeManager(d_ctxt, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; - delete d_ctxt; } void testNull() { diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 665126059..db49e2521 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -67,7 +67,7 @@ public: return d_nextVar++; } - void addClause(SatClause& c, bool lemma) { + void addClause(SatClause& c, bool lemma, uint64_t) { d_addClauseCalled = true; } @@ -93,6 +93,10 @@ public: void renewVar(SatLiteral lit, int level = -1) { } + bool spendResource() { + return false; + } + void interrupt() { } @@ -179,7 +183,7 @@ public: Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false); + d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c), false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -196,19 +200,19 @@ public: d_nodeManager->mkNode(kind::IFF, d_nodeManager->mkNode(kind::OR, c, d), d_nodeManager->mkNode(kind::NOT, - d_nodeManager->mkNode(kind::XOR, e, f)))), false, false ); + d_nodeManager->mkNode(kind::XOR, e, f)))), false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testTrue() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } void testFalse() { NodeManagerScope nms(d_nodeManager); - d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -216,7 +220,7 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IFF, a, b), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -224,7 +228,7 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -241,14 +245,14 @@ public: // d_nodeManager->mkVar(d_nodeManager->integerType()) // ), // d_nodeManager->mkVar(d_nodeManager->integerType()) - // ), false, false); + // ), false, false, RULE_INVALID, Node::null()); // //} void testNot() { NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::NOT, a), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -257,7 +261,7 @@ public: Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node c = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::OR, a, b, c), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -265,10 +269,10 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert(a, false, false); + d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); d_satSolver->reset(); - d_cnfStream->convertAndAssert(b, false, false); + d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null()); TS_ASSERT( d_satSolver->addClauseCalled() ); } @@ -276,7 +280,7 @@ public: NodeManagerScope nms(d_nodeManager); Node a = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); - d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false ); + d_cnfStream->convertAndAssert( d_nodeManager->mkNode(kind::XOR, a, b), false, false, RULE_INVALID, Node::null() ); TS_ASSERT( d_satSolver->addClauseCalled() ); } diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 3dcb2db85..d9963f78c 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -218,41 +218,27 @@ std::cout<<"here\n"; Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons")); Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil")); Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red")); + Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange")); + Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow")); TS_ASSERT_EQUALS(*te, nil); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); TS_ASSERT( ! te.isFinished() ); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)); TS_ASSERT( ! te.isFinished() ); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))); + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); TS_ASSERT( ! te.isFinished() ); - TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil)); TS_ASSERT( ! te.isFinished() ); TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, - d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))))); + d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil))); TS_ASSERT( ! te.isFinished() ); } diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index e2937ccb2..db02ce207 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -14,7 +14,6 @@ ** Black box testing of CVC4::BooleanSimplification. **/ -#include "context/context.h" #include "util/language.h" #include "expr/node.h" #include "expr/kind.h" @@ -26,12 +25,10 @@ #include <set> using namespace CVC4; -using namespace CVC4::context; using namespace std; class BooleanSimplificationBlack : public CxxTest::TestSuite { - Context* d_context; NodeManager* d_nm; NodeManagerScope* d_scope; @@ -70,8 +67,7 @@ class BooleanSimplificationBlack : public CxxTest::TestSuite { public: void setUp() { - d_context = new Context(); - d_nm = new NodeManager(d_context, NULL); + d_nm = new NodeManager(NULL); d_scope = new NodeManagerScope(d_nm); a = d_nm->mkSkolem("a", d_nm->booleanType()); @@ -116,7 +112,6 @@ public: delete d_scope; delete d_nm; - delete d_context; } void testNegate() { |