diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 12:13:13 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 12:13:23 -0600 |
| commit | 93f084750d8a76d63fc74d242944bce0635c2194 (patch) | |
| tree | 8b781cf252fb78e16158e307de973e61f6f331eb /proofs/signatures/th_arrays.plf | |
| parent | 9846e1db91243c3b507300dad318e81e28f9d4f4 (diff) | |
Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
Diffstat (limited to 'proofs/signatures/th_arrays.plf')
| -rwxr-xr-x | proofs/signatures/th_arrays.plf | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf new file mode 100755 index 000000000..6e0e6438d --- /dev/null +++ b/proofs/signatures/th_arrays.plf @@ -0,0 +1,53 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Arrays
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depdends on : th_base.plf
+
+; sorts
+
+(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element
+
+; functions
+(declare write (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (term (array s1 s2))))))))
+(declare read (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (term s2))))))
+
+; inference rules
+(declare row1 (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
+
+
+(declare row (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s1)
+ (! t4 (term s2)
+ (! u (th_holds (not (= _ t2 t3)))
+ (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
+
+(declare ext (! s1 sort
+ (! s2 sort
+ (! f formula
+ (! t1 (term (array s1 s2))
+ (! t2 (term (array s1 s2))
+ (! u (th_holds (not (= _ t1 t2)))
+ (! u1 (! k (term s1)
+ (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
+ (th_holds f)))
+ (th_holds f)))))))))
+
\ No newline at end of file |