THEORY_REALS,
THEORY_REALS_INTS,
THEORY_STRINGS,
- THEORY_QUANTIFIERS
+ THEORY_QUANTIFIERS,
+ THEORY_CARDINALITY_CONSTRAINT
};
private:
if(!options::decisionMode.wasSetByUser()) {
decision::DecisionMode decMode =
// ALL_SUPPORTED
- d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL :
+ d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION :
( // QF_BV
(not d_logic.isQuantified() &&
d_logic.isPure(THEORY_BV)
// QF_LRA
(not d_logic.isQuantified() &&
d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed()
- ) ||
- // Quantifiers
- d_logic.isQuantified()
+ )
? true : false
);
options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
}
}
- if ( options::fmfBoundInt() ){
+ if( d_logic.hasCardinalityConstraints() ){
+ //must have finite model finding on
+ options::finiteModelFind.set( true );
+ }
+ if( options::fmfBoundInt() ){
//must have finite model finding on
options::finiteModelFind.set( true );
- if( options::mbqiMode()!=quantifiers::MBQI_NONE &&
- options::mbqiMode()!=quantifiers::MBQI_FMC &&
- options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){
+ if( ! options::mbqiMode.wasSetByUser() ||
+ ( options::mbqiMode()!=quantifiers::MBQI_NONE &&
+ options::mbqiMode()!=quantifiers::MBQI_FMC &&
+ options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){
//if bounded integers are set, use no MBQI by default
options::mbqiMode.set( quantifiers::MBQI_NONE );
}
Trace("dt-model") << std::endl;
printModelDebug( "dt-model" );
Trace("dt-model") << std::endl;
+
+ /*
+ bool eq_merged = false;
+ std::vector< Node > all_eqc;
+ eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs1_i.isFinished() ){
+ Node eqc = (*eqcs1_i);
+ all_eqc.push_back( eqc );
+ ++eqcs1_i;
+ }
+ //check if equivalence classes have merged
+ for( unsigned i=0; i<all_eqc.size(); i++ ){
+ for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
+ if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
+ Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
+ eq_merged = true;
+ }
+ }
+ }
+ Assert( !eq_merged );
+ */
+
+ //combine the equality engine
m->assertEqualityEngine( &d_equalityEngine );
-/*
- std::vector< TypeEnumerator > vec;
- std::map< TypeNode, int > tes;
+
+ /*
+ //check again if equivalence classes have merged
+ for( unsigned i=0; i<all_eqc.size(); i++ ){
+ for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
+ if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
+ Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
+ eq_merged = true;
+ }
+ }
+ }
+ Assert( !eq_merged );
*/
+
//get all constructors
eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
std::vector< Node > cons;
+ std::vector< Node > nodes;
while( !eqccs_i.isFinished() ){
Node eqc = (*eqccs_i);
//for all equivalence classes that are datatypes
EqcInfo* ei = getOrMakeEqcInfo( eqc );
if( !ei->d_constructor.get().isNull() ){
cons.push_back( ei->d_constructor.get() );
- }
- }
- ++eqccs_i;
- }
-
- //must choose proper representatives
- std::vector< Node > nodes;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- //for all equivalence classes that are datatypes
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
- EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( !ei->d_constructor.get().isNull() ){
- //specify that we should use the constructor as the representative
- //m->assertRepresentative( ei->d_constructor.get() );
}else{
nodes.push_back( eqc );
}
}
- ++eqcs_i;
+ ++eqccs_i;
}
+
unsigned index = 0;
while( index<nodes.size() ){
Node eqc = nodes[index];
}
Trace("dt-cmi") << std::endl;
/*
- if( tes.find( eqc.getType() )==tes.end() ){
- tes[eqc.getType()]=vec.size();
- vec.push_back( TypeEnumerator( eqc.getType() ) );
- }
- bool success;
- Node n;
- do {
- success = true;
- Assert( !vec[tes[eqc.getType()]].isFinished() );
- n = *vec[tes[eqc.getType()]];
- ++vec[tes[eqc.getType()]];
- Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl;
- //check if it is consistent with labels
- size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr());
- if( constructorIndex<pcons.size() && pcons[constructorIndex] ){
- for( unsigned i=0; i<cons.size(); i++ ){
- //check if it is modulo equality the same
- if( cons[i].getOperator()==n.getOperator() ){
- bool diff = false;
- for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
- if( !m->areEqual( cons[i][j], n[j] ) ){
- diff = true;
- break;
- }
- }
- if( !diff ){
- Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
- success = false;
- break;
- }
- }
- }
- }else{
- Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
- success = false;
+ std::map< int, std::map< int, bool > > sels;
+ Trace("dt-cmi") << "Existing selectors : ";
+ NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
+ if( sel_i != d_selector_apps.end() ){
+ NodeList* sel = (*sel_i).second;
+ for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
+ Expr selectorExpr = (*j).getOperator().toExpr();
+ unsigned cindex = Datatype::cindexOf( selectorExpr );
+ unsigned index = Datatype::indexOf( selectorExpr );
+ sels[cindex][index] = true;
+ Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") ";
}
- }while( !success );
+ }
+ Trace("dt-cmi") << std::endl;
*/
+
const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
for( unsigned r=0; r<2; r++ ){
if( neqc.isNull() ){
if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
neqc = getInstantiateCons( eqc, dt, i, false, false );
for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
+ //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
nodes.push_back( neqc[j] );
}
Assert( !neqc.isNull() );
Trace("dt-cmi") << "Assign : " << neqc << std::endl;
m->assertEquality( eqc, neqc, true );
+ /*
+ for( unsigned kk=0; kk<all_eqc.size(); kk++ ){
+ for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){
+ if( m->areEqual( all_eqc[kk], all_eqc[ll] ) ){
+ Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl;
+ Node r = m->getRepresentative( all_eqc[kk] );
+ Trace("dt-cmi") << " { ";
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ Trace("dt-cmi") << (*eqc_i) << " ";
+ ++eqc_i;
+ }
+ Trace("dt-cmi") << "} " << std::endl;
+ }
+ Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) );
+ }
+ }
+ */
//m->assertRepresentative( neqc );
cons.push_back( neqc );
++index;
d_reals(true),
d_linear(true),// for now, "everything enabled" doesn't include non-linear arith
d_differenceLogic(false),
+ d_cardinalityConstraints(false),
d_locked(false) {
for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
d_reals(false),
d_linear(false),
d_differenceLogic(false),
+ d_cardinalityConstraints(false),
d_locked(false) {
setLogicString(logicString);
d_reals(false),
d_linear(false),
d_differenceLogic(false),
+ d_cardinalityConstraints(false),
d_locked(false) {
setLogicString(logicString);
ss << "UF";
++seen;
}
+ if( d_cardinalityConstraints ){
+ ss << "C";
+ }
if(d_theories[THEORY_BV]) {
ss << "BV";
++seen;
enableTheory(THEORY_UF);
p += 2;
}
+ if(!strncmp(p, "C", 1 )) {
+ d_cardinalityConstraints = true;
+ p += 1;
+ }
// allow BV or DT in either order
if(!strncmp(p, "BV", 2)) {
enableTheory(THEORY_BV);
bool d_reals; /**< are reals used in this logic? */
bool d_linear; /**< linear-only arithmetic in this logic? */
bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
+ bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */
bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
return d_differenceLogic;
}
+ /** Does this logic allow cardinality constraints? */
+ bool hasCardinalityConstraints() const {
+ CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
+ return d_cardinalityConstraints;
+ }
// MUTATORS
Node cond = d_models[op]->d_cond[i];
std::vector< Node > children;
for( unsigned j=0; j<cond.getNumChildren(); j++) {
+ TypeNode tn = vars[j].getType();
if (isInterval(cond[j])){
if( !isStar(cond[j][0]) ){
children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) );
if( !isStar(cond[j][1]) ){
children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) );
}
- }else if (!isStar(cond[j])){
+ }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type...
+ d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
Node c = getUsedRepresentative( cond[j] );
children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
}
curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
}
}
+ Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
curr = Rewriter::rewrite( curr );
return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
}
std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) {
switch(mode) {
- case theory::quantifiers::MBQI_DEFAULT:
- out << "MBQI_DEFAULT";
+ case theory::quantifiers::MBQI_GEN_EVAL:
+ out << "MBQI_GEN_EVAL";
break;
case theory::quantifiers::MBQI_NONE:
out << "MBQI_NONE";
case theory::quantifiers::MBQI_INTERVAL:
out << "MBQI_INTERVAL";
break;
+ case theory::quantifiers::MBQI_TRUST:
+ out << "MBQI_TRUST";
+ break;
default:
out << "MbqiMode!UNKNOWN";
}
} AxiomInstMode;
typedef enum {
- /** default, mbqi from CADE 24 paper */
- MBQI_DEFAULT,
+ /** mbqi from CADE 24 paper */
+ MBQI_GEN_EVAL,
/** no mbqi */
MBQI_NONE,
/** implementation that mimics inst-gen */
MBQI_INST_GEN,
- /** mbqi from Section 5.4.2 of AJR thesis */
+ /** default, mbqi from Section 5.4.2 of AJR thesis */
MBQI_FMC,
/** mbqi with integer intervals */
MBQI_FMC_INTERVAL,
option eagerInstQuant --eager-inst-quant bool :default false
apply quantifier instantiation eagerly
-option fullSaturateQuant --full-saturate-quant bool :default true
+option fullSaturateQuant --full-saturate-quant bool :default false
when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
use finite model finding heuristic for quantifier instantiation
-option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
choose mode for model-based quantifier instantiation
option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
only add one instantiation per quantifier per round for mbqi
Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
\n\
default \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
- model finding paper.\n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
+ Modulo Theories.\n\
\n\
none \n\
+ Disable model-based quantifier instantiation.\n\
instgen \n\
+ Use instantiation algorithm that mimics Inst-Gen calculus. \n\
\n\
-fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
- Modulo Theories.\n\
+gen-ev \n\
++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+ model finding paper.\n\
\n\
fmc-interval \n\
-+ Same as fmc, but with intervals for models of integer functions.\n\
++ Same as default, but with intervals for models of integer functions.\n\
\n\
interval \n\
+ Use algorithm that abstracts domain elements as intervals. \n\
}
inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
- if(optarg == "default") {
- return MBQI_DEFAULT;
+ if(optarg == "gen-ev") {
+ return MBQI_GEN_EVAL;
} else if(optarg == "none") {
return MBQI_NONE;
} else if(optarg == "instgen") {
return MBQI_INST_GEN;
- } else if(optarg == "fmc") {
+ } else if(optarg == "default" || optarg == "fmc") {
return MBQI_FMC;
} else if(optarg == "fmc-interval") {
return MBQI_FMC_INTERVAL;
}
d_par_op_map[op][tn1][tn2] = n;
return n;
- }else if( n.getKind()==APPLY_UF ){
+ }else if( inst::Trigger::isAtomicTrigger( n ) ){
return n.getOperator();
}else{
return Node::null();
if (atom.getKind() == kind::EQUAL) {
d_equalityEngine.assertEquality(atom, polarity, fact);
} else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
- // do nothing
+ if( d_thss == NULL ){
+ std::stringstream ss;
+ ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl;
+ ss << "Try using a logic containing \"UFC\"." << std::endl;
+ throw Exception( ss.str() );
+ }
} else {
d_equalityEngine.assertPredicate(atom, polarity, fact);
}
namespace expr {
namespace attr {
struct DatatypeIndexTag {};
+ struct DatatypeConsIndexTag {};
struct DatatypeFiniteTag {};
struct DatatypeWellFoundedTag {};
struct DatatypeFiniteComputedTag {};
}/* CVC4::expr namespace */
typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
+typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
}
}
+size_t Datatype::cindexOf(Expr item) {
+ ExprManagerScope ems(item);
+ CheckArgument(item.getType().isSelector(),
+ item,
+ "arg must be a datatype selector");
+ TNode n = Node::fromExpr(item);
+ if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
+ return cindexOf( item[0] );
+ }else{
+ Assert(n.hasAttribute(DatatypeConsIndexAttr()));
+ return n.getAttribute(DatatypeConsIndexAttr());
+ }
+}
+
void Datatype::resolve(ExprManager* em,
const std::map<std::string, DatatypeType>& resolutions,
const std::vector<Type>& placeholders,
d_resolved = true;
size_t index = 0;
for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
- (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
+ (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
}
const std::vector<Type>& placeholders,
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements)
+ const std::vector< DatatypeType >& paramReplacements, size_t cindex)
throw(IllegalArgumentException, DatatypeResolutionException) {
CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
}
(*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
}
+ Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
(*i).d_resolved = true;
}
const std::vector<Type>& placeholders,
const std::vector<Type>& replacements,
const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements)
+ const std::vector< DatatypeType >& paramReplacements, size_t cindex)
throw(IllegalArgumentException, DatatypeResolutionException);
friend class Datatype;
*/
static size_t indexOf(Expr item) CVC4_PUBLIC;
+ /**
+ * Get the index of constructor corresponding to selector. (Zero is
+ * always the first index.)
+ */
+ static size_t cindexOf(Expr item) CVC4_PUBLIC;
+
/** The type for iterators over constructors. */
typedef DatatypeConstructorIterator iterator;
/** The (const) type for iterators over constructors. */
; COMMAND-LINE: --tlimit-per 2500 -iq
; EXPECT: unknown
-; EXPECT: (:reason-unknown timeout)
+; EXPECT: (:reason-unknown incomplete)
; EXPECT: unsat
(set-option :print-success false)
(set-info :smt-lib-version 2.0)
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
% EXPECT: unsat
(benchmark Isabelle
:status sat
agree466.smt2 \
ALG008-1.smt2 \
german169.smt2 \
- Hoare-z3.931718.smt \
QEpres-uf.855035.smt \
agree467.smt2 \
Arrow_Order-smtlib.778341.smt \
german73.smt2 \
PUZ001+1.smt2 \
refcount24.cvc.smt2 \
- bug0909.smt2 \
- fmf-bound-int.smt2
+ fmf-bound-int.smt2 \
+ fc-simple.smt2 \
+ fc-unsat-tot-2.smt2 \
+ fc-unsat-pent.smt2 \
+ fc-pigeonhole19.smt2
EXTRA_DIST = $(TESTS)
+# disabled for now :
+# Hoare-z3.931718.smt bug0909.smt2
+
#if CVC4_BUILD_PROFILE_COMPETITION
#else
#TESTS += \
-% COMMAND-LINE: --finite-model-find
+% COMMAND-LINE: --finite-model-find --mbqi=gen-ev
% EXPECT: sat
(benchmark Isabelle
:status sat
--- /dev/null
+(set-logic UFC)\r
+(set-info :status unsat)\r
+\r
+(declare-sort P 0)\r
+(declare-sort H 0)\r
+\r
+(declare-fun p () P)\r
+(declare-fun h () H)\r
+\r
+; pigeonhole using native cardinality constraints\r
+(assert (fmf.card p 19))\r
+(assert (not (fmf.card p 18)))\r
+(assert (fmf.card h 18))\r
+(assert (not (fmf.card h 17)))\r
+\r
+; each pigeon has different holes\r
+(declare-fun f (P) H)\r
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))\r
+\r
+(check-sat)
\ No newline at end of file
--- /dev/null
+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun c () U)
+
+(assert (fmf.card c 2))
+(assert (not (fmf.card a 4)))
+
+(check-sat)
--- /dev/null
+(set-logic QF_UFC)\r
+(set-info :status unsat)\r
+\r
+(declare-sort U 0)\r
+\r
+(declare-fun a () U)\r
+(declare-fun b () U)\r
+(declare-fun c () U)\r
+(declare-fun d () U)\r
+(declare-fun e () U)\r
+\r
+(assert (not (= a b)))\r
+(assert (not (= b c)))\r
+(assert (not (= c d)))\r
+(assert (not (= d e)))\r
+(assert (not (= e a)))\r
+\r
+(assert (fmf.card c 2))\r
+\r
+(check-sat)
\ No newline at end of file
--- /dev/null
+(set-logic UFC)\r
+(set-info :status unsat)\r
+\r
+(declare-sort U 0)\r
+\r
+(declare-fun a () U)\r
+(declare-fun b () U)\r
+(declare-fun c () U)\r
+\r
+(assert (not (fmf.card a 2)))\r
+\r
+(assert (forall ((x U)) (or (= x a) (= x b))))\r
+\r
+(check-sat)
\ No newline at end of file
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
(set-logic LRA)
(set-info :status unsat)
(declare-fun x4 () Real)
+; COMMAND-LINE: --full-saturate-quant --decision=internal
+; EXPECT: unsat
(set-logic AUFLIA)
(set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |)
(set-info :smt-lib-version 2.0)
# put it below in "TESTS +="
TESTS = \
length_trick.smt2 \
- length_trick2.smt2 \
length_gen_020.smt2 \
datatypes.smt2 \
datatypes_sat.smt2 \
reachability_back_to_the_future.smt2 \
relation.smt2 \
simulate_rewriting.smt2 \
- native_arrays.smt2
+ native_arrays.smt2 \
+ read5.smt2
-# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
+# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+(set-logic AUF)
+(set-info :source |
+Translated from old SVC processor verification benchmarks. Contact Clark
+Barrett at barrett@cs.nyu.edu for more information.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort Index 0)
+(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index)
+(declare-fun a () Index)
+(declare-fun aaa () Index)
+(declare-fun aa () Index)
+(declare-fun S () Arr)
+(declare-fun vvv () Element)
+(declare-fun v () Element)
+(declare-fun vv () Element)
+(declare-fun bbb () Index)
+(declare-fun www () Element)
+(declare-fun bb () Index)
+(declare-fun ww () Element)
+(declare-fun b () Index)
+(declare-fun w () Element)
+(declare-fun SS () Arr)
+(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false))))
+; rewrite rule definition of arrays theory
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule)))
+(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule)))
+(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat)
+(exit)
tff0.p \
tff0-arith.p \
ARI086$(equals)1.p \
- BOO003-4.p \
DAT001$(equals)1.p \
KRS018+1.p \
KRS063+1.p \
EXTRA_DIST = $(TESTS) \
$(TEST_DEPS_DIST) \
BOO027-1.p \
+ BOO003-4.p \
MGT031-1.p \
NLP114-1.p \
SYN075+1.p
projects / cvc5.git / commitdiff