diff --git a/.gitignore b/.gitignore index e69de29..c0346c5 100644 --- a/.gitignore +++ b/.gitignore @@ -0,0 +1 @@ +/cvc4-1.3.tar.gz diff --git a/cvc4-doxygen.patch b/cvc4-doxygen.patch new file mode 100644 index 0000000..a572bc9 --- /dev/null +++ b/cvc4-doxygen.patch @@ -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 diff --git a/cvc4.spec b/cvc4.spec new file mode 100644 index 0000000..4ae48cd --- /dev/null +++ b/cvc4.spec @@ -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 - 1.3-2 +- Install JNI objects in %%{_jnidir} + +* Wed Jan 22 2014 Jerry James - 1.3-1 +- Initial RPM diff --git a/sat.plf b/sat.plf new file mode 100644 index 0000000..09255f6 --- /dev/null +++ b/sat.plf @@ -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)))))) \ No newline at end of file diff --git a/smt.plf b/smt.plf new file mode 100644 index 0000000..75bfc44 --- /dev/null +++ b/smt.plf @@ -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 ) \ No newline at end of file diff --git a/sources b/sources index e69de29..7bf6add 100644 --- a/sources +++ b/sources @@ -0,0 +1 @@ +a8c2bf10b7fa581a8de283072f4137b6 cvc4-1.3.tar.gz diff --git a/th_base.plf b/th_base.plf new file mode 100644 index 0000000..e66990d --- /dev/null +++ b/th_base.plf @@ -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)))))))))))) +