From f9a4fe48a4ec2355f8fec93d3f47242577df2511 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 5 Jan 2011 03:21:35 +0000 Subject: Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later. --- src/theory/arrays/kinds | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/theory/arrays/kinds') diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 4ad9c7463..7738f50ca 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -4,7 +4,11 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" +theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" + +properties polite stable-infinite + +rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" operator ARRAY_TYPE 2 "array type" @@ -13,3 +17,5 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" + +endtheory \ No newline at end of file -- cgit v1.2.3