read_only = true
help = "introduce reference skolems for shorter explanations"
-[[option]]
- name = "dtUseTesters"
- category = "regular"
- long = "dt-use-testers"
- type = "bool"
- default = "true"
- read_only = true
- help = "do not preprocess away tester predicates"
-
[[option]]
name = "cdtBisimilar"
category = "regular"
read_only = true
help = "infer equalities for trigger terms based on solving arithmetic equalities"
-[[option]]
- name = "inferArithTriggerEqExp"
- category = "regular"
- long = "infer-arith-trigger-eq-exp"
- type = "bool"
- default = "false"
- read_only = true
- help = "record explanations for inferArithTriggerEq"
-
[[option]]
name = "strictTriggers"
category = "regular"
NodeManager::currentNM()->mkConst(true));
}
// could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ?
- else if (!options::dtUseTesters())
- {
- unsigned tindex = indexOf(in.getOperator());
- Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
- << in[0] << " " << tindex << std::endl;
- Node neq = mkTester(in[0], tindex, dt);
- Assert(neq != in);
- Trace("datatypes-rewrite")
- << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to "
- << neq << std::endl;
- return RewriteResponse(REWRITE_AGAIN_FULL, neq);
- }
return RewriteResponse(REWRITE_DONE, in);
}
int DatatypesRewriter::isTester(Node n, Node& a)
{
- if (options::dtUseTesters())
- {
- if (n.getKind() == kind::APPLY_TESTER)
- {
- a = n[0];
- return indexOf(n.getOperator());
- }
- }
- else
+ if (n.getKind() == kind::APPLY_TESTER)
{
- if (n.getKind() == kind::EQUAL)
- {
- for (int i = 1; i >= 0; i--)
- {
- if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
- {
- const Datatype& dt =
- Datatype::datatypeOf(n[i].getOperator().toExpr());
- int ic = isInstCons(n[1 - i], n[i], dt);
- if (ic != -1)
- {
- a = n[1 - i];
- return ic;
- }
- }
- }
- }
+ a = n[0];
+ return indexOf(n.getOperator());
}
return -1;
}
int DatatypesRewriter::isTester(Node n)
{
- if (options::dtUseTesters())
+ if (n.getKind() == kind::APPLY_TESTER)
{
- if (n.getKind() == kind::APPLY_TESTER)
- {
- return indexOf(n.getOperator().toExpr());
- }
- }
- else
- {
- if (n.getKind() == kind::EQUAL)
- {
- for (int i = 1; i >= 0; i--)
- {
- if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
- {
- const Datatype& dt =
- Datatype::datatypeOf(n[i].getOperator().toExpr());
- int ic = isInstCons(n[1 - i], n[i], dt);
- if (ic != -1)
- {
- return ic;
- }
- }
- }
- }
+ return indexOf(n.getOperator().toExpr());
}
return -1;
}
Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
{
- if (options::dtUseTesters())
- {
- return NodeManager::currentNM()->mkNode(
- kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
- }
-#ifdef CVC4_ASSERTIONS
- Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
- Node a;
- int ii = isTester(ret, a);
- Assert(ii == i);
- Assert(a == n);
- return ret;
-#else
- return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
-#endif
+ return NodeManager::currentNM()->mkNode(
+ kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
}
Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt)
if( !cons1.isNull() && !cons2.isNull() ){
Trace("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl;
Node unifEq = cons1.eqNode( cons2 );
- /*
- std::vector< Node > exp;
- std::vector< std::pair< TNode, TNode > > deq_cand;
- bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
- if( !conf ){
- for( unsigned i=0; i<deq_cand.size(); i++ ){
- if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
- conf = true;
- Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second );
- exp.push_back( eq.negate() );
- }
- }
- }
- if( conf ){
- exp.push_back( unifEq );
- d_conflictNode = explain( exp );
- }
- */
std::vector< Node > rew;
if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
d_conflictNode = explain( unifEq );
void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
//add constructor to equivalence class if not done so already
int index = getLabelIndex( eqc, n );
- if( index!=-1 && !eqc->d_inst ){
- if( options::dtUseTesters() ){
- Node exp;
- Node tt;
- if( !eqc->d_constructor.get().isNull() ){
- exp = d_true;
- tt = eqc->d_constructor;
- }else{
- exp = getLabel( n );
- tt = exp[0];
- }
- const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
- //instantiate this equivalence class
- eqc->d_inst = true;
- Node tt_cons = getInstantiateCons( tt, dt, index );
- Node eq;
- if( tt!=tt_cons ){
- eq = tt.eqNode( tt_cons );
- Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
- d_pending.push_back( eq );
- d_pending_exp[ eq ] = exp;
- Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
- Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
- //eqc->d_inst.set( eq );
- d_infer.push_back( eq );
- d_infer_exp.push_back( exp );
- }
- }else{
- eqc->d_inst = true;
- }
- //}
- //else{
- // Debug("datatypes-inst") << "Do not instantiate" << std::endl;
- //}
+ if (index == -1 || eqc->d_inst)
+ {
+ return;
+ }
+ Node exp;
+ Node tt;
+ if (!eqc->d_constructor.get().isNull())
+ {
+ exp = d_true;
+ tt = eqc->d_constructor;
+ }
+ else
+ {
+ exp = getLabel(n);
+ tt = exp[0];
+ }
+ const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
+ // instantiate this equivalence class
+ eqc->d_inst = true;
+ Node tt_cons = getInstantiateCons(tt, dt, index);
+ Node eq;
+ if (tt == tt_cons)
+ {
+ return;
}
+ eq = tt.eqNode(tt_cons);
+ Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq
+ << std::endl;
+ d_pending.push_back(eq);
+ d_pending_exp[eq] = exp;
+ Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
+ Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
+ << std::endl;
+ d_infer.push_back(eq);
+ d_infer_exp.push_back(exp);
}
void TheoryDatatypes::checkCycles() {
}
}
-bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
- if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
- if( n1.getOperator() != n2.getOperator() ) {
- return true;
- } else {
- Assert( n1.getNumChildren() == n2.getNumChildren() );
- for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
- TNode nc1 = getEqcConstructor( n1[i] );
- TNode nc2 = getEqcConstructor( n2[i] );
- if( checkClashModEq( nc1, nc2, exp, deq_cand ) ) {
- if( nc1!=n1[i] ){
- exp.push_back( nc1.eqNode( n1[i] ) );
- }
- if( nc2!=n2[i] ){
- exp.push_back( nc2.eqNode( n2[i] ) );
- }
- return true;
- }
- }
- }
- }else if( n1!=n2 ){
- if( n1.isConst() && n2.isConst() ){
- return true;
- }else{
- if( !areEqual( n1, n2 ) ){
- deq_cand.push_back( std::pair< TNode, TNode >( n1, n2 ) );
- }
- }
- }
- return false;
-}
-
void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
// Compute terms appearing in assertions and shared terms
std::set<Kind> irr_kinds;
void instantiate( EqcInfo* eqc, Node n );
/** must communicate fact */
bool mustCommunicateFact( Node n, Node exp );
- /** check clash mod eq */
- bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
/** get relevant terms */
void getRelevantTerms( std::set<Node>& termSet );
private:
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
-#define USE_INDEX_ORDERING
-
using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
}
}
Trace("fmf-eval-debug") << "Evaluate term " << n << " = ";
- printRepresentativeDebug( "fmf-eval-debug", val );
+ Trace("fmf-eval-debug") << getRepresentative(val);
Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl;
}
}
void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-#ifdef USE_INDEX_ORDERING
//sort arguments in order of least significant vs. most significant variable in default ordering
std::map< Node, std::vector< int > > argIndex;
std::vector< Node > args;
Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
}
Debug("fmf-index-order") << std::endl;
-#else
- d_eval_uf_use_default[n] = true;
-#endif
- }
-}
-
-/*
-Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
- std::vector< Node > children;
- children.push_back(n.getOperator());
- children.insert(children.end(), args.begin(), args.end());
- Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children);
- //make the term model specifically for nv
- makeEvalUfModel( nv );
- int argDepIndex;
- if( d_eval_uf_use_default[nv] ){
- return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex );
- }else{
- return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
}
}
-*/
-
-
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
FirstOrderModel(qe, c, name){
}
}
-/*
-Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
- Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
- for(unsigned i=0; i<args.size(); i++) {
- args[i] = getUsedRepresentative(args[i]);
- }
- Assert( n.getKind()==APPLY_UF );
- return d_models[n.getOperator()]->evaluate(this, args);
-}
-*/
-
void FirstOrderModelFmc::processInitialize( bool ispre ) {
if( ispre ){
for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
return Node::null();
}
-/*
-Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
- Debug("qint-debug") << "get curr uf value " << n << std::endl;
- if( d_models_valid[n] ){
- TypeNode tn = n.getType();
- if( tn.getNumChildren()>0 ){
- tn = tn[tn.getNumChildren()-1];
- }
- return d_models[n]->evaluate( this, tn, args );
- }else{
- return Node::null();
- }
-}
-*/
-
void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size()))
/ (1.0 + static_cast<double>(d_value_pro_con[1][v].size()));
Debug("fmf-model-cons-debug") << " - score( ";
- m->printRepresentativeDebug("fmf-model-cons-debug", v);
+ Debug("fmf-model-cons-debug") << m->getRepresentative(v);
Debug("fmf-model-cons-debug") << " ) = " << score << std::endl;
if (score > maxScore)
{
{
defaultVal = newDefaultVal;
Debug("fmf-model-cons-debug") << "-> Change default value to ";
- m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal);
+ Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
Debug("fmf-model-cons-debug") << std::endl;
}
else
}
// get the default term (this term must be defined non-ground in model)
Debug("fmf-model-cons-debug") << " Choose ";
- m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal);
+ Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
Debug("fmf-model-cons-debug")
<< " as default value (" << defaultTerm << ")" << std::endl;
Debug("fmf-model-cons-debug")
fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
- fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+ Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val;
Debug("fmf-model-cons") << std::endl;
d_uf_model_constructed[op] = true;
}else{
}
if( options::inferArithTriggerEq() ){
- d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
+ d_eq_inference = new quantifiers::EqualityInference(c, false);
}else{
d_eq_inference = NULL;
}
}
}
-//for debugging
-void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
- if( r.isNull() ){
- Trace( c ) << "null";
- }else if( r.getType().isBoolean() ){
- if( areEqual( r, d_true ) ){
- Trace( c ) << "true";
- }else{
- Trace( c ) << "false";
- }
- }else{
- Trace( c ) << getRepresentative( r );
- }
-}
-
-void TheoryModel::printRepresentative( std::ostream& out, Node r ){
- Assert( !r.isNull() );
- if( r.isNull() ){
- out << "null";
- }else if( r.getType().isBoolean() ){
- if( areEqual( r, d_true ) ){
- out << "true";
- }else{
- out << "false";
- }
- }else{
- out << getRepresentative( r );
- }
-}
-
bool TheoryModel::areFunctionValuesEnabled() const
{
return d_enableFuncModels;
Expr getValue(Expr expr) const override;
/** get cardinality for sort */
Cardinality getCardinality(Type t) const override;
- /** print representative debug function */
- void printRepresentativeDebug( const char* c, Node r );
- /** print representative function */
- void printRepresentative( std::ostream& out, Node r );
//---------------------------- function values
/** a map from functions f to a list of all APPLY_UF terms with operator f */
}else{
indent( out, ind );
out << "return ";
- m->printRepresentative( out, d_value );
+ out << m->getRepresentative(d_value);
out << std::endl;
}
}
projects / cvc5.git / commitdiff