[alethe] Enable Alethe tester in regressions

The Alethe tester is amended to succeed when cvc5 does not support producing an Alethe proof for a benchmark. This commit also disables a number of regressions where it is not simple for cvc5 to realize it cannot produce an Alethe proof. Also a few scenarios where the Alethe translation has performance issues.
HanielB · Aug 22, 2024 · be42150 · be42150
1 parent 60d2c7b
commit be42150
Show file tree

Hide file tree

Showing 31 changed files with 77 additions and 16 deletions.
diff --git a/contrib/get-carcara-checker b/contrib/get-carcara-checker
@@ -24,9 +24,10 @@ CARCARA_DIR="$BASE_DIR/carcara"
 mkdir -p $CARCARA_DIR
 
 # download and unpack Carcara
-CARCARA_VERSION="e770994b5d981257d53a83d38a679fa98c144005"
+CARCARA_VERSION="d434d5caa0f2dad65aaa9ac9c20817af53004088"
 download "https://github.com/hanielb/carcara/archive/$CARCARA_VERSION.tar.gz" $BASE_DIR/tmp/carcara.tgz
 tar --strip 1 -xzf $BASE_DIR/tmp/carcara.tgz -C $CARCARA_DIR
+rm $BASE_DIR/tmp/carcara.tgz
 
 # build carcara
 pushd $CARCARA_DIR
@@ -67,4 +68,4 @@ echo "  $CVC_DIR/deps/bin/cvc5-alethe-proof.sh cvc5 <input file> <options>"
 echo "Check a proof:"
 echo "  $CVC_DIR/deps/bin/carcara-check.sh <proof file> <input file>"
 echo "Run cvc5 and check the generated proof:"
-echo "  $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 <input file> <options>"
+echo "  $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 <input file> <options>"
diff --git a/test/regress/cli/regress0/bug1247.smt2 b/test/regress/cli/regress0/bug1247.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --incremental
 ; EXPECT: unsat
+;; define-const is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ABV)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/bv/issue9518.smt2 b/test/regress/cli/regress0/bv/issue9518.smt2
@@ -1,3 +1,5 @@
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :bv-solver bitblast-internal)

diff --git a/test/regress/cli/regress0/datatypes/stream-singleton.smt2 b/test/regress/cli/regress0/datatypes/stream-singleton.smt2
@@ -1,3 +1,5 @@
+;; Codatatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2 b/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2
@@ -3,6 +3,7 @@
 ; DISABLE-TESTER: unsat-core
 ; DISABLE-TESTER: cpc
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alethe
 ; REQUIRES: no-competition
 ; SCRUBBER: grep -o "unsat"
 ; EXPECT: unsat

diff --git a/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2 b/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; The option below forces the granularity "dsl-rewrite", which leads to an Alethe proof with the operators @bv and @bvsize, where the former is applied to a non-constant argument. This is unsupported.
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-const x (_ BitVec 1))
 (set-option :check-proof-steps true)

diff --git a/test/regress/cli/regress0/proofs/proof-components.smt2 b/test/regress/cli/regress0/proofs/proof-components.smt2
@@ -3,6 +3,7 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: lfsc
 ; DISABLE-TESTER: cpc
+; DISABLE-TESTER: alethe
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 b/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2
@@ -3,12 +3,13 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: lfsc
 ; DISABLE-TESTER: cpc
+; DISABLE-TESTER: alethe
 (set-logic UFLIA)
-(declare-fun f (Int) Int) 
-(declare-fun g (Int) Int) 
+(declare-fun f (Int) Int)
+(declare-fun g (Int) Int)
 (declare-fun h (Int) Int)
-(declare-fun a () Int) 
-(declare-fun b () Int) 
+(declare-fun a () Int)
+(declare-fun b () Int)
 (declare-fun c () Int)
 (assert (forall ((x Int)) (> (f x) 5)))
 (assert (forall ((x Int)) (> (h x) 0)))

diff --git a/test/regress/cli/regress0/proofs/unused-def1.smt2 b/test/regress/cli/regress0/proofs/unused-def1.smt2
@@ -1,5 +1,6 @@
 ; EXPECT: unsat
-
+;; define-const is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic UF)
 (declare-const x Bool)
 (define-const p Bool x)

diff --git a/test/regress/cli/regress0/proofs/unused-def2.smt2 b/test/regress/cli/regress0/proofs/unused-def2.smt2
@@ -1,7 +1,8 @@
 ; COMMAND-LINE: --proof-prune-input
 ; SCRUBBER: grep -E "define|unsat"
 ; EXPECT: unsat
-
+;; define-const is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic UF)
 (declare-const x Bool)
 (define-const p Bool x)

diff --git a/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 b/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --ieval=use --term-db-mode=all
 ; EXPECT: unsat
+;; Unary OR implicitly removed by cvc5
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-const x9 Bool)
 (declare-fun p () Int)

diff --git a/test/regress/cli/regress0/smtlib/issue4552.smt2 b/test/regress/cli/regress0/smtlib/issue4552.smt2
@@ -2,6 +2,8 @@
 ; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: unsat
+;; define-const is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic UF)
 (set-option :global-declarations true)
 

diff --git a/test/regress/cli/regress0/tptp/SYN000=2.smt2 b/test/regress/cli/regress0/tptp/SYN000=2.smt2
@@ -1,3 +1,5 @@
+;; Input has to_int applied to an integer
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort $$unsorted 0)

diff --git a/test/regress/cli/regress1/bv/divtest.smt2 b/test/regress/cli/regress1/bv/divtest.smt2
@@ -1,5 +1,7 @@
 ; DISABLE-TESTER: lfsc
 ; DISABLE-TESTER: dsl-proof
+;; slow conversion
+; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (declare-fun x1 () (_ BitVec 12))

diff --git a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; slow conversion
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bvdiv2.smt2 b/test/regress/cli/regress1/bvdiv2.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; slow conversion
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2 b/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; slow conversion
+; DISABLE-TESTER: alethe
 (set-logic QF_UFLIRA)
 (declare-sort FArray 2)
 

diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --ee-mode=distributed
 ; COMMAND-LINE: --ee-mode=central
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :fmf-bound true)

diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: unsat
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-sort e 0)
 (declare-sort p 0)

diff --git a/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2 b/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --enum-inst --ieval=use
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun p (Int) Int)
 (declare-fun H (Int Int Int) Int)

diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
@@ -1,11 +1,13 @@
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-datatypes ((T 0) (D 0)) (((E) (o (b Bool)) (I (t Int)) (i (v D)) (R (l T) (u T))) ((ic (vc U)))))
 (declare-datatypes ((H 0)) (((M (h T)))))
 (declare-fun S (U Int) T)
 (declare-fun n () H)
-(assert (and 
+(assert (and
 (not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (vc (v (S (vc (v E)) 0))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t E))))))))))))))))
 (b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (vc (v (S (vc (v (h n))) z))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t (I i))))))))))) :qid id))))))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2 b/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALIA)
 (declare-fun j () Int)
 (declare-fun a () (Array Int Int))

diff --git a/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2
@@ -1,14 +1,16 @@
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
-(declare-fun a () Real)   
-(assert 
-    (and  
-        (and 
-            (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) 
-            (or  (and  (and  (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0)) 
+(declare-fun a () Real)
+(assert
+    (and
+        (and
+            (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real))
+            (or  (and  (and  (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0))
             (or (<= 0.0 (+  (*  (+ (* 55.0 ?d) 0.0) (* 49.0 ?b)) 0.0))))))))))
         )
     )
-) 
+)
 
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun b () String)
 (assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a))))))

diff --git a/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: -i
 ; EXPECT: unsat
+;; Unary OR is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (push)
 (assert (or (forall ((v Real)) (or (exists ((V Real)) (or (exists ((V Real)) (= 0 (mod (to_int v) (to_int (- v)))))))))))

diff --git a/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 b/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --sygus-inst
 ; EXPECT: unsat
+;; Unary AND is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (assert (and (forall ((v (Array (_ BitVec 1) Bool))) (select v (_ bv0 1)))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 b/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --cbqi-tconstraint --ieval=off
 ; EXPECT: unsat
+;; slow conversion
+; DISABLE-TESTER: alethe
 ; DISABLE-TESTER: dsl-proof
 (set-logic AUFLIRA)
 (set-info :source |http://proval.lri.fr/why-benchmarks |)

diff --git a/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2 b/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --relevant-triggers
 ; EXPECT: unsat
+;; slow conversion
+; DISABLE-TESTER: alethe
 ; DISABLE-TESTER: dsl-proof
 (set-logic AUFLIRA)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2
@@ -1,3 +1,5 @@
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :print-success false)
 (set-logic AUFLIAFS)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/strings/issue6913.smt2 b/test/regress/cli/regress1/strings/issue6913.smt2
@@ -1,5 +1,9 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+;; repeated assumption in local proof lead to confusion with
+;; discharge. Disabling for now while the use of "discharge" is not
+;; properly defined in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun a () String)
 (assert

diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
@@ -294,6 +294,10 @@ def run_internal(self, benchmark_info):
             output, error = output.decode(), error.decode()
             exit_code = self.check_exit_status(EXIT_OK, exit_status, output,
                                                error, cvc5_args)
+            if re.match(r'^unsat\n\(error "Proof unsupported by Alethe:', output):
+                print_ok("OK")
+                return exit_code
+
             if exit_code != EXIT_OK:
                 return exit_code
             original_file = benchmark_info.benchmark_dir + '/' + benchmark_info.benchmark_basename
@@ -511,6 +515,7 @@ def run_internal(self, benchmark_info):
     "abduct": AbductTester(),
     "dump": DumpTester(),
     "dsl-proof": DslProofTester(),
+    "alethe": AletheTester(),
     "cpc": CpcTester()
 }