Skip to content

Commit

Permalink
[alethe] Enable Alethe tester in regressions (cvc5#11179)
Browse files Browse the repository at this point in the history
The Alethe tester is amended to not fail 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.

This commit can only go in after cvc5#11178 is merged.
  • Loading branch information
HanielB authored Sep 16, 2024
1 parent ac0938c commit fe4e8b6
Show file tree
Hide file tree
Showing 31 changed files with 77 additions and 16 deletions.
5 changes: 3 additions & 2 deletions contrib/get-carcara-checker
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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>"
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/bug1247.smt2
Original file line number Diff line number Diff line change
@@ -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)

Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/bv/issue9518.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/datatypes/stream-singleton.smt2
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
;; Codatatypes are not supported in Alethe
; DISABLE-TESTER: alethe
(set-logic QF_ALL)
(set-info :status unsat)

Expand Down
1 change: 1 addition & 0 deletions test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
1 change: 1 addition & 0 deletions test/regress/cli/regress0/proofs/proof-components.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
9 changes: 5 additions & 4 deletions test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down
3 changes: 2 additions & 1 deletion test/regress/cli/regress0/proofs/unused-def1.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
3 changes: 2 additions & 1 deletion test/regress/cli/regress0/proofs/unused-def2.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/smtlib/issue4552.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress0/tptp/SYN000=2.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/bv/divtest.smt2
Original file line number Diff line number Diff line change
@@ -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))
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/bv/incorrect1.smtv1.smt2
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
; DISABLE-TESTER: lfsc
;; slow conversion
; DISABLE-TESTER: alethe
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_BV)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/bvdiv2.smt2
Original file line number Diff line number Diff line change
@@ -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")
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
; EXPECT: unsat
;; slow conversion
; DISABLE-TESTER: alethe
(set-logic QF_UFLIRA)
(declare-sort FArray 2)

Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
4 changes: 3 additions & 1 deletion test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
Original file line number Diff line number Diff line change
@@ -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)
Original file line number Diff line number Diff line change
@@ -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))
Expand Down
16 changes: 9 additions & 7 deletions test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2
Original file line number Diff line number Diff line change
@@ -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))))))
Expand Down
Original file line number Diff line number Diff line change
@@ -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)))))))))))
Expand Down
Original file line number Diff line number Diff line change
@@ -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)
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2
Original file line number Diff line number Diff line change
@@ -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 |)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
2 changes: 2 additions & 0 deletions test/regress/cli/regress1/sets/insert_invariant_37_2.smt2
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
;; Logic not supported in Alethe
; DISABLE-TESTER: alethe
(set-option :print-success false)
(set-logic AUFLIAFS)
(set-info :status unsat)
Expand Down
4 changes: 4 additions & 0 deletions test/regress/cli/regress1/strings/issue6913.smt2
Original file line number Diff line number Diff line change
@@ -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
Expand Down
5 changes: 5 additions & 0 deletions test/regress/cli/run_regression.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -511,6 +515,7 @@ def run_internal(self, benchmark_info):
"abduct": AbductTester(),
"dump": DumpTester(),
"dsl-proof": DslProofTester(),
"alethe": AletheTester(),
"cpc": CpcTester()
}

Expand Down

0 comments on commit fe4e8b6

Please sign in to comment.