summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/simple-rdl-definefun.smt29
-rw-r--r--test/unit/parser/parser_black.h1
-rw-r--r--test/unit/parser/parser_builder_black.h1
3 files changed, 7 insertions, 4 deletions
diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2
index 08e99867a..6b38c6a70 100644
--- a/test/regress/regress0/simple-rdl-definefun.smt2
+++ b/test/regress/regress0/simple-rdl-definefun.smt2
@@ -1,14 +1,15 @@
(set-logic QF_RDL)
(set-info :status unsat)
+(set-info :notes | Simple test, based on simple-rdl.smt2, of define-sort and define-fun |)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-sort U 0)
-(declare-sort A 2)
-(define-sort F (x) (A Real Real))
+(define-sort A (x y) y)
+(define-sort F (x) (A x x))
(declare-fun x2 () (F Real))
-(define-fun minus ((x Real) (z Real)) Real (- x z))
+(define-fun minus ((x Real) (z Real)) (A (A U Bool) (A (F U) Real)) (- x z))
(define-fun less ((x Real) (z Real)) Bool (< x z))
-(define-fun foo ((x Real) (z Real)) Bool (less x z))
+(define-fun foo ((x (F Real)) (z (A U Real))) (F (F Bool)) (less x z))
(assert (not (=> (foo (minus x y) 0) (less x y))))
(check-sat)
(exit)
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 88a6eaf57..4f55edad5 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -32,6 +32,7 @@
using namespace CVC4;
using namespace CVC4::parser;
+using namespace CVC4::language::input;
using namespace std;
class ParserBlack {
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index b130501f5..c661f00d9 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -34,6 +34,7 @@ typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu;
using namespace CVC4;
using namespace CVC4::parser;
+using namespace CVC4::language::input;
using namespace std;
class ParserBuilderBlack : public CxxTest::TestSuite {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback