This commit makes TheoryEngine take into account whether theories are using the central equality engine.
With this commit, the central equality engine can now be optionally enabled via `--ee-mode=central`.
[[option.mode.DISTRIBUTED]]
name = "distributed"
help = "Each theory maintains its own equality engine."
+[[option.mode.CENTRAL]]
+ name = "central"
+ help = "All applicable theories use the central equality engine."
[[option]]
name = "tcMode"
}
// set up of central equality engine
+ if (opts.theory.eeMode == options::EqEngineMode::CENTRAL)
+ {
+ if (!opts.arith.arithEqSolverWasSetByUser)
+ {
+ // use the arithmetic equality solver by default
+ opts.arith.arithEqSolver = true;
+ }
+ }
if (opts.arith.arithEqSolver)
{
if (!opts.arith.arithCongManWasSetByUser)
#include "expr/node_visitor.h"
#include "proof/eager_proof_generator.h"
#include "theory/care_graph.h"
+#include "theory/ee_manager_central.h"
#include "theory/ee_manager_distributed.h"
#include "theory/model_manager.h"
#include "theory/model_manager_distributed.h"
-#include "theory/shared_solver.h"
#include "theory/shared_solver_distributed.h"
#include "theory/theory_engine.h"
d_mmanager.reset(
new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
}
+ else if (options::eeMode() == options::EqEngineMode::CENTRAL)
+ {
+ // for now, the shared solver is the same in both approaches; use the
+ // distributed one for now
+ d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
+ // make the central equality engine manager
+ d_eemanager.reset(
+ new EqEngineManagerCentral(d_te, *d_sharedSolver.get(), d_pnm));
+ // make the distributed model manager
+ d_mmanager.reset(
+ new ModelManagerDistributed(d_te, d_env, *d_eemanager.get()));
+ }
else
{
Unhandled() << "CombinationEngine::finishInit: equality engine mode "
#include "base/check.h"
#include "expr/node_algorithm.h"
+#include "options/arith_options.h"
+#include "options/bv_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/smt_statistics_registry.h"
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
{
// if we are using an equality engine, assert it to the model
- if (d_equalityEngine != nullptr)
+ if (d_equalityEngine != nullptr && !termSet.empty())
{
Trace("model-builder") << "Assert Equality engine for " << d_id
<< std::endl;
{
return false;
}
- // Below are all theories with an equality engine except id ==THEORY_ARITH
+ if (id == THEORY_ARITH)
+ {
+ // conditional on whether we are using the equality solver
+ return options::arithEqSolver();
+ }
+ if (id == THEORY_BV)
+ {
+ // the internal bitblast BV solver doesnt use an equality engine
+ return options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL;
+ }
return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
|| id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
- || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
+ || id == THEORY_SEP || id == THEORY_ARRAYS;
+}
+
+bool Theory::expUsingCentralEqualityEngine(TheoryId id)
+{
+ return id != THEORY_ARITH && usesCentralEqualityEngine(id);
}
} // namespace theory
*/
virtual std::pair<bool, Node> entailmentCheck(TNode lit);
- /** uses central equality engine */
+ /** Return true if this theory uses central equality engine */
bool usesCentralEqualityEngine() const;
/** uses central equality engine (static) */
static bool usesCentralEqualityEngine(TheoryId id);
+ /** Explains/propagates via central equality engine only */
+ static bool expUsingCentralEqualityEngine(TheoryId id);
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
return;
}
- // If sending to the shared terms database, it's also simple
+ // determine the actual theory that will process/explain the fact, which is
+ // THEORY_BUILTIN if the theory uses the central equality engine
+ TheoryId toTheoryIdProp = (Theory::expUsingCentralEqualityEngine(toTheoryId))
+ ? THEORY_BUILTIN
+ : toTheoryId;
+ // If sending to the shared solver, it's also simple
if (toTheoryId == THEORY_BUILTIN) {
- Assert(assertion.getKind() == kind::EQUAL
- || (assertion.getKind() == kind::NOT
- && assertion[0].getKind() == kind::EQUAL))
- << "atom should be an EQUALity, not `" << assertion << "'";
- if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+ if (markPropagation(
+ assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+ {
// assert to the shared solver
bool polarity = assertion.getKind() != kind::NOT;
TNode atom = polarity ? assertion : assertion[0];
// directly to the apropriate theory
if (fromTheoryId == THEORY_SAT_SOLVER) {
// We know that this is normalized, so just send it off to the theory
- if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+ if (markPropagation(
+ assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+ {
// Is it preregistered
bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
// We assert it
// Propagations to the SAT solver are just enqueued for pickup by
// the SAT solver later
if (toTheoryId == THEORY_SAT_SOLVER) {
+ Assert(toTheoryIdProp == toTheoryId);
if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
// Enqueue for propagation to the SAT solver
d_propagatedLiterals.push_back(assertion);
if (normalizedLiteral.isConst()) {
if (!normalizedLiteral.getConst<bool>()) {
// Mark the propagation for explanations
- if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
+ if (markPropagation(normalizedLiteral,
+ originalAssertion,
+ toTheoryIdProp,
+ fromTheoryId))
+ {
// special case, trust node has no proof generator
TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
// Get the explanation (conflict will figure out where it came from)
}
// Try and assert (note that we assert the non-normalized one)
- if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
+ if (markPropagation(
+ assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
+ {
// Check if has been pre-registered with the theory
bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
// Assert away
{
Assert(explanationVector.size() == 1);
Node conclusion = explanationVector[0].d_node;
+ // if the theory explains using the central equality engine, we always start
+ // with THEORY_BUILTIN.
+ if (Theory::expUsingCentralEqualityEngine(explanationVector[0].d_theory))
+ {
+ explanationVector[0].d_theory = THEORY_BUILTIN;
+ }
std::shared_ptr<LazyCDProof> lcp;
if (isProofEnabled())
{
<< "TheoryEngine::explain(): got explanation " << explanation
<< " got from " << toExplain.d_theory << endl;
Assert(explanation != toExplain.d_node)
- << "wasn't sent to you, so why are you explaining it trivially";
+ << "wasn't sent to you, so why are you explaining it trivially, for "
+ "fact "
+ << explanation;
// Mark the explanation
NodeTheoryPair newExplain(
explanation, toExplain.d_theory, toExplain.d_timestamp);
regress0/aufbv/bug493.smtv1.smt2
regress0/aufbv/bug509.smtv1.smt2
regress0/aufbv/bug580.delta.smt2
+ regress0/aufbv/cee-small-shared-eq.smt2
regress0/aufbv/diseqprop.01.smtv1.smt2
regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
regress0/datatypes/bug597-rbt.smt2
regress0/datatypes/bug604.smt2
regress0/datatypes/bug625.smt2
+ regress0/datatypes/canExp-dtPendingMerge.smt2
regress0/datatypes/cdt-model-cade15.smt2
regress0/datatypes/cdt-non-canon-stream.smt2
regress0/datatypes/coda_simp_model.smt2
regress0/sets/pre-proc-univ.smt2
regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
regress0/sets/setel-eq.smt2
+ regress0/sets/sets-deq-dd.smt2
regress0/sets/sets-equal.smt2
regress0/sets/sets-extr.smt2
regress0/sets/sets-inter.smt2
regress1/bv/test-bv-abstraction.smt2
regress1/bv/unsound1.smt2
regress1/bvdiv2.smt2
+ regress1/cee-bug0909-dd-scope.smt2
regress1/constarr3.cvc
regress1/constarr3.smt2
regress1/cores/issue5604.smt2
regress1/datatypes/acyclicity-sr-ground096.smt2
+ regress1/datatypes/cee-prs-small-dd2.smt2
regress1/datatypes/dt-color-2.6.smt2
regress1/datatypes/dt-param-card4-unsat.smt2
regress1/datatypes/error.cvc
regress1/push-pop/arith_lra_02.smt2
regress1/push-pop/bug-fmf-fun-skolem.smt2
regress1/push-pop/bug216.smt2
+ regress1/push-pop/cee-prs-small.smt2
regress1/push-pop/fuzz_1.smt2
regress1/push-pop/fuzz_10.smt2
regress1/push-pop/fuzz_11.smt2
regress1/quantifiers/burns13.smt2
regress1/quantifiers/burns4.smt2
regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
+ regress1/quantifiers/cee-npnt-dd.smt2
+ regress1/quantifiers/cee-os-delta.smt2
regress1/quantifiers/cdt-0208-to.smt2
regress1/quantifiers/const.cvc
regress1/quantifiers/constfunc.cvc
regress1/strings/bug686dd.smt2
regress1/strings/bug768.smt2
regress1/strings/bug799-min.smt2
+ regress1/strings/cee-norn-aes-trivially.smt2
regress1/strings/chapman150408.smt2
regress1/strings/cmu-2db2-extf-reg.smt2
regress1/strings/cmu-5042-0707-2.smt2
regress2/piVC_5581bd.smt2
regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
+ regress2/quantifiers/cee-event-wrong-sat.smt2
regress2/quantifiers/gn-wrong-091018.smt2
regress2/quantifiers/issue3481-unsat1.smt2
regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
# previously sygus inference did not apply, now (correctly) times out
regress1/sygus/issue3498.smt2
regress2/arith/miplib-opt1217--27.smt2
+ regress2/quantifiers/exp-trivially-dd3.smt2
regress2/nl/dumortier-050317.smt2
# timeout on some builds after changes to justification heuristic
regress2/nl/nt-lemmas-bad.smt2
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 1) (_ BitVec 16)))
+(assert (not (= (_ bv0 16) (select a ((_ extract 14 14) (select a (_ bv0 1)))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))
+(declare-fun w () T)
+(declare-fun u () T)
+(assert (= w (B (D u) (B (D u) (C w)))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun S () (Set (_ BitVec 1)))
+(assert (not (= S (as emptyset (Set (_ BitVec 1))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((x5 0)) (((x3) (x4))))
+(declare-sort x 0)
+(declare-sort x1 0)
+(declare-datatypes ((x22 0)) (((x2))))
+(declare-datatypes ((x2 0)) (((x2 (x2 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int)))))
+(declare-sort x30 0)
+(declare-sort x3 0)
+(declare-datatypes ((x4 0)) (((x44 (x43 x3)))))
+(declare-fun x46 (x3) x1)
+(declare-datatypes ((x54 0)) (((x49 (x48 x22)) (x5 (x5 x2)) (d (s x1)))))
+(declare-fun x5 (x22) x2)
+(declare-fun x67 () (Array x x54))
+(declare-fun x6 () (Array x x54))
+(declare-fun x7 () (Array x30 x4))
+(declare-fun x63 () x30)
+(declare-fun x () x)
+(assert (distinct x3 (ite (or (distinct x6 (store x67 x (d (x46 (x43 (select x7 x63)))))) (= x67 (store x67 x (x5 (x2 x4 x3 (x25 (x5 (x48 (select x67 x)))) (x26 (x5 (x48 (select x67 x)))) (x27 (x5 (x48 (select x6 x))))))))) x3 x4)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((r 0)) (((R (x Int)))))
+(declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t)))))
+(declare-fun z () q)
+(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: -i --ee-mode=distributed
+; COMMAND-LINE: -i --ee-mode=central
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatypes ((r 0)) (((r_ctor (x Int)))))
+(declare-datatype tup ((mkt (t1 (Array Int Int)) (t2 (Array Int Int)))))
+(declare-datatypes ((q 0)) (((R (x (Array Int r)) (y tup)))))
+(declare-fun z () q)
+(assert (not (= 1 (select (t2 (y z)) 1))))
+(assert (= z (R ((as const (Array Int r)) (r_ctor 0)) (mkt ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(check-sat)
+(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed
+; COMMAND-LINE: --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-datatype N ((o) (f) (s)))
+(declare-datatype P ((P)))
+(declare-fun G (N P Int) Bool)
+(declare-datatype c ((c (_p P))))
+(declare-fun g (N Int Int) c)
+(assert (forall ((x N)) (not (G x P 0))))
+(assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t)))))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun o (Int) Int)
+(declare-fun f (Int Int) Int)
+(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y))))))
+(assert (= 0 (f (o 0) (o 1))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed
+; COMMAND-LINE: --arith-eq-solver --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun v () String)
+(assert (str.in_re (str.++ "" v) (re.* (str.to_re "z"))))
+(assert (str.in_re v (re.* (re.range "a" "u"))))
+(assert (not (str.in_re v (str.to_re ""))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
+; COMMAND-LINE: --full-saturate-quant --ee-mode=central
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((T@$TypeValue 0) (T@A 0)) (((A)) ((T))))
+(declare-datatypes ((T@$Location 0)) (((P) (G (|t# | T@$TypeValue) (|a#G| Int)))))
+(declare-sort |T@[Int]$Value| 0)
+(declare-datatypes ((T@$Value 0) (T@R 0)) (((E) ($Boolean (|b#$Boolean| Bool)) (I (|i#I| Int)) (D (|a#D| Int)) (V (|v#V| T@R))) ((R (|v#R| |T@[Int]$Value|) (|l#R| Int)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (|domain#M| b) (|contents#M| l)))))
+(declare-fun $EmptyValueArray () T@R)
+(declare-fun m (T@$Value) |T@[Int]$Value|)
+(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool)
+(declare-fun sel (|T@[Int]$Value| Int) T@$Value)
+(declare-fun st (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?x2 T@$Value)) (= ?x2 (sel (st ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 |T@[Int]$Value|) (?x1 Int) (?y1 Int) (?x2 T@$Value)) (= (sel ?x0 ?y1) (sel (st ?x0 ?x1 ?x2) ?y1))))
+(declare-fun $LibraAccount_T_type_value () T@$TypeValue)
+(declare-fun s (l T@$Location) T@$Value)
+(declare-fun $Event_EventHandleGenerator_counter () Int)
+(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
+(assert (= 0 (|l#R| $EmptyValueArray)))
+(assert (forall ((v1 T@$Value) (v2 T@$Value)) (= ($IsEqual_stratified v1 v2) (or (= v1 v2) (forall ((i Int)) (or (> 0 i) (>= i (|l#R| (|v#V| v1))) ($IsEqual_stratified (sel (|v#R| (|v#V| v1)) i) (sel (|v#R| (|v#V| v2)) i))))))))
+(assert (forall ((m@@0 T@M) (a@@0 T@$Value)) (! (or (not (is-D a@@0)) (and (is-I (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| a@@0))))) $Event_EventHandleGenerator_counter)) (forall ((x@@10 Int)) (or (> x@@10 0) (= E (sel (|v#R| (|v#V| (s (|contents#M| m@@0) (G $LibraAccount_T_type_value (|a#D| a@@0))))) x@@10)))))) :qid :skolemid)))
+(declare-fun |Select_[$Location]$bool| (b T@$Location) Bool)
+(declare-fun $m@@0 () T@M)
+(declare-fun $abort_flag@2 () Bool)
+(declare-fun $m@3 () T@M)
+(declare-fun mv () T@$TypeValue)
+(declare-fun inline$$MoveToRaw$0$a@0 () Int)
+(declare-fun |Store_[$Location]$bool| (b T@$Location Bool) b)
+(assert (forall ((?x0 b) (?x1 T@$Location) (?y1 T@$Location) (?x2 Bool)) (or (= ?x1 ?y1) (= (|Select_[$Location]$bool| ?x0 ?y1) (|Select_[$Location]$bool| (|Store_[$Location]$bool| ?x0 ?x1 ?x2) ?y1)))))
+(declare-fun inline$$MoveToRaw$0$l@1 () T@$Location)
+(declare-fun |Store_[$Location]$Value| (l T@$Location T@$Value) l)
+(assert (forall ((?x0 l) (?x1 T@$Location) (?x2 T@$Value)) (= ?x2 (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?x1))))
+(assert (forall ((?x0 l) (?x1 T@$Location) (?y1 T@$Location) (?x2 T@$Value)) (= (s ?x0 ?y1) (s (|Store_[$Location]$Value| ?x0 ?x1 ?x2) ?y1))))
+(declare-fun inline$$Event_EventHandleGenerator_pack$0$$struct@1 () T@$Value)
+(declare-fun inline$$Event_publish_generator$0$$tmp@1 () T@$Value)
+(declare-fun i () T@$Value)
+(assert (and (not $abort_flag@2) (= inline$$Event_publish_generator$0$$tmp@1 (I 0)) (|b#$Boolean| ($Boolean (forall ((addr@@9 T@$Value)) (or (is-D addr@@9) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@9))))))))))) (or (not (=> $abort_flag@2 (|b#$Boolean| ($Boolean (forall ((addr@@4 T@$Value)) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@4)))))))))))))))) (and (= inline$$Event_EventHandleGenerator_pack$0$$struct@1 (V (R (st (st (m E) 0 inline$$Event_publish_generator$0$$tmp@1) 1 i) 1))) (not (=> (= inline$$MoveToRaw$0$a@0 (|a#D| i)) (= inline$$MoveToRaw$0$l@1 (G mv inline$$MoveToRaw$0$a@0)) (or (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| i))))) (not (= $m@3 (M (|Store_[$Location]$bool| (|domain#M| $m@@0) inline$$MoveToRaw$0$l@1 true) (|Store_[$Location]$Value| (|contents#M| $m@@0) inline$$MoveToRaw$0$l@1 inline$$Event_EventHandleGenerator_pack$0$$struct@1)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (|v#R| $EmptyValueArray) 0)) 1))))) (or (not (|b#$Boolean| ($Boolean ($IsEqual_stratified (s (|contents#M| $m@@0) (G mv (|a#D| i))) (V (R (|v#R| (R (st (|v#R| $EmptyValueArray) (|l#R| $EmptyValueArray) (I 0)) 1)) 0)))))) (and (|b#$Boolean| ($Boolean (forall ((addr@@1 T@$Value)) (|b#$Boolean| ($Boolean (or (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G mv (|a#D| addr@@1)))))) (|b#$Boolean| ($Boolean (|b#$Boolean| ($Boolean ($IsEqual_stratified (sel (|v#R| (|v#V| (s (|contents#M| $m@3) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G mv (|a#D| addr@@1))))) $Event_EventHandleGenerator_counter)))))))))))) (|b#$Boolean| ($Boolean (forall ((addr@@3 T@$Value)) (|b#$Boolean| ($Boolean (or (|b#$Boolean| ($Boolean ($IsEqual_stratified (I 0) (sel (|v#R| (|v#V| (s (|contents#M| $m@@0) (G $Event_EventHandleGenerator_type_value (|a#D| addr@@3))))) $Event_EventHandleGenerator_counter)))) (not (|b#$Boolean| ($Boolean (and (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@3) (G mv (|a#D| addr@@3))))) (|b#$Boolean| ($Boolean (not (|b#$Boolean| ($Boolean (|Select_[$Location]$bool| (|domain#M| $m@@0) (G $LibraAccount_T_type_value (|a#D| addr@@3))))))))))))))))))))))))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --ee-mode=distributed --no-check-unsat-cores
+; COMMAND-LINE: --ee-mode=central --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((dA 0)) (((A))))
+(declare-datatypes ((Loc 0)) (((G (g dA) (ag Int)))))
+(declare-sort v 0)
+(declare-datatypes ((T 0) (U 0)) (((E) (I (ii Int)) (D (d Int)) (V (vv U))) ((R (rr v)))))
+(declare-sort b 0)
+(declare-sort l 0)
+(declare-datatypes ((T@M 0)) (((M (dom b) (cnt l)))))
+(declare-fun e () U)
+(declare-fun m (T) v)
+(declare-fun iseq (T T) Bool)
+(declare-fun sel (v Int) T)
+(declare-fun st (v) v)
+(declare-fun s (l Loc) T)
+(declare-fun sb (Loc) Bool)
+(declare-fun m0 () T@M)
+(declare-fun a () Bool)
+(declare-fun im () Loc)
+(declare-fun o (Loc T) l)
+(declare-fun i () T)
+(assert (forall ((?x0 v) (?x1 Int) (?x2 T)) (= ?x2 (sel (st ?x0) ?x1))))
+(assert (forall ((v1 T) (v2 T)) (= (iseq v1 v2) (forall ((i Int)) (iseq (sel (rr (vv v1)) i) (sel (rr (vv v2)) i))))))
+(assert (forall ((?x1 Loc) (?x2 T)) (= ?x2 (s (o ?x1 ?x2) ?x1))))
+(assert (and
+(not a)
+(forall ((?a9 T)) (or (is-D ?a9) (sb (G A (d ?a9)))))
+(or
+(not (=> a (forall (($a T)) (sb (G A (d $a))))))
+(and
+ (not (sb (G A (d i))))
+ (= im (G A (d (I 0))))
+ (= m0 (M (dom m0) (o im (V (R (st (m E)))))))
+ (iseq (s (cnt m0) (G A (d i))) (V (R (rr e))))
+ (or
+ (exists ((?a1 T)) (not (iseq (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0) (sel (rr (vv (s (cnt m0) (G A (d ?a1))))) 0))))
+ (forall ((?a3 T)) (sb (G A (d ?a3)))))))))
+(check-sat)
projects / cvc5.git / commitdiff