This marks APPLY_SELECTOR and SEQ_NTH as unevaluatable kinds.
This means that get-value applied to applications of them e.g. (seq.nth t) will evaluate to c if (seq.nth t) is in the same equivalence class as constant c. (Note that this could be further improved to reason by congruence for (seq.nth s) where s = t, which I'm considering to do on a followup PR).
This removes many of the required -q from the command line arguments of our regressions. This also does some minor cleanup to our regressions to remove -q from further regressions.
// testers are not relevant for model building
d_valuation.setIrrelevantKind(APPLY_TESTER);
d_valuation.setIrrelevantKind(DT_SYGUS_BOUND);
+ // selectors don't always evaluate
+ d_valuation.setUnevaluatedKind(APPLY_SELECTOR);
}
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
// memberships are not relevant for model building
d_valuation.setIrrelevantKind(kind::STRING_IN_REGEXP);
+ // seq nth doesn't always evaluate
+ d_valuation.setUnevaluatedKind(SEQ_NTH);
}
std::string TheoryStrings::identify() const
<= cc.getUpperBound());
}
// if the value was constant, we return it. If it was non-constant,
- // we only return it if we an evaluated kind. This can occur if the
+ // we only return it if we are an evaluated kind. This can occur if the
// children of n failed to evaluate.
if (ret.isConst() || (
d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
d_modelCache[n] = ret;
return ret;
}
+ // Note that we discard the evaluation of the arguments here
+ Trace("model-getvalue-debug") << "Failed to evaluate " << ret << std::endl;
}
// must rewrite the term at this point
ret = rewrite(n);
+ Trace("model-getvalue-debug")
+ << "Look up " << ret << " in equality engine" << std::endl;
// return the representative of the term in the equality engine, if it exists
TypeNode t = ret.getType();
- bool eeHasTerm;
if (!logicInfo().isHigherOrder() && (t.isFunction() || t.isPredicate()))
{
// functions are in the equality engine, but *not* as first-class members
// to the equality engine despite hasTerm returning true. However, they are
// first class members when higher-order is enabled. Hence, the special
// case here.
- eeHasTerm = false;
- }
- else
- {
- eeHasTerm = d_equalityEngine->hasTerm(ret);
}
- if (eeHasTerm)
+ else if (d_equalityEngine->hasTerm(ret))
{
Trace("model-getvalue-debug")
<< "get value from representative " << ret << "..." << std::endl;
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_NRA)
(set-info :smt-lib-version 2.6)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
+(set-logic ALL)
(set-option :nl-ext-ent-conf true)
(declare-const x Int)
(assert (> (* x x) (+ x x)))
-; COMMAND-LINE: -q --incremental
+; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
+(set-logic ALL)
(declare-fun x0 () Real)
(check-sat)
(assert (<= (* x0 (- 1.0)) 0.0))
-; COMMAND-LINE: --incremental -q
+; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
+(set-logic ALL)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
-; COMMAND-LINE: --incremental -q --cegqi-full --produce-unsat-cores
+; COMMAND-LINE: --incremental --cegqi-full --produce-unsat-cores
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: (
; EXPECT: IP_1
; EXPECT: )
+(set-logic ALL)
(declare-const v1 Bool)
(declare-const v9 Bool)
(declare-const v14 Bool)
-; COMMAND-LINE: --incremental -q --produce-unsat-cores
-; COMMAND-LINE: --incremental -q --unsat-cores-mode=sat-proof --produce-unsat-cores
+; COMMAND-LINE: --incremental --produce-unsat-cores
+; COMMAND-LINE: --incremental --unsat-cores-mode=sat-proof --produce-unsat-cores
; EXPECT: sat
; EXPECT: sat
+(set-logic ALL)
(declare-const i2 Int)
(declare-const i5 Int)
(declare-fun st2 () (Set Int))
-; COMMAND-LINE: --incremental -q --produce-unsat-cores
+; COMMAND-LINE: --incremental --produce-unsat-cores
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
+(set-logic ALL)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
-; COMMAND-LINE: -q
; EXPECT: unsat
+(set-logic ALL)
(check-sat-assuming (false))
-; COMMAND-LINE: -i -q
+; COMMAND-LINE: -i
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
+(set-logic ALL)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(pop)
(assert (> e a))
(assert (= e 0))
-(check-sat)
\ No newline at end of file
+(check-sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_DTLIA)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_UFDTLIA)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_FP)
(declare-const x (_ FloatingPoint 11 53))
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_FPLRA)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic HO_ALL)
(set-option :assign-function-values false)
-; COMMAND-LINE: -m -q
+; COMMAND-LINE: -m
; EXPECT: sat
; EXPECT: ((IP true))
(set-logic QF_NRA)
-; COMMAND-LINE: -q
; EXPECT: sat
; EXPECT: ((baz true))
(set-logic QF_NIRA)
-; COMMAND-LINE: -q
+(set-logic ALL)
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
-; COMMAND-LINE: -q
(set-logic QF_AUFBV)
(set-info :status sat)
(declare-fun bv_22-0 () (_ BitVec 1))
-; COMMAND-LINE: -q
(set-logic QF_UFBVLIA)
(set-info :status sat)
(declare-fun f ((_ BitVec 3)) Int)
-; COMMAND-LINE: -i -q --no-debug-check-models
+; COMMAND-LINE: -i --no-debug-check-models
; EXPECT: sat
; EXPECT: sat
(set-logic ALL)
-; COMMAND-LINE: -q
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
-; COMMAND-LINE: -i -q
+; COMMAND-LINE: -i
; EXPECT: unsat
; EXPECT: unsat
(set-logic QF_NRAT)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
; DISABLE-TESTER: dump
-; COMMAND-LINE: -q
; SCRUBBER: grep -o "must have at least 2 children"
; EXPECT: must have at least 2 children
; EXIT: 1
+(set-logic ALL)
(assert (= (+ 0)))
-; COMMAND-LINE: --strict-parsing -q
+; COMMAND-LINE: --strict-parsing
; EXPECT: sat
(set-logic QF_FP)
(declare-fun |c::main::main::3::div@1!0&0#1| () (_ FloatingPoint 8 24))
-; COMMAND-LINE: -q
; EXPECT: unknown
+(set-logic ALL)
(assert (forall ((V (Array Int Int))) (= 0 (select V 0))))
(check-sat)
-; COMMAND-LINE: --cegqi -q
+; COMMAND-LINE: --cegqi
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --seq-array=lazy -q
+; COMMAND-LINE: --seq-array=lazy
(set-logic QF_UFSLIA)
(declare-sort E 0)
-; COMMAND-LINE: --strings-exp --seq-array=lazy -q
+; COMMAND-LINE: --strings-exp --seq-array=lazy
; EXPECT: sat
(set-logic QF_SLIA)
(declare-const x (Seq Int))
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
; EXPECT: sat
-; EXPECT: (((seq.nth y 7) (seq.nth (as seq.empty (Seq Int)) 7)))
+; EXPECT: (((seq.nth y 7) 404))
; EXPECT: (((str.from_code x) "?"))
(set-logic ALL)
(set-option :produce-models true)
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
;EXPECT: sat
(set-logic ALL)
(declare-fun s () (Seq Int))
-; COMMAND-LINE: --strings-exp --seq-array=lazy -q
+; COMMAND-LINE: --strings-exp --seq-array=lazy
; EXPECT: sat
(set-logic ALL)
(declare-sort S 0)
-; COMMAND-LINE: --strings-exp --seq-array=lazy -q
+; COMMAND-LINE: --strings-exp --seq-array=lazy
; EXPECT: sat
(set-logic ALL)
(declare-sort S 0)
-; COMMAND-LINE: --strings-exp --seq-array=lazy -q
+; COMMAND-LINE: --strings-exp --seq-array=lazy
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_ALL)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find --fmf-bound -q
+; COMMAND-LINE: --finite-model-find --fmf-bound
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --ee-mode=distributed -q
-; COMMAND-LINE: --ee-mode=central -q
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
; EXPECT: unsat
+(set-logic ALL)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
-; COMMAND-LINE: --dt-nested-rec -q
+; COMMAND-LINE: --dt-nested-rec
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --fmf-fun --fmf-bound -q
+; COMMAND-LINE: --fmf-fun --fmf-bound
; EXPECT: sat
+; DISABLE-TESTER: model
(set-logic UFDTSLIA)
(set-option :produce-models true)
-; COMMAND-LINE: --fmf-bound -q
+; COMMAND-LINE: --fmf-bound
; EXPECT: sat
(set-logic ALL)
(declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil))))
-; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone -q
+; COMMAND-LINE: --finite-model-find --e-matching --uf-ss-fair-monotone
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL)
(declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL)
(declare-sort b__ 0)
-; COMMAND-LINE: --fmf-fun -q
+; COMMAND-LINE: --fmf-fun
; EXPECT: sat
+; DISABLE-TESTER: model
(set-logic ALL)
(define-fun-rec p2 ((n Int) (p Int)) Bool (
-; COMMAND-LINE: --nl-rlv=always -q
+; COMMAND-LINE: --nl-rlv=always
; EXPECT: sat
(set-logic QF_NRAT)
(set-info :status sat)
-; COMMAND-LINE: -q
; SCRUBBER: sed 's/(.*)/()/g'
; EXPECT: ()
; EXIT: 0
-; COMMAND-LINE: -q
; SCRUBBER: sed 's/(.*)/()/g'
; EXPECT: ()
; EXIT: 0
-; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep -q
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic BV)
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic ALL)
(set-option :strings-exp true)
-; COMMAND-LINE: --strings-exp -q
+; COMMAND-LINE: --strings-exp
; EXPECT: unsat
(set-logic ALL)
(declare-fun a () String)
-; COMMAND-LINE: --decision=internal -q
-; COMMAND-LINE: --decision=justification -q
+; COMMAND-LINE: --decision=internal
+; COMMAND-LINE: --decision=justification
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic QF_BVFP)
-; COMMAND-LINE: --incremental --fmf-fun-rlv -q
+; COMMAND-LINE: --incremental --fmf-fun-rlv
+; DISABLE-TESTER: model
(set-logic ALL)
(declare-datatypes ((Color 0)) (
-; COMMAND-LINE: -q
; EXPECT: sat
(set-logic UFDTLIRA)
(set-option :fmf-bound true)
-; COMMAND-LINE: -q
; EXPECT: unsat
(set-logic QF_SLIA)
(declare-fun a () String)
projects / cvc5.git / commitdiff