rpms/cvc4
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Initial import.

Browse Source
This commit is contained in:
Jerry James 2014-02-03 07:53:17 -07:00
parent a626dad0b0
commit b98f57bca0
7 changed files with 1015 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -0,0 +1 @@
/cvc4-1.3.tar.gz

263
cvc4-doxygen.patch Normal file
View File

@ -0,0 +1,263 @@
--- ./src/decision/options.h.orig 2013-12-06 16:07:43.586866550 -0700
+++ ./src/decision/options.h 2013-12-06 16:07:43.586866550 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file decision/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/expr/expr_manager_template.h.orig 2013-12-03 15:24:58.911994034 -0700
+++ ./src/expr/expr_manager_template.h 2013-12-03 15:24:58.911994034 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.h
+/*! \file expr_manager.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/expr_template.h.orig 2013-11-27 09:42:59.916302990 -0700
+++ ./src/expr/expr_template.h 2013-11-27 09:42:59.916302990 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_template.h
+/*! \file expr.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/kind_template.h.orig 2013-11-11 10:21:58.180347624 -0700
+++ ./src/expr/kind_template.h 2013-11-11 10:21:58.180347624 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file kind_template.h
+/*! \file kind.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/options.h.orig 2013-12-06 16:07:22.010279788 -0700
+++ ./src/expr/options.h 2013-12-06 16:07:22.010279788 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file expr/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/main/options.h.orig 2013-12-06 16:07:45.234911367 -0700
+++ ./src/main/options.h 2013-12-06 16:07:45.234911367 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file main/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options.h.orig 2013-12-06 16:07:21.118255532 -0700
+++ ./src/options/base_options.h 2013-12-06 16:07:21.118255532 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file options/base_options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options_template.h.orig 2013-11-11 10:21:58.276350312 -0700
+++ ./src/options/base_options_template.h 2013-11-11 10:21:58.276350312 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file base_options_template.h
+/*! \file options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/options.h.orig 2013-11-11 10:21:58.284350536 -0700
+++ ./src/options/options.h 2013-11-11 10:21:58.284350536 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file options.h
+/*! \file options/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/parser/options.h.orig 2013-12-06 16:07:46.070934102 -0700
+++ ./src/parser/options.h 2013-12-06 16:07:46.070934102 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file parser/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/printer/options.h.orig 2013-12-06 16:07:39.042742975 -0700
+++ ./src/printer/options.h 2013-12-06 16:07:39.042742975 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file printer/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/proof/options.h.orig 2013-12-06 16:07:38.522728834 -0700
+++ ./src/proof/options.h 2013-12-06 16:07:38.522728834 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file proof/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/prop/options.h.orig 2013-12-06 16:07:38.086716977 -0700
+++ ./src/prop/options.h 2013-12-06 16:07:38.086716977 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file prop/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/smt/options.h.orig 2013-12-06 16:07:42.546838267 -0700
+++ ./src/smt/options.h 2013-12-06 16:07:42.546838267 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file smt/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arith/options.h.orig 2013-12-06 16:07:28.406453727 -0700
+++ ./src/theory/arith/options.h 2013-12-06 16:07:28.406453727 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/arith/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arrays/options.h.orig 2013-12-06 16:07:31.002524327 -0700
+++ ./src/theory/arrays/options.h 2013-12-06 16:07:31.002524327 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/arrays/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/booleans/options.h.orig 2013-12-06 16:07:22.494292954 -0700
+++ ./src/theory/booleans/options.h 2013-12-06 16:07:22.494292954 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/booleans/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/builtin/options.h.orig 2013-12-06 16:07:25.114364203 -0700
+++ ./src/theory/builtin/options.h 2013-12-06 16:07:25.114364203 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/builtin/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/bv/options.h.orig 2013-12-06 16:07:24.114337006 -0700
+++ ./src/theory/bv/options.h 2013-12-06 16:07:24.114337006 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/bv/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/datatypes/options.h.orig 2013-12-06 16:07:24.714353323 -0700
+++ ./src/theory/datatypes/options.h 2013-12-06 16:07:24.714353323 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/datatypes/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/options.h.orig 2013-12-06 16:07:23.074308723 -0700
+++ ./src/theory/options.h 2013-12-06 16:07:23.074308723 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/quantifiers/options.h.orig 2013-12-06 16:07:35.278640613 -0700
+++ ./src/theory/quantifiers/options.h 2013-12-06 16:07:35.278640613 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/quantifiers/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/rewriterules/options.h.orig 2013-12-06 16:07:35.926658235 -0700
+++ ./src/theory/rewriterules/options.h 2013-12-06 16:07:35.926658235 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/rewriterules/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/uf/options.h.orig 2013-12-06 16:07:30.142500939 -0700
+++ ./src/theory/uf/options.h 2013-12-06 16:07:30.142500939 -0700
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/uf/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/util/tls.h.in.orig 2013-12-03 13:43:42.822811181 -0700
+++ ./src/util/tls.h.in 2013-12-03 13:43:42.822811181 -0700
@@ -1,5 +1,5 @@
/********************* */
-/*! \file tls.h.in
+/*! \file tls.h
** \verbatim
** Original author: ACSYS
** Major contributors: Morgan Deters

203
cvc4.spec Normal file
View File

@ -0,0 +1,203 @@
Name: cvc4
Version: 1.3
Release: 2%{?dist}
Summary: Automatic theorem prover for SMT problems
# License breakdown:
# - Files containing code under the Boost license:
# o src/util/channel.h
# o examples/hashsmt/sha1.hpp
# - Files containing code under the BSD license:
# o src/parser/antlr_input_imports.cpp
# o src/parser/bounded_token_buffer.cpp
# - All other files are distributed under the MIT license
License: MIT and BSD and Boost
URL: http://cvc4.cs.nyu.edu/web/
Source0: http://cvc4.cs.nyu.edu/builds/src/%{name}-%{version}.tar.gz
# Updated *.plf files from upstream. These are needed only for the self-tests.
Source1: smt.plf
Source2: sat.plf
Source3: th_base.plf
# Fix some doxygen problems. Upstream plans to fix this differently.
Patch0: %{name}-doxygen.patch
BuildRequires: antlr3-C-devel
BuildRequires: antlr3-tool
BuildRequires: boost-devel
BuildRequires: chrpath
BuildRequires: cxxtest
BuildRequires: doxygen-latex
BuildRequires: ghostscript
BuildRequires: glpk-devel
BuildRequires: gmp-devel
BuildRequires: gperftools-devel
BuildRequires: java-devel >= 1:1.6.0
BuildRequires: jpackage-utils
BuildRequires: lfsc
BuildRequires: perl
BuildRequires: python
BuildRequires: readline-devel
BuildRequires: swig
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
Requires: lfsc
%description
CVC4 is an efficient open-source automatic theorem prover for
satisfiability modulo theories (SMT) problems. It can be used to prove
the validity (or, dually, the satisfiability) of first-order formulas in
a large number of built-in logical theories and their combination.
CVC4 is the fourth in the Cooperating Validity Checker family of tools
(CVC, CVC Lite, CVC3) but does not directly incorporate code from any
previous version. A joint project of NYU and U Iowa, CVC4 aims to
support the features of CVC3 and SMT-LIBv2 while optimizing the design
of the core system architecture and decision procedures to take
advantage of recent engineering and algorithmic advances.
CVC4 is intended to be an open and extensible SMT engine, and it can be
used as a stand-alone tool or as a library, with essentially no limit on
its use for research or commercial purposes.
%package devel
Summary: Headers and other files for developing with %{name}
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
%description devel
Header files and library links for developing applications that use %{name}.
%package doc
Summary: Interface documentation for %{name}
BuildArch: noarch
%description doc
Interface documentation for %{name}.
%package libs
Summary: Library containing an automatic theorem prover for SMT problems
%description libs
Library containing the core of the %{name} automatic theorem prover for
SMT problems.
%package java
Summary: Java interface to %{name}
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
Requires: java-headless
Requires: jpackage-utils
%description java
Java interface to %{name}.
%prep
%setup -q
# The rpm patch macro doesn't understand -T, and we need to it to avoid
# regenerating the very files we're trying to patch.
patch -p0 -T < %{PATCH0}
# Don't change the build flags we want to use and avoid hardcoded rpaths
sed -e '/^if test "$enable_debug_symbols"/,/fi/d' \
-e 's|^hardcode_libdir_flag_spec=.*|hardcode_libdir_flag_spec=""|g' \
-e 's|^runpath_var=LD_RUN_PATH|runpath_var=DIE_RPATH_DIE|g' \
-i configure
# Change the Java installation paths for Fedora
sed -i "s|^\(javalibdir =.*\)jni|\1java/%{name}|" src/bindings/Makefile.in
%build
%configure --enable-proof --enable-language-bindings=all --with-portfolio \
--with-glpk --with-google-perftools --without-compat \
CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -DFEDORA_GLPK_ITCNT -Dlpx_get_int_parm(x,y)=glp_get_it_cnt(x)" \
LFSCARGS="%{_datadir}/lfsc/sat.plf"
# Workaround libtool reordering -Wl,--as-needed after all the libraries
sed -i 's/CC=.g../& -Wl,--as-needed/' builds/*-linux-gnu/default-proof/libtool
# Workaround insufficiently quoted CPPFLAGS
find builds -name Makefile | xargs sed -i 's/-Dlpx.*glp_get_it_cnt(x)/"&"/'
make %{?_smp_mflags}
make doc
%install
%make_install
# Remove unwanted libtool files
find %{buildroot}%{_libdir} -name \*.la | xargs rm -f
# Remove empty directories for language bindings that do not yet exist
rm -fr %{buildroot}%{_libdir}/{csharp,ocaml,perl5,php,pyshared,ruby,tcltk}
rm -fr %{buildroot}%{_datadir}/{csharp,perl5,php,pyshared}
# Make the Java installation match Fedora requirements
if [ "%{_libdir}/java" != "%{_jnidir}" ]; then
mkdir -p %{buildroot}%{_jnidir}
mv %{buildroot}%{_libdir}/java/cvc4 %{buildroot}%{_jnidir}
rmdir %{buildroot}%{_libdir}/java
fi
# Remove still more hardcoded rpaths
chrpath -d %{buildroot}%{_bindir}/* \
%{buildroot}%{_libdir}/lib%{name}*.so.*.*.* \
%{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.*
# Help the debuginfo generator
BUILDS=builds/*-redhat-linux-gnu
for dir in decision expr main parser printer prop smt theory theory/arith \
theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \
theory/quantifiers theory/rewriterules theory/strings theory/uf; do
ln -s $PWD/src/$dir/options $BUILDS/default-proof/src/$dir
done
ln -s default-proof/src $BUILDS
ln -s $PWD/src/options/base_options $BUILDS/default-proof/src/options
ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options
ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options
ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options
ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt
%post libs -p /usr/sbin/ldconfig
%postun libs -p /usr/sbin/ldconfig
%check
# The tests use a large amount of stack space
ulimit -s unlimited
# The tests require unreleased *.plf files from upstream
for mk in $(find builds/*-redhat-linux-gnu/default-proof/test -name Makefile)
do
sed -e 's,^\(LFSCARGS =\).*,\1 %{SOURCE1} %{SOURCE2} %{SOURCE3},' \
-e 's,^\(TESTS_ENVIRONMENT = LFSC=\)".*",\1"lfsc %{SOURCE1} %{SOURCE2} %{SOURCE3}",' \
-i $mk
done
make check
%files
%doc AUTHORS NEWS README RELEASE-NOTES THANKS
%{_bindir}/*
%{_mandir}/man1/*
%{_mandir}/man5/*
%files doc
%doc doc/doxygen/*
%files libs
%doc COPYING
%{_libdir}/lib%{name}*.so.*
%files devel
%{_includedir}/%{name}/
%{_libdir}/lib%{name}*.so
%{_mandir}/man3/*
%files java
%{_javadir}/*.jar
%{_jnidir}/%{name}/
%changelog
* Mon Jan 27 2014 Jerry James <loganjerry@gmail.com> - 1.3-2
- Install JNI objects in %%{_jnidir}
* Wed Jan 22 2014 Jerry James <loganjerry@gmail.com> - 1.3-1
- Initial RPM

127
sat.plf Normal file
View File

@ -0,0 +1,127 @@
(declare bool type)
(declare tt bool)
(declare ff bool)
(declare var type)
(declare lit type)
(declare pos (! x var lit))
(declare neg (! x var lit))
(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))
; constructs for general clauses for R, Q, satlem
(declare concat (! c1 clause (! c2 clause clause)))
(declare clr (! l lit (! c clause clause)))
; code to check resolutions
(program append ((c1 clause) (c2 clause)) clause
(match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
; we use marks as follows:
; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
; -- mark 3 if we did indeed remove the variable positively
; -- mark 4 if we did indeed remove the variable negatively
(program simplify_clause ((c clause)) clause
(match c
(cln cln)
((clc l c1)
(match l
; Set mark 1 on v if it is not set, to indicate we should remove it.
; After processing the rest of the clause, set mark 3 if we were already
; supposed to remove v (so if mark 1 was set when we began). Clear mark3
; if we were not supposed to be removing v when we began this call.
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked3 v v (markvar3 v)) c'))
(ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
; the same as the code for tt, but using different marks.
((neg v)
(let m (ifmarked2 v tt (do (markvar2 v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked4 v v (markvar4 v)) c'))
(ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
((clr l c1)
(match l
; set mark 1 to indicate we should remove v, and fail if
; mark 3 is not set after processing the rest of the clause
; (we will set mark 3 if we remove a positive occurrence of v).
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
(match m (tt v) (ff (markvar v))) c')
(fail clause))))))
; same as the tt case, but with different marks.
((neg v)
(let m2 (ifmarked2 v tt (do (markvar2 v) ff))
(let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
(match m2 (tt v) (ff (markvar2 v))) c')
(fail clause))))))
))))
; resolution proofs
(declare holds (! c clause type))
(declare R (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat (clr (pos n) c1)
(clr (neg n) c2)))))))))
(declare Q (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat (clr (neg n) c1)
(clr (pos n) c2)))))))))
(declare satlem_simplify
(! c1 clause
(! c2 clause
(! c3 clause
(! u1 (holds c1)
(! r (^ (simplify_clause c1) c2)
(! u2 (! x (holds c2) (holds c3))
(holds c3))))))))
(declare satlem
(! c clause
(! c2 clause
(! u (holds c)
(! u2 (! v (holds c) (holds c2))
(holds c2))))))
; A little example to demonstrate simplify_clause.
; It can handle nested clr's of both polarities,
; and correctly cleans up marks when it leaves a
; clr or clc scope. Uncomment and run with
; --show-runs to see it in action.
;
; (check
; (% v1 var
; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
; (clc (pos v1) (clc (pos v1) cln))))
; (satlem _ _ _ u1 (\ x x))))))
;(check
; (% v1 var
; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
; (clr (neg v1) (clc (neg v1) cln)))))
; (satlem _ _ _ u1 (\ x x))))))

313
smt.plf Normal file
View File

@ -0,0 +1,313 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare formula type)
(declare th_holds (! f formula type))
; constants
(declare true formula)
(declare false formula)
; logical connectives
(declare not (! f formula formula))
(declare and (! f1 formula (! f2 formula formula)))
(declare or (! f1 formula (! f2 formula formula)))
(declare impl (! f1 formula (! f2 formula formula)))
(declare iff (! f1 formula (! f2 formula formula)))
(declare xor (! f1 formula (! f2 formula formula)))
(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
; terms
(declare sort type) ; sort in the theory
(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor
(declare term (! t sort type)) ; declared terms in formula
(declare apply (! s1 sort
(! s2 sort
(! t1 (term (arrow s1 s2))
(! t2 (term s1)
(term s2))))))
(declare ite (! s sort
(! f formula
(! t1 (term s)
(! t2 (term s)
(term s))))))
; let/flet
(declare let (! s sort
(! t (term s)
(! f (! v (term s) formula)
formula))))
(declare flet (! f1 formula
(! f2 (! v formula formula)
formula)))
; predicates
(declare = (! s sort
(! x (term s)
(! y (term s)
formula))))
; To avoid duplicating some of the rules (e.g., cong), we will view
; applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".
(declare Bool sort) ; the special sort for predicates
(declare p_app (! x (term Bool) formula)) ; propositional application of term
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Examples
; an example of "(p1 or p2(0)) and t1=t2(1)"
;(! p1 (term Bool)
;(! p2 (term (arrow Int Bool))
;(! t1 (term Int)
;(! t2 (term (arrow Int Int))
;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
; (= _ t1 (apply _ _ t2 1))))
; ...
; another example of "p3(a,b)"
;(! a (term Int)
;(! b (term Int)
;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc.
;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
; ...
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; contradiction
(declare contra
(! f formula
(! r1 (th_holds f)
(! r2 (th_holds (not f))
(th_holds false)))))
;; not not
(declare not_not_intro
(! f formula
(! u (th_holds f)
(th_holds (not (not f))))))
(declare not_not_elim
(! f formula
(! u (th_holds (not (not f)))
(th_holds f))))
;; or elimination
(declare or_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (or f1 f2))
(th_holds f2))))))
(declare or_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f2))
(! u2 (th_holds (or f1 f2))
(th_holds f1))))))
;; and elimination
(declare and_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f1)))))
(declare and_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f2)))))
;; not impl elimination
(declare not_impl_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds f1)))))
(declare not_impl_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds (not f2))))))
;; impl elimination
(declare impl_intro (! f1 formula
(! f2 formula
(! i1 (! u (th_holds f1)
(th_holds f2))
(th_holds (impl f1 f2))))))
(declare impl_elim
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (impl f1 f2))
(th_holds f2))))))
;; iff elimination
(declare iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f1 f2))))))
(declare iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f2 f1))))))
(declare not_iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (not (iff f1 f2)))
(th_holds f2))))))
(declare not_iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (not (iff f1 f2)))
(th_holds (not f2)))))))
;; ite elimination
(declare ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte a b c))
(th_holds b)))))))
(declare ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not b))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte (not a) b c))
(th_holds c)))))))
(declare not_ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not b))))))))
(declare not_ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds b)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte (not a) b c)))
(th_holds (not c))))))))
;; How to do CNF for disjunctions of theory literals.
;;
;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
;;
;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
;; Do this at the beginning of the proof:
;;
;; (decl_atom F1 (\ v1 (\ a1
;; (decl_atom F2 (\ v2 (\ a2
;; ....
;; (decl_atom Fn (\ vn (\ an
;;
;; Our input A is clausified by the following proof:
;;
;;(satlem _ _
;;(asf _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;...
;;(asf _ _ _ an (\ ln
;;(clausify_false
;;
;; (contra _
;; (or_elim_1 _ _ l{n-1}
;; ...
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
;;
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
;;
;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
;; the arguments of contra:
;;
;;(satlem _ _
;;(ast _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;(ast _ _ _ a3 (\ l3
;;(clausify_false
;;
;; (contra _ l3
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ (not_not_intro l1) A))))
;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )

1
sources
View File

@ -0,0 +1 @@
a8c2bf10b7fa581a8de283072f4137b6 cvc4-1.3.tar.gz

107
th_base.plf Normal file
View File

@ -0,0 +1,107 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Atomization / Clausification
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; binding between an LF var and an (atomic) formula
(declare atom (! v var (! p formula type)))
(declare decl_atom
(! f formula
(! u (! v var
(! a (atom v f)
(holds cln)))
(holds cln))))
; direct clausify
(declare clausify_form
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds f)
(holds (clc (pos v) cln)))))))
(declare clausify_form_not
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds (not f))
(holds (clc (neg v) cln)))))))
(declare clausify_false
(! u (th_holds false)
(holds cln)))
(declare th_let_pf
(! f formula
(! u (th_holds f)
(! u2 (! v (th_holds f) (holds cln))
(holds cln)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory reasoning
; - make a series of assumptions and then derive a contradiction (or false)
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare ast
(! v var
(! f formula
(! C clause
(! r (atom v f) ;this is specified
(! u (! o (th_holds f)
(holds C))
(holds (clc (neg v) C))))))))
(declare asf
(! v var
(! f formula
(! C clause
(! r (atom v f)
(! u (! o (th_holds (not f))
(holds C))
(holds (clc (pos v) C))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory of Equality and Congruence Closure
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; temporary :
(declare trust (th_holds false))
(declare refl
(! s sort
(! t (term s)
(th_holds (= s t t)))))
(declare symm (! s sort
(! x (term s)
(! y (term s)
(! u (th_holds (= _ x y))
(th_holds (= _ y x)))))))
(declare trans (! s sort
(! x (term s)
(! y (term s)
(! z (term s)
(! u (th_holds (= _ x y))
(! u (th_holds (= _ y z))
(th_holds (= _ x z)))))))))
(declare cong (! s1 sort
(! s2 sort
(! a1 (term (arrow s1 s2))
(! b1 (term (arrow s1 s2))
(! a2 (term s1)
(! b2 (term s1)
(! u1 (th_holds (= _ a1 b1))
(! u2 (th_holds (= _ a2 b2))
(th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))